%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO014-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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 7.40s 1.67s
% Output : CNFRefutation 7.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 15
% Syntax : Number of clauses : 208 ( 208 unt; 0 nHn; 64 RR)
% Number of literals : 208 ( 207 equ; 2 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 : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 201 ( 42 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t5,axiom,
add(X1,inverse(X1)) = multiplicative_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t28,plain,
add(X1,multiply(inverse(X1),X2)) = multiply(multiplicative_identity,add(X1,X2)),
inference(cp,[status(thm)],[t21,t26]) ).
cnf(t4,axiom,
multiply(multiplicative_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
multiply(multiplicative_identity,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t3029,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(step,[status(thm)],[t28,t19]) ).
cnf(t254,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(orient,[status(thm)],[t3029]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t22,plain,
add(X1,multiply(additive_identity,X2)) = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t21,t16]) ).
cnf(t13,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t38,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t13]) ).
cnf(t42,plain,
multiply(add(multiplicative_identity,X1),X2) = add(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t38,t19]) ).
cnf(t88,plain,
add(X1,multiply(X2,X1)) = multiply(add(multiplicative_identity,X2),X1),
inference(orient,[status(thm)],[t42]) ).
cnf(t2,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t90,plain,
multiply(add(multiplicative_identity,X1),additive_identity) = multiply(X1,additive_identity),
inference(cp,[status(thm)],[t88,t17]) ).
cnf(t10,axiom,
multiply(X1,X2) = multiply(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t68,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t3002,plain,
multiply(additive_identity,add(multiplicative_identity,X1)) = multiply(X1,additive_identity),
inference(step,[status(thm)],[t90,t68]) ).
cnf(t101,plain,
multiply(additive_identity,add(multiplicative_identity,X1)) = multiply(X1,additive_identity),
inference(orient,[status(thm)],[t3002]) ).
cnf(t9,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t104,plain,
multiply(X1,additive_identity) = multiply(additive_identity,add(X1,multiplicative_identity)),
inference(cp,[status(thm)],[t101,t20]) ).
cnf(t111,plain,
multiply(additive_identity,add(X1,multiplicative_identity)) = multiply(X1,additive_identity),
inference(orient,[status(thm)],[t104]) ).
cnf(t3,axiom,
multiply(X1,multiplicative_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t262,plain,
add(X1,multiplicative_identity) = add(X1,inverse(X1)),
inference(cp,[status(thm)],[t254,t18]) ).
cnf(t3030,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(step,[status(thm)],[t262,t26]) ).
cnf(t272,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t3030]) ).
cnf(t3031,plain,
multiply(additive_identity,multiplicative_identity) = multiply(X1,additive_identity),
inference(step,[status(thm)],[t111,t272]) ).
cnf(t3032,plain,
additive_identity = multiply(X1,additive_identity),
inference(step,[status(thm)],[t3031,t18]) ).
cnf(t274,plain,
additive_identity = multiply(X1,additive_identity),
inference(rw,[status(thm)],[t3032]) ).
cnf(t283,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t274]) ).
cnf(t284,plain,
additive_identity = multiply(additive_identity,X1),
inference(cp,[status(thm)],[t283,t68]) ).
cnf(t287,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t284]) ).
cnf(t3054,plain,
add(X1,additive_identity) = multiply(X1,add(X1,X2)),
inference(step,[status(thm)],[t22,t287]) ).
cnf(t3055,plain,
X1 = multiply(X1,add(X1,X2)),
inference(step,[status(thm)],[t3054,t16]) ).
cnf(t337,plain,
multiply(X1,add(X1,X2)) = X1,
inference(orient,[status(thm)],[t3055]) ).
cnf(t363,plain,
add(X1,add(inverse(X1),X2)) = add(X1,inverse(X1)),
inference(cp,[status(thm)],[t254,t337]) ).
cnf(t3076,plain,
add(X1,add(inverse(X1),X2)) = multiplicative_identity,
inference(step,[status(thm)],[t363,t26]) ).
cnf(t595,plain,
add(X1,add(inverse(X1),X2)) = multiplicative_identity,
inference(orient,[status(thm)],[t3076]) ).
cnf(t273,plain,
multiplicative_identity = add(multiplicative_identity,X1),
inference(cp,[status(thm)],[t272,t20]) ).
cnf(t275,plain,
add(multiplicative_identity,X1) = multiplicative_identity,
inference(orient,[status(thm)],[t273]) ).
cnf(t3033,plain,
add(X1,multiply(X2,X1)) = multiply(multiplicative_identity,X1),
inference(step,[status(thm)],[t88,t275]) ).
cnf(t3034,plain,
add(X1,multiply(X2,X1)) = X1,
inference(step,[status(thm)],[t3033,t19]) ).
cnf(t276,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t3034]) ).
cnf(t15,axiom,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t1,axiom,
add(a,b) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t3000,plain,
add(b,a) = c,
inference(step,[status(thm)],[t1,t20]) ).
cnf(t63,plain,
add(b,a) = c,
inference(orient,[status(thm)],[t3000]) ).
cnf(t66,plain,
add(multiply(b,X1),a) = multiply(c,add(X1,a)),
inference(cp,[status(thm)],[t30,t63]) ).
cnf(t3016,plain,
add(a,multiply(b,X1)) = multiply(c,add(X1,a)),
inference(step,[status(thm)],[t66,t20]) ).
cnf(t197,plain,
add(a,multiply(b,X1)) = multiply(c,add(X1,a)),
inference(orient,[status(thm)],[t3016]) ).
cnf(t285,plain,
multiply(c,add(additive_identity,a)) = add(a,additive_identity),
inference(cp,[status(thm)],[t197,t283]) ).
cnf(t3047,plain,
multiply(c,a) = add(a,additive_identity),
inference(step,[status(thm)],[t285,t17]) ).
cnf(t3048,plain,
multiply(c,a) = a,
inference(step,[status(thm)],[t3047,t16]) ).
cnf(t290,plain,
multiply(c,a) = a,
inference(orient,[status(thm)],[t3048]) ).
cnf(t296,plain,
multiply(add(c,X1),a) = add(a,multiply(X1,a)),
inference(cp,[status(thm)],[t38,t290]) ).
cnf(t3056,plain,
multiply(a,add(c,X1)) = add(a,multiply(X1,a)),
inference(step,[status(thm)],[t296,t68]) ).
cnf(t3057,plain,
multiply(a,add(c,X1)) = a,
inference(step,[status(thm)],[t3056,t276]) ).
cnf(t376,plain,
multiply(a,add(c,X1)) = a,
inference(orient,[status(thm)],[t3057]) ).
cnf(t384,plain,
a = multiply(a,add(X1,c)),
inference(cp,[status(thm)],[t376,t20]) ).
cnf(t442,plain,
multiply(a,add(X1,c)) = a,
inference(orient,[status(thm)],[t384]) ).
cnf(t446,plain,
add(X1,c) = add(add(X1,c),a),
inference(cp,[status(thm)],[t276,t442]) ).
cnf(t3074,plain,
add(X1,c) = add(a,add(X1,c)),
inference(step,[status(thm)],[t446,t20]) ).
cnf(t579,plain,
add(a,add(X1,c)) = add(X1,c),
inference(orient,[status(thm)],[t3074]) ).
cnf(t597,plain,
multiplicative_identity = add(inverse(a),c),
inference(cp,[status(thm)],[t595,t579]) ).
cnf(t3077,plain,
multiplicative_identity = add(c,inverse(a)),
inference(step,[status(thm)],[t597,t20]) ).
cnf(t605,plain,
add(c,inverse(a)) = multiplicative_identity,
inference(orient,[status(thm)],[t3077]) ).
cnf(t606,plain,
add(c,multiply(inverse(a),X1)) = multiply(multiplicative_identity,add(c,X1)),
inference(cp,[status(thm)],[t21,t605]) ).
cnf(t3217,plain,
add(c,multiply(inverse(a),X1)) = add(c,X1),
inference(step,[status(thm)],[t606,t19]) ).
cnf(t2874,plain,
add(c,multiply(inverse(a),X1)) = add(c,X1),
inference(orient,[status(thm)],[t3217]) ).
cnf(t12,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t50,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t7,axiom,
multiply(X1,inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t75,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t7]) ).
cnf(t77,plain,
multiply(X1,add(inverse(X1),X2)) = add(additive_identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t50,t75]) ).
cnf(t3103,plain,
multiply(X1,add(inverse(X1),X2)) = multiply(X1,X2),
inference(step,[status(thm)],[t77,t17]) ).
cnf(t1093,plain,
multiply(X1,add(inverse(X1),X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t3103]) ).
cnf(t2876,plain,
add(c,add(inverse(inverse(a)),X1)) = add(c,multiply(inverse(a),X1)),
inference(cp,[status(thm)],[t2874,t1093]) ).
cnf(t1109,plain,
multiply(X1,inverse(inverse(X1))) = multiply(X1,multiplicative_identity),
inference(cp,[status(thm)],[t1093,t26]) ).
cnf(t354,plain,
X1 = multiply(X1,add(X2,X1)),
inference(cp,[status(thm)],[t337,t20]) ).
cnf(t419,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t354]) ).
cnf(t263,plain,
add(X1,inverse(inverse(X1))) = add(X1,additive_identity),
inference(cp,[status(thm)],[t254,t75]) ).
cnf(t3053,plain,
add(X1,inverse(inverse(X1))) = X1,
inference(step,[status(thm)],[t263,t16]) ).
cnf(t332,plain,
add(X1,inverse(inverse(X1))) = X1,
inference(orient,[status(thm)],[t3053]) ).
cnf(t423,plain,
inverse(inverse(X1)) = multiply(inverse(inverse(X1)),X1),
inference(cp,[status(thm)],[t419,t332]) ).
cnf(t3072,plain,
inverse(inverse(X1)) = multiply(X1,inverse(inverse(X1))),
inference(step,[status(thm)],[t423,t68]) ).
cnf(t552,plain,
multiply(X1,inverse(inverse(X1))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t3072]) ).
cnf(t3104,plain,
inverse(inverse(X1)) = multiply(X1,multiplicative_identity),
inference(step,[status(thm)],[t1109,t552]) ).
cnf(t3105,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t3104,t18]) ).
cnf(t1123,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t3105]) ).
cnf(t3219,plain,
add(c,add(a,X1)) = add(c,multiply(inverse(a),X1)),
inference(step,[status(thm)],[t2876,t1123]) ).
cnf(t3220,plain,
add(c,add(a,X1)) = add(c,X1),
inference(step,[status(thm)],[t3219,t2874]) ).
cnf(t2905,plain,
add(c,add(a,X1)) = add(c,X1),
inference(orient,[status(thm)],[t3220]) ).
cnf(t29,plain,
add(X1,multiply(X2,inverse(X1))) = multiply(add(X1,X2),multiplicative_identity),
inference(cp,[status(thm)],[t21,t26]) ).
cnf(t3100,plain,
add(X1,multiply(X2,inverse(X1))) = add(X1,X2),
inference(step,[status(thm)],[t29,t18]) ).
cnf(t1042,plain,
add(X1,multiply(X2,inverse(X1))) = add(X1,X2),
inference(orient,[status(thm)],[t3100]) ).
cnf(t11,axiom,
multiply(inverse(a),inverse(b)) = d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t3001,plain,
multiply(inverse(b),inverse(a)) = d,
inference(step,[status(thm)],[t11,t68]) ).
cnf(t81,plain,
multiply(inverse(b),inverse(a)) = d,
inference(orient,[status(thm)],[t3001]) ).
cnf(t1052,plain,
add(a,inverse(b)) = add(a,d),
inference(cp,[status(thm)],[t1042,t81]) ).
cnf(t3101,plain,
add(a,inverse(b)) = add(d,a),
inference(step,[status(thm)],[t1052,t20]) ).
cnf(t1061,plain,
add(a,inverse(b)) = add(d,a),
inference(orient,[status(thm)],[t3101]) ).
cnf(t2907,plain,
add(c,inverse(b)) = add(c,add(d,a)),
inference(cp,[status(thm)],[t2905,t1061]) ).
cnf(t64,plain,
add(b,multiply(a,X1)) = multiply(c,add(b,X1)),
inference(cp,[status(thm)],[t21,t63]) ).
cnf(t166,plain,
add(b,multiply(a,X1)) = multiply(c,add(b,X1)),
inference(orient,[status(thm)],[t64]) ).
cnf(t286,plain,
multiply(c,add(b,additive_identity)) = add(b,additive_identity),
inference(cp,[status(thm)],[t166,t283]) ).
cnf(t3049,plain,
multiply(c,b) = add(b,additive_identity),
inference(step,[status(thm)],[t286,t16]) ).
cnf(t3050,plain,
multiply(c,b) = b,
inference(step,[status(thm)],[t3049,t16]) ).
cnf(t298,plain,
multiply(c,b) = b,
inference(orient,[status(thm)],[t3050]) ).
cnf(t304,plain,
multiply(add(c,X1),b) = add(b,multiply(X1,b)),
inference(cp,[status(thm)],[t38,t298]) ).
cnf(t3058,plain,
multiply(b,add(c,X1)) = add(b,multiply(X1,b)),
inference(step,[status(thm)],[t304,t68]) ).
cnf(t3059,plain,
multiply(b,add(c,X1)) = b,
inference(step,[status(thm)],[t3058,t276]) ).
cnf(t391,plain,
multiply(b,add(c,X1)) = b,
inference(orient,[status(thm)],[t3059]) ).
cnf(t399,plain,
b = multiply(b,add(X1,c)),
inference(cp,[status(thm)],[t391,t20]) ).
cnf(t451,plain,
multiply(b,add(X1,c)) = b,
inference(orient,[status(thm)],[t399]) ).
cnf(t455,plain,
add(X1,c) = add(add(X1,c),b),
inference(cp,[status(thm)],[t276,t451]) ).
cnf(t3075,plain,
add(X1,c) = add(b,add(X1,c)),
inference(step,[status(thm)],[t455,t20]) ).
cnf(t587,plain,
add(b,add(X1,c)) = add(X1,c),
inference(orient,[status(thm)],[t3075]) ).
cnf(t598,plain,
multiplicative_identity = add(inverse(b),c),
inference(cp,[status(thm)],[t595,t587]) ).
cnf(t3078,plain,
multiplicative_identity = add(c,inverse(b)),
inference(step,[status(thm)],[t598,t20]) ).
cnf(t610,plain,
add(c,inverse(b)) = multiplicative_identity,
inference(orient,[status(thm)],[t3078]) ).
cnf(t3221,plain,
multiplicative_identity = add(c,add(d,a)),
inference(step,[status(thm)],[t2907,t610]) ).
cnf(t2924,plain,
add(c,add(d,a)) = multiplicative_identity,
inference(orient,[status(thm)],[t3221]) ).
cnf(t78,plain,
multiply(X1,add(X2,inverse(X1))) = add(multiply(X1,X2),additive_identity),
inference(cp,[status(thm)],[t50,t75]) ).
cnf(t3215,plain,
multiply(X1,add(X2,inverse(X1))) = multiply(X1,X2),
inference(step,[status(thm)],[t78,t16]) ).
cnf(t2827,plain,
multiply(X1,add(X2,inverse(X1))) = multiply(X1,X2),
inference(orient,[status(thm)],[t3215]) ).
cnf(t2879,plain,
add(c,add(X1,inverse(inverse(a)))) = add(c,multiply(inverse(a),X1)),
inference(cp,[status(thm)],[t2874,t2827]) ).
cnf(t3222,plain,
add(c,add(X1,a)) = add(c,multiply(inverse(a),X1)),
inference(step,[status(thm)],[t2879,t1123]) ).
cnf(t3223,plain,
add(c,add(X1,a)) = add(c,X1),
inference(step,[status(thm)],[t3222,t2874]) ).
cnf(t2933,plain,
add(c,add(X1,a)) = add(c,X1),
inference(orient,[status(thm)],[t3223]) ).
cnf(t3224,plain,
add(c,d) = multiplicative_identity,
inference(step,[status(thm)],[t2924,t2933]) ).
cnf(t2946,plain,
add(c,d) = multiplicative_identity,
inference(rw,[status(thm)],[t3224]) ).
cnf(t3225,plain,
add(d,c) = multiplicative_identity,
inference(step,[status(thm)],[t2946,t20]) ).
cnf(t2947,plain,
add(d,c) = multiplicative_identity,
inference(orient,[status(thm)],[t3225]) ).
cnf(t2948,plain,
add(d,multiply(c,X1)) = multiply(multiplicative_identity,add(d,X1)),
inference(cp,[status(thm)],[t21,t2947]) ).
cnf(t3226,plain,
add(d,multiply(c,X1)) = add(d,X1),
inference(step,[status(thm)],[t2948,t19]) ).
cnf(t2956,plain,
add(d,multiply(c,X1)) = add(d,X1),
inference(orient,[status(thm)],[t3226]) ).
cnf(t2965,plain,
add(d,inverse(c)) = add(d,additive_identity),
inference(cp,[status(thm)],[t2956,t75]) ).
cnf(t421,plain,
multiply(X1,X2) = multiply(multiply(X1,X2),X2),
inference(cp,[status(thm)],[t419,t276]) ).
cnf(t3064,plain,
multiply(X1,X2) = multiply(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t421,t68]) ).
cnf(t503,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t3064]) ).
cnf(t512,plain,
multiply(inverse(b),inverse(a)) = multiply(inverse(a),d),
inference(cp,[status(thm)],[t503,t81]) ).
cnf(t3065,plain,
d = multiply(inverse(a),d),
inference(step,[status(thm)],[t512,t81]) ).
cnf(t3066,plain,
d = multiply(d,inverse(a)),
inference(step,[status(thm)],[t3065,t68]) ).
cnf(t520,plain,
multiply(d,inverse(a)) = d,
inference(orient,[status(thm)],[t3066]) ).
cnf(t522,plain,
inverse(a) = add(inverse(a),d),
inference(cp,[status(thm)],[t276,t520]) ).
cnf(t3067,plain,
inverse(a) = add(d,inverse(a)),
inference(step,[status(thm)],[t522,t20]) ).
cnf(t527,plain,
add(d,inverse(a)) = inverse(a),
inference(orient,[status(thm)],[t3067]) ).
cnf(t530,plain,
add(multiply(d,X1),inverse(a)) = multiply(inverse(a),add(X1,inverse(a))),
inference(cp,[status(thm)],[t30,t527]) ).
cnf(t3082,plain,
add(inverse(a),multiply(d,X1)) = multiply(inverse(a),add(X1,inverse(a))),
inference(step,[status(thm)],[t530,t20]) ).
cnf(t3083,plain,
add(inverse(a),multiply(d,X1)) = inverse(a),
inference(step,[status(thm)],[t3082,t419]) ).
cnf(t666,plain,
add(inverse(a),multiply(d,X1)) = inverse(a),
inference(orient,[status(thm)],[t3083]) ).
cnf(t1098,plain,
multiply(a,multiply(d,X1)) = multiply(a,inverse(a)),
inference(cp,[status(thm)],[t1093,t666]) ).
cnf(t3108,plain,
multiply(a,multiply(d,X1)) = additive_identity,
inference(step,[status(thm)],[t1098,t75]) ).
cnf(t1133,plain,
multiply(a,multiply(d,X1)) = additive_identity,
inference(orient,[status(thm)],[t3108]) ).
cnf(t1134,plain,
additive_identity = multiply(d,a),
inference(cp,[status(thm)],[t1133,t503]) ).
cnf(t1152,plain,
multiply(d,a) = additive_identity,
inference(orient,[status(thm)],[t1134]) ).
cnf(t1155,plain,
multiply(d,add(X1,a)) = add(multiply(d,X1),additive_identity),
inference(cp,[status(thm)],[t50,t1152]) ).
cnf(t3115,plain,
multiply(d,add(X1,a)) = multiply(d,X1),
inference(step,[status(thm)],[t1155,t16]) ).
cnf(t1228,plain,
multiply(d,add(X1,a)) = multiply(d,X1),
inference(orient,[status(thm)],[t3115]) ).
cnf(t1229,plain,
multiply(d,b) = multiply(d,c),
inference(cp,[status(thm)],[t1228,t63]) ).
cnf(t53,plain,
multiply(X1,add(multiplicative_identity,X2)) = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t50,t18]) ).
cnf(t130,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(multiplicative_identity,X2)),
inference(orient,[status(thm)],[t53]) ).
cnf(t3037,plain,
add(X1,multiply(X1,X2)) = multiply(X1,multiplicative_identity),
inference(step,[status(thm)],[t130,t275]) ).
cnf(t3038,plain,
add(X1,multiply(X1,X2)) = X1,
inference(step,[status(thm)],[t3037,t18]) ).
cnf(t278,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t3038]) ).
cnf(t422,plain,
multiply(X1,X2) = multiply(multiply(X1,X2),X1),
inference(cp,[status(thm)],[t419,t278]) ).
cnf(t3068,plain,
multiply(X1,X2) = multiply(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t422,t68]) ).
cnf(t532,plain,
multiply(X1,multiply(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t3068]) ).
cnf(t533,plain,
multiply(inverse(b),inverse(a)) = multiply(inverse(b),d),
inference(cp,[status(thm)],[t532,t81]) ).
cnf(t3069,plain,
d = multiply(inverse(b),d),
inference(step,[status(thm)],[t533,t81]) ).
cnf(t3070,plain,
d = multiply(d,inverse(b)),
inference(step,[status(thm)],[t3069,t68]) ).
cnf(t540,plain,
multiply(d,inverse(b)) = d,
inference(orient,[status(thm)],[t3070]) ).
cnf(t542,plain,
inverse(b) = add(inverse(b),d),
inference(cp,[status(thm)],[t276,t540]) ).
cnf(t3071,plain,
inverse(b) = add(d,inverse(b)),
inference(step,[status(thm)],[t542,t20]) ).
cnf(t547,plain,
add(d,inverse(b)) = inverse(b),
inference(orient,[status(thm)],[t3071]) ).
cnf(t550,plain,
add(multiply(d,X1),inverse(b)) = multiply(inverse(b),add(X1,inverse(b))),
inference(cp,[status(thm)],[t30,t547]) ).
cnf(t3084,plain,
add(inverse(b),multiply(d,X1)) = multiply(inverse(b),add(X1,inverse(b))),
inference(step,[status(thm)],[t550,t20]) ).
cnf(t3085,plain,
add(inverse(b),multiply(d,X1)) = inverse(b),
inference(step,[status(thm)],[t3084,t419]) ).
cnf(t686,plain,
add(inverse(b),multiply(d,X1)) = inverse(b),
inference(orient,[status(thm)],[t3085]) ).
cnf(t1101,plain,
multiply(b,multiply(d,X1)) = multiply(b,inverse(b)),
inference(cp,[status(thm)],[t1093,t686]) ).
cnf(t3110,plain,
multiply(b,multiply(d,X1)) = additive_identity,
inference(step,[status(thm)],[t1101,t75]) ).
cnf(t1167,plain,
multiply(b,multiply(d,X1)) = additive_identity,
inference(orient,[status(thm)],[t3110]) ).
cnf(t1168,plain,
additive_identity = multiply(d,b),
inference(cp,[status(thm)],[t1167,t503]) ).
cnf(t1186,plain,
multiply(d,b) = additive_identity,
inference(orient,[status(thm)],[t1168]) ).
cnf(t3116,plain,
additive_identity = multiply(d,c),
inference(step,[status(thm)],[t1229,t1186]) ).
cnf(t1236,plain,
multiply(d,c) = additive_identity,
inference(orient,[status(thm)],[t3116]) ).
cnf(t1237,plain,
multiply(d,add(c,X1)) = add(additive_identity,multiply(d,X1)),
inference(cp,[status(thm)],[t50,t1236]) ).
cnf(t3135,plain,
multiply(d,add(c,X1)) = multiply(d,X1),
inference(step,[status(thm)],[t1237,t17]) ).
cnf(t1372,plain,
multiply(d,add(c,X1)) = multiply(d,X1),
inference(orient,[status(thm)],[t3135]) ).
cnf(t1379,plain,
multiply(d,inverse(c)) = multiply(d,multiplicative_identity),
inference(cp,[status(thm)],[t1372,t26]) ).
cnf(t3136,plain,
multiply(d,inverse(c)) = d,
inference(step,[status(thm)],[t1379,t18]) ).
cnf(t1387,plain,
multiply(d,inverse(c)) = d,
inference(orient,[status(thm)],[t3136]) ).
cnf(t1393,plain,
inverse(c) = add(inverse(c),d),
inference(cp,[status(thm)],[t276,t1387]) ).
cnf(t3137,plain,
inverse(c) = add(d,inverse(c)),
inference(step,[status(thm)],[t1393,t20]) ).
cnf(t1398,plain,
add(d,inverse(c)) = inverse(c),
inference(orient,[status(thm)],[t3137]) ).
cnf(t3227,plain,
inverse(c) = add(d,additive_identity),
inference(step,[status(thm)],[t2965,t1398]) ).
cnf(t3228,plain,
inverse(c) = d,
inference(step,[status(thm)],[t3227,t16]) ).
cnf(t2984,plain,
inverse(c) = d,
inference(orient,[status(thm)],[t3228]) ).
cnf(goal_0,negated_conjecture,
inverse(c) != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
d != d,
inference(rw,[status(thm)],[goal_0,t2984]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO014-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n002.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:35:04 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.40/1.67 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.40/1.67 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------