%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ROB023-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n018.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 8.32s 7.04s
% Output : CNFRefutation 8.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 5
% Syntax : Number of clauses : 72 ( 72 unt; 0 nHn; 5 RR)
% Number of literals : 72 ( 71 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 120 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t0,axiom,
add(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t6,plain,
X1 = negate(add(negate(X1),negate(add(X1,negate(X1))))),
inference(cp,[status(thm)],[t5,t4]) ).
cnf(t50,plain,
negate(add(negate(X1),negate(add(X1,negate(X1))))) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t12,plain,
X1 = negate(add(negate(add(X2,X1)),negate(add(X1,negate(X2))))),
inference(cp,[status(thm)],[t5,t11]) ).
cnf(t180,plain,
negate(add(negate(add(X1,X2)),negate(add(X2,negate(X1))))) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t200,plain,
X1 = negate(add(negate(add(X2,X1)),negate(add(negate(X2),X1)))),
inference(cp,[status(thm)],[t180,t11]) ).
cnf(t266,plain,
negate(add(negate(add(X1,X2)),negate(add(negate(X1),X2)))) = X2,
inference(orient,[status(thm)],[t200]) ).
cnf(t2,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t14,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t2]) ).
cnf(t17,plain,
add(X1,add(X1,X2)) = add(X1,X2),
inference(cp,[status(thm)],[t14,t4]) ).
cnf(t21,plain,
add(X1,add(X1,X2)) = add(X1,X2),
inference(orient,[status(thm)],[t17]) ).
cnf(t273,plain,
add(X1,X2) = negate(add(negate(add(X1,X2)),negate(add(negate(X1),add(X1,X2))))),
inference(cp,[status(thm)],[t266,t21]) ).
cnf(t18,plain,
add(X1,add(X2,X3)) = add(add(X2,X1),X3),
inference(cp,[status(thm)],[t14,t11]) ).
cnf(t3468,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(step,[status(thm)],[t18,t14]) ).
cnf(t110,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(orient,[status(thm)],[t3468]) ).
cnf(t3493,plain,
add(X1,X2) = negate(add(negate(add(X1,X2)),negate(add(X1,add(negate(X1),X2))))),
inference(step,[status(thm)],[t273,t110]) ).
cnf(t1226,plain,
negate(add(negate(add(X1,X2)),negate(add(X1,add(negate(X1),X2))))) = add(X1,X2),
inference(orient,[status(thm)],[t3493]) ).
cnf(t1246,plain,
add(X1,X2) = negate(add(negate(add(X2,X1)),negate(add(X1,add(negate(X1),X2))))),
inference(cp,[status(thm)],[t1226,t11]) ).
cnf(t2202,plain,
negate(add(negate(add(X1,X2)),negate(add(X2,add(negate(X2),X1))))) = add(X2,X1),
inference(orient,[status(thm)],[t1246]) ).
cnf(t25,plain,
X1 = negate(add(negate(add(X1,X2)),negate(add(X1,negate(add(X1,X2)))))),
inference(cp,[status(thm)],[t5,t21]) ).
cnf(t396,plain,
negate(add(negate(add(X1,X2)),negate(add(X1,negate(add(X1,X2)))))) = X1,
inference(orient,[status(thm)],[t25]) ).
cnf(t13,plain,
X1 = negate(add(negate(add(X1,X2)),negate(add(negate(X2),X1)))),
inference(cp,[status(thm)],[t5,t11]) ).
cnf(t216,plain,
negate(add(negate(add(X1,X2)),negate(add(negate(X2),X1)))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t398,plain,
negate(add(X1,X2)) = negate(add(X1,negate(add(negate(add(X1,X2)),negate(add(negate(add(X1,X2)),negate(add(negate(X2),X1)))))))),
inference(cp,[status(thm)],[t396,t216]) ).
cnf(t3478,plain,
negate(add(X1,X2)) = negate(add(X1,negate(add(negate(add(X1,X2)),X1)))),
inference(step,[status(thm)],[t398,t216]) ).
cnf(t3479,plain,
negate(add(X1,X2)) = negate(add(X1,negate(add(X1,negate(add(X1,X2)))))),
inference(step,[status(thm)],[t3478,t11]) ).
cnf(t442,plain,
negate(add(X1,negate(add(X1,negate(add(X1,X2)))))) = negate(add(X1,X2)),
inference(orient,[status(thm)],[t3479]) ).
cnf(t455,plain,
negate(add(X1,add(X2,X3))) = negate(add(X1,negate(add(X1,negate(add(X2,add(X1,X3))))))),
inference(cp,[status(thm)],[t442,t110]) ).
cnf(t2419,plain,
negate(add(X1,negate(add(X1,negate(add(X2,add(X1,X3))))))) = negate(add(X1,add(X2,X3))),
inference(orient,[status(thm)],[t455]) ).
cnf(t7,plain,
negate(X1) = negate(add(negate(add(negate(X1),X1)),negate(negate(X1)))),
inference(cp,[status(thm)],[t5,t4]) ).
cnf(t3471,plain,
negate(X1) = negate(add(negate(negate(X1)),negate(add(negate(X1),X1)))),
inference(step,[status(thm)],[t7,t11]) ).
cnf(t3472,plain,
negate(X1) = negate(add(negate(negate(X1)),negate(add(X1,negate(X1))))),
inference(step,[status(thm)],[t3471,t11]) ).
cnf(t164,plain,
negate(add(negate(negate(X1)),negate(add(X1,negate(X1))))) = negate(X1),
inference(orient,[status(thm)],[t3472]) ).
cnf(t173,plain,
negate(negate(X1)) = negate(add(negate(add(negate(negate(X1)),add(X1,negate(X1)))),negate(X1))),
inference(cp,[status(thm)],[t5,t164]) ).
cnf(t3484,plain,
negate(negate(X1)) = negate(add(negate(X1),negate(add(negate(negate(X1)),add(X1,negate(X1)))))),
inference(step,[status(thm)],[t173,t11]) ).
cnf(t16,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(cp,[status(thm)],[t14,t11]) ).
cnf(t70,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(orient,[status(thm)],[t16]) ).
cnf(t24,plain,
add(X1,X2) = add(X1,add(X2,X1)),
inference(cp,[status(thm)],[t21,t11]) ).
cnf(t26,plain,
add(X1,add(X2,X1)) = add(X1,X2),
inference(orient,[status(thm)],[t24]) ).
cnf(t77,plain,
add(add(X1,X2),add(X3,X2)) = add(X3,add(X2,X1)),
inference(cp,[status(thm)],[t70,t26]) ).
cnf(t3469,plain,
add(X1,add(X2,add(X3,X2))) = add(X3,add(X2,X1)),
inference(step,[status(thm)],[t77,t14]) ).
cnf(t3470,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(step,[status(thm)],[t3469,t26]) ).
cnf(t135,plain,
add(X1,add(X2,X3)) = add(X3,add(X2,X1)),
inference(orient,[status(thm)],[t3470]) ).
cnf(t3485,plain,
negate(negate(X1)) = negate(add(negate(X1),negate(add(negate(X1),add(X1,negate(negate(X1))))))),
inference(step,[status(thm)],[t3484,t135]) ).
cnf(t3486,plain,
negate(negate(X1)) = negate(add(negate(X1),negate(add(X1,add(negate(X1),negate(negate(X1))))))),
inference(step,[status(thm)],[t3485,t110]) ).
cnf(t855,plain,
negate(add(negate(X1),negate(add(X1,add(negate(X1),negate(negate(X1))))))) = negate(negate(X1)),
inference(orient,[status(thm)],[t3486]) ).
cnf(t2421,plain,
negate(add(negate(X1),add(X1,negate(negate(X1))))) = negate(add(negate(X1),negate(negate(X1)))),
inference(cp,[status(thm)],[t2419,t855]) ).
cnf(t3498,plain,
negate(add(X1,add(negate(X1),negate(negate(X1))))) = negate(add(negate(X1),negate(negate(X1)))),
inference(step,[status(thm)],[t2421,t110]) ).
cnf(t2493,plain,
negate(add(X1,add(negate(X1),negate(negate(X1))))) = negate(add(negate(X1),negate(negate(X1)))),
inference(orient,[status(thm)],[t3498]) ).
cnf(t2601,plain,
add(X1,negate(negate(X1))) = negate(add(negate(add(negate(negate(X1)),X1)),negate(add(negate(X1),negate(negate(X1)))))),
inference(cp,[status(thm)],[t2202,t2493]) ).
cnf(t3499,plain,
add(X1,negate(negate(X1))) = negate(negate(X1)),
inference(step,[status(thm)],[t2601,t216]) ).
cnf(t2630,plain,
add(X1,negate(negate(X1))) = negate(negate(X1)),
inference(orient,[status(thm)],[t3499]) ).
cnf(t2672,plain,
negate(negate(add(negate(X1),negate(add(X1,negate(X1)))))) = add(add(negate(X1),negate(add(X1,negate(X1)))),negate(X1)),
inference(cp,[status(thm)],[t2630,t50]) ).
cnf(t3500,plain,
negate(X1) = add(add(negate(X1),negate(add(X1,negate(X1)))),negate(X1)),
inference(step,[status(thm)],[t2672,t50]) ).
cnf(t3501,plain,
negate(X1) = add(negate(X1),add(negate(add(X1,negate(X1))),negate(X1))),
inference(step,[status(thm)],[t3500,t14]) ).
cnf(t3502,plain,
negate(X1) = add(negate(X1),negate(add(X1,negate(X1)))),
inference(step,[status(thm)],[t3501,t26]) ).
cnf(t2867,plain,
add(negate(X1),negate(add(X1,negate(X1)))) = negate(X1),
inference(orient,[status(thm)],[t3502]) ).
cnf(t3503,plain,
negate(negate(X1)) = X1,
inference(step,[status(thm)],[t50,t2867]) ).
cnf(t2980,plain,
negate(negate(X1)) = X1,
inference(rw,[status(thm)],[t3503]) ).
cnf(t2981,plain,
negate(negate(X1)) = X1,
inference(orient,[status(thm)],[t2980]) ).
cnf(t2988,plain,
add(negate(add(X1,X2)),negate(add(negate(X2),X1))) = negate(X1),
inference(cp,[status(thm)],[t2981,t216]) ).
cnf(t3342,plain,
add(negate(add(X1,X2)),negate(add(negate(X2),X1))) = negate(X1),
inference(orient,[status(thm)],[t2988]) ).
cnf(goal_0,negated_conjecture,
add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b,
file('/export/starexec/sandbox2/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,t11]) ).
cnf(g0_1,plain,
negate(negate(b)) != b,
inference(rw,[status(thm)],[g0_0,t3342]) ).
cnf(g0_2,plain,
b != b,
inference(rw,[status(thm)],[g0_1,t2981]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ROB023-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/5.62 % Computer : n018.cluster.edu
% 0.15/5.62 % Model : x86_64 x86_64
% 0.15/5.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.62 % Memory : 8046.5625MB
% 0.15/5.62 % OS : Linux 6.8.0-71-generic
% 0.15/5.62 % CPULimit : 300
% 0.15/5.62 % WCLimit : 300
% 0.15/5.62 % DateTime : Thu Sep 24 08:30:39 UTC 2026
% 0.15/5.62 % CPUTime :
% 0.15/5.62 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.32/7.04 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.32/7.04 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------