%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO014-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.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:36 PM UTC 2026
% Result : Unsatisfiable 49.42s 7.29s
% Output : CNFRefutation 49.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 20
% Syntax : Number of clauses : 245 ( 245 unt; 0 nHn; 78 RR)
% Number of literals : 245 ( 244 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 : 14 ( 14 usr; 7 con; 0-4 aty)
% Number of variables : 289 ( 42 sgn)
% Comments :
%------------------------------------------------------------------------------
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/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi1,axiom,
product(X,Y,multiply(X,Y)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi0,axiom,
sum(X,Y,add(X,Y)) = true,
file('/export/starexec/sandbox2/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(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/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi4,axiom,
sum(additive_identity,X,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h17,plain,
product(V0,V1,add(additive_identity,multiply(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi1,hi0,hi4,hi4]) ).
cnf(hi21,axiom,
ifeq2(product(X,Y,V),true,ifeq2(product(X,Y,U),true,U,V),V) = V,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t228,plain,
add(multiply(X1,X2),multiply(X3,X2)) = add(additive_identity,multiply(add(X1,X3),X2)),
inference(hyper_resolution,[status(thm)],[hi21,h17,h22]) ).
cnf(hi20,axiom,
ifeq2(sum(X,Y,V),true,ifeq2(sum(X,Y,U),true,U,V),V) = V,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3,plain,
add(additive_identity,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi20,hi4,hi0]) ).
cnf(t259,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t10886,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(step,[status(thm)],[t228,t259]) ).
cnf(t668,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t10886]) ).
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(hi18,axiom,
product(inverse(X),X,additive_identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t81,plain,
add(multiply(additive_identity,X1),multiply(inverse(X1),X1)) = additive_identity,
inference(hyper_resolution,[status(thm)],[hi21,hi18,h21]) ).
cnf(t10894,plain,
multiply(add(additive_identity,inverse(X1)),X1) = additive_identity,
inference(step,[status(thm)],[t81,t668]) ).
cnf(t10895,plain,
multiply(inverse(X1),X1) = additive_identity,
inference(step,[status(thm)],[t10894,t259]) ).
cnf(t908,plain,
multiply(inverse(X1),X1) = additive_identity,
inference(orient,[status(thm)],[t10895]) ).
cnf(t910,plain,
multiply(add(inverse(X1),X2),X1) = add(additive_identity,multiply(X2,X1)),
inference(cp,[status(thm)],[t668,t908]) ).
cnf(t11051,plain,
multiply(add(inverse(X1),X2),X1) = multiply(X2,X1),
inference(step,[status(thm)],[t910,t259]) ).
cnf(t5817,plain,
multiply(add(inverse(X1),X2),X1) = multiply(X2,X1),
inference(orient,[status(thm)],[t11051]) ).
cnf(hi17,axiom,
sum(X,inverse(X),multiplicative_identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t10,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(hyper_resolution,[status(thm)],[hi20,hi0,hi17]) ).
cnf(t509,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t10]) ).
cnf(t5833,plain,
multiply(inverse(inverse(X1)),X1) = multiply(multiplicative_identity,X1),
inference(cp,[status(thm)],[t5817,t509]) ).
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/sandbox2/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(t183,plain,
add(additive_identity,multiply(X1,add(X2,X1))) = add(multiply(additive_identity,X2),X1),
inference(hyper_resolution,[status(thm)],[hi21,h8,h17]) ).
cnf(t10891,plain,
multiply(X1,add(X2,X1)) = add(multiply(additive_identity,X2),X1),
inference(step,[status(thm)],[t183,t259]) ).
cnf(t829,plain,
add(multiply(additive_identity,X1),X2) = multiply(X2,add(X1,X2)),
inference(orient,[status(thm)],[t10891]) ).
cnf(hi6,axiom,
product(multiplicative_identity,X,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
add(additive_identity,multiply(multiplicative_identity,X1)) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi6,h17]) ).
cnf(t10881,plain,
multiply(multiplicative_identity,X1) = X1,
inference(step,[status(thm)],[t21,t259]) ).
cnf(t261,plain,
multiply(multiplicative_identity,X1) = X1,
inference(orient,[status(thm)],[t10881]) ).
cnf(t675,plain,
multiply(add(multiplicative_identity,X1),X2) = add(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t668,t261]) ).
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(t231,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(t367,plain,
add(X1,multiply(X2,add(X1,X2))) = add(multiply(additive_identity,X1),add(X1,X2)),
inference(orient,[status(thm)],[t231]) ).
cnf(t520,plain,
add(multiply(additive_identity,X1),add(X1,inverse(X1))) = add(X1,multiply(inverse(X1),multiplicative_identity)),
inference(cp,[status(thm)],[t367,t509]) ).
cnf(t10951,plain,
add(multiply(additive_identity,X1),multiplicative_identity) = add(X1,multiply(inverse(X1),multiplicative_identity)),
inference(step,[status(thm)],[t520,t509]) ).
cnf(t10952,plain,
multiply(multiplicative_identity,add(X1,multiplicative_identity)) = add(X1,multiply(inverse(X1),multiplicative_identity)),
inference(step,[status(thm)],[t10951,t829]) ).
cnf(t10953,plain,
add(X1,multiplicative_identity) = add(X1,multiply(inverse(X1),multiplicative_identity)),
inference(step,[status(thm)],[t10952,t261]) ).
cnf(hi7,axiom,
product(X,multiplicative_identity,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
add(additive_identity,multiply(X1,multiplicative_identity)) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi7,h17]) ).
cnf(t10880,plain,
multiply(X1,multiplicative_identity) = X1,
inference(step,[status(thm)],[t20,t259]) ).
cnf(t260,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t10880]) ).
cnf(t10954,plain,
add(X1,multiplicative_identity) = add(X1,inverse(X1)),
inference(step,[status(thm)],[t10953,t260]) ).
cnf(t10955,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(step,[status(thm)],[t10954,t509]) ).
cnf(t2394,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t10955]) ).
cnf(hi2,axiom,
ifeq(sum(X,Y,Z),true,sum(Y,X,Z),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h1,plain,
sum(V0,V1,add(V1,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi0]) ).
cnf(t19,plain,
add(X1,X2) = add(X2,X1),
inference(hyper_resolution,[status(thm)],[hi20,hi0,h1]) ).
cnf(t267,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t19]) ).
cnf(t2395,plain,
multiplicative_identity = add(multiplicative_identity,X1),
inference(cp,[status(thm)],[t2394,t267]) ).
cnf(t2403,plain,
add(multiplicative_identity,X1) = multiplicative_identity,
inference(orient,[status(thm)],[t2395]) ).
cnf(t10964,plain,
multiply(multiplicative_identity,X2) = add(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t675,t2403]) ).
cnf(t10965,plain,
X2 = add(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t10964,t261]) ).
cnf(t2699,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t10965]) ).
cnf(t2723,plain,
add(multiply(additive_identity,X1),multiply(X2,X1)) = multiply(multiply(X2,X1),X1),
inference(cp,[status(thm)],[t829,t2699]) ).
cnf(t10976,plain,
multiply(add(additive_identity,X2),X1) = multiply(multiply(X2,X1),X1),
inference(step,[status(thm)],[t2723,t668]) ).
cnf(t10977,plain,
multiply(X2,X1) = multiply(multiply(X2,X1),X1),
inference(step,[status(thm)],[t10976,t259]) ).
cnf(t3059,plain,
multiply(multiply(X1,X2),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t10977]) ).
cnf(t3061,plain,
multiply(inverse(X1),X1) = multiply(additive_identity,X1),
inference(cp,[status(thm)],[t3059,t908]) ).
cnf(t10978,plain,
additive_identity = multiply(additive_identity,X1),
inference(step,[status(thm)],[t3061,t908]) ).
cnf(t3070,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t10978]) ).
cnf(t10979,plain,
add(additive_identity,X2) = multiply(X2,add(X1,X2)),
inference(step,[status(thm)],[t829,t3070]) ).
cnf(t10980,plain,
X2 = multiply(X2,add(X1,X2)),
inference(step,[status(thm)],[t10979,t259]) ).
cnf(t3071,plain,
X2 = multiply(X2,add(X1,X2)),
inference(rw,[status(thm)],[t10980]) ).
cnf(t3079,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t3071]) ).
cnf(t226,plain,
add(additive_identity,multiply(add(X1,X2),add(X1,X3))) = add(X1,multiply(X2,X3)),
inference(hyper_resolution,[status(thm)],[hi21,h17,h20]) ).
cnf(t10883,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(step,[status(thm)],[t226,t259]) ).
cnf(t297,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t10883]) ).
cnf(t511,plain,
add(X1,multiply(inverse(X1),X2)) = multiply(multiplicative_identity,add(X1,X2)),
inference(cp,[status(thm)],[t297,t509]) ).
cnf(t11026,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(step,[status(thm)],[t511,t261]) ).
cnf(t4785,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(orient,[status(thm)],[t11026]) ).
cnf(hi19,axiom,
product(X,inverse(X),additive_identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t106,plain,
add(multiply(additive_identity,inverse(X1)),multiply(X1,inverse(X1))) = additive_identity,
inference(hyper_resolution,[status(thm)],[hi21,hi19,h21]) ).
cnf(t10896,plain,
multiply(add(additive_identity,X1),inverse(X1)) = additive_identity,
inference(step,[status(thm)],[t106,t668]) ).
cnf(t10897,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(step,[status(thm)],[t10896,t259]) ).
cnf(t916,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t10897]) ).
cnf(t4795,plain,
add(X1,inverse(inverse(X1))) = add(X1,additive_identity),
inference(cp,[status(thm)],[t4785,t916]) ).
cnf(hi5,axiom,
sum(X,additive_identity,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t2,plain,
add(X1,additive_identity) = X1,
inference(hyper_resolution,[status(thm)],[hi20,hi0,hi5]) ).
cnf(t256,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t11033,plain,
add(X1,inverse(inverse(X1))) = X1,
inference(step,[status(thm)],[t4795,t256]) ).
cnf(t4829,plain,
add(X1,inverse(inverse(X1))) = X1,
inference(orient,[status(thm)],[t11033]) ).
cnf(t4838,plain,
inverse(inverse(X1)) = multiply(inverse(inverse(X1)),X1),
inference(cp,[status(thm)],[t3079,t4829]) ).
cnf(t4864,plain,
multiply(inverse(inverse(X1)),X1) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t4838]) ).
cnf(t11052,plain,
inverse(inverse(X1)) = multiply(multiplicative_identity,X1),
inference(step,[status(thm)],[t5833,t4864]) ).
cnf(t11053,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t11052,t261]) ).
cnf(t5850,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t11053]) ).
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/sandbox2/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(t203,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(hyper_resolution,[status(thm)],[hi20,h1,h5]) ).
cnf(t306,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t203]) ).
cnf(t298,plain,
add(X1,multiply(additive_identity,X2)) = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t297,t256]) ).
cnf(t10988,plain,
add(X1,additive_identity) = multiply(X1,add(X1,X2)),
inference(step,[status(thm)],[t298,t3070]) ).
cnf(t10989,plain,
X1 = multiply(X1,add(X1,X2)),
inference(step,[status(thm)],[t10988,t256]) ).
cnf(t3099,plain,
multiply(X1,add(X1,X2)) = X1,
inference(orient,[status(thm)],[t10989]) ).
cnf(hi22,negated_conjecture,
sum(x,y,x_plus_y) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t6,plain,
add(y,x) = x_plus_y,
inference(hyper_resolution,[status(thm)],[hi20,hi22,h1]) ).
cnf(t928,plain,
add(y,x) = x_plus_y,
inference(orient,[status(thm)],[t6]) ).
cnf(t3101,plain,
y = multiply(y,x_plus_y),
inference(cp,[status(thm)],[t3099,t928]) ).
cnf(t3108,plain,
multiply(y,x_plus_y) = y,
inference(orient,[status(thm)],[t3101]) ).
cnf(t3109,plain,
x_plus_y = add(x_plus_y,y),
inference(cp,[status(thm)],[t2699,t3108]) ).
cnf(t10990,plain,
x_plus_y = add(y,x_plus_y),
inference(step,[status(thm)],[t3109,t267]) ).
cnf(t3112,plain,
add(y,x_plus_y) = x_plus_y,
inference(orient,[status(thm)],[t10990]) ).
cnf(t3118,plain,
add(x_plus_y,multiply(X1,y)) = multiply(add(X1,x_plus_y),x_plus_y),
inference(cp,[status(thm)],[t306,t3112]) ).
cnf(h7,plain,
product(add(V0,V1),V1,add(multiply(V0,additive_identity),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi14,hi1,hi0,hi4,hi0]) ).
cnf(t190,plain,
add(multiply(X1,X2),multiply(X2,X2)) = add(multiply(X1,additive_identity),X2),
inference(hyper_resolution,[status(thm)],[hi21,h7,h22]) ).
cnf(t10889,plain,
multiply(add(X1,X2),X2) = add(multiply(X1,additive_identity),X2),
inference(step,[status(thm)],[t190,t668]) ).
cnf(t697,plain,
add(multiply(X1,additive_identity),X2) = multiply(add(X1,X2),X2),
inference(orient,[status(thm)],[t10889]) ).
cnf(t2700,plain,
additive_identity = multiply(X1,additive_identity),
inference(cp,[status(thm)],[t2699,t259]) ).
cnf(t2729,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t2700]) ).
cnf(t10966,plain,
add(additive_identity,X2) = multiply(add(X1,X2),X2),
inference(step,[status(thm)],[t697,t2729]) ).
cnf(t10967,plain,
X2 = multiply(add(X1,X2),X2),
inference(step,[status(thm)],[t10966,t259]) ).
cnf(t2733,plain,
X2 = multiply(add(X1,X2),X2),
inference(rw,[status(thm)],[t10967]) ).
cnf(t2834,plain,
multiply(add(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t2733]) ).
cnf(t10993,plain,
add(x_plus_y,multiply(X1,y)) = x_plus_y,
inference(step,[status(thm)],[t3118,t2834]) ).
cnf(t3238,plain,
add(x_plus_y,multiply(X1,y)) = x_plus_y,
inference(orient,[status(thm)],[t10993]) ).
cnf(t3248,plain,
multiply(X1,y) = multiply(multiply(X1,y),x_plus_y),
inference(cp,[status(thm)],[t3079,t3238]) ).
cnf(t3314,plain,
multiply(multiply(X1,y),x_plus_y) = multiply(X1,y),
inference(orient,[status(thm)],[t3248]) ).
cnf(t4878,plain,
multiply(inverse(inverse(y)),y) = multiply(inverse(inverse(y)),x_plus_y),
inference(cp,[status(thm)],[t3314,t4864]) ).
cnf(t11035,plain,
inverse(inverse(y)) = multiply(inverse(inverse(y)),x_plus_y),
inference(step,[status(thm)],[t4878,t4864]) ).
cnf(t5030,plain,
multiply(inverse(inverse(y)),x_plus_y) = inverse(inverse(y)),
inference(orient,[status(thm)],[t11035]) ).
cnf(t5038,plain,
add(inverse(y),x_plus_y) = add(inverse(y),inverse(inverse(y))),
inference(cp,[status(thm)],[t4785,t5030]) ).
cnf(t11036,plain,
add(x_plus_y,inverse(y)) = add(inverse(y),inverse(inverse(y))),
inference(step,[status(thm)],[t5038,t267]) ).
cnf(t11037,plain,
add(x_plus_y,inverse(y)) = multiplicative_identity,
inference(step,[status(thm)],[t11036,t509]) ).
cnf(t5039,plain,
add(x_plus_y,inverse(y)) = multiplicative_identity,
inference(orient,[status(thm)],[t11037]) ).
cnf(t5041,plain,
add(x_plus_y,multiply(X1,inverse(y))) = multiply(add(x_plus_y,X1),multiplicative_identity),
inference(cp,[status(thm)],[t297,t5039]) ).
cnf(t11164,plain,
add(x_plus_y,multiply(X1,inverse(y))) = add(x_plus_y,X1),
inference(step,[status(thm)],[t5041,t260]) ).
cnf(t10686,plain,
add(x_plus_y,multiply(X1,inverse(y))) = add(x_plus_y,X1),
inference(orient,[status(thm)],[t11164]) ).
cnf(hi23,negated_conjecture,
product(inverse(x),inverse(y),x_inverse_times_y_inverse) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t162,plain,
add(multiply(additive_identity,inverse(y)),multiply(inverse(x),inverse(y))) = x_inverse_times_y_inverse,
inference(hyper_resolution,[status(thm)],[hi21,hi23,h21]) ).
cnf(t10898,plain,
multiply(add(additive_identity,inverse(x)),inverse(y)) = x_inverse_times_y_inverse,
inference(step,[status(thm)],[t162,t668]) ).
cnf(t10899,plain,
multiply(inverse(x),inverse(y)) = x_inverse_times_y_inverse,
inference(step,[status(thm)],[t10898,t259]) ).
cnf(t924,plain,
multiply(inverse(x),inverse(y)) = x_inverse_times_y_inverse,
inference(orient,[status(thm)],[t10899]) ).
cnf(t10692,plain,
add(x_plus_y,inverse(x)) = add(x_plus_y,x_inverse_times_y_inverse),
inference(cp,[status(thm)],[t10686,t924]) ).
cnf(t3080,plain,
x = multiply(x,x_plus_y),
inference(cp,[status(thm)],[t3079,t928]) ).
cnf(t3088,plain,
multiply(x,x_plus_y) = x,
inference(orient,[status(thm)],[t3080]) ).
cnf(t3089,plain,
x_plus_y = add(x_plus_y,x),
inference(cp,[status(thm)],[t2699,t3088]) ).
cnf(t3092,plain,
add(x_plus_y,x) = x_plus_y,
inference(orient,[status(thm)],[t3089]) ).
cnf(t3094,plain,
add(x_plus_y,multiply(X1,x)) = multiply(add(x_plus_y,X1),x_plus_y),
inference(cp,[status(thm)],[t297,t3092]) ).
cnf(hi10,axiom,
ifeq(product(V3,X,V4),true,ifeq(product(Z,X,V2),true,ifeq(product(Y,X,V1),true,ifeq(sum(Y,Z,V3),true,sum(V1,V2,V4),true),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(h23,plain,
sum(multiply(additive_identity,V0),multiply(V1,V0),multiply(V1,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi1,hi1,hi1,hi4]) ).
cnf(h2,plain,
sum(multiply(additive_identity,additive_identity),V0,multiply(V0,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi15,hi1,hi1,hi4,hi4]) ).
cnf(t121,plain,
multiply(multiply(X1,additive_identity),multiply(X1,additive_identity)) = multiply(X1,additive_identity),
inference(hyper_resolution,[status(thm)],[hi20,h2,h23]) ).
cnf(t938,plain,
multiply(multiply(X1,additive_identity),multiply(X1,additive_identity)) = multiply(X1,additive_identity),
inference(orient,[status(thm)],[t121]) ).
cnf(t939,plain,
multiply(inverse(additive_identity),additive_identity) = multiply(additive_identity,multiply(inverse(additive_identity),additive_identity)),
inference(cp,[status(thm)],[t938,t908]) ).
cnf(t10936,plain,
additive_identity = multiply(additive_identity,multiply(inverse(additive_identity),additive_identity)),
inference(step,[status(thm)],[t939,t908]) ).
cnf(t10937,plain,
additive_identity = multiply(additive_identity,additive_identity),
inference(step,[status(thm)],[t10936,t908]) ).
cnf(t2265,plain,
multiply(additive_identity,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t10937]) ).
cnf(t2268,plain,
multiply(X1,add(additive_identity,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t829,t2265]) ).
cnf(t10946,plain,
multiply(X1,X1) = add(additive_identity,X1),
inference(step,[status(thm)],[t2268,t259]) ).
cnf(t10947,plain,
multiply(X1,X1) = X1,
inference(step,[status(thm)],[t10946,t259]) ).
cnf(t2279,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t10947]) ).
cnf(t2703,plain,
X1 = add(X1,X1),
inference(cp,[status(thm)],[t2699,t2279]) ).
cnf(t2736,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t2703]) ).
cnf(t2738,plain,
add(X1,multiply(X2,X1)) = multiply(add(X1,X2),X1),
inference(cp,[status(thm)],[t297,t2736]) ).
cnf(t10973,plain,
X1 = multiply(add(X1,X2),X1),
inference(step,[status(thm)],[t2738,t2699]) ).
cnf(t2904,plain,
multiply(add(X1,X2),X1) = X1,
inference(orient,[status(thm)],[t10973]) ).
cnf(t10991,plain,
add(x_plus_y,multiply(X1,x)) = x_plus_y,
inference(step,[status(thm)],[t3094,t2904]) ).
cnf(t3215,plain,
add(x_plus_y,multiply(X1,x)) = x_plus_y,
inference(orient,[status(thm)],[t10991]) ).
cnf(t3218,plain,
multiply(X1,x) = multiply(multiply(X1,x),x_plus_y),
inference(cp,[status(thm)],[t3079,t3215]) ).
cnf(t3290,plain,
multiply(multiply(X1,x),x_plus_y) = multiply(X1,x),
inference(orient,[status(thm)],[t3218]) ).
cnf(t4880,plain,
multiply(inverse(inverse(x)),x) = multiply(inverse(inverse(x)),x_plus_y),
inference(cp,[status(thm)],[t3290,t4864]) ).
cnf(t11039,plain,
inverse(inverse(x)) = multiply(inverse(inverse(x)),x_plus_y),
inference(step,[status(thm)],[t4880,t4864]) ).
cnf(t5108,plain,
multiply(inverse(inverse(x)),x_plus_y) = inverse(inverse(x)),
inference(orient,[status(thm)],[t11039]) ).
cnf(t5116,plain,
add(inverse(x),x_plus_y) = add(inverse(x),inverse(inverse(x))),
inference(cp,[status(thm)],[t4785,t5108]) ).
cnf(t11040,plain,
add(x_plus_y,inverse(x)) = add(inverse(x),inverse(inverse(x))),
inference(step,[status(thm)],[t5116,t267]) ).
cnf(t11041,plain,
add(x_plus_y,inverse(x)) = multiplicative_identity,
inference(step,[status(thm)],[t11040,t509]) ).
cnf(t5117,plain,
add(x_plus_y,inverse(x)) = multiplicative_identity,
inference(orient,[status(thm)],[t11041]) ).
cnf(t11165,plain,
multiplicative_identity = add(x_plus_y,x_inverse_times_y_inverse),
inference(step,[status(thm)],[t10692,t5117]) ).
cnf(t10715,plain,
add(x_plus_y,x_inverse_times_y_inverse) = multiplicative_identity,
inference(orient,[status(thm)],[t11165]) ).
cnf(t10716,plain,
add(x_plus_y,multiply(x_inverse_times_y_inverse,X1)) = multiply(multiplicative_identity,add(x_plus_y,X1)),
inference(cp,[status(thm)],[t297,t10715]) ).
cnf(t11170,plain,
add(x_plus_y,multiply(x_inverse_times_y_inverse,X1)) = add(x_plus_y,X1),
inference(step,[status(thm)],[t10716,t261]) ).
cnf(t10823,plain,
add(x_plus_y,multiply(x_inverse_times_y_inverse,X1)) = add(x_plus_y,X1),
inference(orient,[status(thm)],[t11170]) ).
cnf(t10830,plain,
add(x_plus_y,inverse(x_inverse_times_y_inverse)) = add(x_plus_y,additive_identity),
inference(cp,[status(thm)],[t10823,t916]) ).
cnf(t929,plain,
add(y,multiply(x,X1)) = multiply(x_plus_y,add(y,X1)),
inference(cp,[status(thm)],[t297,t928]) ).
cnf(t3907,plain,
add(y,multiply(x,X1)) = multiply(x_plus_y,add(y,X1)),
inference(orient,[status(thm)],[t929]) ).
cnf(t513,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(multiplicative_identity,add(X2,inverse(X1))),
inference(cp,[status(thm)],[t306,t509]) ).
cnf(t11059,plain,
add(inverse(X1),multiply(X1,X2)) = add(X2,inverse(X1)),
inference(step,[status(thm)],[t513,t261]) ).
cnf(t5881,plain,
add(inverse(X1),multiply(X1,X2)) = add(X2,inverse(X1)),
inference(orient,[status(thm)],[t11059]) ).
cnf(t300,plain,
add(X1,multiply(X2,X3)) = multiply(add(X2,X1),add(X1,X3)),
inference(cp,[status(thm)],[t297,t267]) ).
cnf(t4021,plain,
multiply(add(X1,X2),add(X2,X3)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t300]) ).
cnf(t4023,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t4021,t2736]) ).
cnf(t11005,plain,
add(X1,multiply(X1,X2)) = X1,
inference(step,[status(thm)],[t4023,t3099]) ).
cnf(t4062,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t11005]) ).
cnf(t4074,plain,
inverse(x) = add(inverse(x),x_inverse_times_y_inverse),
inference(cp,[status(thm)],[t4062,t924]) ).
cnf(t11006,plain,
inverse(x) = add(x_inverse_times_y_inverse,inverse(x)),
inference(step,[status(thm)],[t4074,t267]) ).
cnf(t4094,plain,
add(x_inverse_times_y_inverse,inverse(x)) = inverse(x),
inference(orient,[status(thm)],[t11006]) ).
cnf(t4097,plain,
add(inverse(x),multiply(x_inverse_times_y_inverse,X1)) = multiply(inverse(x),add(inverse(x),X1)),
inference(cp,[status(thm)],[t4021,t4094]) ).
cnf(t11019,plain,
add(inverse(x),multiply(x_inverse_times_y_inverse,X1)) = inverse(x),
inference(step,[status(thm)],[t4097,t3099]) ).
cnf(t4573,plain,
add(inverse(x),multiply(x_inverse_times_y_inverse,X1)) = inverse(x),
inference(orient,[status(thm)],[t11019]) ).
cnf(t5825,plain,
multiply(multiply(x_inverse_times_y_inverse,X1),x) = multiply(inverse(x),x),
inference(cp,[status(thm)],[t5817,t4573]) ).
cnf(t11063,plain,
multiply(multiply(x_inverse_times_y_inverse,X1),x) = additive_identity,
inference(step,[status(thm)],[t5825,t908]) ).
cnf(t6058,plain,
multiply(multiply(x_inverse_times_y_inverse,X1),x) = additive_identity,
inference(orient,[status(thm)],[t11063]) ).
cnf(t6059,plain,
additive_identity = multiply(x_inverse_times_y_inverse,x),
inference(cp,[status(thm)],[t6058,t3059]) ).
cnf(t6077,plain,
multiply(x_inverse_times_y_inverse,x) = additive_identity,
inference(orient,[status(thm)],[t6059]) ).
cnf(t6078,plain,
add(x,inverse(x_inverse_times_y_inverse)) = add(inverse(x_inverse_times_y_inverse),additive_identity),
inference(cp,[status(thm)],[t5881,t6077]) ).
cnf(t11064,plain,
add(x,inverse(x_inverse_times_y_inverse)) = inverse(x_inverse_times_y_inverse),
inference(step,[status(thm)],[t6078,t256]) ).
cnf(t6131,plain,
add(x,inverse(x_inverse_times_y_inverse)) = inverse(x_inverse_times_y_inverse),
inference(orient,[status(thm)],[t11064]) ).
cnf(t6140,plain,
x = multiply(x,inverse(x_inverse_times_y_inverse)),
inference(cp,[status(thm)],[t3099,t6131]) ).
cnf(t6146,plain,
multiply(x,inverse(x_inverse_times_y_inverse)) = x,
inference(orient,[status(thm)],[t6140]) ).
cnf(t6148,plain,
multiply(x_plus_y,add(y,inverse(x_inverse_times_y_inverse))) = add(y,x),
inference(cp,[status(thm)],[t3907,t6146]) ).
cnf(t4793,plain,
add(X1,add(X2,inverse(X1))) = add(X1,inverse(X1)),
inference(cp,[status(thm)],[t4785,t3079]) ).
cnf(t11042,plain,
add(X1,add(X2,inverse(X1))) = multiplicative_identity,
inference(step,[status(thm)],[t4793,t509]) ).
cnf(t5176,plain,
add(X1,add(X2,inverse(X1))) = multiplicative_identity,
inference(orient,[status(thm)],[t11042]) ).
cnf(t2705,plain,
inverse(y) = add(inverse(y),x_inverse_times_y_inverse),
inference(cp,[status(thm)],[t2699,t924]) ).
cnf(t10972,plain,
inverse(y) = add(x_inverse_times_y_inverse,inverse(y)),
inference(step,[status(thm)],[t2705,t267]) ).
cnf(t2822,plain,
add(x_inverse_times_y_inverse,inverse(y)) = inverse(y),
inference(orient,[status(thm)],[t10972]) ).
cnf(t4034,plain,
add(inverse(y),multiply(x_inverse_times_y_inverse,X1)) = multiply(inverse(y),add(inverse(y),X1)),
inference(cp,[status(thm)],[t4021,t2822]) ).
cnf(t11018,plain,
add(inverse(y),multiply(x_inverse_times_y_inverse,X1)) = inverse(y),
inference(step,[status(thm)],[t4034,t3099]) ).
cnf(t4547,plain,
add(inverse(y),multiply(x_inverse_times_y_inverse,X1)) = inverse(y),
inference(orient,[status(thm)],[t11018]) ).
cnf(t2835,plain,
multiply(X1,X2) = multiply(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t2834,t2699]) ).
cnf(t3254,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t2835]) ).
cnf(t4555,plain,
inverse(y) = add(inverse(y),multiply(X1,x_inverse_times_y_inverse)),
inference(cp,[status(thm)],[t4547,t3254]) ).
cnf(t4622,plain,
add(inverse(y),multiply(X1,x_inverse_times_y_inverse)) = inverse(y),
inference(orient,[status(thm)],[t4555]) ).
cnf(t4867,plain,
inverse(y) = add(inverse(y),inverse(inverse(x_inverse_times_y_inverse))),
inference(cp,[status(thm)],[t4622,t4864]) ).
cnf(t5474,plain,
add(inverse(y),inverse(inverse(x_inverse_times_y_inverse))) = inverse(y),
inference(orient,[status(thm)],[t4867]) ).
cnf(t5490,plain,
multiplicative_identity = add(inverse(x_inverse_times_y_inverse),inverse(y)),
inference(cp,[status(thm)],[t5176,t5474]) ).
cnf(t11044,plain,
multiplicative_identity = add(inverse(y),inverse(x_inverse_times_y_inverse)),
inference(step,[status(thm)],[t5490,t267]) ).
cnf(t5491,plain,
add(inverse(y),inverse(x_inverse_times_y_inverse)) = multiplicative_identity,
inference(orient,[status(thm)],[t11044]) ).
cnf(t5821,plain,
multiply(inverse(x_inverse_times_y_inverse),y) = multiply(multiplicative_identity,y),
inference(cp,[status(thm)],[t5817,t5491]) ).
cnf(t11057,plain,
multiply(inverse(x_inverse_times_y_inverse),y) = y,
inference(step,[status(thm)],[t5821,t261]) ).
cnf(t5860,plain,
multiply(inverse(x_inverse_times_y_inverse),y) = y,
inference(orient,[status(thm)],[t11057]) ).
cnf(t5864,plain,
inverse(x_inverse_times_y_inverse) = add(inverse(x_inverse_times_y_inverse),y),
inference(cp,[status(thm)],[t4062,t5860]) ).
cnf(t11060,plain,
inverse(x_inverse_times_y_inverse) = add(y,inverse(x_inverse_times_y_inverse)),
inference(step,[status(thm)],[t5864,t267]) ).
cnf(t5962,plain,
add(y,inverse(x_inverse_times_y_inverse)) = inverse(x_inverse_times_y_inverse),
inference(orient,[status(thm)],[t11060]) ).
cnf(t11065,plain,
multiply(x_plus_y,inverse(x_inverse_times_y_inverse)) = add(y,x),
inference(step,[status(thm)],[t6148,t5962]) ).
cnf(t11066,plain,
multiply(x_plus_y,inverse(x_inverse_times_y_inverse)) = x_plus_y,
inference(step,[status(thm)],[t11065,t928]) ).
cnf(t6167,plain,
multiply(x_plus_y,inverse(x_inverse_times_y_inverse)) = x_plus_y,
inference(orient,[status(thm)],[t11066]) ).
cnf(t6173,plain,
inverse(x_inverse_times_y_inverse) = add(inverse(x_inverse_times_y_inverse),x_plus_y),
inference(cp,[status(thm)],[t2699,t6167]) ).
cnf(t11069,plain,
inverse(x_inverse_times_y_inverse) = add(x_plus_y,inverse(x_inverse_times_y_inverse)),
inference(step,[status(thm)],[t6173,t267]) ).
cnf(t6188,plain,
add(x_plus_y,inverse(x_inverse_times_y_inverse)) = inverse(x_inverse_times_y_inverse),
inference(orient,[status(thm)],[t11069]) ).
cnf(t11171,plain,
inverse(x_inverse_times_y_inverse) = add(x_plus_y,additive_identity),
inference(step,[status(thm)],[t10830,t6188]) ).
cnf(t11172,plain,
inverse(x_inverse_times_y_inverse) = x_plus_y,
inference(step,[status(thm)],[t11171,t256]) ).
cnf(t10856,plain,
inverse(x_inverse_times_y_inverse) = x_plus_y,
inference(orient,[status(thm)],[t11172]) ).
cnf(t10861,plain,
x_inverse_times_y_inverse = inverse(x_plus_y),
inference(cp,[status(thm)],[t5850,t10856]) ).
cnf(t10870,plain,
inverse(x_plus_y) = x_inverse_times_y_inverse,
inference(orient,[status(thm)],[t10861]) ).
cnf(goal_0,negated_conjecture,
inverse(x_plus_y) != x_inverse_times_y_inverse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
x_inverse_times_y_inverse != x_inverse_times_y_inverse,
inference(rw,[status(thm)],[goal_0,t10870]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO014-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.38 % Computer : n003.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Fri Sep 25 06:33:38 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 49.42/7.29 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.42/7.29 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------