%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO014-4 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 12:59:37 PM UTC 2026
% Result : Unsatisfiable 6.30s 1.81s
% Output : CNFRefutation 6.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 9
% Syntax : Number of clauses : 151 ( 151 unt; 0 nHn; 4 RR)
% Number of literals : 151 ( 150 equ; 3 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 288 ( 38 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t7,axiom,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t2,axiom,
add(X1,inverse(X1)) = multiplicative_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t2]) ).
cnf(t35,plain,
add(X1,multiply(X2,inverse(X1))) = multiply(add(X1,X2),multiplicative_identity),
inference(cp,[status(thm)],[t20,t33]) ).
cnf(t1,axiom,
multiply(X1,multiplicative_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t15024,plain,
add(X1,multiply(X2,inverse(X1))) = add(X1,X2),
inference(step,[status(thm)],[t35,t8]) ).
cnf(t198,plain,
add(X1,multiply(X2,inverse(X1))) = add(X1,X2),
inference(orient,[status(thm)],[t15024]) ).
cnf(t5,axiom,
multiply(X1,X2) = multiply(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t200,plain,
add(X1,X2) = add(X1,multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t198,t10]) ).
cnf(t233,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(orient,[status(thm)],[t200]) ).
cnf(t3,axiom,
multiply(X1,inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t3]) ).
cnf(t240,plain,
add(X1,inverse(inverse(X1))) = add(X1,additive_identity),
inference(cp,[status(thm)],[t233,t17]) ).
cnf(t6,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t13,plain,
multiply(X1,add(multiplicative_identity,X2)) = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t12,t8]) ).
cnf(t42,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(multiplicative_identity,X2)),
inference(orient,[status(thm)],[t13]) ).
cnf(t47,plain,
multiply(X1,add(multiplicative_identity,X2)) = add(X1,multiply(X2,X1)),
inference(cp,[status(thm)],[t42,t10]) ).
cnf(t65,plain,
add(X1,multiply(X2,X1)) = multiply(X1,add(multiplicative_identity,X2)),
inference(orient,[status(thm)],[t47]) ).
cnf(t19,plain,
multiply(X1,add(X2,inverse(X1))) = add(multiply(X1,X2),additive_identity),
inference(cp,[status(thm)],[t12,t17]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t14991,plain,
multiply(X1,add(X2,inverse(X1))) = multiply(X1,X2),
inference(step,[status(thm)],[t19,t9]) ).
cnf(t99,plain,
multiply(X1,add(X2,inverse(X1))) = multiply(X1,X2),
inference(orient,[status(thm)],[t14991]) ).
cnf(t101,plain,
multiply(X1,X1) = multiply(X1,multiplicative_identity),
inference(cp,[status(thm)],[t99,t33]) ).
cnf(t14992,plain,
multiply(X1,X1) = X1,
inference(step,[status(thm)],[t101,t8]) ).
cnf(t108,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t14992]) ).
cnf(t110,plain,
multiply(X1,add(X2,X1)) = add(multiply(X1,X2),X1),
inference(cp,[status(thm)],[t12,t108]) ).
cnf(t4,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t15003,plain,
multiply(X1,add(X2,X1)) = add(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t110,t28]) ).
cnf(t15004,plain,
multiply(X1,add(X2,X1)) = multiply(X1,add(multiplicative_identity,X2)),
inference(step,[status(thm)],[t15003,t42]) ).
cnf(t135,plain,
multiply(X1,add(X2,X1)) = multiply(X1,add(multiplicative_identity,X2)),
inference(orient,[status(thm)],[t15004]) ).
cnf(t69,plain,
multiply(inverse(X1),add(multiplicative_identity,X1)) = add(inverse(X1),additive_identity),
inference(cp,[status(thm)],[t65,t17]) ).
cnf(t14985,plain,
multiply(inverse(X1),add(multiplicative_identity,X1)) = inverse(X1),
inference(step,[status(thm)],[t69,t9]) ).
cnf(t76,plain,
multiply(inverse(X1),add(multiplicative_identity,X1)) = inverse(X1),
inference(orient,[status(thm)],[t14985]) ).
cnf(t80,plain,
multiply(add(multiplicative_identity,X1),add(multiplicative_identity,inverse(X1))) = add(add(multiplicative_identity,X1),inverse(X1)),
inference(cp,[status(thm)],[t65,t76]) ).
cnf(t14986,plain,
add(multiplicative_identity,multiply(X1,inverse(X1))) = add(add(multiplicative_identity,X1),inverse(X1)),
inference(step,[status(thm)],[t80,t20]) ).
cnf(t14987,plain,
add(multiplicative_identity,additive_identity) = add(add(multiplicative_identity,X1),inverse(X1)),
inference(step,[status(thm)],[t14986,t17]) ).
cnf(t14988,plain,
multiplicative_identity = add(add(multiplicative_identity,X1),inverse(X1)),
inference(step,[status(thm)],[t14987,t9]) ).
cnf(t14989,plain,
multiplicative_identity = add(inverse(X1),add(multiplicative_identity,X1)),
inference(step,[status(thm)],[t14988,t28]) ).
cnf(t82,plain,
add(inverse(X1),add(multiplicative_identity,X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t14989]) ).
cnf(t140,plain,
multiply(add(multiplicative_identity,X1),add(multiplicative_identity,inverse(X1))) = multiply(add(multiplicative_identity,X1),multiplicative_identity),
inference(cp,[status(thm)],[t135,t82]) ).
cnf(t15005,plain,
add(multiplicative_identity,multiply(X1,inverse(X1))) = multiply(add(multiplicative_identity,X1),multiplicative_identity),
inference(step,[status(thm)],[t140,t20]) ).
cnf(t15006,plain,
add(multiplicative_identity,additive_identity) = multiply(add(multiplicative_identity,X1),multiplicative_identity),
inference(step,[status(thm)],[t15005,t17]) ).
cnf(t15007,plain,
multiplicative_identity = multiply(add(multiplicative_identity,X1),multiplicative_identity),
inference(step,[status(thm)],[t15006,t9]) ).
cnf(t15008,plain,
multiplicative_identity = add(multiplicative_identity,X1),
inference(step,[status(thm)],[t15007,t8]) ).
cnf(t155,plain,
add(multiplicative_identity,X1) = multiplicative_identity,
inference(orient,[status(thm)],[t15008]) ).
cnf(t15013,plain,
add(X1,multiply(X2,X1)) = multiply(X1,multiplicative_identity),
inference(step,[status(thm)],[t65,t155]) ).
cnf(t15014,plain,
add(X1,multiply(X2,X1)) = X1,
inference(step,[status(thm)],[t15013,t8]) ).
cnf(t158,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t15014]) ).
cnf(t103,plain,
multiply(X1,X2) = multiply(X1,add(inverse(X1),X2)),
inference(cp,[status(thm)],[t99,t28]) ).
cnf(t205,plain,
multiply(X1,add(inverse(X1),X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t103]) ).
cnf(t209,plain,
multiply(X1,inverse(inverse(X1))) = multiply(X1,multiplicative_identity),
inference(cp,[status(thm)],[t205,t33]) ).
cnf(t15025,plain,
multiply(X1,inverse(inverse(X1))) = X1,
inference(step,[status(thm)],[t209,t8]) ).
cnf(t214,plain,
multiply(X1,inverse(inverse(X1))) = X1,
inference(orient,[status(thm)],[t15025]) ).
cnf(t218,plain,
inverse(inverse(X1)) = add(inverse(inverse(X1)),X1),
inference(cp,[status(thm)],[t158,t214]) ).
cnf(t15026,plain,
inverse(inverse(X1)) = add(X1,inverse(inverse(X1))),
inference(step,[status(thm)],[t218,t28]) ).
cnf(t219,plain,
add(X1,inverse(inverse(X1))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t15026]) ).
cnf(t15029,plain,
inverse(inverse(X1)) = add(X1,additive_identity),
inference(step,[status(thm)],[t240,t219]) ).
cnf(t15030,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t15029,t9]) ).
cnf(t247,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t15030]) ).
cnf(t251,plain,
add(inverse(X1),X2) = add(inverse(X1),multiply(X1,X2)),
inference(cp,[status(thm)],[t233,t247]) ).
cnf(t539,plain,
add(inverse(X1),multiply(X1,X2)) = add(inverse(X1),X2),
inference(orient,[status(thm)],[t251]) ).
cnf(t15017,plain,
multiply(X1,add(X2,X1)) = multiply(X1,multiplicative_identity),
inference(step,[status(thm)],[t135,t155]) ).
cnf(t15018,plain,
multiply(X1,add(X2,X1)) = X1,
inference(step,[status(thm)],[t15017,t8]) ).
cnf(t161,plain,
multiply(X1,add(X2,X1)) = X1,
inference(rw,[status(thm)],[t15018]) ).
cnf(t164,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t161]) ).
cnf(t15009,plain,
add(X1,multiply(X1,X2)) = multiply(X1,multiplicative_identity),
inference(step,[status(thm)],[t42,t155]) ).
cnf(t15010,plain,
add(X1,multiply(X1,X2)) = X1,
inference(step,[status(thm)],[t15009,t8]) ).
cnf(t156,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t15010]) ).
cnf(t165,plain,
multiply(X1,X2) = multiply(multiply(X1,X2),X1),
inference(cp,[status(thm)],[t164,t156]) ).
cnf(t15020,plain,
multiply(X1,X2) = multiply(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t165,t10]) ).
cnf(t177,plain,
multiply(X1,multiply(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t15020]) ).
cnf(t180,plain,
multiply(X1,add(X2,multiply(X1,X3))) = add(multiply(X1,X2),multiply(X1,X3)),
inference(cp,[status(thm)],[t12,t177]) ).
cnf(t15105,plain,
multiply(X1,add(X2,multiply(X1,X3))) = multiply(X1,add(X2,X3)),
inference(step,[status(thm)],[t180,t12]) ).
cnf(t5044,plain,
multiply(X1,add(X2,multiply(X1,X3))) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t15105]) ).
cnf(t179,plain,
multiply(X1,add(multiply(X1,X2),X3)) = add(multiply(X1,X2),multiply(X1,X3)),
inference(cp,[status(thm)],[t12,t177]) ).
cnf(t15103,plain,
multiply(X1,add(multiply(X1,X2),X3)) = multiply(X1,add(X2,X3)),
inference(step,[status(thm)],[t179,t12]) ).
cnf(t4533,plain,
multiply(X1,add(multiply(X1,X2),X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t15103]) ).
cnf(t14,plain,
multiply(X1,add(X2,X3)) = add(multiply(X2,X1),multiply(X1,X3)),
inference(cp,[status(thm)],[t12,t10]) ).
cnf(t289,plain,
add(multiply(X1,X2),multiply(X2,X3)) = multiply(X2,add(X1,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t4537,plain,
multiply(X1,add(X2,multiply(X2,X3))) = multiply(X1,multiply(X2,add(X1,X3))),
inference(cp,[status(thm)],[t4533,t289]) ).
cnf(t15104,plain,
multiply(X1,X2) = multiply(X1,multiply(X2,add(X1,X3))),
inference(step,[status(thm)],[t4537,t156]) ).
cnf(t4665,plain,
multiply(X1,multiply(X2,add(X1,X3))) = multiply(X1,X2),
inference(orient,[status(thm)],[t15104]) ).
cnf(t171,plain,
add(X1,X2) = add(add(X1,X2),X2),
inference(cp,[status(thm)],[t158,t164]) ).
cnf(t15022,plain,
add(X1,X2) = add(X2,add(X1,X2)),
inference(step,[status(thm)],[t171,t28]) ).
cnf(t188,plain,
add(X1,add(X2,X1)) = add(X2,X1),
inference(orient,[status(thm)],[t15022]) ).
cnf(t4689,plain,
multiply(X1,X2) = multiply(X1,multiply(X2,add(X3,X1))),
inference(cp,[status(thm)],[t4665,t188]) ).
cnf(t4845,plain,
multiply(X1,multiply(X2,add(X3,X1))) = multiply(X1,X2),
inference(orient,[status(thm)],[t4689]) ).
cnf(t4872,plain,
multiply(multiply(X1,X2),X3) = multiply(multiply(X1,X2),multiply(X3,X1)),
inference(cp,[status(thm)],[t4845,t156]) ).
cnf(t7728,plain,
multiply(multiply(X1,X2),multiply(X3,X1)) = multiply(multiply(X1,X2),X3),
inference(orient,[status(thm)],[t4872]) ).
cnf(t7739,plain,
multiply(multiply(X1,X2),X3) = multiply(multiply(X3,X1),multiply(X1,X2)),
inference(cp,[status(thm)],[t7728,t10]) ).
cnf(t4681,plain,
multiply(X1,X2) = multiply(X1,multiply(add(X1,X3),X2)),
inference(cp,[status(thm)],[t4665,t10]) ).
cnf(t4754,plain,
multiply(X1,multiply(add(X1,X2),X3)) = multiply(X1,X3),
inference(orient,[status(thm)],[t4681]) ).
cnf(t4788,plain,
multiply(X1,X2) = multiply(X1,multiply(add(X3,X1),X2)),
inference(cp,[status(thm)],[t4754,t188]) ).
cnf(t4939,plain,
multiply(X1,multiply(add(X2,X1),X3)) = multiply(X1,X3),
inference(orient,[status(thm)],[t4788]) ).
cnf(t4984,plain,
multiply(multiply(X1,X2),X3) = multiply(multiply(X1,X2),multiply(X2,X3)),
inference(cp,[status(thm)],[t4939,t158]) ).
cnf(t8243,plain,
multiply(multiply(X1,X2),multiply(X2,X3)) = multiply(multiply(X1,X2),X3),
inference(orient,[status(thm)],[t4984]) ).
cnf(t15124,plain,
multiply(multiply(X1,X2),X3) = multiply(multiply(X3,X1),X2),
inference(step,[status(thm)],[t7739,t8243]) ).
cnf(t9757,plain,
multiply(multiply(X1,X2),X3) = multiply(multiply(X3,X1),X2),
inference(orient,[status(thm)],[t15124]) ).
cnf(t9769,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(cp,[status(thm)],[t9757,t10]) ).
cnf(t10209,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t9769]) ).
cnf(t10240,plain,
multiply(X1,multiply(X2,inverse(multiply(X1,X2)))) = additive_identity,
inference(cp,[status(thm)],[t10209,t17]) ).
cnf(t10372,plain,
multiply(X1,multiply(X2,inverse(multiply(X1,X2)))) = additive_identity,
inference(orient,[status(thm)],[t10240]) ).
cnf(t10415,plain,
add(X1,multiply(X2,inverse(multiply(inverse(X1),X2)))) = add(X1,additive_identity),
inference(cp,[status(thm)],[t233,t10372]) ).
cnf(t15201,plain,
add(X1,multiply(X2,inverse(multiply(inverse(X1),X2)))) = X1,
inference(step,[status(thm)],[t10415,t9]) ).
cnf(t14040,plain,
add(X1,multiply(X2,inverse(multiply(inverse(X1),X2)))) = X1,
inference(orient,[status(thm)],[t15201]) ).
cnf(t14092,plain,
multiply(X1,add(X2,inverse(multiply(inverse(X2),X1)))) = multiply(X1,X2),
inference(cp,[status(thm)],[t5044,t14040]) ).
cnf(t239,plain,
add(X1,add(X2,inverse(X1))) = add(X1,inverse(X1)),
inference(cp,[status(thm)],[t233,t164]) ).
cnf(t15032,plain,
add(X1,add(X2,inverse(X1))) = multiplicative_identity,
inference(step,[status(thm)],[t239,t33]) ).
cnf(t263,plain,
add(X1,add(X2,inverse(X1))) = multiplicative_identity,
inference(orient,[status(thm)],[t15032]) ).
cnf(t264,plain,
multiplicative_identity = add(inverse(X1),add(X2,X1)),
inference(cp,[status(thm)],[t263,t247]) ).
cnf(t336,plain,
add(inverse(X1),add(X2,X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t264]) ).
cnf(t342,plain,
multiplicative_identity = add(inverse(multiply(X1,X2)),X1),
inference(cp,[status(thm)],[t336,t156]) ).
cnf(t15035,plain,
multiplicative_identity = add(X1,inverse(multiply(X1,X2))),
inference(step,[status(thm)],[t342,t28]) ).
cnf(t374,plain,
add(X1,inverse(multiply(X1,X2))) = multiplicative_identity,
inference(orient,[status(thm)],[t15035]) ).
cnf(t381,plain,
multiply(X1,inverse(multiply(inverse(X1),X2))) = multiply(X1,multiplicative_identity),
inference(cp,[status(thm)],[t205,t374]) ).
cnf(t15041,plain,
multiply(X1,inverse(multiply(inverse(X1),X2))) = X1,
inference(step,[status(thm)],[t381,t8]) ).
cnf(t453,plain,
multiply(X1,inverse(multiply(inverse(X1),X2))) = X1,
inference(orient,[status(thm)],[t15041]) ).
cnf(t464,plain,
inverse(multiply(inverse(X1),X2)) = add(inverse(multiply(inverse(X1),X2)),X1),
inference(cp,[status(thm)],[t158,t453]) ).
cnf(t15113,plain,
inverse(multiply(inverse(X1),X2)) = add(X1,inverse(multiply(inverse(X1),X2))),
inference(step,[status(thm)],[t464,t28]) ).
cnf(t6411,plain,
add(X1,inverse(multiply(inverse(X1),X2))) = inverse(multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t15113]) ).
cnf(t15202,plain,
multiply(X1,inverse(multiply(inverse(X2),X1))) = multiply(X1,X2),
inference(step,[status(thm)],[t14092,t6411]) ).
cnf(t14120,plain,
multiply(X1,inverse(multiply(inverse(X2),X1))) = multiply(X1,X2),
inference(orient,[status(thm)],[t15202]) ).
cnf(t14175,plain,
add(inverse(X1),inverse(multiply(inverse(X2),X1))) = add(inverse(X1),multiply(X1,X2)),
inference(cp,[status(thm)],[t539,t14120]) ).
cnf(t255,plain,
add(inverse(X1),X2) = add(inverse(X1),multiply(X2,X1)),
inference(cp,[status(thm)],[t198,t247]) ).
cnf(t585,plain,
add(inverse(X1),multiply(X2,X1)) = add(inverse(X1),X2),
inference(orient,[status(thm)],[t255]) ).
cnf(t207,plain,
multiply(X1,multiply(X2,inverse(X1))) = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t205,t158]) ).
cnf(t15028,plain,
multiply(X1,multiply(X2,inverse(X1))) = additive_identity,
inference(step,[status(thm)],[t207,t17]) ).
cnf(t229,plain,
multiply(X1,multiply(X2,inverse(X1))) = additive_identity,
inference(orient,[status(thm)],[t15028]) ).
cnf(t252,plain,
additive_identity = multiply(inverse(X1),multiply(X2,X1)),
inference(cp,[status(thm)],[t229,t247]) ).
cnf(t267,plain,
multiply(inverse(X1),multiply(X2,X1)) = additive_identity,
inference(orient,[status(thm)],[t252]) ).
cnf(t597,plain,
add(inverse(multiply(X1,X2)),inverse(X2)) = add(inverse(multiply(X1,X2)),additive_identity),
inference(cp,[status(thm)],[t585,t267]) ).
cnf(t15099,plain,
add(inverse(X2),inverse(multiply(X1,X2))) = add(inverse(multiply(X1,X2)),additive_identity),
inference(step,[status(thm)],[t597,t28]) ).
cnf(t15100,plain,
add(inverse(X2),inverse(multiply(X1,X2))) = inverse(multiply(X1,X2)),
inference(step,[status(thm)],[t15099,t9]) ).
cnf(t3996,plain,
add(inverse(X1),inverse(multiply(X2,X1))) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t15100]) ).
cnf(t15206,plain,
inverse(multiply(inverse(X2),X1)) = add(inverse(X1),multiply(X1,X2)),
inference(step,[status(thm)],[t14175,t3996]) ).
cnf(t15207,plain,
inverse(multiply(inverse(X2),X1)) = add(inverse(X1),X2),
inference(step,[status(thm)],[t15206,t539]) ).
cnf(t14479,plain,
inverse(multiply(inverse(X1),X2)) = add(inverse(X2),X1),
inference(orient,[status(thm)],[t15207]) ).
cnf(t14546,plain,
multiply(inverse(X1),X2) = inverse(add(inverse(X2),X1)),
inference(cp,[status(thm)],[t247,t14479]) ).
cnf(t14740,plain,
inverse(add(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t14546]) ).
cnf(t14797,plain,
multiply(inverse(X1),inverse(X2)) = inverse(add(X2,X1)),
inference(cp,[status(thm)],[t14740,t247]) ).
cnf(t14909,plain,
multiply(inverse(X1),inverse(X2)) = inverse(add(X2,X1)),
inference(orient,[status(thm)],[t14797]) ).
cnf(goal_0,negated_conjecture,
multiply(inverse(a),inverse(b)) != inverse(add(a,b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
inverse(add(b,a)) != inverse(add(a,b)),
inference(rw,[status(thm)],[goal_0,t14909]) ).
cnf(g0_1,plain,
inverse(add(b,a)) != inverse(add(b,a)),
inference(rw,[status(thm)],[g0_0,t28]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO014-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 06:32:32 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.30/1.81 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.30/1.81 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------