%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO015-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.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:37 PM UTC 2026
% Result : Unsatisfiable 43.74s 6.92s
% Output : CNFRefutation 43.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 23
% Syntax : Number of clauses : 165 ( 165 unt; 0 nHn; 59 RR)
% Number of literals : 165 ( 164 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 : 210 ( 14 sgn)
% Comments :
%------------------------------------------------------------------------------
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(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(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(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(t221,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(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(t18320,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(step,[status(thm)],[t221,t259]) ).
cnf(t281,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t18320]) ).
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(t18,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)],[t18]) ).
cnf(t283,plain,
add(X1,multiply(X2,X3)) = multiply(add(X2,X1),add(X1,X3)),
inference(cp,[status(thm)],[t281,t267]) ).
cnf(t3148,plain,
multiply(add(X1,X2),add(X2,X3)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t283]) ).
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(t212,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(hyper_resolution,[status(thm)],[hi20,h1,h5]) ).
cnf(t287,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t212]) ).
cnf(hi17,axiom,
sum(X,inverse(X),multiplicative_identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(hyper_resolution,[status(thm)],[hi20,hi0,hi17]) ).
cnf(t454,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t9]) ).
cnf(t458,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(multiplicative_identity,add(X2,inverse(X1))),
inference(cp,[status(thm)],[t287,t454]) ).
cnf(hi6,axiom,
product(multiplicative_identity,X,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
add(additive_identity,multiply(multiplicative_identity,X1)) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi6,h17]) ).
cnf(t18318,plain,
multiply(multiplicative_identity,X1) = X1,
inference(step,[status(thm)],[t20,t259]) ).
cnf(t261,plain,
multiply(multiplicative_identity,X1) = X1,
inference(orient,[status(thm)],[t18318]) ).
cnf(t18470,plain,
add(inverse(X1),multiply(X1,X2)) = add(X2,inverse(X1)),
inference(step,[status(thm)],[t458,t261]) ).
cnf(t6331,plain,
add(inverse(X1),multiply(X1,X2)) = add(X2,inverse(X1)),
inference(orient,[status(thm)],[t18470]) ).
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(t282,plain,
add(X1,multiply(additive_identity,X2)) = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t281,t256]) ).
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(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(t202,plain,
add(multiply(additive_identity,X1),multiply(X2,X1)) = add(additive_identity,multiply(X2,X1)),
inference(hyper_resolution,[status(thm)],[hi21,h17,h21]) ).
cnf(t18325,plain,
add(multiply(additive_identity,X1),multiply(X2,X1)) = multiply(X2,X1),
inference(step,[status(thm)],[t202,t259]) ).
cnf(t734,plain,
add(multiply(additive_identity,X1),multiply(X2,X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t18325]) ).
cnf(hi18,axiom,
product(inverse(X),X,additive_identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t74,plain,
add(multiply(additive_identity,X1),multiply(inverse(X1),X1)) = additive_identity,
inference(hyper_resolution,[status(thm)],[hi21,hi18,h21]) ).
cnf(t18329,plain,
multiply(inverse(X1),X1) = additive_identity,
inference(step,[status(thm)],[t74,t734]) ).
cnf(t794,plain,
multiply(inverse(X1),X1) = additive_identity,
inference(orient,[status(thm)],[t18329]) ).
cnf(t796,plain,
multiply(inverse(X1),X1) = add(multiply(additive_identity,X1),additive_identity),
inference(cp,[status(thm)],[t734,t794]) ).
cnf(t18368,plain,
additive_identity = add(multiply(additive_identity,X1),additive_identity),
inference(step,[status(thm)],[t796,t794]) ).
cnf(t18369,plain,
additive_identity = multiply(additive_identity,X1),
inference(step,[status(thm)],[t18368,t256]) ).
cnf(t2196,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t18369]) ).
cnf(t18386,plain,
add(X1,additive_identity) = multiply(X1,add(X1,X2)),
inference(step,[status(thm)],[t282,t2196]) ).
cnf(t18387,plain,
X1 = multiply(X1,add(X1,X2)),
inference(step,[status(thm)],[t18386,t256]) ).
cnf(t2210,plain,
multiply(X1,add(X1,X2)) = X1,
inference(orient,[status(thm)],[t18387]) ).
cnf(t456,plain,
add(X1,multiply(inverse(X1),X2)) = multiply(multiplicative_identity,add(X1,X2)),
inference(cp,[status(thm)],[t281,t454]) ).
cnf(t18394,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(step,[status(thm)],[t456,t261]) ).
cnf(t2672,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(orient,[status(thm)],[t18394]) ).
cnf(t2674,plain,
add(X1,X1) = add(X1,additive_identity),
inference(cp,[status(thm)],[t2672,t794]) ).
cnf(t18395,plain,
add(X1,X1) = X1,
inference(step,[status(thm)],[t2674,t256]) ).
cnf(t2692,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t18395]) ).
cnf(t2693,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t281,t2692]) ).
cnf(t18400,plain,
add(X1,multiply(X1,X2)) = X1,
inference(step,[status(thm)],[t2693,t2210]) ).
cnf(t2849,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t18400]) ).
cnf(hi22,negated_conjecture,
product(x,y,x_times_y) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t53,plain,
add(multiply(additive_identity,y),multiply(x,y)) = x_times_y,
inference(hyper_resolution,[status(thm)],[hi21,hi22,h21]) ).
cnf(t18331,plain,
multiply(x,y) = x_times_y,
inference(step,[status(thm)],[t53,t734]) ).
cnf(t808,plain,
multiply(x,y) = x_times_y,
inference(orient,[status(thm)],[t18331]) ).
cnf(t2850,plain,
x = add(x,x_times_y),
inference(cp,[status(thm)],[t2849,t808]) ).
cnf(t18401,plain,
x = add(x_times_y,x),
inference(step,[status(thm)],[t2850,t267]) ).
cnf(t2867,plain,
add(x_times_y,x) = x,
inference(orient,[status(thm)],[t18401]) ).
cnf(t2873,plain,
x_times_y = multiply(x_times_y,x),
inference(cp,[status(thm)],[t2210,t2867]) ).
cnf(t2878,plain,
multiply(x_times_y,x) = x_times_y,
inference(orient,[status(thm)],[t2873]) ).
cnf(t6353,plain,
add(x,inverse(x_times_y)) = add(inverse(x_times_y),x_times_y),
inference(cp,[status(thm)],[t6331,t2878]) ).
cnf(t18477,plain,
add(x,inverse(x_times_y)) = add(x_times_y,inverse(x_times_y)),
inference(step,[status(thm)],[t6353,t267]) ).
cnf(t18478,plain,
add(x,inverse(x_times_y)) = multiplicative_identity,
inference(step,[status(thm)],[t18477,t454]) ).
cnf(t6407,plain,
add(x,inverse(x_times_y)) = multiplicative_identity,
inference(orient,[status(thm)],[t18478]) ).
cnf(t6412,plain,
add(inverse(x_times_y),multiply(x,X1)) = multiply(multiplicative_identity,add(inverse(x_times_y),X1)),
inference(cp,[status(thm)],[t3148,t6407]) ).
cnf(t18535,plain,
add(inverse(x_times_y),multiply(x,X1)) = add(inverse(x_times_y),X1),
inference(step,[status(thm)],[t6412,t261]) ).
cnf(t8813,plain,
add(inverse(x_times_y),multiply(x,X1)) = add(inverse(x_times_y),X1),
inference(orient,[status(thm)],[t18535]) ).
cnf(t8819,plain,
add(inverse(x_times_y),y) = add(inverse(x_times_y),x_times_y),
inference(cp,[status(thm)],[t8813,t808]) ).
cnf(t18536,plain,
add(y,inverse(x_times_y)) = add(inverse(x_times_y),x_times_y),
inference(step,[status(thm)],[t8819,t267]) ).
cnf(t18537,plain,
add(y,inverse(x_times_y)) = add(x_times_y,inverse(x_times_y)),
inference(step,[status(thm)],[t18536,t267]) ).
cnf(t18538,plain,
add(y,inverse(x_times_y)) = multiplicative_identity,
inference(step,[status(thm)],[t18537,t454]) ).
cnf(t8854,plain,
add(y,inverse(x_times_y)) = multiplicative_identity,
inference(orient,[status(thm)],[t18538]) ).
cnf(t8859,plain,
add(inverse(x_times_y),multiply(y,X1)) = multiply(multiplicative_identity,add(inverse(x_times_y),X1)),
inference(cp,[status(thm)],[t3148,t8854]) ).
cnf(t18577,plain,
add(inverse(x_times_y),multiply(y,X1)) = add(inverse(x_times_y),X1),
inference(step,[status(thm)],[t8859,t261]) ).
cnf(t10395,plain,
add(inverse(x_times_y),multiply(y,X1)) = add(inverse(x_times_y),X1),
inference(orient,[status(thm)],[t18577]) ).
cnf(t241,axiom,
ifeq2(sum(X1,X2,X3),true,ifeq2(sum(X1,X2,X4),true,X4,X3),X3) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t266,plain,
ifeq2(sum(X1,X2,X3),true,ifeq2(sum(X1,X2,X4),true,X4,X3),X3) = X3,
inference(orient,[status(thm)],[t241]) ).
cnf(t16,axiom,
sum(X1,additive_identity,X1) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t941,plain,
sum(X1,additive_identity,X1) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t942,plain,
X1 = ifeq2(true,true,ifeq2(sum(X1,additive_identity,X2),true,X2,X1),X1),
inference(cp,[status(thm)],[t266,t941]) ).
cnf(t27,axiom,
ifeq2(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t264,plain,
ifeq2(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t27]) ).
cnf(t18680,plain,
X1 = ifeq2(sum(X1,additive_identity,X2),true,X2,X1),
inference(step,[status(thm)],[t942,t264]) ).
cnf(t18291,plain,
ifeq2(sum(X1,additive_identity,X2),true,X2,X1) = X1,
inference(orient,[status(thm)],[t18680]) ).
cnf(hi8,axiom,
ifeq(product(X,V3,V4),true,ifeq(product(X,Z,V2),true,ifeq(product(X,Y,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(hi19,axiom,
product(X,inverse(X),additive_identity) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(hi23,negated_conjecture,
sum(inverse(x),inverse(y),x_inverse_plus_y_inverse) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t157,plain,
sum(multiply(y,inverse(x)),additive_identity,multiply(y,x_inverse_plus_y_inverse)) = true,
inference(hyper_resolution,[status(thm)],[hi8,hi1,hi19,hi1,hi23]) ).
cnf(t969,plain,
sum(multiply(y,inverse(x)),additive_identity,multiply(y,x_inverse_plus_y_inverse)) = true,
inference(orient,[status(thm)],[t157]) ).
cnf(t18292,plain,
multiply(y,inverse(x)) = ifeq2(true,true,multiply(y,x_inverse_plus_y_inverse),multiply(y,inverse(x))),
inference(cp,[status(thm)],[t18291,t969]) ).
cnf(t18681,plain,
multiply(y,inverse(x)) = multiply(y,x_inverse_plus_y_inverse),
inference(step,[status(thm)],[t18292,t264]) ).
cnf(t18294,plain,
multiply(y,inverse(x)) = multiply(y,x_inverse_plus_y_inverse),
inference(orient,[status(thm)],[t18681]) ).
cnf(t18296,plain,
add(inverse(x_times_y),inverse(x)) = add(inverse(x_times_y),multiply(y,x_inverse_plus_y_inverse)),
inference(cp,[status(thm)],[t10395,t18294]) ).
cnf(t285,plain,
add(X1,multiply(X2,X3)) = multiply(add(X1,X2),add(X3,X1)),
inference(cp,[status(thm)],[t281,t267]) ).
cnf(t5317,plain,
multiply(add(X1,X2),add(X3,X1)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t285]) ).
cnf(t6411,plain,
add(inverse(x_times_y),multiply(X1,x)) = multiply(add(inverse(x_times_y),X1),multiplicative_identity),
inference(cp,[status(thm)],[t5317,t6407]) ).
cnf(hi7,axiom,
product(X,multiplicative_identity,X) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
add(additive_identity,multiply(X1,multiplicative_identity)) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi7,h17]) ).
cnf(t18317,plain,
multiply(X1,multiplicative_identity) = X1,
inference(step,[status(thm)],[t19,t259]) ).
cnf(t260,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t18317]) ).
cnf(t18533,plain,
add(inverse(x_times_y),multiply(X1,x)) = add(inverse(x_times_y),X1),
inference(step,[status(thm)],[t6411,t260]) ).
cnf(t8658,plain,
add(inverse(x_times_y),multiply(X1,x)) = add(inverse(x_times_y),X1),
inference(orient,[status(thm)],[t18533]) ).
cnf(t8662,plain,
add(inverse(x_times_y),inverse(x)) = add(inverse(x_times_y),additive_identity),
inference(cp,[status(thm)],[t8658,t794]) ).
cnf(t18534,plain,
add(inverse(x_times_y),inverse(x)) = inverse(x_times_y),
inference(step,[status(thm)],[t8662,t256]) ).
cnf(t8689,plain,
add(inverse(x_times_y),inverse(x)) = inverse(x_times_y),
inference(orient,[status(thm)],[t18534]) ).
cnf(t18683,plain,
inverse(x_times_y) = add(inverse(x_times_y),multiply(y,x_inverse_plus_y_inverse)),
inference(step,[status(thm)],[t18296,t8689]) ).
cnf(t18684,plain,
inverse(x_times_y) = add(inverse(x_times_y),x_inverse_plus_y_inverse),
inference(step,[status(thm)],[t18683,t10395]) ).
cnf(t18685,plain,
inverse(x_times_y) = add(x_inverse_plus_y_inverse,inverse(x_times_y)),
inference(step,[status(thm)],[t18684,t267]) ).
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(t194,plain,
add(additive_identity,multiply(X1,add(X2,X1))) = add(multiply(additive_identity,X2),X1),
inference(hyper_resolution,[status(thm)],[hi21,h8,h17]) ).
cnf(t18324,plain,
multiply(X1,add(X2,X1)) = add(multiply(additive_identity,X2),X1),
inference(step,[status(thm)],[t194,t259]) ).
cnf(t689,plain,
add(multiply(additive_identity,X1),X2) = multiply(X2,add(X1,X2)),
inference(orient,[status(thm)],[t18324]) ).
cnf(t18372,plain,
add(additive_identity,X2) = multiply(X2,add(X1,X2)),
inference(step,[status(thm)],[t689,t2196]) ).
cnf(t18373,plain,
X2 = multiply(X2,add(X1,X2)),
inference(step,[status(thm)],[t18372,t259]) ).
cnf(t2203,plain,
X2 = multiply(X2,add(X1,X2)),
inference(rw,[status(thm)],[t18373]) ).
cnf(t2378,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t2203]) ).
cnf(t23,plain,
add(inverse(x),inverse(y)) = x_inverse_plus_y_inverse,
inference(hyper_resolution,[status(thm)],[hi20,hi0,hi23]) ).
cnf(t18332,plain,
add(inverse(y),inverse(x)) = x_inverse_plus_y_inverse,
inference(step,[status(thm)],[t23,t267]) ).
cnf(t811,plain,
add(inverse(y),inverse(x)) = x_inverse_plus_y_inverse,
inference(orient,[status(thm)],[t18332]) ).
cnf(t2379,plain,
inverse(x) = multiply(inverse(x),x_inverse_plus_y_inverse),
inference(cp,[status(thm)],[t2378,t811]) ).
cnf(t2385,plain,
multiply(inverse(x),x_inverse_plus_y_inverse) = inverse(x),
inference(orient,[status(thm)],[t2379]) ).
cnf(t2675,plain,
add(x,x_inverse_plus_y_inverse) = add(x,inverse(x)),
inference(cp,[status(thm)],[t2672,t2385]) ).
cnf(t18396,plain,
add(x_inverse_plus_y_inverse,x) = add(x,inverse(x)),
inference(step,[status(thm)],[t2675,t267]) ).
cnf(t18397,plain,
add(x_inverse_plus_y_inverse,x) = multiplicative_identity,
inference(step,[status(thm)],[t18396,t454]) ).
cnf(t2703,plain,
add(x_inverse_plus_y_inverse,x) = multiplicative_identity,
inference(orient,[status(thm)],[t18397]) ).
cnf(t2704,plain,
add(x_inverse_plus_y_inverse,multiply(x,X1)) = multiply(multiplicative_identity,add(x_inverse_plus_y_inverse,X1)),
inference(cp,[status(thm)],[t281,t2703]) ).
cnf(t18403,plain,
add(x_inverse_plus_y_inverse,multiply(x,X1)) = add(x_inverse_plus_y_inverse,X1),
inference(step,[status(thm)],[t2704,t261]) ).
cnf(t2995,plain,
add(x_inverse_plus_y_inverse,multiply(x,X1)) = add(x_inverse_plus_y_inverse,X1),
inference(orient,[status(thm)],[t18403]) ).
cnf(t2997,plain,
add(x_inverse_plus_y_inverse,y) = add(x_inverse_plus_y_inverse,x_times_y),
inference(cp,[status(thm)],[t2995,t808]) ).
cnf(t18404,plain,
add(y,x_inverse_plus_y_inverse) = add(x_inverse_plus_y_inverse,x_times_y),
inference(step,[status(thm)],[t2997,t267]) ).
cnf(t2214,plain,
inverse(y) = multiply(inverse(y),x_inverse_plus_y_inverse),
inference(cp,[status(thm)],[t2210,t811]) ).
cnf(t2376,plain,
multiply(inverse(y),x_inverse_plus_y_inverse) = inverse(y),
inference(orient,[status(thm)],[t2214]) ).
cnf(t2676,plain,
add(y,x_inverse_plus_y_inverse) = add(y,inverse(y)),
inference(cp,[status(thm)],[t2672,t2376]) ).
cnf(t18398,plain,
add(y,x_inverse_plus_y_inverse) = multiplicative_identity,
inference(step,[status(thm)],[t2676,t454]) ).
cnf(t2710,plain,
add(y,x_inverse_plus_y_inverse) = multiplicative_identity,
inference(orient,[status(thm)],[t18398]) ).
cnf(t18405,plain,
multiplicative_identity = add(x_inverse_plus_y_inverse,x_times_y),
inference(step,[status(thm)],[t18404,t2710]) ).
cnf(t18406,plain,
multiplicative_identity = add(x_times_y,x_inverse_plus_y_inverse),
inference(step,[status(thm)],[t18405,t267]) ).
cnf(t3013,plain,
add(x_times_y,x_inverse_plus_y_inverse) = multiplicative_identity,
inference(orient,[status(thm)],[t18406]) ).
cnf(t3018,plain,
add(x_inverse_plus_y_inverse,multiply(x_times_y,X1)) = multiply(multiplicative_identity,add(X1,x_inverse_plus_y_inverse)),
inference(cp,[status(thm)],[t287,t3013]) ).
cnf(t18429,plain,
add(x_inverse_plus_y_inverse,multiply(x_times_y,X1)) = add(X1,x_inverse_plus_y_inverse),
inference(step,[status(thm)],[t3018,t261]) ).
cnf(t3692,plain,
add(x_inverse_plus_y_inverse,multiply(x_times_y,X1)) = add(X1,x_inverse_plus_y_inverse),
inference(orient,[status(thm)],[t18429]) ).
cnf(t107,plain,
add(multiply(additive_identity,inverse(X1)),multiply(X1,inverse(X1))) = additive_identity,
inference(hyper_resolution,[status(thm)],[hi21,hi19,h21]) ).
cnf(t18330,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(step,[status(thm)],[t107,t734]) ).
cnf(t801,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t18330]) ).
cnf(t3699,plain,
add(inverse(x_times_y),x_inverse_plus_y_inverse) = add(x_inverse_plus_y_inverse,additive_identity),
inference(cp,[status(thm)],[t3692,t801]) ).
cnf(t18430,plain,
add(x_inverse_plus_y_inverse,inverse(x_times_y)) = add(x_inverse_plus_y_inverse,additive_identity),
inference(step,[status(thm)],[t3699,t267]) ).
cnf(t18431,plain,
add(x_inverse_plus_y_inverse,inverse(x_times_y)) = x_inverse_plus_y_inverse,
inference(step,[status(thm)],[t18430,t256]) ).
cnf(t3714,plain,
add(x_inverse_plus_y_inverse,inverse(x_times_y)) = x_inverse_plus_y_inverse,
inference(orient,[status(thm)],[t18431]) ).
cnf(t18686,plain,
inverse(x_times_y) = x_inverse_plus_y_inverse,
inference(step,[status(thm)],[t18685,t3714]) ).
cnf(t18305,plain,
inverse(x_times_y) = x_inverse_plus_y_inverse,
inference(orient,[status(thm)],[t18686]) ).
cnf(goal_0,negated_conjecture,
inverse(x_times_y) != x_inverse_plus_y_inverse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
x_inverse_plus_y_inverse != x_inverse_plus_y_inverse,
inference(rw,[status(thm)],[goal_0,t18305]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO015-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 06:33:33 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 43.74/6.92 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 43.74/6.92 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------