%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO025-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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:39 PM UTC 2026
% Result : Unsatisfiable 6.49s 1.32s
% Output : CNFRefutation 6.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 85
% Number of leaves : 12
% Syntax : Number of clauses : 245 ( 245 unt; 0 nHn; 114 RR)
% Number of literals : 245 ( 244 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-3 aty)
% Number of variables : 192 ( 44 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t40,axiom,
sFlat0 = inverse(b),
introduced(definition) ).
cnf(t401,plain,
inverse(b) = sFlat0,
inference(orient,[status(thm)],[t40]) ).
cnf(t41,axiom,
sFlat1 = multiply(b,inverse(b)),
introduced(definition) ).
cnf(t393,plain,
multiply(b,inverse(b)) = sFlat1,
inference(orient,[status(thm)],[t41]) ).
cnf(t3336,plain,
multiply(b,sFlat0) = sFlat1,
inference(step,[status(thm)],[t393,t401]) ).
cnf(t403,plain,
multiply(b,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t3336]) ).
cnf(t411,plain,
multiply(b,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t403]) ).
cnf(t42,axiom,
sFlat2 = inverse(a),
introduced(definition) ).
cnf(t398,plain,
inverse(a) = sFlat2,
inference(orient,[status(thm)],[t42]) ).
cnf(t43,axiom,
sFlat3 = multiply(a,inverse(a)),
introduced(definition) ).
cnf(t390,plain,
multiply(a,inverse(a)) = sFlat3,
inference(orient,[status(thm)],[t43]) ).
cnf(t3335,plain,
multiply(a,sFlat2) = sFlat3,
inference(step,[status(thm)],[t390,t398]) ).
cnf(t400,plain,
multiply(a,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t3335]) ).
cnf(t406,plain,
multiply(a,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t400]) ).
cnf(u1,axiom,
pixley(X,Y,Y) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
pixley(X,Y,Z) = add(multiply(X,inverse(Y)),add(multiply(X,Z),multiply(inverse(Y),Z))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
add(multiply(X1,inverse(X2)),add(multiply(X1,X2),multiply(inverse(X2),X2))) = X1,
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t196,plain,
add(multiply(X1,inverse(X2)),add(multiply(X1,X2),multiply(inverse(X2),X2))) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t2,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t379,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
inference(orient,[status(thm)],[t2]) ).
cnf(t3326,plain,
add(multiply(X1,inverse(X2)),multiply(X2,add(X1,inverse(X2)))) = X1,
inference(step,[status(thm)],[t196,t379]) ).
cnf(t385,plain,
add(multiply(X1,inverse(X2)),multiply(X2,add(X1,inverse(X2)))) = X1,
inference(rw,[status(thm)],[t3326]) ).
cnf(t2286,plain,
add(multiply(X1,inverse(X2)),multiply(X2,add(X1,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t385]) ).
cnf(u0,axiom,
pixley(X,X,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3,plain,
add(multiply(X1,inverse(X1)),add(multiply(X1,X2),multiply(inverse(X1),X2))) = X2,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t45,plain,
add(multiply(X1,inverse(X1)),add(multiply(X1,X2),multiply(inverse(X1),X2))) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t3324,plain,
add(multiply(X1,inverse(X1)),multiply(X2,add(X1,inverse(X1)))) = X2,
inference(step,[status(thm)],[t45,t379]) ).
cnf(t383,plain,
add(multiply(X1,inverse(X1)),multiply(X2,add(X1,inverse(X1)))) = X2,
inference(rw,[status(thm)],[t3324]) ).
cnf(t0,axiom,
add(X1,inverse(X1)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t396,plain,
add(X1,inverse(X1)) = n1,
inference(orient,[status(thm)],[t0]) ).
cnf(t3415,plain,
add(multiply(X1,inverse(X1)),multiply(X2,n1)) = X2,
inference(step,[status(thm)],[t383,t396]) ).
cnf(t1542,plain,
add(multiply(X1,inverse(X1)),multiply(X2,n1)) = X2,
inference(orient,[status(thm)],[t3415]) ).
cnf(t1545,plain,
X1 = add(multiply(b,sFlat0),multiply(X1,n1)),
inference(cp,[status(thm)],[t1542,t401]) ).
cnf(t3417,plain,
X1 = add(sFlat1,multiply(X1,n1)),
inference(step,[status(thm)],[t1545,t411]) ).
cnf(t1569,plain,
add(sFlat1,multiply(X1,n1)) = X1,
inference(orient,[status(thm)],[t3417]) ).
cnf(u2,axiom,
pixley(X,Y,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
add(multiply(X1,inverse(X2)),add(multiply(X1,X1),multiply(inverse(X2),X1))) = X1,
inference(definition_unfolding,[status(thm)],[u2,d0]) ).
cnf(t234,plain,
add(multiply(X1,inverse(X2)),add(multiply(X1,X1),multiply(inverse(X2),X1))) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t3325,plain,
add(multiply(X1,inverse(X2)),multiply(X1,add(X1,inverse(X2)))) = X1,
inference(step,[status(thm)],[t234,t379]) ).
cnf(t384,plain,
add(multiply(X1,inverse(X2)),multiply(X1,add(X1,inverse(X2)))) = X1,
inference(rw,[status(thm)],[t3325]) ).
cnf(t2119,plain,
add(multiply(X1,inverse(X2)),multiply(X1,add(X1,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t384]) ).
cnf(t2123,plain,
X1 = add(multiply(X1,sFlat2),multiply(X1,add(X1,inverse(a)))),
inference(cp,[status(thm)],[t2119,t398]) ).
cnf(t3466,plain,
X1 = add(multiply(X1,sFlat2),multiply(X1,add(X1,sFlat2))),
inference(step,[status(thm)],[t2123,t398]) ).
cnf(t2180,plain,
add(multiply(X1,sFlat2),multiply(X1,add(X1,sFlat2))) = X1,
inference(orient,[status(thm)],[t3466]) ).
cnf(t1,axiom,
multiply(add(X1,X2),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44,plain,
multiply(add(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t382,plain,
multiply(X1,X2) = multiply(multiply(X2,add(X3,X1)),multiply(X1,X2)),
inference(cp,[status(thm)],[t44,t379]) ).
cnf(t621,plain,
multiply(multiply(X1,add(X2,X3)),multiply(X3,X1)) = multiply(X3,X1),
inference(orient,[status(thm)],[t382]) ).
cnf(t1553,plain,
multiply(multiply(X1,n1),X2) = multiply(multiply(X2,X1),multiply(multiply(X1,n1),X2)),
inference(cp,[status(thm)],[t621,t1542]) ).
cnf(t1935,plain,
multiply(multiply(X1,X2),multiply(multiply(X2,n1),X1)) = multiply(multiply(X2,n1),X1),
inference(orient,[status(thm)],[t1553]) ).
cnf(t399,plain,
n1 = add(a,sFlat2),
inference(cp,[status(thm)],[t396,t398]) ).
cnf(t404,plain,
add(a,sFlat2) = n1,
inference(orient,[status(thm)],[t399]) ).
cnf(t637,plain,
multiply(sFlat2,X1) = multiply(multiply(X1,n1),multiply(sFlat2,X1)),
inference(cp,[status(thm)],[t621,t404]) ).
cnf(t683,plain,
multiply(multiply(X1,n1),multiply(sFlat2,X1)) = multiply(sFlat2,X1),
inference(orient,[status(thm)],[t637]) ).
cnf(t2000,plain,
multiply(multiply(X1,n1),multiply(sFlat2,X1)) = multiply(multiply(multiply(sFlat2,X1),X1),multiply(sFlat2,X1)),
inference(cp,[status(thm)],[t1935,t683]) ).
cnf(t3461,plain,
multiply(sFlat2,X1) = multiply(multiply(multiply(sFlat2,X1),X1),multiply(sFlat2,X1)),
inference(step,[status(thm)],[t2000,t683]) ).
cnf(t2063,plain,
multiply(multiply(multiply(sFlat2,X1),X1),multiply(sFlat2,X1)) = multiply(sFlat2,X1),
inference(orient,[status(thm)],[t3461]) ).
cnf(t624,plain,
multiply(X1,add(X2,add(X3,X1))) = multiply(add(X3,X1),multiply(X1,add(X2,add(X3,X1)))),
inference(cp,[status(thm)],[t621,t44]) ).
cnf(t381,plain,
multiply(X1,add(X2,add(X3,X1))) = add(multiply(X2,X1),X1),
inference(cp,[status(thm)],[t379,t44]) ).
cnf(t561,plain,
multiply(X1,add(X2,add(X3,X1))) = add(multiply(X2,X1),X1),
inference(orient,[status(thm)],[t381]) ).
cnf(t3385,plain,
add(multiply(X2,X1),X1) = multiply(add(X3,X1),multiply(X1,add(X2,add(X3,X1)))),
inference(step,[status(thm)],[t624,t561]) ).
cnf(t3386,plain,
add(multiply(X2,X1),X1) = multiply(add(X3,X1),add(multiply(X2,X1),X1)),
inference(step,[status(thm)],[t3385,t561]) ).
cnf(t1108,plain,
multiply(add(X1,X2),add(multiply(X3,X2),X2)) = add(multiply(X3,X2),X2),
inference(orient,[status(thm)],[t3386]) ).
cnf(t407,plain,
multiply(sFlat2,add(a,X1)) = add(sFlat3,multiply(X1,sFlat2)),
inference(cp,[status(thm)],[t379,t406]) ).
cnf(t423,plain,
add(sFlat3,multiply(X1,sFlat2)) = multiply(sFlat2,add(a,X1)),
inference(orient,[status(thm)],[t407]) ).
cnf(t405,plain,
sFlat2 = multiply(n1,sFlat2),
inference(cp,[status(thm)],[t44,t404]) ).
cnf(t414,plain,
multiply(n1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t405]) ).
cnf(t424,plain,
multiply(sFlat2,add(a,n1)) = add(sFlat3,sFlat2),
inference(cp,[status(thm)],[t423,t414]) ).
cnf(t428,plain,
multiply(sFlat2,add(a,n1)) = add(sFlat3,sFlat2),
inference(orient,[status(thm)],[t424]) ).
cnf(t688,plain,
multiply(sFlat2,add(a,n1)) = multiply(multiply(add(a,n1),n1),add(sFlat3,sFlat2)),
inference(cp,[status(thm)],[t683,t428]) ).
cnf(t3366,plain,
add(sFlat3,sFlat2) = multiply(multiply(add(a,n1),n1),add(sFlat3,sFlat2)),
inference(step,[status(thm)],[t688,t428]) ).
cnf(t3367,plain,
add(sFlat3,sFlat2) = multiply(n1,add(sFlat3,sFlat2)),
inference(step,[status(thm)],[t3366,t44]) ).
cnf(t700,plain,
multiply(n1,add(sFlat3,sFlat2)) = add(sFlat3,sFlat2),
inference(orient,[status(thm)],[t3367]) ).
cnf(t703,plain,
multiply(sFlat2,n1) = multiply(add(sFlat3,sFlat2),multiply(sFlat2,n1)),
inference(cp,[status(thm)],[t621,t700]) ).
cnf(t717,plain,
multiply(add(sFlat3,sFlat2),multiply(sFlat2,n1)) = multiply(sFlat2,n1),
inference(orient,[status(thm)],[t703]) ).
cnf(t1137,plain,
add(multiply(add(sFlat3,sFlat2),multiply(sFlat2,n1)),multiply(sFlat2,n1)) = multiply(add(X1,multiply(sFlat2,n1)),add(multiply(sFlat2,n1),multiply(sFlat2,n1))),
inference(cp,[status(thm)],[t1108,t717]) ).
cnf(t3398,plain,
add(multiply(sFlat2,n1),multiply(sFlat2,n1)) = multiply(add(X1,multiply(sFlat2,n1)),add(multiply(sFlat2,n1),multiply(sFlat2,n1))),
inference(step,[status(thm)],[t1137,t717]) ).
cnf(t3399,plain,
multiply(n1,add(sFlat2,sFlat2)) = multiply(add(X1,multiply(sFlat2,n1)),add(multiply(sFlat2,n1),multiply(sFlat2,n1))),
inference(step,[status(thm)],[t3398,t379]) ).
cnf(t415,plain,
multiply(sFlat2,add(n1,X1)) = add(sFlat2,multiply(X1,sFlat2)),
inference(cp,[status(thm)],[t379,t414]) ).
cnf(t459,plain,
add(sFlat2,multiply(X1,sFlat2)) = multiply(sFlat2,add(n1,X1)),
inference(orient,[status(thm)],[t415]) ).
cnf(t460,plain,
multiply(sFlat2,add(n1,n1)) = add(sFlat2,sFlat2),
inference(cp,[status(thm)],[t459,t414]) ).
cnf(t463,plain,
multiply(sFlat2,add(n1,n1)) = add(sFlat2,sFlat2),
inference(orient,[status(thm)],[t460]) ).
cnf(t687,plain,
multiply(sFlat2,add(n1,n1)) = multiply(multiply(add(n1,n1),n1),add(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t683,t463]) ).
cnf(t3364,plain,
add(sFlat2,sFlat2) = multiply(multiply(add(n1,n1),n1),add(sFlat2,sFlat2)),
inference(step,[status(thm)],[t687,t463]) ).
cnf(t3365,plain,
add(sFlat2,sFlat2) = multiply(n1,add(sFlat2,sFlat2)),
inference(step,[status(thm)],[t3364,t44]) ).
cnf(t695,plain,
multiply(n1,add(sFlat2,sFlat2)) = add(sFlat2,sFlat2),
inference(orient,[status(thm)],[t3365]) ).
cnf(t3400,plain,
add(sFlat2,sFlat2) = multiply(add(X1,multiply(sFlat2,n1)),add(multiply(sFlat2,n1),multiply(sFlat2,n1))),
inference(step,[status(thm)],[t3399,t695]) ).
cnf(t3401,plain,
add(sFlat2,sFlat2) = multiply(add(X1,multiply(sFlat2,n1)),multiply(n1,add(sFlat2,sFlat2))),
inference(step,[status(thm)],[t3400,t379]) ).
cnf(t3402,plain,
add(sFlat2,sFlat2) = multiply(add(X1,multiply(sFlat2,n1)),add(sFlat2,sFlat2)),
inference(step,[status(thm)],[t3401,t695]) ).
cnf(t1280,plain,
multiply(add(X1,multiply(sFlat2,n1)),add(sFlat2,sFlat2)) = add(sFlat2,sFlat2),
inference(orient,[status(thm)],[t3402]) ).
cnf(t1551,plain,
add(sFlat2,sFlat2) = multiply(sFlat2,add(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t1280,t1542]) ).
cnf(t1711,plain,
multiply(sFlat2,add(sFlat2,sFlat2)) = add(sFlat2,sFlat2),
inference(orient,[status(thm)],[t1551]) ).
cnf(t2182,plain,
sFlat2 = add(multiply(sFlat2,sFlat2),add(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t2180,t1711]) ).
cnf(t2193,plain,
add(multiply(sFlat2,sFlat2),add(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t2182]) ).
cnf(t2223,plain,
multiply(sFlat2,multiply(sFlat2,sFlat2)) = sFlat2,
inference(rw,[status(thm)],[t2193]) ).
cnf(t2243,plain,
multiply(sFlat2,multiply(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t2223]) ).
cnf(t2247,plain,
multiply(sFlat2,multiply(sFlat2,sFlat2)) = multiply(multiply(sFlat2,multiply(sFlat2,sFlat2)),multiply(sFlat2,multiply(sFlat2,sFlat2))),
inference(cp,[status(thm)],[t2063,t2243]) ).
cnf(t3490,plain,
sFlat2 = multiply(multiply(sFlat2,multiply(sFlat2,sFlat2)),multiply(sFlat2,multiply(sFlat2,sFlat2))),
inference(step,[status(thm)],[t2247,t2243]) ).
cnf(t3491,plain,
sFlat2 = multiply(sFlat2,multiply(sFlat2,multiply(sFlat2,sFlat2))),
inference(step,[status(thm)],[t3490,t2243]) ).
cnf(t3492,plain,
sFlat2 = multiply(sFlat2,sFlat2),
inference(step,[status(thm)],[t3491,t2243]) ).
cnf(t2252,plain,
multiply(sFlat2,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t3492]) ).
cnf(t2265,plain,
multiply(sFlat2,add(sFlat2,X1)) = add(sFlat2,multiply(X1,sFlat2)),
inference(cp,[status(thm)],[t379,t2252]) ).
cnf(t3514,plain,
multiply(sFlat2,add(sFlat2,X1)) = multiply(sFlat2,add(n1,X1)),
inference(step,[status(thm)],[t2265,t459]) ).
cnf(t2399,plain,
multiply(sFlat2,add(n1,X1)) = multiply(sFlat2,add(sFlat2,X1)),
inference(orient,[status(thm)],[t3514]) ).
cnf(t2403,plain,
multiply(sFlat2,add(sFlat2,inverse(n1))) = multiply(sFlat2,n1),
inference(cp,[status(thm)],[t2399,t396]) ).
cnf(t2264,plain,
multiply(sFlat2,add(a,sFlat2)) = add(sFlat3,sFlat2),
inference(cp,[status(thm)],[t423,t2252]) ).
cnf(t3501,plain,
multiply(sFlat2,n1) = add(sFlat3,sFlat2),
inference(step,[status(thm)],[t2264,t404]) ).
cnf(t1611,plain,
multiply(sFlat2,add(a,n1)) = add(sFlat3,sFlat2),
inference(rw,[status(thm)],[t428]) ).
cnf(t1570,plain,
add(X1,n1) = add(sFlat1,n1),
inference(cp,[status(thm)],[t1569,t44]) ).
cnf(t1612,plain,
add(X1,n1) = add(sFlat1,n1),
inference(orient,[status(thm)],[t1570]) ).
cnf(t1628,plain,
add(sFlat1,n1) = add(X1,n1),
inference(cp,[status(thm)],[t1612,t1612]) ).
cnf(t3422,plain,
add(sFlat0,n1) = add(X1,n1),
inference(step,[status(thm)],[t1628,t1612]) ).
cnf(t1637,plain,
add(sFlat0,n1) = add(X1,n1),
inference(orient,[status(thm)],[t3422]) ).
cnf(t1644,plain,
add(X1,n1) = add(X2,n1),
inference(cp,[status(thm)],[t1637,t1637]) ).
cnf(t1662,plain,
add(X1,n1) = add(X2,n1),
inference(orient,[status(thm)],[t1644]) ).
cnf(t3438,plain,
multiply(sFlat2,add(sFlat0,n1)) = add(sFlat3,sFlat2),
inference(step,[status(thm)],[t1611,t1662]) ).
cnf(t1609,plain,
multiply(sFlat2,add(n1,n1)) = add(sFlat2,sFlat2),
inference(rw,[status(thm)],[t463]) ).
cnf(t3435,plain,
multiply(sFlat2,add(sFlat0,n1)) = add(sFlat2,sFlat2),
inference(step,[status(thm)],[t1609,t1662]) ).
cnf(t1723,plain,
multiply(sFlat2,add(sFlat0,n1)) = add(sFlat2,sFlat2),
inference(orient,[status(thm)],[t3435]) ).
cnf(t3439,plain,
add(sFlat2,sFlat2) = add(sFlat3,sFlat2),
inference(step,[status(thm)],[t3438,t1723]) ).
cnf(t1730,plain,
add(sFlat3,sFlat2) = add(sFlat2,sFlat2),
inference(orient,[status(thm)],[t3439]) ).
cnf(t2198,plain,
add(multiply(multiply(sFlat2,sFlat2),sFlat2),sFlat2) = multiply(sFlat2,sFlat2),
inference(cp,[status(thm)],[t561,t2193]) ).
cnf(t416,plain,
multiply(sFlat2,add(X1,n1)) = add(multiply(X1,sFlat2),sFlat2),
inference(cp,[status(thm)],[t379,t414]) ).
cnf(t466,plain,
add(multiply(X1,sFlat2),sFlat2) = multiply(sFlat2,add(X1,n1)),
inference(orient,[status(thm)],[t416]) ).
cnf(t1724,plain,
add(sFlat2,sFlat2) = multiply(sFlat2,add(X1,n1)),
inference(cp,[status(thm)],[t1723,t1662]) ).
cnf(t1738,plain,
multiply(sFlat2,add(X1,n1)) = add(sFlat2,sFlat2),
inference(orient,[status(thm)],[t1724]) ).
cnf(t3442,plain,
add(multiply(X1,sFlat2),sFlat2) = add(sFlat2,sFlat2),
inference(step,[status(thm)],[t466,t1738]) ).
cnf(t1739,plain,
add(multiply(X1,sFlat2),sFlat2) = add(sFlat2,sFlat2),
inference(orient,[status(thm)],[t3442]) ).
cnf(t3467,plain,
add(sFlat2,sFlat2) = multiply(sFlat2,sFlat2),
inference(step,[status(thm)],[t2198,t1739]) ).
cnf(t2202,plain,
add(sFlat2,sFlat2) = multiply(sFlat2,sFlat2),
inference(orient,[status(thm)],[t3467]) ).
cnf(t3470,plain,
add(sFlat3,sFlat2) = multiply(sFlat2,sFlat2),
inference(step,[status(thm)],[t1730,t2202]) ).
cnf(t2205,plain,
add(sFlat3,sFlat2) = multiply(sFlat2,sFlat2),
inference(orient,[status(thm)],[t3470]) ).
cnf(t3495,plain,
add(sFlat3,sFlat2) = sFlat2,
inference(step,[status(thm)],[t2205,t2252]) ).
cnf(t2255,plain,
add(sFlat3,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t3495]) ).
cnf(t3502,plain,
multiply(sFlat2,n1) = sFlat2,
inference(step,[status(thm)],[t3501,t2255]) ).
cnf(t2270,plain,
multiply(sFlat2,n1) = sFlat2,
inference(orient,[status(thm)],[t3502]) ).
cnf(t3518,plain,
multiply(sFlat2,add(sFlat2,inverse(n1))) = sFlat2,
inference(step,[status(thm)],[t2403,t2270]) ).
cnf(t2415,plain,
multiply(sFlat2,add(sFlat2,inverse(n1))) = sFlat2,
inference(orient,[status(thm)],[t3518]) ).
cnf(t2423,plain,
sFlat2 = add(multiply(sFlat2,inverse(n1)),sFlat2),
inference(cp,[status(thm)],[t2119,t2415]) ).
cnf(t2424,plain,
add(multiply(sFlat2,inverse(n1)),sFlat2) = sFlat2,
inference(orient,[status(thm)],[t2423]) ).
cnf(t2425,plain,
multiply(sFlat2,inverse(n1)) = add(multiply(multiply(sFlat2,inverse(n1)),sFlat2),multiply(multiply(sFlat2,inverse(n1)),sFlat2)),
inference(cp,[status(thm)],[t2180,t2424]) ).
cnf(t3532,plain,
multiply(sFlat2,inverse(n1)) = multiply(sFlat2,add(multiply(sFlat2,inverse(n1)),multiply(sFlat2,inverse(n1)))),
inference(step,[status(thm)],[t2425,t379]) ).
cnf(t3533,plain,
multiply(sFlat2,inverse(n1)) = multiply(sFlat2,multiply(inverse(n1),add(sFlat2,sFlat2))),
inference(step,[status(thm)],[t3532,t379]) ).
cnf(t3499,plain,
add(sFlat2,sFlat2) = sFlat2,
inference(step,[status(thm)],[t2202,t2252]) ).
cnf(t2259,plain,
add(sFlat2,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t3499]) ).
cnf(t3534,plain,
multiply(sFlat2,inverse(n1)) = multiply(sFlat2,multiply(inverse(n1),sFlat2)),
inference(step,[status(thm)],[t3533,t2259]) ).
cnf(t625,plain,
multiply(inverse(X1),X2) = multiply(multiply(X2,n1),multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t621,t396]) ).
cnf(t729,plain,
multiply(multiply(X1,n1),multiply(inverse(X2),X1)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t625]) ).
cnf(t2283,plain,
multiply(inverse(X1),sFlat2) = multiply(sFlat2,multiply(inverse(X1),sFlat2)),
inference(cp,[status(thm)],[t729,t2270]) ).
cnf(t2543,plain,
multiply(sFlat2,multiply(inverse(X1),sFlat2)) = multiply(inverse(X1),sFlat2),
inference(orient,[status(thm)],[t2283]) ).
cnf(t3535,plain,
multiply(sFlat2,inverse(n1)) = multiply(inverse(n1),sFlat2),
inference(step,[status(thm)],[t3534,t2543]) ).
cnf(t2551,plain,
multiply(inverse(n1),sFlat2) = multiply(sFlat2,inverse(n1)),
inference(orient,[status(thm)],[t3535]) ).
cnf(t2558,plain,
inverse(n1) = add(multiply(sFlat2,inverse(n1)),multiply(inverse(n1),add(inverse(n1),sFlat2))),
inference(cp,[status(thm)],[t2180,t2551]) ).
cnf(t397,plain,
inverse(X1) = multiply(n1,inverse(X1)),
inference(cp,[status(thm)],[t44,t396]) ).
cnf(t420,plain,
multiply(n1,inverse(X1)) = inverse(X1),
inference(orient,[status(thm)],[t397]) ).
cnf(t1543,plain,
X1 = add(inverse(n1),multiply(X1,n1)),
inference(cp,[status(thm)],[t1542,t420]) ).
cnf(t1745,plain,
add(inverse(n1),multiply(X1,n1)) = X1,
inference(orient,[status(thm)],[t1543]) ).
cnf(t2273,plain,
sFlat2 = add(inverse(n1),sFlat2),
inference(cp,[status(thm)],[t1745,t2270]) ).
cnf(t2315,plain,
add(inverse(n1),sFlat2) = sFlat2,
inference(orient,[status(thm)],[t2273]) ).
cnf(t3536,plain,
inverse(n1) = add(multiply(sFlat2,inverse(n1)),multiply(inverse(n1),sFlat2)),
inference(step,[status(thm)],[t2558,t2315]) ).
cnf(t3537,plain,
inverse(n1) = add(multiply(sFlat2,inverse(n1)),multiply(sFlat2,inverse(n1))),
inference(step,[status(thm)],[t3536,t2551]) ).
cnf(t3538,plain,
inverse(n1) = multiply(inverse(n1),add(sFlat2,sFlat2)),
inference(step,[status(thm)],[t3537,t379]) ).
cnf(t3539,plain,
inverse(n1) = multiply(inverse(n1),sFlat2),
inference(step,[status(thm)],[t3538,t2259]) ).
cnf(t3540,plain,
inverse(n1) = multiply(sFlat2,inverse(n1)),
inference(step,[status(thm)],[t3539,t2551]) ).
cnf(t2562,plain,
multiply(sFlat2,inverse(n1)) = inverse(n1),
inference(orient,[status(thm)],[t3540]) ).
cnf(t2566,plain,
multiply(inverse(n1),add(sFlat2,X1)) = add(inverse(n1),multiply(X1,inverse(n1))),
inference(cp,[status(thm)],[t379,t2562]) ).
cnf(t421,plain,
multiply(inverse(X1),add(n1,X2)) = add(inverse(X1),multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t379,t420]) ).
cnf(t602,plain,
add(inverse(X1),multiply(X2,inverse(X1))) = multiply(inverse(X1),add(n1,X2)),
inference(orient,[status(thm)],[t421]) ).
cnf(t3567,plain,
multiply(inverse(n1),add(sFlat2,X1)) = multiply(inverse(n1),add(n1,X1)),
inference(step,[status(thm)],[t2566,t602]) ).
cnf(t2784,plain,
multiply(inverse(n1),add(n1,X1)) = multiply(inverse(n1),add(sFlat2,X1)),
inference(orient,[status(thm)],[t3567]) ).
cnf(t2787,plain,
multiply(inverse(n1),add(sFlat2,inverse(n1))) = multiply(inverse(n1),n1),
inference(cp,[status(thm)],[t2784,t396]) ).
cnf(t3515,plain,
add(sFlat2,multiply(X1,sFlat2)) = multiply(sFlat2,add(sFlat2,X1)),
inference(step,[status(thm)],[t459,t2399]) ).
cnf(t2400,plain,
add(sFlat2,multiply(X1,sFlat2)) = multiply(sFlat2,add(sFlat2,X1)),
inference(orient,[status(thm)],[t3515]) ).
cnf(t2552,plain,
multiply(sFlat2,add(sFlat2,inverse(n1))) = add(sFlat2,multiply(sFlat2,inverse(n1))),
inference(cp,[status(thm)],[t2400,t2551]) ).
cnf(t3543,plain,
sFlat2 = add(sFlat2,multiply(sFlat2,inverse(n1))),
inference(step,[status(thm)],[t2552,t2415]) ).
cnf(t3544,plain,
sFlat2 = add(sFlat2,inverse(n1)),
inference(step,[status(thm)],[t3543,t2562]) ).
cnf(t2576,plain,
add(sFlat2,inverse(n1)) = sFlat2,
inference(orient,[status(thm)],[t3544]) ).
cnf(t3571,plain,
multiply(inverse(n1),sFlat2) = multiply(inverse(n1),n1),
inference(step,[status(thm)],[t2787,t2576]) ).
cnf(t3541,plain,
multiply(inverse(n1),sFlat2) = inverse(n1),
inference(step,[status(thm)],[t2551,t2562]) ).
cnf(t2563,plain,
multiply(inverse(n1),sFlat2) = inverse(n1),
inference(orient,[status(thm)],[t3541]) ).
cnf(t3572,plain,
inverse(n1) = multiply(inverse(n1),n1),
inference(step,[status(thm)],[t3571,t2563]) ).
cnf(t2799,plain,
multiply(inverse(n1),n1) = inverse(n1),
inference(orient,[status(thm)],[t3572]) ).
cnf(t2805,plain,
multiply(n1,add(inverse(n1),X1)) = add(inverse(n1),multiply(X1,n1)),
inference(cp,[status(thm)],[t379,t2799]) ).
cnf(t3577,plain,
multiply(n1,add(inverse(n1),X1)) = X1,
inference(step,[status(thm)],[t2805,t1745]) ).
cnf(t2832,plain,
multiply(n1,add(inverse(n1),X1)) = X1,
inference(orient,[status(thm)],[t3577]) ).
cnf(t2836,plain,
multiply(X1,n1) = multiply(n1,X1),
inference(cp,[status(thm)],[t2832,t1745]) ).
cnf(t2981,plain,
multiply(X1,n1) = multiply(n1,X1),
inference(orient,[status(thm)],[t2836]) ).
cnf(t2990,plain,
X1 = add(sFlat1,multiply(n1,X1)),
inference(cp,[status(thm)],[t1569,t2981]) ).
cnf(t3071,plain,
add(sFlat1,multiply(n1,X1)) = X1,
inference(orient,[status(thm)],[t2990]) ).
cnf(t3076,plain,
inverse(X1) = add(sFlat1,inverse(X1)),
inference(cp,[status(thm)],[t3071,t420]) ).
cnf(t3085,plain,
add(sFlat1,inverse(X1)) = inverse(X1),
inference(orient,[status(thm)],[t3076]) ).
cnf(t3086,plain,
inverse(sFlat1) = n1,
inference(cp,[status(thm)],[t3085,t396]) ).
cnf(t3097,plain,
inverse(sFlat1) = n1,
inference(orient,[status(thm)],[t3086]) ).
cnf(t3104,plain,
X1 = add(multiply(X1,n1),multiply(sFlat1,add(X1,inverse(sFlat1)))),
inference(cp,[status(thm)],[t2286,t3097]) ).
cnf(t3679,plain,
X1 = add(multiply(X1,n1),multiply(sFlat1,add(X1,n1))),
inference(step,[status(thm)],[t3104,t3097]) ).
cnf(t1175,plain,
add(multiply(add(X1,X2),X2),X2) = multiply(add(X3,X2),add(X2,X2)),
inference(cp,[status(thm)],[t1108,t44]) ).
cnf(t3395,plain,
add(X2,X2) = multiply(add(X3,X2),add(X2,X2)),
inference(step,[status(thm)],[t1175,t44]) ).
cnf(t1243,plain,
multiply(add(X1,X2),add(X2,X2)) = add(X2,X2),
inference(orient,[status(thm)],[t3395]) ).
cnf(t1548,plain,
add(multiply(X1,n1),multiply(X1,n1)) = multiply(X1,add(multiply(X1,n1),multiply(X1,n1))),
inference(cp,[status(thm)],[t1243,t1542]) ).
cnf(t3445,plain,
multiply(n1,add(X1,X1)) = multiply(X1,add(multiply(X1,n1),multiply(X1,n1))),
inference(step,[status(thm)],[t1548,t379]) ).
cnf(t3446,plain,
multiply(n1,add(X1,X1)) = multiply(X1,multiply(n1,add(X1,X1))),
inference(step,[status(thm)],[t3445,t379]) ).
cnf(t1772,plain,
multiply(X1,multiply(n1,add(X1,X1))) = multiply(n1,add(X1,X1)),
inference(orient,[status(thm)],[t3446]) ).
cnf(t1777,plain,
multiply(n1,add(n1,n1)) = multiply(n1,multiply(n1,add(X1,n1))),
inference(cp,[status(thm)],[t1772,t1662]) ).
cnf(t3447,plain,
multiply(n1,add(sFlat0,n1)) = multiply(n1,multiply(n1,add(X1,n1))),
inference(step,[status(thm)],[t1777,t1662]) ).
cnf(t1784,plain,
multiply(n1,multiply(n1,add(X1,n1))) = multiply(n1,add(sFlat0,n1)),
inference(orient,[status(thm)],[t3447]) ).
cnf(t380,plain,
multiply(X1,add(add(X2,X1),X3)) = add(X1,multiply(X3,X1)),
inference(cp,[status(thm)],[t379,t44]) ).
cnf(t543,plain,
multiply(X1,add(add(X2,X1),X3)) = add(X1,multiply(X3,X1)),
inference(orient,[status(thm)],[t380]) ).
cnf(t1673,plain,
add(X1,multiply(n1,X1)) = multiply(X1,add(X2,n1)),
inference(cp,[status(thm)],[t543,t1662]) ).
cnf(t1797,plain,
add(X1,multiply(n1,X1)) = multiply(X1,add(X2,n1)),
inference(orient,[status(thm)],[t1673]) ).
cnf(t2835,plain,
n1 = add(n1,multiply(n1,n1)),
inference(cp,[status(thm)],[t2832,t1797]) ).
cnf(t3578,plain,
n1 = multiply(n1,add(sFlat0,n1)),
inference(step,[status(thm)],[t2835,t1797]) ).
cnf(t2869,plain,
multiply(n1,add(sFlat0,n1)) = n1,
inference(orient,[status(thm)],[t3578]) ).
cnf(t3579,plain,
multiply(n1,multiply(n1,add(X1,n1))) = n1,
inference(step,[status(thm)],[t1784,t2869]) ).
cnf(t2870,plain,
multiply(n1,multiply(n1,add(X1,n1))) = n1,
inference(orient,[status(thm)],[t3579]) ).
cnf(t2881,plain,
n1 = multiply(n1,n1),
inference(cp,[status(thm)],[t2870,t2869]) ).
cnf(t2885,plain,
multiply(n1,n1) = n1,
inference(orient,[status(thm)],[t2881]) ).
cnf(t2891,plain,
n1 = add(sFlat1,n1),
inference(cp,[status(thm)],[t1569,t2885]) ).
cnf(t3588,plain,
n1 = add(sFlat0,n1),
inference(step,[status(thm)],[t2891,t1662]) ).
cnf(t2904,plain,
add(sFlat0,n1) = n1,
inference(orient,[status(thm)],[t3588]) ).
cnf(t2913,plain,
n1 = add(X1,n1),
inference(cp,[status(thm)],[t2904,t1662]) ).
cnf(t2930,plain,
add(X1,n1) = n1,
inference(orient,[status(thm)],[t2913]) ).
cnf(t3680,plain,
X1 = add(multiply(X1,n1),multiply(sFlat1,n1)),
inference(step,[status(thm)],[t3679,t2930]) ).
cnf(t3681,plain,
X1 = multiply(n1,add(X1,sFlat1)),
inference(step,[status(thm)],[t3680,t379]) ).
cnf(t3299,plain,
multiply(n1,add(X1,sFlat1)) = X1,
inference(orient,[status(thm)],[t3681]) ).
cnf(t1544,plain,
X1 = add(multiply(a,sFlat2),multiply(X1,n1)),
inference(cp,[status(thm)],[t1542,t398]) ).
cnf(t3416,plain,
X1 = add(sFlat3,multiply(X1,n1)),
inference(step,[status(thm)],[t1544,t406]) ).
cnf(t1557,plain,
add(sFlat3,multiply(X1,n1)) = X1,
inference(orient,[status(thm)],[t3416]) ).
cnf(t2991,plain,
X1 = add(sFlat3,multiply(n1,X1)),
inference(cp,[status(thm)],[t1557,t2981]) ).
cnf(t3119,plain,
add(sFlat3,multiply(n1,X1)) = X1,
inference(orient,[status(thm)],[t2991]) ).
cnf(t3100,plain,
X1 = add(multiply(sFlat1,n1),multiply(X1,n1)),
inference(cp,[status(thm)],[t1542,t3097]) ).
cnf(t3640,plain,
X1 = multiply(n1,add(sFlat1,X1)),
inference(step,[status(thm)],[t3100,t379]) ).
cnf(t3169,plain,
multiply(n1,add(sFlat1,X1)) = X1,
inference(orient,[status(thm)],[t3640]) ).
cnf(t3176,plain,
add(sFlat1,X1) = add(sFlat3,X1),
inference(cp,[status(thm)],[t3119,t3169]) ).
cnf(t3271,plain,
add(sFlat3,X1) = add(sFlat1,X1),
inference(orient,[status(thm)],[t3176]) ).
cnf(t3300,plain,
sFlat3 = multiply(n1,add(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t3299,t3271]) ).
cnf(t3682,plain,
sFlat3 = sFlat1,
inference(step,[status(thm)],[t3300,t3169]) ).
cnf(t3311,plain,
sFlat3 = sFlat1,
inference(orient,[status(thm)],[t3682]) ).
cnf(t3683,plain,
multiply(a,sFlat2) = sFlat1,
inference(step,[status(thm)],[t406,t3311]) ).
cnf(t3312,plain,
multiply(a,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t3683]) ).
cnf(goal_0,negated_conjecture,
multiply(b,inverse(b)) != multiply(a,inverse(a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(b,sFlat0) != multiply(a,inverse(a)),
inference(rw,[status(thm)],[goal_0,t401]) ).
cnf(g0_1,plain,
sFlat1 != multiply(a,inverse(a)),
inference(rw,[status(thm)],[g0_0,t411]) ).
cnf(g0_2,plain,
sFlat1 != multiply(a,sFlat2),
inference(rw,[status(thm)],[g0_1,t398]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t3312]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO025-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n001.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:40:54 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.49/1.32 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.49/1.32 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------