%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM339+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Thu Sep 24 01:38:59 PM UTC 2026
% Result : Theorem 96.01s 12.55s
% Output : CNFRefutation 96.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 24
% Syntax : Number of formulae : 90 ( 30 unt; 5 def)
% Number of atoms : 253 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 321 ( 158 ~; 139 |; 12 &)
% ( 6 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 14 ( 13 usr; 6 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 196 ( 194 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
rdn_translate(n1,rdn_pos(rdnn(n1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f255,axiom,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f256,axiom,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f257,axiom,
rdn_non_zero_digit(rdnn(n1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f278,axiom,
! [D,Db,Ob] :
( rdn_non_zero(Ob)
=> rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f279,axiom,
! [X] :
( rdn_non_zero_digit(rdnn(X))
=> rdn_non_zero(rdnn(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,axiom,
! [D,O] :
( rdn_non_zero(O)
=> rdn_non_zero(rdn(rdnn(D),O)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f289,axiom,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( ( rdn_translate(Z,rdn_neg(RDN_Z))
& rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Z,RDN_Y)
& rdn_positive_less(RDN_X,RDN_Y)
& rdn_translate(Y,rdn_neg(RDN_Y))
& rdn_translate(X,rdn_pos(RDN_X)) )
=> sum(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f296,axiom,
! [X,Y,Z] :
( sum(Y,Z,X)
<=> difference(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f297,axiom,
! [C,D1,D2,RD,ID] :
( ( rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(n0))
& rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(n0)) )
=> rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdnn(RD)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f299,axiom,
! [C,D1,D2,O2,RD,RO,ID,IC1,IC2,NC] :
( ( rdn_non_zero(RO)
& rdn_non_zero(O2)
& rdn_add_with_carry(rdnn(NC),rdnn(n0),O2,RO)
& rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(NC),rdnn(n0))
& rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
& rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) )
=> rdn_add_with_carry(rdnn(C),rdnn(D1),rdn(rdnn(D2),O2),rdn(rdnn(RD),RO)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f302,axiom,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f303,axiom,
rdn_digit_add(rdnn(n0),rdnn(n1),rdnn(n1),rdnn(n0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f304,axiom,
rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(n2),rdnn(n0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f312,axiom,
rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f319,axiom,
rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(n8),rdnn(n0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f322,axiom,
rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(n2),rdnn(n0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f382,axiom,
rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(n8),rdnn(n0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f402,conjecture,
? [X] : difference(nn127,n1,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f403,negated_conjecture,
~ ? [X] : difference(nn127,n1,X),
inference(negated_conjecture,[status(cth)],[f402]) ).
fof(f405,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f658,plain,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f659,plain,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f660,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f686,plain,
! [D,Db,Ob] :
( rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob))
| ~ rdn_non_zero(Ob) ),
inference(pre_NNF_transformation,[status(thm)],[f278]) ).
fof(f687,plain,
! [Ob] :
( ! [D,Db] : rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob))
| ~ rdn_non_zero(Ob) ),
inference(miniscoping,[status(thm)],[f686]) ).
fof(f688,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X1),rdn(rdnn(X2),X0))
| ~ rdn_non_zero(X0) ),
inference(cnf_transformation,[status(thm)],[f687]) ).
fof(f689,plain,
! [X] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ),
inference(pre_NNF_transformation,[status(thm)],[f279]) ).
fof(f690,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(cnf_transformation,[status(thm)],[f689]) ).
fof(f691,plain,
! [D,O] :
( rdn_non_zero(rdn(rdnn(D),O))
| ~ rdn_non_zero(O) ),
inference(pre_NNF_transformation,[status(thm)],[f280]) ).
fof(f692,plain,
! [O] :
( ! [D] : rdn_non_zero(rdn(rdnn(D),O))
| ~ rdn_non_zero(O) ),
inference(miniscoping,[status(thm)],[f691]) ).
fof(f693,plain,
! [X0,X1] :
( rdn_non_zero(rdn(rdnn(X1),X0))
| ~ rdn_non_zero(X0) ),
inference(cnf_transformation,[status(thm)],[f692]) ).
fof(f722,plain,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( sum(X,Y,Z)
| ~ rdn_translate(Z,rdn_neg(RDN_Z))
| ~ rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Z,RDN_Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_neg(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(pre_NNF_transformation,[status(thm)],[f289]) ).
fof(f723,plain,
! [X,Y,Z] :
( sum(X,Y,Z)
| ! [RDN_Z] :
( ~ rdn_translate(Z,rdn_neg(RDN_Z))
| ! [RDN_X,RDN_Y] :
( ~ rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Z,RDN_Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_neg(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ) ) ),
inference(miniscoping,[status(thm)],[f722]) ).
fof(f724,plain,
! [X0,X1,X2,X3,X4,X5] :
( sum(X0,X2,X5)
| ~ rdn_translate(X5,rdn_neg(X4))
| ~ rdn_add_with_carry(rdnn(n0),X1,X4,X3)
| ~ rdn_positive_less(X1,X3)
| ~ rdn_translate(X2,rdn_neg(X3))
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(cnf_transformation,[status(thm)],[f723]) ).
fof(f743,plain,
! [X,Y,Z] :
( ( ~ difference(X,Y,Z)
| sum(Y,Z,X) )
& ( difference(X,Y,Z)
| ~ sum(Y,Z,X) ) ),
inference(NNF_transformation,[status(thm)],[f296]) ).
fof(f744,plain,
( ! [X,Y,Z] :
( ~ difference(X,Y,Z)
| sum(Y,Z,X) )
& ! [X,Y,Z] :
( difference(X,Y,Z)
| ~ sum(Y,Z,X) ) ),
inference(miniscoping,[status(thm)],[f743]) ).
fof(f745,plain,
! [X0,X1,X2] :
( difference(X2,X0,X1)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f744]) ).
fof(f747,plain,
! [C,D1,D2,RD,ID] :
( rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdnn(RD))
| ~ rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(n0))
| ~ rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(n0)) ),
inference(pre_NNF_transformation,[status(thm)],[f297]) ).
fof(f748,plain,
! [C,D1,D2,RD] :
( rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdnn(RD))
| ! [ID] :
( ~ rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(n0))
| ~ rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(n0)) ) ),
inference(miniscoping,[status(thm)],[f747]) ).
fof(f749,plain,
! [X0,X1,X2,X3,X4] :
( rdn_add_with_carry(rdnn(X3),rdnn(X0),rdnn(X1),rdnn(X4))
| ~ rdn_digit_add(rdnn(X2),rdnn(X3),rdnn(X4),rdnn(n0))
| ~ rdn_digit_add(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(n0)) ),
inference(cnf_transformation,[status(thm)],[f748]) ).
fof(f753,plain,
! [C,D1,D2,O2,RD,RO,ID,IC1,IC2,NC] :
( rdn_add_with_carry(rdnn(C),rdnn(D1),rdn(rdnn(D2),O2),rdn(rdnn(RD),RO))
| ~ rdn_non_zero(RO)
| ~ rdn_non_zero(O2)
| ~ rdn_add_with_carry(rdnn(NC),rdnn(n0),O2,RO)
| ~ rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(NC),rdnn(n0))
| ~ rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
| ~ rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) ),
inference(pre_NNF_transformation,[status(thm)],[f299]) ).
fof(f754,plain,
! [C,D1,D2,O2,RD,RO] :
( rdn_add_with_carry(rdnn(C),rdnn(D1),rdn(rdnn(D2),O2),rdn(rdnn(RD),RO))
| ~ rdn_non_zero(RO)
| ~ rdn_non_zero(O2)
| ! [NC] :
( ~ rdn_add_with_carry(rdnn(NC),rdnn(n0),O2,RO)
| ! [IC1,IC2] :
( ~ rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(NC),rdnn(n0))
| ! [ID] :
( ~ rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
| ~ rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) ) ) ) ),
inference(miniscoping,[status(thm)],[f753]) ).
fof(f755,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( rdn_add_with_carry(rdnn(X4),rdnn(X0),rdn(rdnn(X1),X8),rdn(rdnn(X5),X9))
| ~ rdn_non_zero(X9)
| ~ rdn_non_zero(X8)
| ~ rdn_add_with_carry(rdnn(X7),rdnn(n0),X8,X9)
| ~ rdn_digit_add(rdnn(X3),rdnn(X6),rdnn(X7),rdnn(n0))
| ~ rdn_digit_add(rdnn(X2),rdnn(X4),rdnn(X5),rdnn(X6))
| ~ rdn_digit_add(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3)) ),
inference(cnf_transformation,[status(thm)],[f754]) ).
fof(f761,plain,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f762,plain,
rdn_digit_add(rdnn(n0),rdnn(n1),rdnn(n1),rdnn(n0)),
inference(cnf_transformation,[status(thm)],[f303]) ).
fof(f763,plain,
rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(n2),rdnn(n0)),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f771,plain,
rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0)),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f778,plain,
rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(n8),rdnn(n0)),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f781,plain,
rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(n2),rdnn(n0)),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f841,plain,
rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(n8),rdnn(n0)),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f861,plain,
! [X] : ~ difference(nn127,n1,X),
inference(pre_NNF_transformation,[status(thm)],[f403]) ).
fof(f862,plain,
! [X0] : ~ difference(nn127,n1,X0),
inference(cnf_transformation,[status(thm)],[f861]) ).
fof(f1078,plain,
! [X0,X1] :
( rdn_add_with_carry(rdnn(n0),rdnn(X0),rdnn(X1),rdnn(n1))
| ~ rdn_digit_add(rdnn(X0),rdnn(X1),rdnn(n1),rdnn(n0)) ),
inference(resolution,[status(thm)],[f771,f749]) ).
fof(f1343,definition,
( sQ13_spl
<=> rdn_non_zero(rdnn(n1)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1345,plain,
( sQ13_spl
| ~ rdn_non_zero(rdnn(n1)) ),
inference(component_clause,[status(thm)],[f1343]) ).
fof(f3865,plain,
rdn_add_with_carry(rdnn(n0),rdnn(n0),rdnn(n1),rdnn(n1)),
inference(resolution,[status(thm)],[f1078,f762]) ).
fof(f3952,plain,
( sQ13_spl
| ~ rdn_non_zero_digit(rdnn(n1)) ),
inference(resolution,[status(thm)],[f1345,f690]) ).
fof(f3953,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3952,f660]) ).
fof(f3954,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f3953]) ).
fof(f8547,plain,
! [X0,X1,X2,X3,X4,X5] :
( difference(X5,X0,X2)
| ~ rdn_translate(X5,rdn_neg(X4))
| ~ rdn_add_with_carry(rdnn(n0),X1,X4,X3)
| ~ rdn_positive_less(X1,X3)
| ~ rdn_translate(X2,rdn_neg(X3))
| ~ rdn_translate(X0,rdn_pos(X1)) ),
inference(resolution,[status(thm)],[f724,f745]) ).
fof(f8561,plain,
! [X0,X1,X2,X3] :
( ~ rdn_translate(nn127,rdn_neg(X3))
| ~ rdn_add_with_carry(rdnn(n0),X0,X3,X2)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_neg(X2))
| ~ rdn_translate(n1,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f8547,f862]) ).
fof(f8563,plain,
! [X0,X1,X2] :
( ~ rdn_add_with_carry(rdnn(n0),X0,rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))),X2)
| ~ rdn_positive_less(X0,X2)
| ~ rdn_translate(X1,rdn_neg(X2))
| ~ rdn_translate(n1,rdn_pos(X0)) ),
inference(resolution,[status(thm)],[f8561,f658]) ).
fof(f8564,plain,
! [X0,X1] :
( ~ rdn_add_with_carry(rdnn(n0),rdnn(n1),rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))),X1)
| ~ rdn_positive_less(rdnn(n1),X1)
| ~ rdn_translate(X0,rdn_neg(X1)) ),
inference(resolution,[status(thm)],[f8563,f405]) ).
fof(f8614,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ rdn_non_zero(X2)
| ~ rdn_non_zero(rdn(rdnn(n2),rdnn(n1)))
| ~ rdn_add_with_carry(rdnn(X6),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X2)
| ~ rdn_digit_add(rdnn(X4),rdnn(X5),rdnn(X6),rdnn(n0))
| ~ rdn_digit_add(rdnn(X3),rdnn(n0),rdnn(X1),rdnn(X5))
| ~ rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(X3),rdnn(X4))
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(X1),X2))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f8564,f755]) ).
fof(f8615,definition,
! [X0,X1,X2,X3,X4,X5,X6] :
( sQ519_spl
<=> ( ~ rdn_non_zero(X2)
| ~ rdn_add_with_carry(rdnn(X6),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X2)
| ~ rdn_digit_add(rdnn(X4),rdnn(X5),rdnn(X6),rdnn(n0))
| ~ rdn_digit_add(rdnn(X3),rdnn(n0),rdnn(X1),rdnn(X5))
| ~ rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(X3),rdnn(X4))
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(X1),X2))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(X1),X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition]) ).
fof(f8616,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ519_spl
| ~ rdn_non_zero(X2)
| ~ rdn_add_with_carry(rdnn(X6),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X2)
| ~ rdn_digit_add(rdnn(X4),rdnn(X5),rdnn(X6),rdnn(n0))
| ~ rdn_digit_add(rdnn(X3),rdnn(n0),rdnn(X1),rdnn(X5))
| ~ rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(X3),rdnn(X4))
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(X1),X2))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(X1),X2))) ),
inference(component_clause,[status(thm)],[f8615]) ).
fof(f8618,definition,
( sQ520_spl
<=> rdn_non_zero(rdn(rdnn(n2),rdnn(n1))) ),
introduced(definition,[new_symbols(definition,[sQ520_spl])],[split_symbol_definition]) ).
fof(f8620,plain,
( sQ520_spl
| ~ rdn_non_zero(rdn(rdnn(n2),rdnn(n1))) ),
inference(component_clause,[status(thm)],[f8618]) ).
fof(f8621,plain,
( ~ sQ520_spl
| sQ519_spl ),
inference(split_clause,[status(thm)],[f8614,f8615,f8618]) ).
fof(f8622,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ519_spl
| ~ rdn_non_zero(X2)
| ~ rdn_add_with_carry(rdnn(X6),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X2)
| ~ rdn_digit_add(rdnn(X4),rdnn(X5),rdnn(X6),rdnn(n0))
| ~ rdn_digit_add(rdnn(X3),rdnn(n0),rdnn(X1),rdnn(X5))
| ~ rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(X3),rdnn(X4))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(X1),X2))) ),
inference(forward_subsumption_resolution,[status(thm)],[f8616,f688]) ).
fof(f8623,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ519_spl
| ~ rdn_non_zero(X2)
| ~ rdn_add_with_carry(rdnn(X4),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X2)
| ~ rdn_digit_add(rdnn(n0),rdnn(X3),rdnn(X4),rdnn(n0))
| ~ rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(X1),rdnn(X3))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(X1),X2))) ),
inference(resolution,[status(thm)],[f8622,f778]) ).
fof(f8624,plain,
! [X0,X1,X2] :
( ~ sQ519_spl
| ~ rdn_non_zero(X1)
| ~ rdn_add_with_carry(rdnn(X2),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X1)
| ~ rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(X2),rdnn(n0))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),X1))) ),
inference(resolution,[status(thm)],[f8623,f841]) ).
fof(f8625,plain,
! [X0,X1] :
( ~ sQ519_spl
| ~ rdn_non_zero(X1)
| ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X1)
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),X1))) ),
inference(resolution,[status(thm)],[f8624,f761]) ).
fof(f8800,plain,
( sQ520_spl
| ~ rdn_non_zero(rdnn(n1)) ),
inference(resolution,[status(thm)],[f8620,f693]) ).
fof(f8801,plain,
( sQ520_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f8800,f1343,f8618]) ).
fof(f12445,plain,
( ~ sQ519_spl
| ~ rdn_non_zero(rdn(rdnn(n2),rdnn(n1)))
| ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),rdn(rdnn(n2),rdnn(n1))) ),
inference(resolution,[status(thm)],[f659,f8625]) ).
fof(f12458,definition,
( sQ658_spl
<=> rdn_add_with_carry(rdnn(n0),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),rdn(rdnn(n2),rdnn(n1))) ),
introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition]) ).
fof(f12460,plain,
( sQ658_spl
| ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),rdn(rdnn(n2),rdnn(n1))) ),
inference(component_clause,[status(thm)],[f12458]) ).
fof(f12461,plain,
( ~ sQ519_spl
| ~ sQ520_spl
| ~ sQ658_spl ),
inference(split_clause,[status(thm)],[f12445,f12458,f8618,f8615]) ).
fof(f12683,plain,
! [X0,X1,X2,X3] :
( sQ658_spl
| ~ rdn_non_zero(rdnn(n1))
| ~ rdn_non_zero(rdnn(n1))
| ~ rdn_add_with_carry(rdnn(X3),rdnn(n0),rdnn(n1),rdnn(n1))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X3),rdnn(n0))
| ~ rdn_digit_add(rdnn(X0),rdnn(n0),rdnn(n2),rdnn(X2))
| ~ rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(X0),rdnn(X1)) ),
inference(resolution,[status(thm)],[f12460,f755]) ).
fof(f12684,definition,
! [X0,X1,X2,X3] :
( sQ663_spl
<=> ( ~ rdn_add_with_carry(rdnn(X3),rdnn(n0),rdnn(n1),rdnn(n1))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X3),rdnn(n0))
| ~ rdn_digit_add(rdnn(X0),rdnn(n0),rdnn(n2),rdnn(X2))
| ~ rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(X0),rdnn(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ663_spl])],[split_symbol_definition]) ).
fof(f12685,plain,
! [X0,X1,X2,X3] :
( ~ sQ663_spl
| ~ rdn_add_with_carry(rdnn(X3),rdnn(n0),rdnn(n1),rdnn(n1))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X3),rdnn(n0))
| ~ rdn_digit_add(rdnn(X0),rdnn(n0),rdnn(n2),rdnn(X2))
| ~ rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(X0),rdnn(X1)) ),
inference(component_clause,[status(thm)],[f12684]) ).
fof(f12687,plain,
( sQ658_spl
| ~ sQ13_spl
| sQ663_spl ),
inference(split_clause,[status(thm)],[f12683,f12684,f1343,f12458]) ).
fof(f13506,plain,
! [X0,X1] :
( ~ sQ663_spl
| ~ rdn_add_with_carry(rdnn(X1),rdnn(n0),rdnn(n1),rdnn(n1))
| ~ rdn_digit_add(rdnn(n0),rdnn(X0),rdnn(X1),rdnn(n0))
| ~ rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(n2),rdnn(X0)) ),
inference(resolution,[status(thm)],[f12685,f763]) ).
fof(f13509,plain,
! [X0] :
( ~ sQ663_spl
| ~ rdn_add_with_carry(rdnn(X0),rdnn(n0),rdnn(n1),rdnn(n1))
| ~ rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(X0),rdnn(n0)) ),
inference(resolution,[status(thm)],[f13506,f781]) ).
fof(f13510,plain,
( ~ sQ663_spl
| ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdnn(n1),rdnn(n1)) ),
inference(resolution,[status(thm)],[f13509,f761]) ).
fof(f13511,plain,
( ~ sQ663_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13510,f3865]) ).
fof(f13512,plain,
~ sQ663_spl,
inference(contradiction_clause,[status(thm)],[f13511]) ).
fof(f13513,plain,
$false,
inference(sat_refutation,[status(thm)],[f3954,f8621,f8801,f12461,f12687,f13512]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM339+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.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 : Mon Sep 21 02:23:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 96.01/12.55 % Refutation found
% 96.01/12.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 96.01/12.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 34.63/13.85 % Elapsed time: 13.270233 seconds
% 34.63/13.85 % CPU time: 93.808422 seconds
% 34.63/13.85 % Total memory used: 660.862 MB
% 34.63/13.85 % Net memory used: 605.452 MB
%------------------------------------------------------------------------------