%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ROB022-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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 02:39:37 PM UTC 2026
% Result : Unsatisfiable 7.17s 1.57s
% Output : CNFRefutation 7.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 5
% Syntax : Number of clauses : 141 ( 141 unt; 0 nHn; 70 RR)
% Number of literals : 141 ( 140 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 109 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t1]) ).
cnf(t3,axiom,
negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4,plain,
negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t10,plain,
X1 = negate(add(negate(add(X1,X2)),negate(add(negate(X2),X1)))),
inference(cp,[status(thm)],[t4,t8]) ).
cnf(t252,plain,
negate(add(negate(add(X1,X2)),negate(add(negate(X2),X1)))) = X1,
inference(orient,[status(thm)],[t10]) ).
cnf(t275,plain,
negate(add(X1,negate(X2))) = negate(add(negate(add(negate(add(X1,negate(X2))),add(X1,X2))),X1)),
inference(cp,[status(thm)],[t252,t4]) ).
cnf(t9040,plain,
negate(add(X1,negate(X2))) = negate(add(X1,negate(add(negate(add(X1,negate(X2))),add(X1,X2))))),
inference(step,[status(thm)],[t275,t8]) ).
cnf(t2,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t2]) ).
cnf(t12,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t31,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(orient,[status(thm)],[t12]) ).
cnf(t48,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(cp,[status(thm)],[t31,t8]) ).
cnf(t77,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(orient,[status(thm)],[t48]) ).
cnf(t9041,plain,
negate(add(X1,negate(X2))) = negate(add(X1,negate(add(X2,add(X1,negate(add(X1,negate(X2)))))))),
inference(step,[status(thm)],[t9040,t77]) ).
cnf(t4797,plain,
negate(add(X1,negate(add(X2,add(X1,negate(add(X1,negate(X2)))))))) = negate(add(X1,negate(X2))),
inference(orient,[status(thm)],[t9041]) ).
cnf(t9,plain,
X1 = negate(add(negate(add(X2,X1)),negate(add(X1,negate(X2))))),
inference(cp,[status(thm)],[t4,t8]) ).
cnf(t198,plain,
negate(add(negate(add(X1,X2)),negate(add(X2,negate(X1))))) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t225,plain,
X1 = negate(add(negate(add(X2,X1)),negate(add(negate(X2),X1)))),
inference(cp,[status(thm)],[t198,t8]) ).
cnf(t305,plain,
negate(add(negate(add(X1,X2)),negate(add(negate(X1),X2)))) = X2,
inference(orient,[status(thm)],[t225]) ).
cnf(t0,axiom,
add(c,negate(c)) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
add(c,negate(c)) = c,
inference(orient,[status(thm)],[t0]) ).
cnf(t19,plain,
c = negate(add(negate(add(c,c)),negate(c))),
inference(cp,[status(thm)],[t4,t16]) ).
cnf(t8904,plain,
c = negate(add(negate(c),negate(add(c,c)))),
inference(step,[status(thm)],[t19,t8]) ).
cnf(t27,plain,
negate(add(negate(c),negate(add(c,c)))) = c,
inference(orient,[status(thm)],[t8904]) ).
cnf(t29,plain,
negate(c) = negate(add(negate(add(negate(c),add(c,c))),c)),
inference(cp,[status(thm)],[t4,t27]) ).
cnf(t8910,plain,
negate(c) = negate(add(c,negate(add(negate(c),add(c,c))))),
inference(step,[status(thm)],[t29,t8]) ).
cnf(t8911,plain,
negate(c) = negate(add(c,negate(add(c,add(c,negate(c)))))),
inference(step,[status(thm)],[t8910,t77]) ).
cnf(t17,plain,
add(c,add(negate(c),X1)) = add(c,X1),
inference(cp,[status(thm)],[t11,t16]) ).
cnf(t20,plain,
add(c,add(negate(c),X1)) = add(c,X1),
inference(orient,[status(thm)],[t17]) ).
cnf(t21,plain,
add(c,X1) = add(c,add(X1,negate(c))),
inference(cp,[status(thm)],[t20,t8]) ).
cnf(t23,plain,
add(c,add(X1,negate(c))) = add(c,X1),
inference(orient,[status(thm)],[t21]) ).
cnf(t8912,plain,
negate(c) = negate(add(c,negate(add(c,c)))),
inference(step,[status(thm)],[t8911,t23]) ).
cnf(t186,plain,
negate(add(c,negate(add(c,c)))) = negate(c),
inference(orient,[status(thm)],[t8912]) ).
cnf(t188,plain,
c = negate(add(negate(add(c,add(c,c))),negate(c))),
inference(cp,[status(thm)],[t4,t186]) ).
cnf(t8913,plain,
c = negate(add(negate(c),negate(add(c,add(c,c))))),
inference(step,[status(thm)],[t188,t8]) ).
cnf(t190,plain,
negate(add(negate(c),negate(add(c,add(c,c))))) = c,
inference(orient,[status(thm)],[t8913]) ).
cnf(t192,plain,
negate(c) = negate(add(negate(add(negate(c),add(c,add(c,c)))),c)),
inference(cp,[status(thm)],[t4,t190]) ).
cnf(t8914,plain,
negate(c) = negate(add(c,negate(add(negate(c),add(c,add(c,c)))))),
inference(step,[status(thm)],[t192,t8]) ).
cnf(t86,plain,
add(add(negate(c),X1),add(c,X2)) = add(X2,add(c,X1)),
inference(cp,[status(thm)],[t77,t20]) ).
cnf(t8909,plain,
add(negate(c),add(X1,add(c,X2))) = add(X2,add(c,X1)),
inference(step,[status(thm)],[t86,t11]) ).
cnf(t151,plain,
add(negate(c),add(X1,add(c,X2))) = add(X2,add(c,X1)),
inference(orient,[status(thm)],[t8909]) ).
cnf(t8915,plain,
negate(c) = negate(add(c,negate(add(c,add(c,c))))),
inference(step,[status(thm)],[t8914,t151]) ).
cnf(t194,plain,
negate(add(c,negate(add(c,add(c,c))))) = negate(c),
inference(orient,[status(thm)],[t8915]) ).
cnf(t308,plain,
negate(add(c,add(c,c))) = negate(add(negate(c),negate(add(negate(c),negate(add(c,add(c,c))))))),
inference(cp,[status(thm)],[t305,t194]) ).
cnf(t8928,plain,
negate(add(c,add(c,c))) = negate(add(negate(c),c)),
inference(step,[status(thm)],[t308,t190]) ).
cnf(t8929,plain,
negate(add(c,add(c,c))) = negate(add(c,negate(c))),
inference(step,[status(thm)],[t8928,t8]) ).
cnf(t8930,plain,
negate(add(c,add(c,c))) = negate(c),
inference(step,[status(thm)],[t8929,t16]) ).
cnf(t396,plain,
negate(add(c,add(c,c))) = negate(c),
inference(orient,[status(thm)],[t8930]) ).
cnf(t402,plain,
add(c,c) = negate(add(negate(c),negate(add(add(c,c),negate(c))))),
inference(cp,[status(thm)],[t198,t396]) ).
cnf(t8931,plain,
add(c,c) = negate(add(negate(c),negate(add(c,add(c,negate(c)))))),
inference(step,[status(thm)],[t402,t11]) ).
cnf(t8932,plain,
add(c,c) = negate(add(negate(c),negate(add(c,c)))),
inference(step,[status(thm)],[t8931,t23]) ).
cnf(t307,plain,
negate(add(c,c)) = negate(add(negate(c),negate(add(negate(c),negate(add(c,c)))))),
inference(cp,[status(thm)],[t305,t186]) ).
cnf(t8919,plain,
negate(add(c,c)) = negate(add(negate(c),c)),
inference(step,[status(thm)],[t307,t27]) ).
cnf(t8920,plain,
negate(add(c,c)) = negate(add(c,negate(c))),
inference(step,[status(thm)],[t8919,t8]) ).
cnf(t8921,plain,
negate(add(c,c)) = negate(c),
inference(step,[status(thm)],[t8920,t16]) ).
cnf(t362,plain,
negate(add(c,c)) = negate(c),
inference(orient,[status(thm)],[t8921]) ).
cnf(t8933,plain,
add(c,c) = negate(add(negate(c),negate(c))),
inference(step,[status(thm)],[t8932,t362]) ).
cnf(t363,plain,
c = negate(add(negate(c),negate(add(c,negate(c))))),
inference(cp,[status(thm)],[t4,t362]) ).
cnf(t8923,plain,
c = negate(add(negate(c),negate(c))),
inference(step,[status(thm)],[t363,t16]) ).
cnf(t372,plain,
negate(add(negate(c),negate(c))) = c,
inference(orient,[status(thm)],[t8923]) ).
cnf(t8934,plain,
add(c,c) = c,
inference(step,[status(thm)],[t8933,t372]) ).
cnf(t404,plain,
add(c,c) = c,
inference(orient,[status(thm)],[t8934]) ).
cnf(t405,plain,
add(c,add(c,X1)) = add(c,X1),
inference(cp,[status(thm)],[t11,t404]) ).
cnf(t414,plain,
add(c,add(c,X1)) = add(c,X1),
inference(orient,[status(thm)],[t405]) ).
cnf(t429,plain,
add(c,X1) = negate(add(negate(add(c,X1)),negate(add(add(c,X1),negate(c))))),
inference(cp,[status(thm)],[t198,t414]) ).
cnf(t8935,plain,
add(c,X1) = negate(add(negate(add(c,X1)),negate(add(c,add(X1,negate(c)))))),
inference(step,[status(thm)],[t429,t11]) ).
cnf(t8936,plain,
add(c,X1) = negate(add(negate(add(c,X1)),negate(add(c,X1)))),
inference(step,[status(thm)],[t8935,t23]) ).
cnf(t513,plain,
negate(add(negate(add(c,X1)),negate(add(c,X1)))) = add(c,X1),
inference(orient,[status(thm)],[t8936]) ).
cnf(t4884,plain,
add(c,negate(add(X1,add(c,negate(add(c,negate(X1))))))) = negate(add(negate(add(c,negate(X1))),negate(add(c,negate(add(X1,add(c,negate(add(c,negate(X1)))))))))),
inference(cp,[status(thm)],[t513,t4797]) ).
cnf(t9042,plain,
add(c,negate(add(X1,add(c,negate(add(c,negate(X1))))))) = negate(add(negate(add(c,negate(X1))),negate(add(c,negate(X1))))),
inference(step,[status(thm)],[t4884,t4797]) ).
cnf(t9043,plain,
add(c,negate(add(X1,add(c,negate(add(c,negate(X1))))))) = add(c,negate(X1)),
inference(step,[status(thm)],[t9042,t513]) ).
cnf(t4923,plain,
add(c,negate(add(X1,add(c,negate(add(c,negate(X1))))))) = add(c,negate(X1)),
inference(orient,[status(thm)],[t9043]) ).
cnf(t13,plain,
add(X1,add(X2,X3)) = add(add(X2,X1),X3),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t8905,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(step,[status(thm)],[t13,t11]) ).
cnf(t58,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(orient,[status(thm)],[t8905]) ).
cnf(t4925,plain,
add(c,negate(X1)) = add(c,negate(add(c,add(X1,negate(add(c,negate(X1))))))),
inference(cp,[status(thm)],[t4923,t58]) ).
cnf(t5010,plain,
add(c,negate(add(c,add(X1,negate(add(c,negate(X1))))))) = add(c,negate(X1)),
inference(orient,[status(thm)],[t4925]) ).
cnf(t378,plain,
X1 = negate(add(negate(add(add(negate(c),negate(c)),X1)),negate(add(c,X1)))),
inference(cp,[status(thm)],[t305,t372]) ).
cnf(t9003,plain,
X1 = negate(add(negate(add(c,X1)),negate(add(add(negate(c),negate(c)),X1)))),
inference(step,[status(thm)],[t378,t8]) ).
cnf(t9004,plain,
X1 = negate(add(negate(add(c,X1)),negate(add(negate(c),add(negate(c),X1))))),
inference(step,[status(thm)],[t9003,t11]) ).
cnf(t2789,plain,
negate(add(negate(add(c,X1)),negate(add(negate(c),add(negate(c),X1))))) = X1,
inference(orient,[status(thm)],[t9004]) ).
cnf(t2802,plain,
negate(c) = negate(add(negate(c),negate(add(negate(c),add(negate(c),negate(c)))))),
inference(cp,[status(thm)],[t2789,t16]) ).
cnf(t2862,plain,
negate(add(negate(c),negate(add(negate(c),add(negate(c),negate(c)))))) = negate(c),
inference(orient,[status(thm)],[t2802]) ).
cnf(t5030,plain,
add(c,negate(add(negate(c),negate(add(negate(c),add(negate(c),negate(c))))))) = add(c,negate(add(c,add(add(negate(c),negate(add(negate(c),add(negate(c),negate(c))))),negate(add(c,negate(c))))))),
inference(cp,[status(thm)],[t5010,t2862]) ).
cnf(t9057,plain,
add(c,negate(c)) = add(c,negate(add(c,add(add(negate(c),negate(add(negate(c),add(negate(c),negate(c))))),negate(add(c,negate(c))))))),
inference(step,[status(thm)],[t5030,t2862]) ).
cnf(t9058,plain,
c = add(c,negate(add(c,add(add(negate(c),negate(add(negate(c),add(negate(c),negate(c))))),negate(add(c,negate(c))))))),
inference(step,[status(thm)],[t9057,t16]) ).
cnf(t9059,plain,
c = add(c,negate(add(c,add(negate(c),add(negate(add(negate(c),add(negate(c),negate(c)))),negate(add(c,negate(c)))))))),
inference(step,[status(thm)],[t9058,t11]) ).
cnf(t9060,plain,
c = add(c,negate(add(c,add(negate(add(negate(c),add(negate(c),negate(c)))),negate(add(c,negate(c))))))),
inference(step,[status(thm)],[t9059,t20]) ).
cnf(t9061,plain,
c = add(c,negate(add(c,add(negate(add(c,negate(c))),negate(add(negate(c),add(negate(c),negate(c)))))))),
inference(step,[status(thm)],[t9060,t8]) ).
cnf(t9062,plain,
c = add(c,negate(add(c,add(negate(c),negate(add(negate(c),add(negate(c),negate(c)))))))),
inference(step,[status(thm)],[t9061,t16]) ).
cnf(t9063,plain,
c = add(c,negate(add(c,negate(add(negate(c),add(negate(c),negate(c))))))),
inference(step,[status(thm)],[t9062,t20]) ).
cnf(t5478,plain,
add(c,negate(add(c,negate(add(negate(c),add(negate(c),negate(c))))))) = c,
inference(orient,[status(thm)],[t9063]) ).
cnf(t5507,plain,
add(c,negate(add(negate(c),add(negate(c),negate(c))))) = add(c,negate(add(add(negate(c),add(negate(c),negate(c))),c))),
inference(cp,[status(thm)],[t4923,t5478]) ).
cnf(t9064,plain,
add(c,negate(add(negate(c),add(negate(c),negate(c))))) = add(c,negate(add(negate(c),add(add(negate(c),negate(c)),c)))),
inference(step,[status(thm)],[t5507,t11]) ).
cnf(t9065,plain,
add(c,negate(add(negate(c),add(negate(c),negate(c))))) = add(c,negate(add(c,add(add(negate(c),negate(c)),negate(c))))),
inference(step,[status(thm)],[t9064,t77]) ).
cnf(t9066,plain,
add(c,negate(add(negate(c),add(negate(c),negate(c))))) = add(c,negate(add(c,add(negate(c),negate(c))))),
inference(step,[status(thm)],[t9065,t23]) ).
cnf(t9067,plain,
add(c,negate(add(negate(c),add(negate(c),negate(c))))) = add(c,negate(add(c,negate(c)))),
inference(step,[status(thm)],[t9066,t20]) ).
cnf(t9068,plain,
add(c,negate(add(negate(c),add(negate(c),negate(c))))) = add(c,negate(c)),
inference(step,[status(thm)],[t9067,t16]) ).
cnf(t9069,plain,
add(c,negate(add(negate(c),add(negate(c),negate(c))))) = c,
inference(step,[status(thm)],[t9068,t16]) ).
cnf(t5522,plain,
add(c,negate(add(negate(c),add(negate(c),negate(c))))) = c,
inference(orient,[status(thm)],[t9069]) ).
cnf(t5537,plain,
negate(add(negate(c),add(negate(c),negate(c)))) = negate(add(negate(c),negate(add(negate(c),negate(add(negate(c),add(negate(c),negate(c)))))))),
inference(cp,[status(thm)],[t305,t5522]) ).
cnf(t9070,plain,
negate(add(negate(c),add(negate(c),negate(c)))) = negate(add(negate(c),negate(c))),
inference(step,[status(thm)],[t5537,t2862]) ).
cnf(t9071,plain,
negate(add(negate(c),add(negate(c),negate(c)))) = c,
inference(step,[status(thm)],[t9070,t372]) ).
cnf(t5561,plain,
negate(add(negate(c),add(negate(c),negate(c)))) = c,
inference(orient,[status(thm)],[t9071]) ).
cnf(t5565,plain,
add(negate(c),negate(c)) = negate(add(negate(add(c,add(negate(c),negate(c)))),c)),
inference(cp,[status(thm)],[t305,t5561]) ).
cnf(t9073,plain,
add(negate(c),negate(c)) = negate(add(c,negate(add(c,add(negate(c),negate(c)))))),
inference(step,[status(thm)],[t5565,t8]) ).
cnf(t9074,plain,
add(negate(c),negate(c)) = negate(add(c,negate(add(c,negate(c))))),
inference(step,[status(thm)],[t9073,t20]) ).
cnf(t9075,plain,
add(negate(c),negate(c)) = negate(add(c,negate(c))),
inference(step,[status(thm)],[t9074,t16]) ).
cnf(t9076,plain,
add(negate(c),negate(c)) = negate(c),
inference(step,[status(thm)],[t9075,t16]) ).
cnf(t5591,plain,
add(negate(c),negate(c)) = negate(c),
inference(orient,[status(thm)],[t9076]) ).
cnf(t5592,plain,
add(negate(c),add(negate(c),X1)) = add(negate(c),X1),
inference(cp,[status(thm)],[t11,t5591]) ).
cnf(t5648,plain,
add(negate(c),add(negate(c),X1)) = add(negate(c),X1),
inference(orient,[status(thm)],[t5592]) ).
cnf(t5670,plain,
add(negate(c),X1) = negate(add(negate(add(c,add(negate(c),X1))),negate(add(negate(c),X1)))),
inference(cp,[status(thm)],[t305,t5648]) ).
cnf(t9131,plain,
add(negate(c),X1) = negate(add(negate(add(negate(c),X1)),negate(add(c,add(negate(c),X1))))),
inference(step,[status(thm)],[t5670,t8]) ).
cnf(t9132,plain,
add(negate(c),X1) = negate(add(negate(add(negate(c),X1)),negate(add(c,X1)))),
inference(step,[status(thm)],[t9131,t20]) ).
cnf(t9133,plain,
add(negate(c),X1) = negate(add(negate(add(c,X1)),negate(add(negate(c),X1)))),
inference(step,[status(thm)],[t9132,t8]) ).
cnf(t9134,plain,
add(negate(c),X1) = X1,
inference(step,[status(thm)],[t9133,t305]) ).
cnf(t5688,plain,
add(negate(c),X1) = X1,
inference(orient,[status(thm)],[t9134]) ).
cnf(t5725,plain,
negate(add(negate(c),negate(X1))) = negate(negate(add(X1,add(negate(c),negate(add(negate(c),negate(X1))))))),
inference(cp,[status(thm)],[t4797,t5688]) ).
cnf(t9146,plain,
negate(negate(X1)) = negate(negate(add(X1,add(negate(c),negate(add(negate(c),negate(X1))))))),
inference(step,[status(thm)],[t5725,t5688]) ).
cnf(t9147,plain,
negate(negate(X1)) = negate(negate(add(X1,negate(add(negate(c),negate(X1)))))),
inference(step,[status(thm)],[t9146,t5688]) ).
cnf(t9148,plain,
negate(negate(X1)) = negate(negate(add(X1,negate(negate(X1))))),
inference(step,[status(thm)],[t9147,t5688]) ).
cnf(t5696,plain,
negate(c) = negate(add(negate(X1),negate(add(negate(c),negate(X1))))),
inference(cp,[status(thm)],[t4,t5688]) ).
cnf(t9139,plain,
negate(c) = negate(add(negate(X1),negate(negate(X1)))),
inference(step,[status(thm)],[t5696,t5688]) ).
cnf(t5756,plain,
negate(add(negate(X1),negate(negate(X1)))) = negate(c),
inference(orient,[status(thm)],[t9139]) ).
cnf(t5761,plain,
negate(c) = negate(add(X1,negate(negate(add(negate(add(X1,X2)),negate(add(negate(X2),X1))))))),
inference(cp,[status(thm)],[t5756,t252]) ).
cnf(t9140,plain,
negate(c) = negate(add(X1,negate(X1))),
inference(step,[status(thm)],[t5761,t252]) ).
cnf(t5802,plain,
negate(add(X1,negate(X1))) = negate(c),
inference(orient,[status(thm)],[t9140]) ).
cnf(t5822,plain,
X1 = negate(add(negate(c),negate(add(X1,negate(negate(X1)))))),
inference(cp,[status(thm)],[t4,t5802]) ).
cnf(t9142,plain,
X1 = negate(negate(add(X1,negate(negate(X1))))),
inference(step,[status(thm)],[t5822,t5688]) ).
cnf(t5873,plain,
negate(negate(add(X1,negate(negate(X1))))) = X1,
inference(orient,[status(thm)],[t9142]) ).
cnf(t9149,plain,
negate(negate(X1)) = X1,
inference(step,[status(thm)],[t9148,t5873]) ).
cnf(t5971,plain,
negate(negate(X1)) = X1,
inference(orient,[status(thm)],[t9149]) ).
cnf(t5987,plain,
add(negate(add(X1,X2)),negate(add(negate(X2),X1))) = negate(X1),
inference(cp,[status(thm)],[t5971,t252]) ).
cnf(t8777,plain,
add(negate(add(X1,X2)),negate(add(negate(X2),X1))) = negate(X1),
inference(orient,[status(thm)],[t5987]) ).
cnf(goal_0,negated_conjecture,
add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
add(negate(add(negate(b),a)),negate(add(negate(a),negate(b)))) != b,
inference(rw,[status(thm)],[goal_0,t8]) ).
cnf(g0_1,plain,
negate(negate(b)) != b,
inference(rw,[status(thm)],[g0_0,t8777]) ).
cnf(g0_2,plain,
b != b,
inference(rw,[status(thm)],[g0_1,t5971]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ROB022-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n009.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 : Thu Sep 24 08:28:14 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.17/1.57 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.17/1.57 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------