%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM420-1.000 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.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:19:58 PM UTC 2026
% Result : Unsatisfiable 62.00s 8.22s
% Output : Proof 62.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 29
% Syntax : Number of formulae : 199 ( 151 unt; 0 def)
% Number of atoms : 279 ( 194 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 202 ( 122 ~; 80 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-4 aty)
% Number of variables : 281 ( 90 sgn 86 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t18,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t510,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t18]) ).
cnf(f0,axiom,
( plus(X2,times(X4,X3)) != plus(X1,times(X5,X3))
| ~ less(X2,X3)
| ~ less(X1,X3)
| ~ less(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f0_nnf,plain,
! [X1,X2,X3,X4,X5] :
( plus(X2,times(X4,X3)) != plus(X1,times(X5,X3))
| ~ less(X2,X3)
| ~ less(X1,X3)
| ~ less(X1,X2) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X1,X2,X3,X4,X5] :
( plus(X2,times(X4,X3)) != plus(X1,times(X5,X3))
| ~ less(X2,X3)
| ~ less(X1,X3)
| ~ less(X1,X2) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( plus(X1,times(X3,X2)) != plus(X0,times(X4,X2))
| ~ less(X1,X2)
| ~ less(X0,X2)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t69,plain,
or(not(less(X1,X2)),or(not(less(X1,X3)),or(not(less(X2,X3)),not(eq(plus(X2,times(X4,X3)),plus(X1,times(X5,X3))))))) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t155,plain,
or(not(less(X1,X2)),or(not(less(X1,X3)),or(not(less(X2,X3)),not(eq(plus(X2,times(X4,X3)),plus(X1,times(X5,X3))))))) = true,
inference(orient,[status(thm)],[t69]) ).
cnf(f7,axiom,
plus(n0,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_8) ).
fof(f7_nnf,plain,
! [X1] : plus(n0,X1) = X1,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X1] : plus(n0,X1) = X1,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
plus(n0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t9,plain,
plus(n0,X1) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t80,plain,
plus(n0,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t162,plain,
true = or(not(less(n0,X1)),or(not(less(n0,X2)),or(not(less(X1,X2)),not(eq(plus(X1,times(X3,X2)),times(X4,X2)))))),
inference(cp,[status(thm)],[t155,t80]) ).
cnf(t36938,plain,
or(not(less(n0,X1)),or(not(less(n0,X2)),or(not(less(X1,X2)),not(eq(plus(X1,times(X3,X2)),times(X4,X2)))))) = true,
inference(orient,[status(thm)],[t162]) ).
cnf(f77,negated_conjecture,
( less(n1,X7)
| X7 != p__0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_44) ).
fof(f77_nnf,plain,
! [X7] :
( less(n1,X7)
| X7 != p__0 ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
! [X7] :
( less(n1,X7)
| X7 != p__0 ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c77,plain,
( less(n1,X0)
| X0 != p__0 ),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t22,plain,
ifeq(X1,p__0,less(n1,X1),true) = true,
inference(equality_encoding,[status(esa)],[c77]) ).
cnf(t106,plain,
ifeq(X1,p__0,less(n1,X1),true) = true,
inference(orient,[status(thm)],[t22]) ).
cnf(t14,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t83,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(t107,plain,
true = less(n1,p__0),
inference(cp,[status(thm)],[t106,t83]) ).
cnf(t530,plain,
less(n1,p__0) = true,
inference(orient,[status(thm)],[t107]) ).
cnf(t37196,plain,
true = or(not(less(n0,n1)),or(not(less(n0,p__0)),or(not(true),not(eq(plus(n1,times(X1,p__0)),times(X2,p__0)))))),
inference(cp,[status(thm)],[t36938,t530]) ).
cnf(f29,axiom,
less(n0,plus(X1,n1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_30) ).
fof(f29_nnf,plain,
! [X1] : less(n0,plus(X1,n1)),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X1] : less(n0,plus(X1,n1)),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
less(n0,plus(X0,n1)),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(t15,plain,
less(n0,plus(X1,n1)) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t144,plain,
less(n0,plus(X1,n1)) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t145,plain,
true = less(n0,n1),
inference(cp,[status(thm)],[t144,t80]) ).
cnf(t550,plain,
less(n0,n1) = true,
inference(orient,[status(thm)],[t145]) ).
cnf(t38624,plain,
true = or(not(true),or(not(less(n0,p__0)),or(not(true),not(eq(plus(n1,times(X1,p__0)),times(X2,p__0)))))),
inference(step,[status(thm)],[t37196,t550]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t511,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t38625,plain,
true = or(false,or(not(less(n0,p__0)),or(not(true),not(eq(plus(n1,times(X1,p__0)),times(X2,p__0)))))),
inference(step,[status(thm)],[t38624,t511]) ).
cnf(t6,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t96,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t38626,plain,
true = or(not(less(n0,p__0)),or(not(true),not(eq(plus(n1,times(X1,p__0)),times(X2,p__0))))),
inference(step,[status(thm)],[t38625,t96]) ).
cnf(f33,axiom,
( less(X6,X3)
| ~ less(plus(X6,n1),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_34) ).
fof(f33_nnf,plain,
! [X6,X3] :
( less(X6,X3)
| ~ less(plus(X6,n1),X3) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [X6,X3] :
( less(X6,X3)
| ~ less(plus(X6,n1),X3) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( less(X0,X1)
| ~ less(plus(X0,n1),X1) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(t48,plain,
ifeq(less(plus(X1,n1),X2),true,less(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t134,plain,
ifeq(less(plus(X1,n1),X2),true,less(X1,X2),true) = true,
inference(orient,[status(thm)],[t48]) ).
cnf(t135,plain,
true = ifeq(less(n1,X1),true,less(n0,X1),true),
inference(cp,[status(thm)],[t134,t80]) ).
cnf(t1333,plain,
ifeq(less(n1,X1),true,less(n0,X1),true) = true,
inference(orient,[status(thm)],[t135]) ).
cnf(t1334,plain,
true = ifeq(true,true,less(n0,p__0),true),
inference(cp,[status(thm)],[t1333,t530]) ).
cnf(t38205,plain,
true = less(n0,p__0),
inference(step,[status(thm)],[t1334,t83]) ).
cnf(t1335,plain,
less(n0,p__0) = true,
inference(orient,[status(thm)],[t38205]) ).
cnf(t38627,plain,
true = or(not(true),or(not(true),not(eq(plus(n1,times(X1,p__0)),times(X2,p__0))))),
inference(step,[status(thm)],[t38626,t1335]) ).
cnf(t38628,plain,
true = or(false,or(not(true),not(eq(plus(n1,times(X1,p__0)),times(X2,p__0))))),
inference(step,[status(thm)],[t38627,t511]) ).
cnf(t38629,plain,
true = or(not(true),not(eq(plus(n1,times(X1,p__0)),times(X2,p__0)))),
inference(step,[status(thm)],[t38628,t96]) ).
cnf(t38630,plain,
true = or(false,not(eq(plus(n1,times(X1,p__0)),times(X2,p__0)))),
inference(step,[status(thm)],[t38629,t511]) ).
cnf(t38631,plain,
true = not(eq(plus(n1,times(X1,p__0)),times(X2,p__0))),
inference(step,[status(thm)],[t38630,t96]) ).
cnf(t37280,plain,
not(eq(plus(n1,times(X1,p__0)),times(X2,p__0))) = true,
inference(orient,[status(thm)],[t38631]) ).
cnf(f24,axiom,
plus(times(X1,X2),X1) = times(X1,plus(X2,n1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_25) ).
fof(f24_nnf,plain,
! [X1,X2] : plus(times(X1,X2),X1) = times(X1,plus(X2,n1)),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X1,X2] : plus(times(X1,X2),X1) = times(X1,plus(X2,n1)),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
plus(times(X0,X1),X0) = times(X0,plus(X1,n1)),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t40,plain,
times(X1,plus(X2,n1)) = plus(times(X1,X2),X1),
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(f5,axiom,
plus(X1,X2) = plus(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(f5_nnf,plain,
! [X1,X2] : plus(X1,X2) = plus(X2,X1),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X1,X2] : plus(X1,X2) = plus(X2,X1),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t16,plain,
plus(X1,X2) = plus(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t199,plain,
plus(X1,X2) = plus(X2,X1),
inference(orient,[status(thm)],[t16]) ).
cnf(t38141,plain,
times(X1,plus(X2,n1)) = plus(X1,times(X1,X2)),
inference(step,[status(thm)],[t40,t199]) ).
cnf(t305,plain,
plus(X1,times(X1,X2)) = times(X1,plus(X2,n1)),
inference(orient,[status(thm)],[t38141]) ).
cnf(t37281,plain,
true = not(eq(times(n1,plus(p__0,n1)),times(X1,p__0))),
inference(cp,[status(thm)],[t37280,t305]) ).
cnf(f19,axiom,
times(n1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
fof(f19_nnf,plain,
! [X1] : times(n1,X1) = X1,
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X1] : times(n1,X1) = X1,
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
times(n1,X0) = X0,
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t12,plain,
times(n1,X1) = X1,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t82,plain,
times(n1,X1) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t38632,plain,
true = not(eq(plus(p__0,n1),times(X1,p__0))),
inference(step,[status(thm)],[t37281,t82]) ).
cnf(t37295,plain,
not(eq(plus(p__0,n1),times(X1,p__0))) = true,
inference(orient,[status(thm)],[t38632]) ).
cnf(t37302,plain,
false = ifeq(true,true,eq(plus(p__0,n1),times(X1,p__0)),false),
inference(cp,[status(thm)],[t510,t37295]) ).
cnf(t38634,plain,
false = eq(plus(p__0,n1),times(X1,p__0)),
inference(step,[status(thm)],[t37302,t83]) ).
cnf(t37312,plain,
eq(plus(p__0,n1),times(X1,p__0)) = false,
inference(orient,[status(thm)],[t38634]) ).
cnf(f14,axiom,
times(X1,X2) = times(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
fof(f14_nnf,plain,
! [X1,X2] : times(X1,X2) = times(X2,X1),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X1,X2] : times(X1,X2) = times(X2,X1),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
times(X0,X1) = times(X1,X0),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t17,plain,
times(X1,X2) = times(X2,X1),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t382,plain,
times(X1,X2) = times(X2,X1),
inference(orient,[status(thm)],[t17]) ).
cnf(t37314,plain,
false = eq(plus(p__0,n1),times(p__0,X1)),
inference(cp,[status(thm)],[t37312,t382]) ).
cnf(t37325,plain,
eq(plus(p__0,n1),times(p__0,X1)) = false,
inference(orient,[status(thm)],[t37314]) ).
cnf(t26,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t94,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t26]) ).
cnf(f81,negated_conjecture,
( times(s_1(X10),s_4(X10)) = X10
| X10 = n1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_48) ).
fof(f81_nnf,plain,
! [X10] :
( times(s_1(X10),s_4(X10)) = X10
| X10 = n1 ),
inference(nnf_transformation,[status(thm)],[f81]) ).
fof(f81_sk,plain,
! [X10] :
( times(s_1(X10),s_4(X10)) = X10
| X10 = n1 ),
inference(skolemisation,[status(esa)],[f81_nnf]) ).
cnf(c81,plain,
( times(s_1(X0),s_4(X0)) = X0
| X0 = n1 ),
inference(cnf_transformation,[status(esa)],[f81_sk]) ).
cnf(t52,plain,
or(eq(X1,n1),eq(times(s_1(X1),s_4(X1)),X1)) = true,
inference(equality_encoding,[status(esa)],[c81]) ).
cnf(t188,plain,
or(eq(X1,n1),eq(times(s_1(X1),s_4(X1)),X1)) = true,
inference(orient,[status(thm)],[t52]) ).
cnf(t411,plain,
or(eq(X1,n1),eq(times(s_1(X1),s_4(X1)),X1)) = true,
inference(rw,[status(thm)],[t188]) ).
cnf(t38378,plain,
or(eq(X1,n1),eq(times(s_4(X1),s_1(X1)),X1)) = true,
inference(step,[status(thm)],[t411,t382]) ).
cnf(t15488,plain,
or(eq(X1,n1),eq(times(s_4(X1),s_1(X1)),X1)) = true,
inference(orient,[status(thm)],[t38378]) ).
cnf(f13,axiom,
plus(n1,plus(X1,n1)) != n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_14) ).
fof(f13_nnf,plain,
! [X1] : plus(n1,plus(X1,n1)) != n1,
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X1] : plus(n1,plus(X1,n1)) != n1,
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
plus(n1,plus(X0,n1)) != n1,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t21,plain,
eq(plus(n1,plus(X1,n1)),n1) = false,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t519,plain,
eq(plus(n1,plus(X1,n1)),n1) = false,
inference(orient,[status(thm)],[t21]) ).
cnf(t522,plain,
false = eq(plus(n1,plus(n1,X1)),n1),
inference(cp,[status(thm)],[t519,t199]) ).
cnf(t852,plain,
eq(plus(n1,plus(n1,X1)),n1) = false,
inference(orient,[status(thm)],[t522]) ).
cnf(f51,negated_conjecture,
( p__0 = plus(s_7(p__0),n1)
| ~ less(n0,p__0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_18) ).
fof(f51_nnf,plain,
( p__0 = plus(s_7(p__0),n1)
| ~ less(n0,p__0) ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
( p__0 = plus(s_7(p__0),n1)
| ~ less(n0,p__0) ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
( p__0 = plus(s_7(p__0),n1)
| ~ less(n0,p__0) ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(t61,plain,
ifeq(less(n0,p__0),true,p__0,plus(s_7(p__0),n1)) = plus(s_7(p__0),n1),
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(t38148,plain,
ifeq(less(n0,p__0),true,p__0,plus(n1,s_7(p__0))) = plus(s_7(p__0),n1),
inference(step,[status(thm)],[t61,t199]) ).
cnf(t38149,plain,
ifeq(less(n0,p__0),true,p__0,plus(n1,s_7(p__0))) = plus(n1,s_7(p__0)),
inference(step,[status(thm)],[t38148,t199]) ).
cnf(t381,plain,
ifeq(less(n0,p__0),true,p__0,plus(n1,s_7(p__0))) = plus(n1,s_7(p__0)),
inference(orient,[status(thm)],[t38149]) ).
cnf(t38208,plain,
ifeq(true,true,p__0,plus(n1,s_7(p__0))) = plus(n1,s_7(p__0)),
inference(step,[status(thm)],[t381,t1335]) ).
cnf(t38209,plain,
p__0 = plus(n1,s_7(p__0)),
inference(step,[status(thm)],[t38208,t83]) ).
cnf(t1349,plain,
p__0 = plus(n1,s_7(p__0)),
inference(rw,[status(thm)],[t38209]) ).
cnf(t1353,plain,
plus(n1,s_7(p__0)) = p__0,
inference(orient,[status(thm)],[t1349]) ).
cnf(t1377,plain,
false = eq(plus(n1,p__0),n1),
inference(cp,[status(thm)],[t852,t1353]) ).
cnf(t38218,plain,
false = eq(plus(p__0,n1),n1),
inference(step,[status(thm)],[t1377,t199]) ).
cnf(t1421,plain,
eq(plus(p__0,n1),n1) = false,
inference(orient,[status(thm)],[t38218]) ).
cnf(t15539,plain,
true = or(false,eq(times(s_4(plus(p__0,n1)),s_1(plus(p__0,n1))),plus(p__0,n1))),
inference(cp,[status(thm)],[t15488,t1421]) ).
cnf(t38420,plain,
true = eq(times(s_4(plus(p__0,n1)),s_1(plus(p__0,n1))),plus(p__0,n1)),
inference(step,[status(thm)],[t15539,t96]) ).
cnf(f86,negated_conjecture,
( s_1(X10) = p__0
| X10 = n1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_53) ).
fof(f86_nnf,plain,
! [X10] :
( s_1(X10) = p__0
| X10 = n1 ),
inference(nnf_transformation,[status(thm)],[f86]) ).
fof(f86_sk,plain,
! [X10] :
( s_1(X10) = p__0
| X10 = n1 ),
inference(skolemisation,[status(esa)],[f86_nnf]) ).
cnf(c86,plain,
( s_1(X0) = p__0
| X0 = n1 ),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
cnf(t32,plain,
or(eq(X1,n1),eq(s_1(X1),p__0)) = true,
inference(equality_encoding,[status(esa)],[c86]) ).
cnf(t190,plain,
or(eq(X1,n1),eq(s_1(X1),p__0)) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(t524,plain,
true = or(false,eq(s_1(plus(n1,plus(X1,n1))),p__0)),
inference(cp,[status(thm)],[t190,t519]) ).
cnf(t38197,plain,
true = eq(s_1(plus(n1,plus(X1,n1))),p__0),
inference(step,[status(thm)],[t524,t96]) ).
cnf(t1173,plain,
eq(s_1(plus(n1,plus(X1,n1))),p__0) = true,
inference(orient,[status(thm)],[t38197]) ).
cnf(t1176,plain,
p__0 = ifeq(true,true,s_1(plus(n1,plus(X1,n1))),p__0),
inference(cp,[status(thm)],[t94,t1173]) ).
cnf(t38198,plain,
p__0 = s_1(plus(n1,plus(X1,n1))),
inference(step,[status(thm)],[t1176,t83]) ).
cnf(t1178,plain,
s_1(plus(n1,plus(X1,n1))) = p__0,
inference(orient,[status(thm)],[t38198]) ).
cnf(t1180,plain,
p__0 = s_1(plus(n1,plus(n1,X1))),
inference(cp,[status(thm)],[t1178,t199]) ).
cnf(t1181,plain,
s_1(plus(n1,plus(n1,X1))) = p__0,
inference(orient,[status(thm)],[t1180]) ).
cnf(t1374,plain,
p__0 = s_1(plus(n1,p__0)),
inference(cp,[status(thm)],[t1181,t1353]) ).
cnf(t38217,plain,
p__0 = s_1(plus(p__0,n1)),
inference(step,[status(thm)],[t1374,t199]) ).
cnf(t1383,plain,
s_1(plus(p__0,n1)) = p__0,
inference(orient,[status(thm)],[t38217]) ).
cnf(t38421,plain,
true = eq(times(s_4(plus(p__0,n1)),p__0),plus(p__0,n1)),
inference(step,[status(thm)],[t38420,t1383]) ).
cnf(t38422,plain,
true = eq(times(p__0,s_4(plus(p__0,n1))),plus(p__0,n1)),
inference(step,[status(thm)],[t38421,t382]) ).
cnf(t18169,plain,
eq(times(p__0,s_4(plus(p__0,n1))),plus(p__0,n1)) = true,
inference(orient,[status(thm)],[t38422]) ).
cnf(t18170,plain,
plus(p__0,n1) = ifeq(true,true,times(p__0,s_4(plus(p__0,n1))),plus(p__0,n1)),
inference(cp,[status(thm)],[t94,t18169]) ).
cnf(t38423,plain,
plus(p__0,n1) = times(p__0,s_4(plus(p__0,n1))),
inference(step,[status(thm)],[t18170,t83]) ).
cnf(t18171,plain,
times(p__0,s_4(plus(p__0,n1))) = plus(p__0,n1),
inference(orient,[status(thm)],[t38423]) ).
cnf(t37335,plain,
false = eq(plus(p__0,n1),plus(p__0,n1)),
inference(cp,[status(thm)],[t37325,t18171]) ).
cnf(t3,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t192,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t38637,plain,
false = true,
inference(step,[status(thm)],[t37335,t192]) ).
cnf(t37351,plain,
false = true,
inference(orient,[status(thm)],[t38637]) ).
cnf(f15,axiom,
plus(X1,n1) != n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_16) ).
fof(f15_nnf,plain,
! [X1] : plus(X1,n1) != n0,
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X1] : plus(X1,n1) != n0,
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
plus(X0,n1) != n0,
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(f28,axiom,
( plus(X1,times(X4,X3)) != plus(X2,times(X5,X3))
| ~ less(X2,X3)
| ~ less(X1,X3)
| ~ less(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_29) ).
fof(f28_nnf,plain,
! [X1,X2,X3,X4,X5] :
( plus(X1,times(X4,X3)) != plus(X2,times(X5,X3))
| ~ less(X2,X3)
| ~ less(X1,X3)
| ~ less(X1,X2) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X1,X2,X3,X4,X5] :
( plus(X1,times(X4,X3)) != plus(X2,times(X5,X3))
| ~ less(X2,X3)
| ~ less(X1,X3)
| ~ less(X1,X2) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( plus(X0,times(X3,X2)) != plus(X1,times(X4,X2))
| ~ less(X1,X2)
| ~ less(X0,X2)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(f30,axiom,
( X1 != n1
| ~ less(n1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_31) ).
fof(f30_nnf,plain,
! [X1] :
( X1 != n1
| ~ less(n1,X1) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X1] :
( X1 != n1
| ~ less(n1,X1) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( X0 != n1
| ~ less(n1,X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f32,axiom,
( n1 != times(X2,X1)
| ~ less(n1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_33) ).
fof(f32_nnf,plain,
! [X1,X2] :
( n1 != times(X2,X1)
| ~ less(n1,X1) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [X1,X2] :
( n1 != times(X2,X1)
| ~ less(n1,X1) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( n1 != times(X1,X0)
| ~ less(n1,X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(f36,negated_conjecture,
~ element(plus(X10,plus(X12,n1)),X13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
fof(f36_nnf,plain,
! [X10,X12,X13] : ~ element(plus(X10,plus(X12,n1)),X13),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X10,X12,X13] : ~ element(plus(X10,plus(X12,n1)),X13),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
~ element(plus(X0,plus(X1,n1)),X2),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(f42,negated_conjecture,
~ element(X1,X13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_9) ).
fof(f42_nnf,plain,
! [X1,X13] : ~ element(X1,X13),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [X1,X13] : ~ element(X1,X13),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
~ element(X0,X1),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(f47,negated_conjecture,
( plus(X8,times(X9,p__0)) != plus(n0,times(X22,p__0))
| ~ less(X8,p__0)
| ~ less(n0,p__0)
| ~ less(X8,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_14) ).
fof(f47_nnf,plain,
! [X8,X9,X22] :
( plus(X8,times(X9,p__0)) != plus(n0,times(X22,p__0))
| ~ less(X8,p__0)
| ~ less(n0,p__0)
| ~ less(X8,n0) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [X8,X9,X22] :
( plus(X8,times(X9,p__0)) != plus(n0,times(X22,p__0))
| ~ less(X8,p__0)
| ~ less(n0,p__0)
| ~ less(X8,n0) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
( plus(X0,times(X1,p__0)) != plus(n0,times(X2,p__0))
| ~ less(X0,p__0)
| ~ less(n0,p__0)
| ~ less(X0,n0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(f57,negated_conjecture,
( plus(X8,times(X9,p__0)) != plus(n0,times(X22,p__0))
| ~ less(X8,p__0)
| ~ less(n0,p__0)
| ~ less(n0,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_24) ).
fof(f57_nnf,plain,
! [X8,X9,X22] :
( plus(X8,times(X9,p__0)) != plus(n0,times(X22,p__0))
| ~ less(X8,p__0)
| ~ less(n0,p__0)
| ~ less(n0,X8) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [X8,X9,X22] :
( plus(X8,times(X9,p__0)) != plus(n0,times(X22,p__0))
| ~ less(X8,p__0)
| ~ less(n0,p__0)
| ~ less(n0,X8) ),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c57,plain,
( plus(X0,times(X1,p__0)) != plus(n0,times(X2,p__0))
| ~ less(X0,p__0)
| ~ less(n0,p__0)
| ~ less(n0,X0) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(f58,negated_conjecture,
plus(n1,plus(X11,n1)) != n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_25) ).
fof(f58_nnf,plain,
! [X11] : plus(n1,plus(X11,n1)) != n1,
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
! [X11] : plus(n1,plus(X11,n1)) != n1,
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
plus(n1,plus(X0,n1)) != n1,
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f87,negated_conjecture,
( n1 != times(X12,X7)
| X7 != p__0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_54) ).
fof(f87_nnf,plain,
! [X7,X12] :
( n1 != times(X12,X7)
| X7 != p__0 ),
inference(nnf_transformation,[status(thm)],[f87]) ).
fof(f87_sk,plain,
! [X7,X12] :
( n1 != times(X12,X7)
| X7 != p__0 ),
inference(skolemisation,[status(esa)],[f87_nnf]) ).
cnf(c87,plain,
( n1 != times(X1,X0)
| X0 != p__0 ),
inference(cnf_transformation,[status(esa)],[f87_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c13,c15,c28,c30,c32,c36,c42,c47,c57,c58,c87]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t37351]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM420-1.000 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.34 % Computer : n014.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Thu Sep 24 03:52:48 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 62.00/8.22 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 62.00/8.22 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------