%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO015-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 : 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:22 PM UTC 2026
% Result : Unsatisfiable 182.16s 23.39s
% Output : CNFRefutation 182.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 23
% Syntax : Number of formulae : 196 ( 105 unt; 0 def)
% Number of atoms : 397 ( 70 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 404 ( 203 ~; 201 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 469 ( 469 !; 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(f11,axiom,
! [Y,X,V1,Z,V2,V3,V4] :
( sum(V1,V2,V4)
| ~ product(V3,X,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(f14,axiom,
! [X,Y,V1,Z,V2,V3,V4] :
( sum(X,V3,V4)
| ~ product(V1,V2,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(f19,axiom,
! [X] : product(inverse(X),X,additive_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,negated_conjecture,
product(x,y,x_times_y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
sum(inverse(x),inverse(y),x_inverse_plus_y_inverse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
inverse(x_times_y) != x_inverse_plus_y_inverse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,plain,
! [X0,X1] : sum(X0,X1,add(X0,X1)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f27,plain,
! [X0,X1] : product(X0,X1,multiply(X0,X1)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f28,plain,
! [X0,X1,X2] :
( sum(X1,X0,X2)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f29,plain,
! [X0,X1,X2] :
( product(X1,X0,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f30,plain,
! [X0] : sum(additive_identity,X0,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f31,plain,
! [X0] : sum(X0,additive_identity,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f32,plain,
! [X0] : product(multiplicative_identity,X0,X0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f33,plain,
! [X0] : product(X0,multiplicative_identity,X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f34,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(f35,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( sum(X2,X4,X6)
| ~ product(X0,X5,X6)
| ~ sum(X1,X3,X5)
| ~ product(X0,X3,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,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(f37,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( product(X0,X5,X6)
| ~ sum(X2,X4,X6)
| ~ sum(X1,X3,X5)
| ~ product(X0,X3,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
! [V1,V2,V4] :
( sum(V1,V2,V4)
| ! [X,V3] :
( ~ product(V3,X,V4)
| ! [Y,Z] :
( ~ sum(Y,Z,V3)
| ~ product(Z,X,V2)
| ~ product(Y,X,V1) ) ) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f39,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( sum(X2,X4,X6)
| ~ product(X5,X1,X6)
| ~ sum(X0,X3,X5)
| ~ product(X3,X1,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f42,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(f43,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( product(X2,X4,X6)
| ~ sum(X0,X5,X6)
| ~ product(X1,X3,X5)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f44,plain,
! [X,V3,V4] :
( sum(X,V3,V4)
| ! [V1,V2] :
( ~ product(V1,V2,V4)
| ! [Y,Z] :
( ~ product(Y,Z,V3)
| ~ sum(X,Z,V2)
| ~ sum(X,Y,V1) ) ) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f45,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( sum(X0,X5,X6)
| ~ product(X2,X4,X6)
| ~ product(X1,X3,X5)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,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(f47,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( product(X2,X4,X6)
| ~ sum(X5,X1,X6)
| ~ product(X0,X3,X5)
| ~ sum(X3,X1,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f48,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(f49,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( sum(X5,X1,X6)
| ~ product(X2,X4,X6)
| ~ product(X0,X3,X5)
| ~ sum(X3,X1,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f51,plain,
! [X0] : sum(X0,inverse(X0),multiplicative_identity),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f52,plain,
! [X0] : product(inverse(X0),X0,additive_identity),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f53,plain,
! [X0] : product(X0,inverse(X0),additive_identity),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f54,plain,
! [U,V] :
( U = V
| ! [X,Y] :
( ~ sum(X,Y,V)
| ~ sum(X,Y,U) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f55,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ sum(X0,X1,X3)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
! [U,V] :
( U = V
| ! [X,Y] :
( ~ product(X,Y,V)
| ~ product(X,Y,U) ) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f57,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
product(x,y,x_times_y),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f59,plain,
sum(inverse(x),inverse(y),x_inverse_plus_y_inverse),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f60,plain,
inverse(x_times_y) != x_inverse_plus_y_inverse,
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f64,plain,
! [X0,X1] : sum(X0,X1,add(X1,X0)),
inference(resolution,[status(thm)],[f28,f26]) ).
fof(f69,plain,
! [X0,X1] : product(X0,X1,multiply(X1,X0)),
inference(resolution,[status(thm)],[f29,f27]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( sum(x_times_y,X1,X3)
| ~ product(x,X2,X3)
| ~ sum(y,X0,X2)
| ~ product(x,X0,X1) ),
inference(resolution,[status(thm)],[f35,f58]) ).
fof(f75,plain,
! [X0,X1,X2,X3,X4] :
( sum(additive_identity,X2,X4)
| ~ product(X0,X3,X4)
| ~ sum(inverse(X0),X1,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f35,f53]) ).
fof(f76,plain,
! [X0,X1,X2,X3,X4] :
( sum(X0,X2,X4)
| ~ product(X0,X3,X4)
| ~ sum(multiplicative_identity,X1,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f35,f33]) ).
fof(f77,plain,
! [X0,X1,X2,X3,X4,X5] :
( sum(multiply(X0,X3),X2,X5)
| ~ product(X0,X4,X5)
| ~ sum(X3,X1,X4)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f35,f27]) ).
fof(f81,plain,
! [X0,X1,X2,X3,X4] :
( product(multiplicative_identity,X3,X4)
| ~ sum(X2,X1,X4)
| ~ sum(X2,X0,X3)
| ~ product(multiplicative_identity,X0,X1) ),
inference(resolution,[status(thm)],[f37,f32]) ).
fof(f82,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,X3,X4)
| ~ sum(additive_identity,X2,X4)
| ~ sum(inverse(X0),X1,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f37,f53]) ).
fof(f84,plain,
! [X0,X1,X2,X3,X4,X5] :
( product(X0,X4,X5)
| ~ sum(multiply(X0,X3),X2,X5)
| ~ sum(X3,X1,X4)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f37,f27]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( sum(x_times_y,X1,X3)
| ~ product(X2,y,X3)
| ~ sum(x,X0,X2)
| ~ product(X0,y,X1) ),
inference(resolution,[status(thm)],[f39,f58]) ).
fof(f100,plain,
! [X0,X1] :
( X0 = X1
| ~ sum(additive_identity,X0,X1) ),
inference(resolution,[status(thm)],[f55,f30]) ).
fof(f102,plain,
! [X0,X1] :
( X0 = X1
| ~ sum(X0,additive_identity,X1) ),
inference(resolution,[status(thm)],[f55,f31]) ).
fof(f103,plain,
! [X0,X1,X2] :
( add(X1,X0) = X2
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f55,f64]) ).
fof(f104,plain,
! [X0,X1,X2] :
( add(X0,X1) = X2
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f55,f26]) ).
fof(f116,plain,
! [X0] : X0 = add(X0,additive_identity),
inference(resolution,[status(thm)],[f100,f64]) ).
fof(f123,plain,
! [X0,X1,X2,X3,X4] :
( product(X2,X1,X4)
| ~ sum(additive_identity,X3,X4)
| ~ product(X2,X0,X3)
| ~ sum(additive_identity,X0,X1) ),
inference(resolution,[status(thm)],[f43,f30]) ).
fof(f127,plain,
! [X0,X1,X2,X3,X4,X5] :
( product(add(X0,X3),X2,X5)
| ~ sum(X0,X4,X5)
| ~ product(X3,X1,X4)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f43,f26]) ).
fof(f135,plain,
! [X0,X1,X2,X3,X4] :
( sum(additive_identity,X3,X4)
| ~ product(X2,X1,X4)
| ~ product(X2,X0,X3)
| ~ sum(additive_identity,X0,X1) ),
inference(resolution,[status(thm)],[f45,f30]) ).
fof(f155,plain,
! [X0,X1,X2,X3,X4,X5] :
( product(add(X3,X1),X2,X5)
| ~ sum(X4,X1,X5)
| ~ product(X3,X0,X4)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f47,f26]) ).
fof(f167,plain,
! [X0,X1,X2,X3,X4] :
( sum(X3,X1,X4)
| ~ product(X1,X2,X4)
| ~ product(additive_identity,X0,X3)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f49,f30]) ).
fof(f182,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(resolution,[status(thm)],[f103,f26]) ).
fof(f184,plain,
! [X0] :
( x_times_y = X0
| ~ product(x,y,X0) ),
inference(resolution,[status(thm)],[f57,f58]) ).
fof(f185,plain,
! [X0,X1] :
( additive_identity = X1
| ~ product(inverse(X0),X0,X1) ),
inference(resolution,[status(thm)],[f57,f52]) ).
fof(f189,plain,
! [X0,X1,X2] :
( multiply(X1,X0) = X2
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f57,f69]) ).
fof(f190,plain,
! [X0,X1,X2] :
( multiply(X0,X1) = X2
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f57,f27]) ).
fof(f213,plain,
add(inverse(y),inverse(x)) = x_inverse_plus_y_inverse,
inference(resolution,[status(thm)],[f59,f103]) ).
fof(f220,plain,
add(inverse(x),inverse(y)) = x_inverse_plus_y_inverse,
inference(forward_demodulation,[status(thm)],[f182,f213]) ).
fof(f232,plain,
! [X0,X1] :
( sum(x_times_y,x,X1)
| ~ product(x,X0,X1)
| ~ sum(y,multiplicative_identity,X0) ),
inference(resolution,[status(thm)],[f72,f33]) ).
fof(f282,plain,
! [X0,X1,X2,X3] :
( sum(additive_identity,multiply(X1,X0),X3)
| ~ product(X0,X2,X3)
| ~ sum(inverse(X0),X1,X2) ),
inference(resolution,[status(thm)],[f75,f69]) ).
fof(f290,plain,
! [X0] : additive_identity = multiply(X0,inverse(X0)),
inference(resolution,[status(thm)],[f185,f69]) ).
fof(f300,plain,
! [X0,X1,X2,X3] :
( sum(X2,multiply(X0,X2),X3)
| ~ product(X2,X1,X3)
| ~ sum(multiplicative_identity,X0,X1) ),
inference(resolution,[status(thm)],[f76,f69]) ).
fof(f301,plain,
! [X0,X1,X2,X3] :
( sum(X2,multiply(X2,X0),X3)
| ~ product(X2,X1,X3)
| ~ sum(multiplicative_identity,X0,X1) ),
inference(resolution,[status(thm)],[f76,f27]) ).
fof(f316,plain,
! [X0,X1,X2,X3] :
( sum(multiply(inverse(X1),X0),additive_identity,X3)
| ~ product(inverse(X1),X2,X3)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f77,f52]) ).
fof(f320,plain,
! [X0,X1,X2,X3,X4] :
( sum(multiply(X3,X0),multiply(X1,X3),X4)
| ~ product(X3,X2,X4)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f77,f69]) ).
fof(f336,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(resolution,[status(thm)],[f189,f27]) ).
fof(f390,plain,
! [X0,X1,X2,X3] :
( product(multiplicative_identity,X2,X3)
| ~ sum(X0,X1,X3)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f81,f32]) ).
fof(f404,plain,
! [X0,X1,X2,X3] :
( product(X0,X2,X3)
| ~ sum(additive_identity,multiply(X1,X0),X3)
| ~ sum(inverse(X0),X1,X2) ),
inference(resolution,[status(thm)],[f82,f69]) ).
fof(f446,plain,
! [X0,X1,X2,X3,X4] :
( product(X3,X2,X4)
| ~ sum(multiply(X3,X0),multiply(X3,X1),X4)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f84,f27]) ).
fof(f464,plain,
! [X0,X1] :
( sum(x_times_y,y,X1)
| ~ product(X0,y,X1)
| ~ sum(x,multiplicative_identity,X0) ),
inference(resolution,[status(thm)],[f88,f32]) ).
fof(f535,plain,
! [X0,X1,X2] :
( product(multiplicative_identity,add(X1,X0),X2)
| ~ sum(X0,X1,X2) ),
inference(resolution,[status(thm)],[f390,f64]) ).
fof(f594,plain,
! [X0,X1] : product(multiplicative_identity,add(X0,X1),add(X1,X0)),
inference(resolution,[status(thm)],[f535,f26]) ).
fof(f940,plain,
! [X0,X1,X2,X3] :
( product(X0,X1,X3)
| ~ sum(additive_identity,X2,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f123,f30]) ).
fof(f1030,plain,
! [X0,X1,X2,X3,X4] :
( product(add(X3,X0),add(X1,X3),X4)
| ~ sum(X3,X2,X4)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f127,f64]) ).
fof(f1046,plain,
! [X0,X1,X2,X3] :
( sum(additive_identity,X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f135,f30]) ).
fof(f1177,plain,
! [X0,X1,X2] :
( product(X0,X1,X2)
| ~ sum(additive_identity,multiply(X0,X1),X2) ),
inference(resolution,[status(thm)],[f940,f27]) ).
fof(f1261,plain,
! [X0,X1,X2,X3,X4] :
( product(add(X0,X3),add(X1,X3),X4)
| ~ sum(X2,X3,X4)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f155,f26]) ).
fof(f1285,plain,
! [X0,X1,X2,X3] :
( sum(X1,X2,X3)
| ~ product(X2,add(X0,X2),X3)
| ~ product(additive_identity,X0,X1) ),
inference(resolution,[status(thm)],[f167,f26]) ).
fof(f1294,plain,
! [X0,X1,X2] :
( sum(additive_identity,multiply(X1,X0),X2)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f1046,f69]) ).
fof(f1369,plain,
! [X0,X1] : sum(additive_identity,multiply(X0,X1),multiply(X1,X0)),
inference(resolution,[status(thm)],[f1294,f27]) ).
fof(f1413,plain,
! [X0,X1,X2] :
( multiply(X1,X0) = X2
| ~ sum(additive_identity,multiply(X0,X1),X2) ),
inference(resolution,[status(thm)],[f1369,f55]) ).
fof(f2022,plain,
( sum(x_times_y,x,x)
| ~ sum(y,multiplicative_identity,multiplicative_identity) ),
inference(resolution,[status(thm)],[f232,f33]) ).
fof(f2689,plain,
! [X0,X1] :
( sum(additive_identity,multiply(inverse(inverse(X0)),X0),X1)
| ~ product(X0,multiplicative_identity,X1) ),
inference(resolution,[status(thm)],[f282,f51]) ).
fof(f2690,plain,
! [X0,X1] :
( sum(additive_identity,multiply(additive_identity,X0),X1)
| ~ product(X0,inverse(X0),X1) ),
inference(resolution,[status(thm)],[f282,f31]) ).
fof(f2699,plain,
! [X0,X1] :
( sum(additive_identity,multiply(X0,inverse(inverse(X0))),X1)
| ~ product(X0,multiplicative_identity,X1) ),
inference(forward_demodulation,[status(thm)],[f336,f2689]) ).
fof(f2983,plain,
! [X0,X1,X2] :
( sum(X0,multiply(X1,X0),X2)
| ~ product(X0,add(X1,multiplicative_identity),X2) ),
inference(resolution,[status(thm)],[f300,f64]) ).
fof(f2994,plain,
! [X0,X1,X2] :
( sum(X0,multiply(X0,X1),X2)
| ~ product(X0,add(X1,multiplicative_identity),X2) ),
inference(resolution,[status(thm)],[f301,f64]) ).
fof(f3043,plain,
! [X0,X1] :
( sum(multiply(inverse(inverse(X0)),X0),additive_identity,X1)
| ~ product(inverse(inverse(X0)),multiplicative_identity,X1) ),
inference(resolution,[status(thm)],[f316,f51]) ).
fof(f3061,plain,
! [X0,X1] :
( sum(multiply(X0,inverse(inverse(X0))),additive_identity,X1)
| ~ product(inverse(inverse(X0)),multiplicative_identity,X1) ),
inference(forward_demodulation,[status(thm)],[f336,f3043]) ).
fof(f3125,plain,
! [X0,X1,X2] :
( sum(multiply(X0,X2),multiply(inverse(X2),X0),X1)
| ~ product(X0,multiplicative_identity,X1) ),
inference(resolution,[status(thm)],[f320,f51]) ).
fof(f4498,plain,
! [X0,X1,X2] :
( product(X1,add(inverse(X1),X0),X2)
| ~ sum(additive_identity,multiply(X0,X1),X2) ),
inference(resolution,[status(thm)],[f404,f26]) ).
fof(f5404,plain,
! [X0,X1] :
( product(X0,x_inverse_plus_y_inverse,X1)
| ~ sum(multiply(X0,inverse(x)),multiply(X0,inverse(y)),X1) ),
inference(resolution,[status(thm)],[f446,f59]) ).
fof(f5436,plain,
( sum(x_times_y,y,y)
| ~ sum(x,multiplicative_identity,multiplicative_identity) ),
inference(resolution,[status(thm)],[f464,f32]) ).
fof(f9316,plain,
! [X0,X1,X2,X3] :
( product(add(X0,X2),add(X1,X0),X3)
| ~ sum(X0,multiply(X1,X2),X3) ),
inference(resolution,[status(thm)],[f1030,f69]) ).
fof(f12829,plain,
! [X0,X1] :
( product(add(x,X0),add(y,X0),X1)
| ~ sum(x_times_y,X0,X1) ),
inference(resolution,[status(thm)],[f1261,f58]) ).
fof(f18508,plain,
! [X0] : sum(additive_identity,multiply(additive_identity,X0),additive_identity),
inference(resolution,[status(thm)],[f2690,f53]) ).
fof(f18521,plain,
! [X0] : product(additive_identity,X0,additive_identity),
inference(resolution,[status(thm)],[f18508,f1177]) ).
fof(f18848,plain,
! [X0,X1,X2] :
( sum(additive_identity,X0,X2)
| ~ product(X0,add(X1,X0),X2) ),
inference(resolution,[status(thm)],[f18521,f1285]) ).
fof(f19998,plain,
! [X0] : sum(additive_identity,multiply(X0,inverse(inverse(X0))),X0),
inference(resolution,[status(thm)],[f2699,f33]) ).
fof(f20088,plain,
! [X0] : multiply(inverse(inverse(X0)),X0) = X0,
inference(resolution,[status(thm)],[f19998,f1413]) ).
fof(f20173,plain,
! [X0] : multiply(X0,inverse(inverse(X0))) = X0,
inference(forward_demodulation,[status(thm)],[f336,f20088]) ).
fof(f21181,plain,
! [X0] : sum(additive_identity,multiplicative_identity,add(multiplicative_identity,X0)),
inference(resolution,[status(thm)],[f18848,f594]) ).
fof(f21185,plain,
! [X0,X1] : sum(additive_identity,X0,multiply(add(X1,X0),X0)),
inference(resolution,[status(thm)],[f18848,f69]) ).
fof(f21198,plain,
! [X0,X1] : sum(additive_identity,X0,multiply(X0,add(X1,X0))),
inference(forward_demodulation,[status(thm)],[f336,f21185]) ).
fof(f21226,plain,
! [X0] : multiplicative_identity = add(multiplicative_identity,X0),
inference(resolution,[status(thm)],[f21181,f100]) ).
fof(f21455,plain,
! [X0] : multiplicative_identity = add(X0,multiplicative_identity),
inference(paramodulation,[status(thm)],[f182,f21226]) ).
fof(f21543,plain,
! [X0] : sum(X0,multiplicative_identity,multiplicative_identity),
inference(paramodulation,[status(thm)],[f21226,f64]) ).
fof(f21810,plain,
! [X0,X1,X2] :
( sum(X0,multiply(X2,X0),X1)
| ~ product(X0,multiplicative_identity,X1) ),
inference(forward_demodulation,[status(thm)],[f21455,f2983]) ).
fof(f21817,plain,
! [X0,X1] : sum(X0,multiply(X1,X0),X0),
inference(resolution,[status(thm)],[f21810,f33]) ).
fof(f21835,plain,
! [X0,X1,X2] :
( sum(X0,multiply(X0,X2),X1)
| ~ product(X0,multiplicative_identity,X1) ),
inference(forward_demodulation,[status(thm)],[f21455,f2994]) ).
fof(f21842,plain,
! [X0,X1] : sum(X0,multiply(X0,X1),X0),
inference(resolution,[status(thm)],[f21835,f33]) ).
fof(f21859,plain,
sum(x_times_y,y,y),
inference(backward_subsumption_resolution,[status(thm)],[f5436,f21543]) ).
fof(f21860,plain,
sum(x_times_y,x,x),
inference(backward_subsumption_resolution,[status(thm)],[f2022,f21543]) ).
fof(f22609,plain,
! [X0,X1] : sum(multiply(X0,X1),X1,X1),
inference(resolution,[status(thm)],[f21817,f28]) ).
fof(f22812,plain,
! [X0,X1] : add(X0,multiply(X0,X1)) = X0,
inference(resolution,[status(thm)],[f21842,f104]) ).
fof(f22979,plain,
add(x_times_y,y) = y,
inference(resolution,[status(thm)],[f21859,f104]) ).
fof(f23005,plain,
add(y,x_times_y) = y,
inference(forward_demodulation,[status(thm)],[f182,f22979]) ).
fof(f23085,plain,
add(x_times_y,x) = x,
inference(resolution,[status(thm)],[f21860,f104]) ).
fof(f23111,plain,
add(x,x_times_y) = x,
inference(forward_demodulation,[status(thm)],[f182,f23085]) ).
fof(f23309,plain,
! [X0,X1] :
( sum(X0,additive_identity,X1)
| ~ product(inverse(inverse(X0)),multiplicative_identity,X1) ),
inference(forward_demodulation,[status(thm)],[f20173,f3061]) ).
fof(f23311,plain,
! [X0] : sum(X0,additive_identity,inverse(inverse(X0))),
inference(resolution,[status(thm)],[f23309,f33]) ).
fof(f25026,plain,
! [X0,X1] : sum(multiply(X0,X1),multiply(inverse(X1),X0),X0),
inference(resolution,[status(thm)],[f3125,f33]) ).
fof(f25207,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(resolution,[status(thm)],[f23311,f102]) ).
fof(f26125,plain,
! [X0,X1] : X0 = multiply(X0,add(X1,X0)),
inference(resolution,[status(thm)],[f21198,f100]) ).
fof(f26462,plain,
x_times_y = multiply(x_times_y,x),
inference(paramodulation,[status(thm)],[f23111,f26125]) ).
fof(f26463,plain,
x_times_y = multiply(x_times_y,y),
inference(paramodulation,[status(thm)],[f23005,f26125]) ).
fof(f26469,plain,
inverse(y) = multiply(inverse(y),x_inverse_plus_y_inverse),
inference(paramodulation,[status(thm)],[f220,f26125]) ).
fof(f26477,plain,
! [X0,X1] : X0 = multiply(X0,add(X0,X1)),
inference(paramodulation,[status(thm)],[f182,f26125]) ).
fof(f26557,plain,
x_times_y = multiply(x,x_times_y),
inference(forward_demodulation,[status(thm)],[f336,f26462]) ).
fof(f26558,plain,
x_times_y = multiply(y,x_times_y),
inference(forward_demodulation,[status(thm)],[f336,f26463]) ).
fof(f26559,plain,
inverse(y) = multiply(x_inverse_plus_y_inverse,inverse(y)),
inference(forward_demodulation,[status(thm)],[f336,f26469]) ).
fof(f27265,plain,
inverse(x) = multiply(inverse(x),x_inverse_plus_y_inverse),
inference(paramodulation,[status(thm)],[f220,f26477]) ).
fof(f27354,plain,
inverse(x) = multiply(x_inverse_plus_y_inverse,inverse(x)),
inference(forward_demodulation,[status(thm)],[f336,f27265]) ).
fof(f36719,plain,
! [X0,X1] : product(X0,add(inverse(X0),X1),multiply(X0,X1)),
inference(resolution,[status(thm)],[f4498,f1369]) ).
fof(f41355,plain,
! [X0,X1] : add(multiply(X0,X1),multiply(inverse(X1),X0)) = X0,
inference(resolution,[status(thm)],[f25026,f104]) ).
fof(f43810,plain,
! [X0,X1] : multiply(X0,add(inverse(X0),X1)) = multiply(X0,X1),
inference(resolution,[status(thm)],[f36719,f190]) ).
fof(f50704,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X0,multiply(inverse(X0),X1)),
inference(paramodulation,[status(thm)],[f22812,f43810]) ).
fof(f50882,plain,
! [X0,X1] : additive_identity = multiply(X0,multiply(inverse(X0),X1)),
inference(forward_demodulation,[status(thm)],[f290,f50704]) ).
fof(f51287,plain,
! [X0,X1] : additive_identity = multiply(inverse(X0),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f25207,f50882]) ).
fof(f52318,plain,
additive_identity = multiply(inverse(x_inverse_plus_y_inverse),inverse(x)),
inference(paramodulation,[status(thm)],[f27354,f51287]) ).
fof(f52319,plain,
additive_identity = multiply(inverse(x_inverse_plus_y_inverse),inverse(y)),
inference(paramodulation,[status(thm)],[f26559,f51287]) ).
fof(f52320,plain,
additive_identity = multiply(inverse(y),x_times_y),
inference(paramodulation,[status(thm)],[f26558,f51287]) ).
fof(f52326,plain,
additive_identity = multiply(inverse(x),x_times_y),
inference(paramodulation,[status(thm)],[f26557,f51287]) ).
fof(f52504,plain,
additive_identity = multiply(inverse(x),inverse(x_inverse_plus_y_inverse)),
inference(forward_demodulation,[status(thm)],[f336,f52318]) ).
fof(f52505,plain,
additive_identity = multiply(inverse(y),inverse(x_inverse_plus_y_inverse)),
inference(forward_demodulation,[status(thm)],[f336,f52319]) ).
fof(f52506,plain,
additive_identity = multiply(x_times_y,inverse(y)),
inference(forward_demodulation,[status(thm)],[f336,f52320]) ).
fof(f52511,plain,
additive_identity = multiply(x_times_y,inverse(x)),
inference(forward_demodulation,[status(thm)],[f336,f52326]) ).
fof(f53180,plain,
! [X0] :
( product(x_times_y,x_inverse_plus_y_inverse,X0)
| ~ sum(additive_identity,multiply(x_times_y,inverse(y)),X0) ),
inference(paramodulation,[status(thm)],[f52511,f5404]) ).
fof(f53336,plain,
! [X0] :
( product(x_times_y,x_inverse_plus_y_inverse,X0)
| ~ sum(additive_identity,additive_identity,X0) ),
inference(forward_demodulation,[status(thm)],[f52506,f53180]) ).
fof(f60810,plain,
add(multiply(inverse(x_inverse_plus_y_inverse),x),additive_identity) = inverse(x_inverse_plus_y_inverse),
inference(paramodulation,[status(thm)],[f52504,f41355]) ).
fof(f60985,plain,
multiply(inverse(x_inverse_plus_y_inverse),x) = inverse(x_inverse_plus_y_inverse),
inference(forward_demodulation,[status(thm)],[f116,f60810]) ).
fof(f60986,plain,
multiply(x,inverse(x_inverse_plus_y_inverse)) = inverse(x_inverse_plus_y_inverse),
inference(forward_demodulation,[status(thm)],[f336,f60985]) ).
fof(f61401,plain,
add(multiply(inverse(x_inverse_plus_y_inverse),y),additive_identity) = inverse(x_inverse_plus_y_inverse),
inference(paramodulation,[status(thm)],[f52505,f41355]) ).
fof(f61578,plain,
multiply(inverse(x_inverse_plus_y_inverse),y) = inverse(x_inverse_plus_y_inverse),
inference(forward_demodulation,[status(thm)],[f116,f61401]) ).
fof(f61579,plain,
multiply(y,inverse(x_inverse_plus_y_inverse)) = inverse(x_inverse_plus_y_inverse),
inference(forward_demodulation,[status(thm)],[f336,f61578]) ).
fof(f64700,plain,
add(x,inverse(x_inverse_plus_y_inverse)) = x,
inference(paramodulation,[status(thm)],[f60986,f22812]) ).
fof(f65934,plain,
add(y,inverse(x_inverse_plus_y_inverse)) = y,
inference(paramodulation,[status(thm)],[f61579,f22812]) ).
fof(f88668,plain,
! [X0,X1] : product(add(multiply(X0,X1),X0),add(inverse(X1),multiply(X0,X1)),X0),
inference(resolution,[status(thm)],[f9316,f25026]) ).
fof(f88755,plain,
! [X0,X1] : product(add(X0,multiply(X0,X1)),add(inverse(X1),multiply(X0,X1)),X0),
inference(forward_demodulation,[status(thm)],[f182,f88668]) ).
fof(f88756,plain,
! [X0,X1] : product(X0,add(inverse(X1),multiply(X0,X1)),X0),
inference(forward_demodulation,[status(thm)],[f22812,f88755]) ).
fof(f96731,plain,
! [X0,X1] : multiply(X0,add(inverse(X1),multiply(X0,X1))) = X0,
inference(resolution,[status(thm)],[f88756,f190]) ).
fof(f137102,plain,
product(x_times_y,x_inverse_plus_y_inverse,additive_identity),
inference(resolution,[status(thm)],[f53336,f30]) ).
fof(f137199,plain,
multiply(x_times_y,x_inverse_plus_y_inverse) = additive_identity,
inference(resolution,[status(thm)],[f137102,f190]) ).
fof(f137280,plain,
multiply(x_times_y,add(inverse(x_inverse_plus_y_inverse),additive_identity)) = x_times_y,
inference(paramodulation,[status(thm)],[f137199,f96731]) ).
fof(f137491,plain,
multiply(x_times_y,inverse(x_inverse_plus_y_inverse)) = x_times_y,
inference(forward_demodulation,[status(thm)],[f116,f137280]) ).
fof(f138149,plain,
sum(x_times_y,inverse(x_inverse_plus_y_inverse),inverse(x_inverse_plus_y_inverse)),
inference(paramodulation,[status(thm)],[f137491,f22609]) ).
fof(f143615,plain,
product(add(x,inverse(x_inverse_plus_y_inverse)),add(y,inverse(x_inverse_plus_y_inverse)),inverse(x_inverse_plus_y_inverse)),
inference(resolution,[status(thm)],[f138149,f12829]) ).
fof(f143699,plain,
product(x,add(y,inverse(x_inverse_plus_y_inverse)),inverse(x_inverse_plus_y_inverse)),
inference(forward_demodulation,[status(thm)],[f64700,f143615]) ).
fof(f143700,plain,
product(x,y,inverse(x_inverse_plus_y_inverse)),
inference(forward_demodulation,[status(thm)],[f65934,f143699]) ).
fof(f143777,plain,
x_times_y = inverse(x_inverse_plus_y_inverse),
inference(resolution,[status(thm)],[f143700,f184]) ).
fof(f144127,plain,
x_inverse_plus_y_inverse = inverse(x_times_y),
inference(paramodulation,[status(thm)],[f143777,f25207]) ).
fof(f144300,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f144127,f60]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO015-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n026.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 13:50:52 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 182.16/23.39 % Refutation found
% 182.16/23.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 182.16/23.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 182.16/23.45 % Elapsed time: 23.081144 seconds
% 182.16/23.45 % CPU time: 182.701042 seconds
% 182.16/23.45 % Total memory used: 388.628 MB
% 182.16/23.45 % Net memory used: 328.329 MB
%------------------------------------------------------------------------------