%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO017-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 : Fri Sep 25 12:59:38 PM UTC 2026
% Result : Unsatisfiable 37.19s 5.71s
% Output : CNFRefutation 37.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 18
% Syntax : Number of clauses : 79 ( 79 unt; 0 nHn; 11 RR)
% Number of literals : 79 ( 78 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-4 aty)
% Number of variables : 144 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t204,axiom,
ifeq(product(X1,X2,X3),true,product(X2,X1,X3),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1300,plain,
ifeq(product(X1,X2,X3),true,product(X2,X1,X3),true) = true,
inference(orient,[status(thm)],[t204]) ).
cnf(hi2,axiom,
ifeq(sum(X,Y,Z),true,sum(Y,X,Z),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi0,axiom,
sum(X,Y,add(X,Y)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h1,plain,
sum(V0,V1,add(V1,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi0]) ).
cnf(hi12,axiom,
ifeq(product(Y,Z,V3),true,ifeq(sum(X,V3,V4),true,ifeq(sum(X,Z,V2),true,ifeq(sum(X,Y,V1),true,product(V1,V2,V4),true),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi1,axiom,
product(X,Y,multiply(X,Y)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi22,axiom,
sum(x,y,z) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t167,plain,
product(z,add(x,X1),add(multiply(y,X1),x)) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi1,h1,hi0,hi22]) ).
cnf(hi15,axiom,
ifeq(product(V1,V2,V4),true,ifeq(product(Y,Z,V3),true,ifeq(sum(Z,X,V2),true,ifeq(sum(Y,X,V1),true,sum(V3,X,V4),true),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h5,plain,
sum(multiply(V0,V1),V2,multiply(add(V0,V2),add(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi15,hi1,hi1,hi0,hi0]) ).
cnf(hi20,axiom,
ifeq2(sum(X,Y,V),true,ifeq2(sum(X,Y,U),true,U,V),V) = V,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t209,plain,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
inference(hyper_resolution,[status(thm)],[hi20,hi0,h5]) ).
cnf(t208,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(hyper_resolution,[status(thm)],[hi20,h1,h5]) ).
cnf(t416,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t208]) ).
cnf(t3329,plain,
add(X2,multiply(X1,X3)) = add(multiply(X1,X3),X2),
inference(step,[status(thm)],[t209,t416]) ).
cnf(t440,plain,
add(X1,multiply(X2,X3)) = add(multiply(X2,X3),X1),
inference(orient,[status(thm)],[t3329]) ).
cnf(t3342,plain,
product(z,add(x,X1),add(x,multiply(y,X1))) = true,
inference(step,[status(thm)],[t167,t440]) ).
cnf(t1006,plain,
product(z,add(x,X1),add(x,multiply(y,X1))) = true,
inference(orient,[status(thm)],[t3342]) ).
cnf(hi11,axiom,
ifeq(product(Z,X,V2),true,ifeq(product(Y,X,V1),true,ifeq(sum(V1,V2,V4),true,ifeq(sum(Y,Z,V3),true,product(V3,X,V4),true),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h22,plain,
product(add(V0,V1),V2,add(multiply(V0,V2),multiply(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi1,hi1,hi0,hi0]) ).
cnf(hi21,axiom,
ifeq2(product(X,Y,V),true,ifeq2(product(X,Y,U),true,U,V),V) = V,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t196,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(hyper_resolution,[status(thm)],[hi21,hi1,h22]) ).
cnf(t359,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t196]) ).
cnf(hi6,axiom,
product(multiplicative_identity,X,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
multiply(multiplicative_identity,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi1,hi6]) ).
cnf(t257,plain,
multiply(multiplicative_identity,X1) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t364,plain,
multiply(add(multiplicative_identity,X1),X2) = add(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t359,t257]) ).
cnf(h20,plain,
product(add(V0,V1),add(V0,V2),add(V0,multiply(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi1,hi0,hi0,hi0]) ).
cnf(hi14,axiom,
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/sandbox/benchmark/theBenchmark.p') ).
cnf(hi4,axiom,
sum(additive_identity,X,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(h8,plain,
product(V0,add(V1,V0),add(multiply(additive_identity,V1),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi14,hi1,hi0,hi0,hi4]) ).
cnf(t225,plain,
add(multiply(additive_identity,X1),add(X1,X2)) = add(X1,multiply(X2,add(X1,X2))),
inference(hyper_resolution,[status(thm)],[hi21,h8,h20]) ).
cnf(t650,plain,
add(X1,multiply(X2,add(X1,X2))) = add(multiply(additive_identity,X1),add(X1,X2)),
inference(orient,[status(thm)],[t225]) ).
cnf(hi17,axiom,
sum(X,inverse(X),multiplicative_identity) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(hyper_resolution,[status(thm)],[hi20,hi0,hi17]) ).
cnf(t751,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t9]) ).
cnf(t762,plain,
add(multiply(additive_identity,X1),add(X1,inverse(X1))) = add(X1,multiply(inverse(X1),multiplicative_identity)),
inference(cp,[status(thm)],[t650,t751]) ).
cnf(t3366,plain,
add(multiply(additive_identity,X1),multiplicative_identity) = add(X1,multiply(inverse(X1),multiplicative_identity)),
inference(step,[status(thm)],[t762,t751]) ).
cnf(h4,plain,
sum(multiply(additive_identity,V0),V1,multiply(V1,add(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi15,hi1,hi1,hi0,hi4]) ).
cnf(t126,plain,
multiply(X1,add(X2,X1)) = add(multiply(additive_identity,X2),X1),
inference(hyper_resolution,[status(thm)],[hi20,hi0,h4]) ).
cnf(t285,plain,
add(multiply(additive_identity,X1),X2) = multiply(X2,add(X1,X2)),
inference(orient,[status(thm)],[t126]) ).
cnf(t3367,plain,
multiply(multiplicative_identity,add(X1,multiplicative_identity)) = add(X1,multiply(inverse(X1),multiplicative_identity)),
inference(step,[status(thm)],[t3366,t285]) ).
cnf(t3368,plain,
add(X1,multiplicative_identity) = add(X1,multiply(inverse(X1),multiplicative_identity)),
inference(step,[status(thm)],[t3367,t257]) ).
cnf(hi7,axiom,
product(X,multiplicative_identity,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t7,plain,
multiply(X1,multiplicative_identity) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi1,hi7]) ).
cnf(t256,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t3369,plain,
add(X1,multiplicative_identity) = add(X1,inverse(X1)),
inference(step,[status(thm)],[t3368,t256]) ).
cnf(t3370,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(step,[status(thm)],[t3369,t751]) ).
cnf(t2789,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t3370]) ).
cnf(t19,plain,
add(X1,X2) = add(X2,X1),
inference(hyper_resolution,[status(thm)],[hi20,hi0,h1]) ).
cnf(t559,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t19]) ).
cnf(t2790,plain,
multiplicative_identity = add(multiplicative_identity,X1),
inference(cp,[status(thm)],[t2789,t559]) ).
cnf(t2796,plain,
add(multiplicative_identity,X1) = multiplicative_identity,
inference(orient,[status(thm)],[t2790]) ).
cnf(t3380,plain,
multiply(multiplicative_identity,X2) = add(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t364,t2796]) ).
cnf(t3381,plain,
X2 = add(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t3380,t257]) ).
cnf(t3078,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t3381]) ).
cnf(h21,plain,
product(V0,V1,add(multiply(additive_identity,V1),multiply(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi1,hi1,hi0,hi4]) ).
cnf(t64,plain,
add(multiply(additive_identity,multiplicative_identity),multiply(X1,multiplicative_identity)) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi7,h21]) ).
cnf(t3325,plain,
add(additive_identity,multiply(X1,multiplicative_identity)) = X1,
inference(step,[status(thm)],[t64,t256]) ).
cnf(t3326,plain,
add(additive_identity,X1) = X1,
inference(step,[status(thm)],[t3325,t256]) ).
cnf(t262,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t3326]) ).
cnf(t3079,plain,
additive_identity = multiply(X1,additive_identity),
inference(cp,[status(thm)],[t3078,t262]) ).
cnf(t3115,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t3079]) ).
cnf(t3123,plain,
true = product(z,add(x,additive_identity),add(x,additive_identity)),
inference(cp,[status(thm)],[t1006,t3115]) ).
cnf(hi5,axiom,
sum(X,additive_identity,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t2,plain,
add(X1,additive_identity) = X1,
inference(hyper_resolution,[status(thm)],[hi20,hi0,hi5]) ).
cnf(t258,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t3392,plain,
true = product(z,x,add(x,additive_identity)),
inference(step,[status(thm)],[t3123,t258]) ).
cnf(t3393,plain,
true = product(z,x,x),
inference(step,[status(thm)],[t3392,t258]) ).
cnf(t3230,plain,
product(z,x,x) = true,
inference(orient,[status(thm)],[t3393]) ).
cnf(t3231,plain,
true = ifeq(true,true,product(x,z,x),true),
inference(cp,[status(thm)],[t1300,t3230]) ).
cnf(t23,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t263,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t23]) ).
cnf(t3395,plain,
true = product(x,z,x),
inference(step,[status(thm)],[t3231,t263]) ).
cnf(t3301,plain,
product(x,z,x) = true,
inference(orient,[status(thm)],[t3395]) ).
cnf(goal_0,negated_conjecture,
product(x,z,x) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t3301]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO017-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n005.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Fri Sep 25 06:33:18 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 37.19/5.71 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.19/5.71 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------