%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ROB005-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 : n003.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:34 PM UTC 2026
% Result : Unsatisfiable 12.99s 2.16s
% Output : CNFRefutation 12.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 5
% Syntax : Number of clauses : 158 ( 158 unt; 0 nHn; 62 RR)
% Number of literals : 158 ( 157 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 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 : 174 ( 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(t9,plain,
X1 = negate(add(negate(add(X2,X1)),negate(add(X1,negate(X2))))),
inference(cp,[status(thm)],[t4,t8]) ).
cnf(t131,plain,
negate(add(negate(add(X1,X2)),negate(add(X2,negate(X1))))) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t146,plain,
X1 = negate(add(negate(add(X2,X1)),negate(add(negate(X2),X1)))),
inference(cp,[status(thm)],[t131,t8]) ).
cnf(t189,plain,
negate(add(negate(add(X1,X2)),negate(add(negate(X1),X2)))) = X2,
inference(orient,[status(thm)],[t146]) ).
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(t13,plain,
add(X1,add(X2,X3)) = add(add(X2,X1),X3),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t28406,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(step,[status(thm)],[t13,t11]) ).
cnf(t80,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(orient,[status(thm)],[t28406]) ).
cnf(t201,plain,
add(X1,X2) = negate(add(negate(add(X1,add(X3,X2))),negate(add(negate(X3),add(X1,X2))))),
inference(cp,[status(thm)],[t189,t80]) ).
cnf(t4314,plain,
negate(add(negate(add(X1,add(X2,X3))),negate(add(negate(X2),add(X1,X3))))) = add(X1,X3),
inference(orient,[status(thm)],[t201]) ).
cnf(t140,plain,
add(X1,X2) = negate(add(negate(add(X1,add(X3,X2))),negate(add(add(X1,X2),negate(X3))))),
inference(cp,[status(thm)],[t131,t80]) ).
cnf(t28450,plain,
add(X1,X2) = negate(add(negate(add(X1,add(X3,X2))),negate(add(X1,add(X2,negate(X3)))))),
inference(step,[status(thm)],[t140,t11]) ).
cnf(t3321,plain,
negate(add(negate(add(X1,add(X2,X3))),negate(add(X1,add(X3,negate(X2)))))) = add(X1,X3),
inference(orient,[status(thm)],[t28450]) ).
cnf(t3352,plain,
add(X1,X2) = negate(add(negate(add(X1,add(X3,X2))),negate(add(X1,add(negate(X3),X2))))),
inference(cp,[status(thm)],[t3321,t8]) ).
cnf(t5234,plain,
negate(add(negate(add(X1,add(X2,X3))),negate(add(X1,add(negate(X2),X3))))) = add(X1,X3),
inference(orient,[status(thm)],[t3352]) ).
cnf(t0,axiom,
add(c,c) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
add(c,c) = c,
inference(orient,[status(thm)],[t0]) ).
cnf(t18,plain,
c = negate(add(negate(c),negate(add(c,negate(c))))),
inference(cp,[status(thm)],[t4,t16]) ).
cnf(t39,plain,
negate(add(negate(c),negate(add(c,negate(c))))) = c,
inference(orient,[status(thm)],[t18]) ).
cnf(t42,plain,
X1 = negate(add(negate(add(X1,add(negate(c),negate(add(c,negate(c)))))),negate(add(X1,c)))),
inference(cp,[status(thm)],[t4,t39]) ).
cnf(t28468,plain,
X1 = negate(add(negate(add(X1,c)),negate(add(X1,add(negate(c),negate(add(c,negate(c)))))))),
inference(step,[status(thm)],[t42,t8]) ).
cnf(t9239,plain,
negate(add(negate(add(X1,c)),negate(add(X1,add(negate(c),negate(add(c,negate(c)))))))) = X1,
inference(orient,[status(thm)],[t28468]) ).
cnf(t9241,plain,
c = negate(add(negate(c),negate(add(c,add(negate(c),negate(add(c,negate(c)))))))),
inference(cp,[status(thm)],[t9239,t16]) ).
cnf(t9342,plain,
negate(add(negate(c),negate(add(c,add(negate(c),negate(add(c,negate(c)))))))) = c,
inference(orient,[status(thm)],[t9241]) ).
cnf(t9344,plain,
negate(c) = negate(add(negate(add(negate(c),add(c,add(negate(c),negate(add(c,negate(c))))))),c)),
inference(cp,[status(thm)],[t4,t9342]) ).
cnf(t28507,plain,
negate(c) = negate(add(c,negate(add(negate(c),add(c,add(negate(c),negate(add(c,negate(c))))))))),
inference(step,[status(thm)],[t9344,t8]) ).
cnf(t28508,plain,
negate(c) = negate(add(c,negate(add(c,add(negate(c),add(negate(c),negate(add(c,negate(c))))))))),
inference(step,[status(thm)],[t28507,t80]) ).
cnf(t14868,plain,
negate(add(c,negate(add(c,add(negate(c),add(negate(c),negate(add(c,negate(c))))))))) = negate(c),
inference(orient,[status(thm)],[t28508]) ).
cnf(t12,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t43,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(orient,[status(thm)],[t12]) ).
cnf(t79,plain,
X1 = negate(add(negate(add(X2,add(X3,X1))),negate(add(X1,negate(add(X2,X3)))))),
inference(cp,[status(thm)],[t4,t43]) ).
cnf(t1554,plain,
negate(add(negate(add(X1,add(X2,X3))),negate(add(X3,negate(add(X1,X2)))))) = X3,
inference(orient,[status(thm)],[t79]) ).
cnf(t17,plain,
add(c,add(c,X1)) = add(c,X1),
inference(cp,[status(thm)],[t11,t16]) ).
cnf(t19,plain,
add(c,add(c,X1)) = add(c,X1),
inference(orient,[status(thm)],[t17]) ).
cnf(t21,plain,
c = negate(add(negate(add(c,X1)),negate(add(c,negate(add(c,X1)))))),
inference(cp,[status(thm)],[t4,t19]) ).
cnf(t330,plain,
negate(add(negate(add(c,X1)),negate(add(c,negate(add(c,X1)))))) = c,
inference(orient,[status(thm)],[t21]) ).
cnf(t347,plain,
negate(add(c,negate(add(c,X1)))) = negate(add(negate(add(add(c,X1),negate(add(c,negate(add(c,X1)))))),c)),
inference(cp,[status(thm)],[t189,t330]) ).
cnf(t28511,plain,
negate(add(c,negate(add(c,X1)))) = negate(add(c,negate(add(add(c,X1),negate(add(c,negate(add(c,X1)))))))),
inference(step,[status(thm)],[t347,t8]) ).
cnf(t28512,plain,
negate(add(c,negate(add(c,X1)))) = negate(add(c,negate(add(c,add(X1,negate(add(c,negate(add(c,X1))))))))),
inference(step,[status(thm)],[t28511,t11]) ).
cnf(t15094,plain,
negate(add(c,negate(add(c,add(X1,negate(add(c,negate(add(c,X1))))))))) = negate(add(c,negate(add(c,X1)))),
inference(orient,[status(thm)],[t28512]) ).
cnf(t41,plain,
negate(c) = negate(add(negate(add(negate(c),add(c,negate(c)))),c)),
inference(cp,[status(thm)],[t4,t39]) ).
cnf(t28407,plain,
negate(c) = negate(add(c,negate(add(negate(c),add(c,negate(c)))))),
inference(step,[status(thm)],[t41,t8]) ).
cnf(t28408,plain,
negate(c) = negate(add(c,negate(add(c,add(negate(c),negate(c)))))),
inference(step,[status(thm)],[t28407,t80]) ).
cnf(t228,plain,
negate(add(c,negate(add(c,add(negate(c),negate(c)))))) = negate(c),
inference(orient,[status(thm)],[t28408]) ).
cnf(t230,plain,
c = negate(add(negate(add(c,add(c,add(negate(c),negate(c))))),negate(c))),
inference(cp,[status(thm)],[t4,t228]) ).
cnf(t28414,plain,
c = negate(add(negate(c),negate(add(c,add(c,add(negate(c),negate(c))))))),
inference(step,[status(thm)],[t230,t8]) ).
cnf(t28415,plain,
c = negate(add(negate(c),negate(add(c,add(negate(c),negate(c)))))),
inference(step,[status(thm)],[t28414,t19]) ).
cnf(t296,plain,
negate(add(negate(c),negate(add(c,add(negate(c),negate(c)))))) = c,
inference(orient,[status(thm)],[t28415]) ).
cnf(t301,plain,
negate(add(c,add(negate(c),negate(c)))) = negate(add(negate(add(c,negate(add(c,add(negate(c),negate(c)))))),c)),
inference(cp,[status(thm)],[t189,t296]) ).
cnf(t28416,plain,
negate(add(c,add(negate(c),negate(c)))) = negate(add(c,negate(add(c,negate(add(c,add(negate(c),negate(c)))))))),
inference(step,[status(thm)],[t301,t8]) ).
cnf(t28417,plain,
negate(add(c,add(negate(c),negate(c)))) = negate(add(c,negate(c))),
inference(step,[status(thm)],[t28416,t228]) ).
cnf(t309,plain,
negate(add(c,add(negate(c),negate(c)))) = negate(add(c,negate(c))),
inference(orient,[status(thm)],[t28417]) ).
cnf(t15112,plain,
negate(add(c,negate(add(c,add(negate(c),negate(c)))))) = negate(add(c,negate(add(c,add(add(negate(c),negate(c)),negate(add(c,negate(add(c,negate(c)))))))))),
inference(cp,[status(thm)],[t15094,t309]) ).
cnf(t28513,plain,
negate(add(c,negate(add(c,negate(c))))) = negate(add(c,negate(add(c,add(add(negate(c),negate(c)),negate(add(c,negate(add(c,negate(c)))))))))),
inference(step,[status(thm)],[t15112,t309]) ).
cnf(t28418,plain,
negate(add(c,negate(add(c,negate(c))))) = negate(c),
inference(step,[status(thm)],[t228,t309]) ).
cnf(t318,plain,
negate(add(c,negate(add(c,negate(c))))) = negate(c),
inference(rw,[status(thm)],[t28418]) ).
cnf(t319,plain,
negate(add(c,negate(add(c,negate(c))))) = negate(c),
inference(orient,[status(thm)],[t318]) ).
cnf(t28514,plain,
negate(c) = negate(add(c,negate(add(c,add(add(negate(c),negate(c)),negate(add(c,negate(add(c,negate(c)))))))))),
inference(step,[status(thm)],[t28513,t319]) ).
cnf(t28515,plain,
negate(c) = negate(add(c,negate(add(c,add(negate(c),add(negate(c),negate(add(c,negate(add(c,negate(c))))))))))),
inference(step,[status(thm)],[t28514,t11]) ).
cnf(t28516,plain,
negate(c) = negate(add(c,negate(add(c,add(negate(c),add(negate(c),negate(c))))))),
inference(step,[status(thm)],[t28515,t319]) ).
cnf(t15270,plain,
negate(add(c,negate(add(c,add(negate(c),add(negate(c),negate(c))))))) = negate(c),
inference(orient,[status(thm)],[t28516]) ).
cnf(t15279,plain,
negate(add(c,add(negate(c),add(negate(c),negate(c))))) = negate(add(negate(c),negate(add(negate(c),negate(add(c,add(negate(c),add(negate(c),negate(c))))))))),
inference(cp,[status(thm)],[t189,t15270]) ).
cnf(t10,plain,
X1 = negate(add(negate(add(X1,X2)),negate(add(negate(X2),X1)))),
inference(cp,[status(thm)],[t4,t8]) ).
cnf(t155,plain,
negate(add(negate(add(X1,X2)),negate(add(negate(X2),X1)))) = X1,
inference(orient,[status(thm)],[t10]) ).
cnf(t171,plain,
negate(add(X1,negate(X2))) = negate(add(negate(add(negate(add(X1,negate(X2))),add(X2,X1))),X1)),
inference(cp,[status(thm)],[t155,t131]) ).
cnf(t28440,plain,
negate(add(X1,negate(X2))) = negate(add(X1,negate(add(negate(add(X1,negate(X2))),add(X2,X1))))),
inference(step,[status(thm)],[t171,t8]) ).
cnf(t66,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(cp,[status(thm)],[t43,t8]) ).
cnf(t104,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(orient,[status(thm)],[t66]) ).
cnf(t28441,plain,
negate(add(X1,negate(X2))) = negate(add(X1,negate(add(X1,add(X2,negate(add(X1,negate(X2)))))))),
inference(step,[status(thm)],[t28440,t104]) ).
cnf(t1146,plain,
negate(add(X1,negate(add(X1,add(X2,negate(add(X1,negate(X2)))))))) = negate(add(X1,negate(X2))),
inference(orient,[status(thm)],[t28441]) ).
cnf(t1215,plain,
c = negate(add(negate(add(c,add(X1,negate(add(c,negate(X1)))))),negate(add(c,negate(X1))))),
inference(cp,[status(thm)],[t330,t1146]) ).
cnf(t28487,plain,
c = negate(add(negate(add(c,negate(X1))),negate(add(c,add(X1,negate(add(c,negate(X1)))))))),
inference(step,[status(thm)],[t1215,t8]) ).
cnf(t12188,plain,
negate(add(negate(add(c,negate(X1))),negate(add(c,add(X1,negate(add(c,negate(X1)))))))) = c,
inference(orient,[status(thm)],[t28487]) ).
cnf(t12295,plain,
c = negate(add(negate(add(c,negate(add(c,negate(c))))),negate(add(c,add(add(c,add(negate(c),negate(c))),negate(add(c,negate(add(c,add(negate(c),negate(c))))))))))),
inference(cp,[status(thm)],[t12188,t309]) ).
cnf(t28488,plain,
c = negate(add(negate(c),negate(add(c,add(add(c,add(negate(c),negate(c))),negate(add(c,negate(add(c,add(negate(c),negate(c))))))))))),
inference(step,[status(thm)],[t12295,t319]) ).
cnf(t28489,plain,
c = negate(add(negate(c),negate(add(c,add(c,add(add(negate(c),negate(c)),negate(add(c,negate(add(c,add(negate(c),negate(c)))))))))))),
inference(step,[status(thm)],[t28488,t11]) ).
cnf(t28490,plain,
c = negate(add(negate(c),negate(add(c,add(add(negate(c),negate(c)),negate(add(c,negate(add(c,add(negate(c),negate(c))))))))))),
inference(step,[status(thm)],[t28489,t19]) ).
cnf(t28491,plain,
c = negate(add(negate(c),negate(add(c,add(negate(c),add(negate(c),negate(add(c,negate(add(c,add(negate(c),negate(c)))))))))))),
inference(step,[status(thm)],[t28490,t11]) ).
cnf(t28492,plain,
c = negate(add(negate(c),negate(add(c,add(negate(c),add(negate(c),negate(add(c,negate(add(c,negate(c))))))))))),
inference(step,[status(thm)],[t28491,t309]) ).
cnf(t28493,plain,
c = negate(add(negate(c),negate(add(c,add(negate(c),add(negate(c),negate(c))))))),
inference(step,[status(thm)],[t28492,t319]) ).
cnf(t12527,plain,
negate(add(negate(c),negate(add(c,add(negate(c),add(negate(c),negate(c))))))) = c,
inference(orient,[status(thm)],[t28493]) ).
cnf(t28517,plain,
negate(add(c,add(negate(c),add(negate(c),negate(c))))) = negate(add(negate(c),c)),
inference(step,[status(thm)],[t15279,t12527]) ).
cnf(t28518,plain,
negate(add(c,add(negate(c),add(negate(c),negate(c))))) = negate(add(c,negate(c))),
inference(step,[status(thm)],[t28517,t8]) ).
cnf(t15382,plain,
negate(add(c,add(negate(c),add(negate(c),negate(c))))) = negate(add(c,negate(c))),
inference(orient,[status(thm)],[t28518]) ).
cnf(t15448,plain,
add(negate(c),negate(c)) = negate(add(negate(add(c,negate(c))),negate(add(add(negate(c),negate(c)),negate(add(c,negate(c))))))),
inference(cp,[status(thm)],[t1554,t15382]) ).
cnf(t28519,plain,
add(negate(c),negate(c)) = negate(add(negate(add(c,negate(c))),negate(add(negate(c),add(negate(c),negate(add(c,negate(c)))))))),
inference(step,[status(thm)],[t15448,t11]) ).
cnf(t167,plain,
X1 = negate(add(negate(add(X2,add(X1,X3))),negate(add(negate(add(X2,X3)),X1)))),
inference(cp,[status(thm)],[t155,t80]) ).
cnf(t2086,plain,
negate(add(negate(add(X1,add(X2,X3))),negate(add(negate(add(X1,X3)),X2)))) = X2,
inference(orient,[status(thm)],[t167]) ).
cnf(t2172,plain,
X1 = negate(add(negate(add(negate(c),add(X1,negate(add(c,negate(c)))))),negate(add(c,X1)))),
inference(cp,[status(thm)],[t2086,t39]) ).
cnf(t28503,plain,
X1 = negate(add(negate(add(c,X1)),negate(add(negate(c),add(X1,negate(add(c,negate(c)))))))),
inference(step,[status(thm)],[t2172,t8]) ).
cnf(t13546,plain,
negate(add(negate(add(c,X1)),negate(add(negate(c),add(X1,negate(add(c,negate(c)))))))) = X1,
inference(orient,[status(thm)],[t28503]) ).
cnf(t28520,plain,
add(negate(c),negate(c)) = negate(c),
inference(step,[status(thm)],[t28519,t13546]) ).
cnf(t15519,plain,
add(negate(c),negate(c)) = negate(c),
inference(orient,[status(thm)],[t28520]) ).
cnf(t15520,plain,
add(negate(c),add(negate(c),X1)) = add(negate(c),X1),
inference(cp,[status(thm)],[t11,t15519]) ).
cnf(t15625,plain,
add(negate(c),add(negate(c),X1)) = add(negate(c),X1),
inference(orient,[status(thm)],[t15520]) ).
cnf(t28521,plain,
negate(add(c,negate(add(c,add(negate(c),negate(add(c,negate(c)))))))) = negate(c),
inference(step,[status(thm)],[t14868,t15625]) ).
cnf(t15771,plain,
negate(add(c,negate(add(c,add(negate(c),negate(add(c,negate(c)))))))) = negate(c),
inference(rw,[status(thm)],[t28521]) ).
cnf(t16814,plain,
negate(add(c,negate(add(c,add(negate(c),negate(add(c,negate(c)))))))) = negate(c),
inference(orient,[status(thm)],[t15771]) ).
cnf(t16823,plain,
negate(add(c,add(negate(c),negate(add(c,negate(c)))))) = negate(add(negate(c),negate(add(negate(c),negate(add(c,add(negate(c),negate(add(c,negate(c)))))))))),
inference(cp,[status(thm)],[t189,t16814]) ).
cnf(t28530,plain,
negate(add(c,add(negate(c),negate(add(c,negate(c)))))) = negate(add(negate(c),c)),
inference(step,[status(thm)],[t16823,t9342]) ).
cnf(t28531,plain,
negate(add(c,add(negate(c),negate(add(c,negate(c)))))) = negate(add(c,negate(c))),
inference(step,[status(thm)],[t28530,t8]) ).
cnf(t16929,plain,
negate(add(c,add(negate(c),negate(add(c,negate(c)))))) = negate(add(c,negate(c))),
inference(orient,[status(thm)],[t28531]) ).
cnf(t16949,plain,
add(c,negate(add(c,negate(c)))) = negate(add(negate(add(c,negate(c))),negate(add(c,add(negate(negate(c)),negate(add(c,negate(c)))))))),
inference(cp,[status(thm)],[t5234,t16929]) ).
cnf(t143,plain,
negate(add(X1,X2)) = negate(add(negate(add(add(X1,negate(X2)),negate(add(X1,X2)))),X1)),
inference(cp,[status(thm)],[t131,t4]) ).
cnf(t28424,plain,
negate(add(X1,X2)) = negate(add(X1,negate(add(add(X1,negate(X2)),negate(add(X1,X2)))))),
inference(step,[status(thm)],[t143,t8]) ).
cnf(t28425,plain,
negate(add(X1,X2)) = negate(add(X1,negate(add(X1,add(negate(X2),negate(add(X1,X2))))))),
inference(step,[status(thm)],[t28424,t11]) ).
cnf(t689,plain,
negate(add(X1,negate(add(X1,add(negate(X2),negate(add(X1,X2))))))) = negate(add(X1,X2)),
inference(orient,[status(thm)],[t28425]) ).
cnf(t759,plain,
c = negate(add(negate(add(c,add(negate(X1),negate(add(c,X1))))),negate(add(c,X1)))),
inference(cp,[status(thm)],[t330,t689]) ).
cnf(t28457,plain,
c = negate(add(negate(add(c,X1)),negate(add(c,add(negate(X1),negate(add(c,X1))))))),
inference(step,[status(thm)],[t759,t8]) ).
cnf(t5782,plain,
negate(add(negate(add(c,X1)),negate(add(c,add(negate(X1),negate(add(c,X1))))))) = c,
inference(orient,[status(thm)],[t28457]) ).
cnf(t28532,plain,
add(c,negate(add(c,negate(c)))) = c,
inference(step,[status(thm)],[t16949,t5782]) ).
cnf(t17065,plain,
add(c,negate(add(c,negate(c)))) = c,
inference(orient,[status(thm)],[t28532]) ).
cnf(t17074,plain,
add(X1,negate(add(c,negate(c)))) = negate(add(negate(add(X1,c)),negate(add(negate(c),add(X1,negate(add(c,negate(c)))))))),
inference(cp,[status(thm)],[t4314,t17065]) ).
cnf(t58,plain,
X1 = negate(add(negate(add(X2,add(X1,X3))),negate(add(X1,negate(add(X3,X2)))))),
inference(cp,[status(thm)],[t4,t43]) ).
cnf(t1426,plain,
negate(add(negate(add(X1,add(X2,X3))),negate(add(X2,negate(add(X3,X1)))))) = X2,
inference(orient,[status(thm)],[t58]) ).
cnf(t1508,plain,
X1 = negate(add(negate(add(negate(add(c,negate(c))),add(X1,negate(c)))),negate(add(X1,c)))),
inference(cp,[status(thm)],[t1426,t39]) ).
cnf(t28500,plain,
X1 = negate(add(negate(add(X1,c)),negate(add(negate(add(c,negate(c))),add(X1,negate(c)))))),
inference(step,[status(thm)],[t1508,t8]) ).
cnf(t28501,plain,
X1 = negate(add(negate(add(X1,c)),negate(add(negate(c),add(X1,negate(add(c,negate(c)))))))),
inference(step,[status(thm)],[t28500,t104]) ).
cnf(t13199,plain,
negate(add(negate(add(X1,c)),negate(add(negate(c),add(X1,negate(add(c,negate(c)))))))) = X1,
inference(orient,[status(thm)],[t28501]) ).
cnf(t28548,plain,
add(X1,negate(add(c,negate(c)))) = X1,
inference(step,[status(thm)],[t17074,t13199]) ).
cnf(t17901,plain,
add(X1,negate(add(c,negate(c)))) = X1,
inference(orient,[status(thm)],[t28548]) ).
cnf(t7,plain,
X1 = negate(add(negate(add(X1,add(negate(add(X2,X3)),negate(add(X2,negate(X3)))))),negate(add(X1,X2)))),
inference(cp,[status(thm)],[t4,t4]) ).
cnf(t28478,plain,
X1 = negate(add(negate(add(X1,X2)),negate(add(X1,add(negate(add(X2,X3)),negate(add(X2,negate(X3)))))))),
inference(step,[status(thm)],[t7,t8]) ).
cnf(t10156,plain,
negate(add(negate(add(X1,X2)),negate(add(X1,add(negate(add(X2,X3)),negate(add(X2,negate(X3)))))))) = X1,
inference(orient,[status(thm)],[t28478]) ).
cnf(t203,plain,
add(X1,X2) = negate(add(negate(add(X2,add(X3,X1))),negate(add(negate(X3),add(X1,X2))))),
inference(cp,[status(thm)],[t189,t43]) ).
cnf(t4458,plain,
negate(add(negate(add(X1,add(X2,X3))),negate(add(negate(X2),add(X3,X1))))) = add(X3,X1),
inference(orient,[status(thm)],[t203]) ).
cnf(t17072,plain,
add(negate(add(c,negate(c))),X1) = negate(add(negate(add(X1,c)),negate(add(negate(c),add(negate(add(c,negate(c))),X1))))),
inference(cp,[status(thm)],[t4458,t17065]) ).
cnf(t148,plain,
X1 = negate(add(negate(add(add(negate(c),negate(add(c,negate(c)))),X1)),negate(add(X1,c)))),
inference(cp,[status(thm)],[t131,t39]) ).
cnf(t28469,plain,
X1 = negate(add(negate(add(X1,c)),negate(add(add(negate(c),negate(add(c,negate(c)))),X1)))),
inference(step,[status(thm)],[t148,t8]) ).
cnf(t28470,plain,
X1 = negate(add(negate(add(X1,c)),negate(add(negate(c),add(negate(add(c,negate(c))),X1))))),
inference(step,[status(thm)],[t28469,t11]) ).
cnf(t9428,plain,
negate(add(negate(add(X1,c)),negate(add(negate(c),add(negate(add(c,negate(c))),X1))))) = X1,
inference(orient,[status(thm)],[t28470]) ).
cnf(t28535,plain,
add(negate(add(c,negate(c))),X1) = X1,
inference(step,[status(thm)],[t17072,t9428]) ).
cnf(t17186,plain,
add(negate(add(c,negate(c))),X1) = X1,
inference(orient,[status(thm)],[t28535]) ).
cnf(t17344,plain,
negate(add(c,negate(c))) = negate(add(negate(X1),negate(add(negate(add(c,negate(c))),add(negate(add(X1,X2)),negate(add(X1,negate(X2)))))))),
inference(cp,[status(thm)],[t10156,t17186]) ).
cnf(t28543,plain,
negate(add(c,negate(c))) = negate(add(negate(X1),negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))))),
inference(step,[status(thm)],[t17344,t17186]) ).
cnf(t28544,plain,
negate(add(c,negate(c))) = negate(add(negate(X1),X1)),
inference(step,[status(thm)],[t28543,t4]) ).
cnf(t28545,plain,
negate(add(c,negate(c))) = negate(add(X1,negate(X1))),
inference(step,[status(thm)],[t28544,t8]) ).
cnf(t17415,plain,
negate(add(c,negate(c))) = negate(add(X1,negate(X1))),
inference(orient,[status(thm)],[t28545]) ).
cnf(t17902,plain,
X1 = add(X1,negate(add(X2,negate(X2)))),
inference(cp,[status(thm)],[t17901,t17415]) ).
cnf(t18445,plain,
add(X1,negate(add(X2,negate(X2)))) = X1,
inference(orient,[status(thm)],[t17902]) ).
cnf(t18549,plain,
negate(negate(X1)) = negate(negate(add(X1,negate(negate(X1))))),
inference(cp,[status(thm)],[t189,t18445]) ).
cnf(t17647,plain,
X1 = negate(add(negate(add(c,negate(c))),negate(add(X1,negate(negate(X1)))))),
inference(cp,[status(thm)],[t4,t17415]) ).
cnf(t28551,plain,
X1 = negate(negate(add(X1,negate(negate(X1))))),
inference(step,[status(thm)],[t17647,t17186]) ).
cnf(t18288,plain,
negate(negate(add(X1,negate(negate(X1))))) = X1,
inference(orient,[status(thm)],[t28551]) ).
cnf(t28552,plain,
negate(negate(X1)) = X1,
inference(step,[status(thm)],[t18549,t18288]) ).
cnf(t18641,plain,
negate(negate(X1)) = X1,
inference(orient,[status(thm)],[t28552]) ).
cnf(t18718,plain,
add(negate(add(X1,X2)),negate(add(negate(X2),X1))) = negate(X1),
inference(cp,[status(thm)],[t18641,t155]) ).
cnf(t28121,plain,
add(negate(add(X1,X2)),negate(add(negate(X2),X1))) = negate(X1),
inference(orient,[status(thm)],[t18718]) ).
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,t28121]) ).
cnf(g0_2,plain,
b != b,
inference(rw,[status(thm)],[g0_1,t18641]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ROB005-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n003.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:26:05 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 12.99/2.16 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.99/2.16 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------