%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUN135-1.006 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:29:37 PM UTC 2026
% Result : Unsatisfiable 7.15s 1.55s
% Output : CNFRefutation 7.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 14
% Syntax : Number of clauses : 138 ( 138 unt; 0 nHn; 17 RR)
% Number of literals : 138 ( 137 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-4 aty)
% Number of variables : 285 ( 17 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(eg0,negated_conjecture,
perfectp(X) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
eq(perfectp(X1),true) = efalse,
inference(equality_encoding,[status(esa)],[eg0]) ).
cnf(t41,plain,
eq(perfectp(X1),true) = efalse,
inference(orient,[status(thm)],[t4]) ).
cnf(t14,axiom,
if(qtd0(X1,X2),f(s(X1),minus(X2,X1),X3,X4),f(X1,X4,X3,X4)) = f(s(X1),s(X2),X3,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
if(qtd0(X1,X2),f(s(X1),minus(X2,X1),X3,X4),f(X1,X4,X3,X4)) = f(s(X1),s(X2),X3,X4),
inference(orient,[status(thm)],[t14]) ).
cnf(t10,axiom,
minus(s(X1),s(X2)) = minus(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t36,plain,
minus(s(X1),s(X2)) = minus(X1,X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t38,plain,
f(s(s(X1)),s(s(X2)),X3,X4) = if(qtd0(s(X1),s(X2)),f(s(s(X1)),minus(X2,X1),X3,X4),f(s(X1),X4,X3,X4)),
inference(cp,[status(thm)],[t20,t36]) ).
cnf(t11,axiom,
qtd0(s(X1),s(X2)) = qtd0(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
qtd0(s(X1),s(X2)) = qtd0(X1,X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t2028,plain,
f(s(s(X1)),s(s(X2)),X3,X4) = if(qtd0(X1,X2),f(s(s(X1)),minus(X2,X1),X3,X4),f(s(X1),X4,X3,X4)),
inference(step,[status(thm)],[t38,t30]) ).
cnf(t256,plain,
if(qtd0(X1,X2),f(s(s(X1)),minus(X2,X1),X3,X4),f(s(X1),X4,X3,X4)) = f(s(s(X1)),s(s(X2)),X3,X4),
inference(orient,[status(thm)],[t2028]) ).
cnf(t258,plain,
f(s(s(s(X1))),s(s(s(X2))),X3,X4) = if(qtd0(X1,X2),f(s(s(s(X1))),minus(s(X2),s(X1)),X3,X4),f(s(s(X1)),X4,X3,X4)),
inference(cp,[status(thm)],[t256,t30]) ).
cnf(t2059,plain,
f(s(s(s(X1))),s(s(s(X2))),X3,X4) = if(qtd0(X1,X2),f(s(s(s(X1))),minus(X2,X1),X3,X4),f(s(s(X1)),X4,X3,X4)),
inference(step,[status(thm)],[t258,t36]) ).
cnf(t614,plain,
if(qtd0(X1,X2),f(s(s(s(X1))),minus(X2,X1),X3,X4),f(s(s(X1)),X4,X3,X4)) = f(s(s(s(X1))),s(s(s(X2))),X3,X4),
inference(orient,[status(thm)],[t2059]) ).
cnf(t616,plain,
f(s(s(s(s(X1)))),s(s(s(s(X2)))),X3,X4) = if(qtd0(X1,X2),f(s(s(s(s(X1)))),minus(s(X2),s(X1)),X3,X4),f(s(s(s(X1))),X4,X3,X4)),
inference(cp,[status(thm)],[t614,t30]) ).
cnf(t2110,plain,
f(s(s(s(s(X1)))),s(s(s(s(X2)))),X3,X4) = if(qtd0(X1,X2),f(s(s(s(s(X1)))),minus(X2,X1),X3,X4),f(s(s(s(X1))),X4,X3,X4)),
inference(step,[status(thm)],[t616,t36]) ).
cnf(t1318,plain,
if(qtd0(X1,X2),f(s(s(s(s(X1)))),minus(X2,X1),X3,X4),f(s(s(s(X1))),X4,X3,X4)) = f(s(s(s(s(X1)))),s(s(s(s(X2)))),X3,X4),
inference(orient,[status(thm)],[t2110]) ).
cnf(t3,axiom,
qtd0(zero,X1) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
qtd0(zero,X1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t1319,plain,
f(s(s(s(s(zero)))),s(s(s(s(X1)))),X2,X3) = if(true,f(s(s(s(s(zero)))),minus(X1,zero),X2,X3),f(s(s(s(zero))),X3,X2,X3)),
inference(cp,[status(thm)],[t1318,t34]) ).
cnf(t6,axiom,
if(true,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
if(true,X1,X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t2111,plain,
f(s(s(s(s(zero)))),s(s(s(s(X1)))),X2,X3) = f(s(s(s(s(zero)))),minus(X1,zero),X2,X3),
inference(step,[status(thm)],[t1319,t17]) ).
cnf(t2,axiom,
minus(X1,zero) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
minus(X1,zero) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t2112,plain,
f(s(s(s(s(zero)))),s(s(s(s(X1)))),X2,X3) = f(s(s(s(s(zero)))),X1,X2,X3),
inference(step,[status(thm)],[t2111,t15]) ).
cnf(t1369,plain,
f(s(s(s(s(zero)))),s(s(s(s(X1)))),X2,X3) = f(s(s(s(s(zero)))),X1,X2,X3),
inference(orient,[status(thm)],[t2112]) ).
cnf(t13,axiom,
f(X1,X2,minus(X3,s(X1)),X2) = f(s(X1),zero,X3,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
f(X1,X2,minus(X3,s(X1)),X2) = f(s(X1),zero,X3,X2),
inference(orient,[status(thm)],[t13]) ).
cnf(t37,plain,
f(s(X1),zero,s(X2),X3) = f(X1,X3,minus(X2,X1),X3),
inference(cp,[status(thm)],[t18,t36]) ).
cnf(t58,plain,
f(s(X1),zero,s(X2),X3) = f(X1,X3,minus(X2,X1),X3),
inference(orient,[status(thm)],[t37]) ).
cnf(t1376,plain,
f(s(s(s(s(zero)))),X1,minus(X2,s(s(s(s(zero))))),s(s(s(s(X1))))) = f(s(s(s(s(s(zero))))),zero,s(X2),s(s(s(s(X1))))),
inference(cp,[status(thm)],[t1369,t58]) ).
cnf(t1478,plain,
f(s(s(s(s(zero)))),X1,minus(X2,s(s(s(s(zero))))),s(s(s(s(X1))))) = f(s(s(s(s(s(zero))))),zero,s(X2),s(s(s(s(X1))))),
inference(orient,[status(thm)],[t1376]) ).
cnf(t7,axiom,
qtd0(s(X1),zero) = false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
qtd0(s(X1),zero) = false,
inference(orient,[status(thm)],[t7]) ).
cnf(t259,plain,
f(s(s(s(X1))),s(s(zero)),X2,X3) = if(false,f(s(s(s(X1))),minus(zero,s(X1)),X2,X3),f(s(s(X1)),X3,X2,X3)),
inference(cp,[status(thm)],[t256,t32]) ).
cnf(t5,axiom,
if(false,X1,X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
if(false,X1,X2) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t2031,plain,
f(s(s(s(X1))),s(s(zero)),X2,X3) = f(s(s(X1)),X3,X2,X3),
inference(step,[status(thm)],[t259,t16]) ).
cnf(t303,plain,
f(s(s(s(X1))),s(s(zero)),X2,X3) = f(s(s(X1)),X3,X2,X3),
inference(orient,[status(thm)],[t2031]) ).
cnf(t33,plain,
f(s(s(X1)),s(zero),X2,X3) = if(false,f(s(s(X1)),minus(zero,s(X1)),X2,X3),f(s(X1),X3,X2,X3)),
inference(cp,[status(thm)],[t20,t32]) ).
cnf(t2007,plain,
f(s(s(X1)),s(zero),X2,X3) = f(s(X1),X3,X2,X3),
inference(step,[status(thm)],[t33,t16]) ).
cnf(t51,plain,
f(s(s(X1)),s(zero),X2,X3) = f(s(X1),X3,X2,X3),
inference(orient,[status(thm)],[t2007]) ).
cnf(t313,plain,
f(s(s(s(X1))),s(s(zero)),X2,X3) = f(s(s(s(X1))),s(zero),X2,X3),
inference(cp,[status(thm)],[t303,t51]) ).
cnf(t323,plain,
f(s(s(s(X1))),s(s(zero)),X2,X3) = f(s(s(s(X1))),s(zero),X2,X3),
inference(orient,[status(thm)],[t313]) ).
cnf(t1481,plain,
f(s(s(s(s(s(zero))))),zero,s(X1),s(s(s(s(s(s(zero))))))) = f(s(s(s(s(zero)))),s(zero),minus(X1,s(s(s(s(zero))))),s(s(s(s(s(s(zero))))))),
inference(cp,[status(thm)],[t1478,t323]) ).
cnf(t55,plain,
f(s(s(X1)),s(zero),minus(X2,s(s(X1))),X3) = f(s(s(X1)),zero,X2,X3),
inference(cp,[status(thm)],[t51,t18]) ).
cnf(t97,plain,
f(s(s(X1)),s(zero),minus(X2,s(s(X1))),X3) = f(s(s(X1)),zero,X2,X3),
inference(orient,[status(thm)],[t55]) ).
cnf(t2123,plain,
f(s(s(s(s(s(zero))))),zero,s(X1),s(s(s(s(s(s(zero))))))) = f(s(s(s(s(zero)))),zero,X1,s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t1481,t97]) ).
cnf(t1494,plain,
f(s(s(s(s(s(zero))))),zero,s(X1),s(s(s(s(s(s(zero))))))) = f(s(s(s(s(zero)))),zero,X1,s(s(s(s(s(s(zero))))))),
inference(orient,[status(thm)],[t2123]) ).
cnf(t61,plain,
f(s(s(X1)),zero,s(X2),X3) = f(s(s(X1)),s(zero),minus(X2,s(X1)),X3),
inference(cp,[status(thm)],[t58,t51]) ).
cnf(t86,plain,
f(s(s(X1)),s(zero),minus(X2,s(X1)),X3) = f(s(s(X1)),zero,s(X2),X3),
inference(orient,[status(thm)],[t61]) ).
cnf(t88,plain,
f(s(s(X1)),zero,s(s(X2)),X3) = f(s(s(X1)),s(zero),minus(X2,X1),X3),
inference(cp,[status(thm)],[t86,t36]) ).
cnf(t90,plain,
f(s(s(X1)),s(zero),minus(X2,X1),X3) = f(s(s(X1)),zero,s(s(X2)),X3),
inference(orient,[status(thm)],[t88]) ).
cnf(t93,plain,
f(s(s(s(X1))),zero,s(s(s(X2))),X3) = f(s(s(s(X1))),s(zero),minus(X2,X1),X3),
inference(cp,[status(thm)],[t90,t36]) ).
cnf(t102,plain,
f(s(s(s(X1))),s(zero),minus(X2,X1),X3) = f(s(s(s(X1))),zero,s(s(s(X2))),X3),
inference(orient,[status(thm)],[t93]) ).
cnf(t105,plain,
f(s(s(s(s(X1)))),zero,s(s(s(s(X2)))),X3) = f(s(s(s(s(X1)))),s(zero),minus(X2,X1),X3),
inference(cp,[status(thm)],[t102,t36]) ).
cnf(t508,plain,
f(s(s(s(s(X1)))),zero,s(s(s(s(X2)))),X3) = f(s(s(s(s(X1)))),s(zero),minus(X2,X1),X3),
inference(orient,[status(thm)],[t105]) ).
cnf(t518,plain,
f(s(s(s(s(s(X1))))),zero,s(s(s(s(s(X2))))),X3) = f(s(s(s(s(s(X1))))),s(zero),minus(X2,X1),X3),
inference(cp,[status(thm)],[t508,t36]) ).
cnf(t1238,plain,
f(s(s(s(s(s(X1))))),zero,s(s(s(s(s(X2))))),X3) = f(s(s(s(s(s(X1))))),s(zero),minus(X2,X1),X3),
inference(orient,[status(thm)],[t518]) ).
cnf(t1495,plain,
f(s(s(s(s(zero)))),zero,s(s(s(s(X1)))),s(s(s(s(s(s(zero))))))) = f(s(s(s(s(s(zero))))),s(zero),minus(X1,zero),s(s(s(s(s(s(zero))))))),
inference(cp,[status(thm)],[t1494,t1238]) ).
cnf(t2130,plain,
f(s(s(s(s(zero)))),s(zero),minus(X1,zero),s(s(s(s(s(s(zero))))))) = f(s(s(s(s(s(zero))))),s(zero),minus(X1,zero),s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t1495,t508]) ).
cnf(t2131,plain,
f(s(s(s(s(zero)))),s(zero),X1,s(s(s(s(s(s(zero))))))) = f(s(s(s(s(s(zero))))),s(zero),minus(X1,zero),s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t2130,t15]) ).
cnf(t2132,plain,
f(s(s(s(s(zero)))),s(zero),X1,s(s(s(s(s(s(zero))))))) = f(s(s(s(s(s(zero))))),s(zero),X1,s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t2131,t15]) ).
cnf(t1550,plain,
f(s(s(s(s(s(zero))))),s(zero),X1,s(s(s(s(s(s(zero))))))) = f(s(s(s(s(zero)))),s(zero),X1,s(s(s(s(s(s(zero))))))),
inference(orient,[status(thm)],[t2132]) ).
cnf(t12,axiom,
f(X1,s(zero),s(X1),s(X1)) = perfectp(s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
f(X1,s(zero),s(X1),s(X1)) = perfectp(s(X1)),
inference(orient,[status(thm)],[t12]) ).
cnf(t1552,plain,
f(s(s(s(s(zero)))),s(zero),s(s(s(s(s(s(zero)))))),s(s(s(s(s(s(zero))))))) = perfectp(s(s(s(s(s(s(zero))))))),
inference(cp,[status(thm)],[t1550,t19]) ).
cnf(t1556,plain,
f(s(s(s(s(zero)))),s(zero),s(s(s(s(s(s(zero)))))),s(s(s(s(s(s(zero))))))) = perfectp(s(s(s(s(s(s(zero))))))),
inference(orient,[status(thm)],[t1552]) ).
cnf(t1995,plain,
f(s(s(s(s(zero)))),s(zero),s(s(s(s(s(s(zero)))))),s(s(s(s(s(s(zero))))))) = perfectp(s(s(s(s(s(s(zero))))))),
inference(rw,[status(thm)],[t1556]) ).
cnf(t615,plain,
f(s(s(s(zero))),s(s(s(X1))),X2,X3) = if(true,f(s(s(s(zero))),minus(X1,zero),X2,X3),f(s(s(zero)),X3,X2,X3)),
inference(cp,[status(thm)],[t614,t34]) ).
cnf(t2060,plain,
f(s(s(s(zero))),s(s(s(X1))),X2,X3) = f(s(s(s(zero))),minus(X1,zero),X2,X3),
inference(step,[status(thm)],[t615,t17]) ).
cnf(t2061,plain,
f(s(s(s(zero))),s(s(s(X1))),X2,X3) = f(s(s(s(zero))),X1,X2,X3),
inference(step,[status(thm)],[t2060,t15]) ).
cnf(t657,plain,
f(s(s(s(zero))),s(s(s(X1))),X2,X3) = f(s(s(s(zero))),X1,X2,X3),
inference(orient,[status(thm)],[t2061]) ).
cnf(t661,plain,
f(s(s(s(zero))),X1,X2,s(s(s(X1)))) = f(s(s(s(s(zero)))),s(zero),X2,s(s(s(X1)))),
inference(cp,[status(thm)],[t657,t51]) ).
cnf(t780,plain,
f(s(s(s(zero))),X1,X2,s(s(s(X1)))) = f(s(s(s(s(zero)))),s(zero),X2,s(s(s(X1)))),
inference(orient,[status(thm)],[t661]) ).
cnf(t781,plain,
f(s(s(s(s(zero)))),s(zero),X1,s(s(s(s(s(s(X2))))))) = f(s(s(s(zero))),X2,X1,s(s(s(s(s(s(X2))))))),
inference(cp,[status(thm)],[t780,t657]) ).
cnf(t1977,plain,
f(s(s(s(s(zero)))),s(zero),X1,s(s(s(s(s(s(X2))))))) = f(s(s(s(zero))),X2,X1,s(s(s(s(s(s(X2))))))),
inference(orient,[status(thm)],[t781]) ).
cnf(t2146,plain,
f(s(s(s(zero))),zero,s(s(s(s(s(s(zero)))))),s(s(s(s(s(s(zero))))))) = perfectp(s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t1995,t1977]) ).
cnf(t104,plain,
f(s(s(s(zero))),zero,s(s(s(X1))),X2) = f(s(s(s(zero))),s(zero),X1,X2),
inference(cp,[status(thm)],[t102,t15]) ).
cnf(t107,plain,
f(s(s(s(zero))),zero,s(s(s(X1))),X2) = f(s(s(s(zero))),s(zero),X1,X2),
inference(orient,[status(thm)],[t104]) ).
cnf(t2147,plain,
f(s(s(s(zero))),s(zero),s(s(s(zero))),s(s(s(s(s(s(zero))))))) = perfectp(s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t2146,t107]) ).
cnf(t257,plain,
f(s(s(zero)),s(s(X1)),X2,X3) = if(true,f(s(s(zero)),minus(X1,zero),X2,X3),f(s(zero),X3,X2,X3)),
inference(cp,[status(thm)],[t256,t34]) ).
cnf(t2029,plain,
f(s(s(zero)),s(s(X1)),X2,X3) = f(s(s(zero)),minus(X1,zero),X2,X3),
inference(step,[status(thm)],[t257,t17]) ).
cnf(t2030,plain,
f(s(s(zero)),s(s(X1)),X2,X3) = f(s(s(zero)),X1,X2,X3),
inference(step,[status(thm)],[t2029,t15]) ).
cnf(t295,plain,
f(s(s(zero)),s(s(X1)),X2,X3) = f(s(s(zero)),X1,X2,X3),
inference(orient,[status(thm)],[t2030]) ).
cnf(t103,plain,
f(s(s(s(X1))),zero,s(s(s(X2))),X3) = f(s(s(X1)),X3,minus(X2,X1),X3),
inference(cp,[status(thm)],[t102,t51]) ).
cnf(t177,plain,
f(s(s(s(X1))),zero,s(s(s(X2))),X3) = f(s(s(X1)),X3,minus(X2,X1),X3),
inference(orient,[status(thm)],[t103]) ).
cnf(t297,plain,
f(s(s(zero)),X1,minus(X2,zero),s(s(X1))) = f(s(s(s(zero))),zero,s(s(s(X2))),s(s(X1))),
inference(cp,[status(thm)],[t295,t177]) ).
cnf(t2036,plain,
f(s(s(zero)),X1,X2,s(s(X1))) = f(s(s(s(zero))),zero,s(s(s(X2))),s(s(X1))),
inference(step,[status(thm)],[t297,t15]) ).
cnf(t2037,plain,
f(s(s(zero)),X1,X2,s(s(X1))) = f(s(s(s(zero))),s(zero),X2,s(s(X1))),
inference(step,[status(thm)],[t2036,t107]) ).
cnf(t355,plain,
f(s(s(zero)),X1,X2,s(s(X1))) = f(s(s(s(zero))),s(zero),X2,s(s(X1))),
inference(orient,[status(thm)],[t2037]) ).
cnf(t356,plain,
f(s(s(s(zero))),s(zero),X1,s(s(s(s(X2))))) = f(s(s(zero)),X2,X1,s(s(s(s(X2))))),
inference(cp,[status(thm)],[t355,t295]) ).
cnf(t421,plain,
f(s(s(s(zero))),s(zero),X1,s(s(s(s(X2))))) = f(s(s(zero)),X2,X1,s(s(s(s(X2))))),
inference(orient,[status(thm)],[t356]) ).
cnf(t425,plain,
f(s(s(s(zero))),s(zero),X1,s(s(s(s(s(s(X2))))))) = f(s(s(zero)),X2,X1,s(s(s(s(s(s(X2))))))),
inference(cp,[status(thm)],[t421,t295]) ).
cnf(t1220,plain,
f(s(s(s(zero))),s(zero),X1,s(s(s(s(s(s(X2))))))) = f(s(s(zero)),X2,X1,s(s(s(s(s(s(X2))))))),
inference(orient,[status(thm)],[t425]) ).
cnf(t2148,plain,
f(s(s(zero)),zero,s(s(s(zero))),s(s(s(s(s(s(zero))))))) = perfectp(s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t2147,t1220]) ).
cnf(t92,plain,
f(s(s(zero)),zero,s(s(X1)),X2) = f(s(s(zero)),s(zero),X1,X2),
inference(cp,[status(thm)],[t90,t15]) ).
cnf(t95,plain,
f(s(s(zero)),zero,s(s(X1)),X2) = f(s(s(zero)),s(zero),X1,X2),
inference(orient,[status(thm)],[t92]) ).
cnf(t2149,plain,
f(s(s(zero)),s(zero),s(zero),s(s(s(s(s(s(zero))))))) = perfectp(s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t2148,t95]) ).
cnf(t35,plain,
f(s(zero),s(X1),X2,X3) = if(true,f(s(zero),minus(X1,zero),X2,X3),f(zero,X3,X2,X3)),
inference(cp,[status(thm)],[t20,t34]) ).
cnf(t2005,plain,
f(s(zero),s(X1),X2,X3) = f(s(zero),minus(X1,zero),X2,X3),
inference(step,[status(thm)],[t35,t17]) ).
cnf(t2006,plain,
f(s(zero),s(X1),X2,X3) = f(s(zero),X1,X2,X3),
inference(step,[status(thm)],[t2005,t15]) ).
cnf(t46,plain,
f(s(zero),s(X1),X2,X3) = f(s(zero),X1,X2,X3),
inference(orient,[status(thm)],[t2006]) ).
cnf(t62,plain,
f(s(s(zero)),zero,s(X1),s(X2)) = f(s(zero),X2,minus(X1,s(zero)),s(X2)),
inference(cp,[status(thm)],[t58,t46]) ).
cnf(t81,plain,
f(s(zero),X1,minus(X2,s(zero)),s(X1)) = f(s(s(zero)),zero,s(X2),s(X1)),
inference(orient,[status(thm)],[t62]) ).
cnf(t82,plain,
f(s(s(zero)),zero,s(X1),s(s(X2))) = f(s(zero),X2,minus(X1,s(zero)),s(s(X2))),
inference(cp,[status(thm)],[t81,t46]) ).
cnf(t99,plain,
f(s(zero),X1,minus(X2,s(zero)),s(s(X1))) = f(s(s(zero)),zero,s(X2),s(s(X1))),
inference(orient,[status(thm)],[t82]) ).
cnf(t100,plain,
f(s(s(zero)),zero,s(X1),s(s(s(X2)))) = f(s(zero),X2,minus(X1,s(zero)),s(s(s(X2)))),
inference(cp,[status(thm)],[t99,t46]) ).
cnf(t121,plain,
f(s(zero),X1,minus(X2,s(zero)),s(s(s(X1)))) = f(s(s(zero)),zero,s(X2),s(s(s(X1)))),
inference(orient,[status(thm)],[t100]) ).
cnf(t122,plain,
f(s(s(zero)),zero,s(X1),s(s(s(s(X2))))) = f(s(zero),X2,minus(X1,s(zero)),s(s(s(s(X2))))),
inference(cp,[status(thm)],[t121,t46]) ).
cnf(t147,plain,
f(s(zero),X1,minus(X2,s(zero)),s(s(s(s(X1))))) = f(s(s(zero)),zero,s(X2),s(s(s(s(X1))))),
inference(orient,[status(thm)],[t122]) ).
cnf(t148,plain,
f(s(s(zero)),zero,s(X1),s(s(s(s(s(X2)))))) = f(s(zero),X2,minus(X1,s(zero)),s(s(s(s(s(X2)))))),
inference(cp,[status(thm)],[t147,t46]) ).
cnf(t159,plain,
f(s(zero),X1,minus(X2,s(zero)),s(s(s(s(s(X1)))))) = f(s(s(zero)),zero,s(X2),s(s(s(s(s(X1)))))),
inference(orient,[status(thm)],[t148]) ).
cnf(t160,plain,
f(s(s(zero)),zero,s(X1),s(s(s(s(s(s(X2))))))) = f(s(zero),X2,minus(X1,s(zero)),s(s(s(s(s(s(X2))))))),
inference(cp,[status(thm)],[t159,t46]) ).
cnf(t193,plain,
f(s(zero),X1,minus(X2,s(zero)),s(s(s(s(s(s(X1))))))) = f(s(s(zero)),zero,s(X2),s(s(s(s(s(s(X1))))))),
inference(orient,[status(thm)],[t160]) ).
cnf(t195,plain,
f(s(s(zero)),zero,s(s(X1)),s(s(s(s(s(s(X2))))))) = f(s(zero),X2,minus(X1,zero),s(s(s(s(s(s(X2))))))),
inference(cp,[status(thm)],[t193,t36]) ).
cnf(t2087,plain,
f(s(s(zero)),s(zero),X1,s(s(s(s(s(s(X2))))))) = f(s(zero),X2,minus(X1,zero),s(s(s(s(s(s(X2))))))),
inference(step,[status(thm)],[t195,t95]) ).
cnf(t2088,plain,
f(s(s(zero)),s(zero),X1,s(s(s(s(s(s(X2))))))) = f(s(zero),X2,X1,s(s(s(s(s(s(X2))))))),
inference(step,[status(thm)],[t2087,t15]) ).
cnf(t842,plain,
f(s(s(zero)),s(zero),X1,s(s(s(s(s(s(X2))))))) = f(s(zero),X2,X1,s(s(s(s(s(s(X2))))))),
inference(orient,[status(thm)],[t2088]) ).
cnf(t2150,plain,
f(s(zero),zero,s(zero),s(s(s(s(s(s(zero))))))) = perfectp(s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t2149,t842]) ).
cnf(t63,plain,
f(s(zero),zero,s(X1),X2) = f(zero,X2,X1,X2),
inference(cp,[status(thm)],[t58,t15]) ).
cnf(t67,plain,
f(s(zero),zero,s(X1),X2) = f(zero,X2,X1,X2),
inference(orient,[status(thm)],[t63]) ).
cnf(t8,axiom,
f(zero,X1,zero,X2) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
f(zero,X1,zero,X2) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t70,plain,
f(s(zero),zero,s(zero),X1) = true,
inference(cp,[status(thm)],[t67,t28]) ).
cnf(t73,plain,
f(s(zero),zero,s(zero),X1) = true,
inference(orient,[status(thm)],[t70]) ).
cnf(t2151,plain,
true = perfectp(s(s(s(s(s(s(zero))))))),
inference(step,[status(thm)],[t2150,t73]) ).
cnf(t1998,plain,
perfectp(s(s(s(s(s(s(zero))))))) = true,
inference(orient,[status(thm)],[t2151]) ).
cnf(t1999,plain,
efalse = eq(true,true),
inference(cp,[status(thm)],[t41,t1998]) ).
cnf(t1,plain,
eq(X1,X1) = etrue,
introduced(definition) ).
cnf(t40,plain,
eq(X1,X1) = etrue,
inference(orient,[status(thm)],[t1]) ).
cnf(t2152,plain,
efalse = etrue,
inference(step,[status(thm)],[t1999,t40]) ).
cnf(t2000,plain,
efalse = etrue,
inference(orient,[status(thm)],[t2152]) ).
cnf(goal_0,negated_conjecture,
etrue != efalse,
introduced(definition) ).
cnf(g0_0,plain,
etrue != etrue,
inference(rw,[status(thm)],[goal_0,t2000]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUN135-1.006 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n015.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 06:08:10 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.15/1.55 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.15/1.55 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------