%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO017-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:23 PM UTC 2026
% Result : Unsatisfiable 60.08s 18.16s
% Output : CNFRefutation 60.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 13
% Syntax : Number of formulae : 57 ( 57 unt; 0 def)
% Number of atoms : 57 ( 56 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-4 aty)
% Number of variables : 130 ( 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq2(A,A,B,C) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : product(X,Y,multiply(X,Y)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] : ifeq(sum(X,Y,Z),true,sum(Y,X,Z),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] : ifeq(product(X,Y,Z),true,product(Y,X,Z),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] : sum(additive_identity,X,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] : sum(X,additive_identity,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Z,V2,Y,V1,V4,V3] : ifeq(product(X,Z,V2),true,ifeq(product(X,Y,V1),true,ifeq(sum(V1,V2,V4),true,ifeq(sum(Y,Z,V3),true,product(X,V3,V4),true),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [Y,Z,V3,X,V4,V2,V1] : ifeq(product(Y,Z,V3),true,ifeq(sum(V3,X,V4),true,ifeq(sum(Z,X,V2),true,ifeq(sum(Y,X,V1),true,product(V1,V2,V4),true),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] : product(X,inverse(X),additive_identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X,Y,V,U] : ifeq2(product(X,Y,V),true,ifeq2(product(X,Y,U),true,U,V),V) = V,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
sum(x,y,z) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
product(x,z,x) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,plain,
! [X0,X1,X2] : ifeq2(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f28,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f30,plain,
! [X0,X1] : product(X0,X1,multiply(X0,X1)) = true,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f31,plain,
! [X0,X1,X2] : ifeq(sum(X0,X1,X2),true,sum(X1,X0,X2),true) = true,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f32,plain,
! [X0,X1,X2] : ifeq(product(X0,X1,X2),true,product(X1,X0,X2),true) = true,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f33,plain,
! [X0] : sum(additive_identity,X0,X0) = true,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f34,plain,
! [X0] : sum(X0,additive_identity,X0) = true,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f38,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq(product(X0,X1,X2),true,ifeq(product(X0,X3,X4),true,ifeq(sum(X4,X2,X5),true,ifeq(sum(X3,X1,X6),true,product(X0,X6,X5),true),true),true),true) = true,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f43,plain,
! [X0,X1,X2,X3,X4,X5,X6] : ifeq(product(X0,X1,X2),true,ifeq(sum(X2,X3,X4),true,ifeq(sum(X1,X3,X5),true,ifeq(sum(X0,X3,X6),true,product(X6,X5,X4),true),true),true),true) = true,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f48,plain,
! [X0] : product(X0,inverse(X0),additive_identity) = true,
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f50,plain,
! [X0,X1,X2,X3] : ifeq2(product(X0,X1,X2),true,ifeq2(product(X0,X1,X3),true,X3,X2),X2) = X2,
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f51,plain,
sum(x,y,z) = true,
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f52,plain,
product(x,z,x) != true,
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f55,plain,
! [X0,X1,X2,X3,X4] : ifeq(product(X0,X1,additive_identity),true,ifeq(product(X0,X2,X3),true,ifeq(true,true,ifeq(sum(X2,X1,X4),true,product(X0,X4,X3),true),true),true),true) = true,
inference(paramodulation,[status(thm)],[f34,f38]) ).
fof(f60,plain,
! [X0,X1,X2,X3,X4] : ifeq(product(X0,X1,additive_identity),true,ifeq(product(X0,X2,X3),true,ifeq(sum(X2,X1,X4),true,product(X0,X4,X3),true),true),true) = true,
inference(forward_demodulation,[status(thm)],[f28,f55]) ).
fof(f80,plain,
! [X0,X1,X2] : ifeq(product(X0,X1,additive_identity),true,ifeq(product(X0,additive_identity,X2),true,ifeq(true,true,product(X0,X1,X2),true),true),true) = true,
inference(paramodulation,[status(thm)],[f33,f60]) ).
fof(f84,plain,
! [X0,X1,X2] : ifeq(product(X0,X1,additive_identity),true,ifeq(product(X0,additive_identity,X2),true,product(X0,X1,X2),true),true) = true,
inference(forward_demodulation,[status(thm)],[f28,f80]) ).
fof(f117,plain,
! [X0,X1,X2,X3,X4] : ifeq(product(X0,X1,additive_identity),true,ifeq(true,true,ifeq(sum(X1,X2,X3),true,ifeq(sum(X0,X2,X4),true,product(X4,X3,X2),true),true),true),true) = true,
inference(paramodulation,[status(thm)],[f33,f43]) ).
fof(f128,plain,
! [X0,X1,X2,X3,X4] : ifeq(product(X0,X1,additive_identity),true,ifeq(sum(X1,X2,X3),true,ifeq(sum(X0,X2,X4),true,product(X4,X3,X2),true),true),true) = true,
inference(forward_demodulation,[status(thm)],[f28,f117]) ).
fof(f175,plain,
ifeq(true,true,sum(y,x,z),true) = true,
inference(paramodulation,[status(thm)],[f51,f31]) ).
fof(f184,plain,
sum(y,x,z) = true,
inference(forward_demodulation,[status(thm)],[f28,f175]) ).
fof(f238,plain,
! [X0,X1] : ifeq(true,true,ifeq(product(X0,additive_identity,X1),true,product(X0,inverse(X0),X1),true),true) = true,
inference(paramodulation,[status(thm)],[f48,f84]) ).
fof(f258,plain,
! [X0,X1] : ifeq(product(X0,additive_identity,X1),true,product(X0,inverse(X0),X1),true) = true,
inference(forward_demodulation,[status(thm)],[f28,f238]) ).
fof(f297,plain,
! [X0,X1] : ifeq(true,true,product(X0,X1,multiply(X1,X0)),true) = true,
inference(paramodulation,[status(thm)],[f30,f32]) ).
fof(f303,plain,
! [X0,X1] : product(X0,X1,multiply(X1,X0)) = true,
inference(forward_demodulation,[status(thm)],[f28,f297]) ).
fof(f882,plain,
! [X0,X1,X2] : ifeq2(product(X0,X1,X2),true,ifeq2(true,true,multiply(X1,X0),X2),X2) = X2,
inference(paramodulation,[status(thm)],[f303,f50]) ).
fof(f885,plain,
! [X0,X1,X2] : ifeq2(product(X0,X1,X2),true,multiply(X1,X0),X2) = X2,
inference(forward_demodulation,[status(thm)],[f27,f882]) ).
fof(f904,plain,
! [X0] : ifeq2(true,true,multiply(inverse(X0),X0),additive_identity) = additive_identity,
inference(paramodulation,[status(thm)],[f48,f885]) ).
fof(f914,plain,
! [X0] : multiply(inverse(X0),X0) = additive_identity,
inference(forward_demodulation,[status(thm)],[f27,f904]) ).
fof(f1739,plain,
! [X0] : ifeq(true,true,product(X0,inverse(X0),multiply(X0,additive_identity)),true) = true,
inference(paramodulation,[status(thm)],[f30,f258]) ).
fof(f1749,plain,
! [X0] : product(X0,inverse(X0),multiply(X0,additive_identity)) = true,
inference(forward_demodulation,[status(thm)],[f28,f1739]) ).
fof(f1783,plain,
! [X0] : ifeq2(true,true,multiply(inverse(X0),X0),multiply(X0,additive_identity)) = multiply(X0,additive_identity),
inference(paramodulation,[status(thm)],[f1749,f885]) ).
fof(f1810,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(X0,additive_identity),
inference(forward_demodulation,[status(thm)],[f27,f1783]) ).
fof(f1811,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(forward_demodulation,[status(thm)],[f914,f1810]) ).
fof(f1868,plain,
! [X0] : product(X0,additive_identity,additive_identity) = true,
inference(paramodulation,[status(thm)],[f1811,f30]) ).
fof(f2580,plain,
! [X0,X1,X2] : ifeq(product(X0,additive_identity,additive_identity),true,ifeq(true,true,ifeq(sum(X0,X1,X2),true,product(X2,X1,X1),true),true),true) = true,
inference(paramodulation,[status(thm)],[f33,f128]) ).
fof(f2635,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(true,true,ifeq(sum(X0,X1,X2),true,product(X2,X1,X1),true),true),true) = true,
inference(forward_demodulation,[status(thm)],[f1868,f2580]) ).
fof(f2636,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(sum(X0,X1,X2),true,product(X2,X1,X1),true),true) = true,
inference(forward_demodulation,[status(thm)],[f28,f2635]) ).
fof(f2637,plain,
! [X0,X1,X2] : ifeq(sum(X0,X1,X2),true,product(X2,X1,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f28,f2636]) ).
fof(f3304,plain,
ifeq(true,true,product(z,x,x),true) = true,
inference(paramodulation,[status(thm)],[f184,f2637]) ).
fof(f3361,plain,
product(z,x,x) = true,
inference(forward_demodulation,[status(thm)],[f28,f3304]) ).
fof(f3792,plain,
ifeq(true,true,product(x,z,x),true) = true,
inference(paramodulation,[status(thm)],[f3361,f32]) ).
fof(f3804,plain,
product(x,z,x) = true,
inference(forward_demodulation,[status(thm)],[f28,f3792]) ).
fof(f3805,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3804,f52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO017-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/10.47 % Computer : n004.cluster.edu
% 0.19/10.47 % Model : x86_64 x86_64
% 0.19/10.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/10.47 % Memory : 8046.5625MB
% 0.19/10.47 % OS : Linux 6.8.0-71-generic
% 0.19/10.47 % CPULimit : 300
% 0.19/10.47 % WCLimit : 300
% 0.19/10.47 % DateTime : Mon Sep 21 13:48:34 UTC 2026
% 0.19/10.47 % CPUTime :
% 0.19/10.48 % Drodi V4.1.1
% 60.08/18.16 % Refutation found
% 60.08/18.16 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 60.08/18.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.67/18.44 % Elapsed time: 7.953505 seconds
% 6.67/18.44 % CPU time: 61.468147 seconds
% 6.67/18.44 % Total memory used: 604.040 MB
% 6.67/18.44 % Net memory used: 589.336 MB
%------------------------------------------------------------------------------