%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM473+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 01:40:39 PM UTC 2026
% Result : Theorem 21.34s 3.17s
% Output : CNFRefutation 21.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 32
% Syntax : Number of formulae : 129 ( 27 unt; 21 def)
% Number of atoms : 386 ( 85 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 420 ( 163 ~; 171 |; 54 &)
% ( 23 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 20 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 78 ( 70 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& W1 != W2
& W0 != sz00 )
=> ( sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W0,W1)
& W0 != sz00 )
=> ! [W2] :
( W2 = sdtsldt0(W1,W0)
<=> ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,hypothesis,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xl) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
( doDivides0(xl,sdtpldt0(xm,xn))
& ? [W0] :
( sdtpldt0(xm,xn) = sdtasdt0(xl,W0)
& aNaturalNumber0(W0) )
& doDivides0(xl,xm)
& ? [W0] :
( xm = sdtasdt0(xl,W0)
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
xl != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
( xp = sdtsldt0(xm,xl)
& xm = sdtasdt0(xl,xp)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
( xq = sdtsldt0(sdtpldt0(xm,xn),xl)
& sdtpldt0(xm,xn) = sdtasdt0(xl,xq)
& aNaturalNumber0(xq) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( sdtlseqdt0(xm,sdtpldt0(xm,xn))
& ? [W0] :
( sdtpldt0(xm,W0) = sdtpldt0(xm,xn)
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,conjecture,
( sdtlseqdt0(xp,xq)
| ? [W0] :
( sdtpldt0(xp,W0) = xq
& aNaturalNumber0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
~ ( sdtlseqdt0(xp,xq)
| ? [W0] :
( sdtpldt0(xp,W0) = xq
& aNaturalNumber0(W0) ) ),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f50,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f51,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f97,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f98,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f101,plain,
! [W0,W1] :
( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f102,plain,
! [X0,X1] :
( X1 != X0
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f109,plain,
! [W0,W1,W2] :
( ( sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))
& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) )
| ~ sdtlseqdt0(W1,W2)
| W1 = W2
| W0 = sz00
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f111,plain,
! [X0,X1,X2] :
( sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f123,plain,
! [W0,W1] :
( ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f124,plain,
! [W0,W1] :
( ( ( ! [W2] :
( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2) )
| doDivides0(W0,W1) )
& ( ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) )
| ~ doDivides0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [W0,W1] :
( ( ( ! [W2] :
( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2) )
| doDivides0(W0,W1) )
& ( ( W1 = sdtasdt0(W0,sK1_skl(W1,W0))
& aNaturalNumber0(sK1_skl(W1,W0)) )
| ~ doDivides0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f124]) ).
fof(f128,plain,
! [X0,X1,X2] :
( X1 != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f129,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtsldt0(W1,W0)
<=> ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) )
| ~ doDivides0(W0,W1)
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f130,plain,
! [W0,W1] :
( ! [W2] :
( ( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2)
| W2 = sdtsldt0(W1,W0) )
& ( ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) )
| W2 != sdtsldt0(W1,W0) ) )
| ~ doDivides0(W0,W1)
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f129]) ).
fof(f131,plain,
! [W0,W1] :
( ( ! [W2] :
( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2)
| W2 = sdtsldt0(W1,W0) )
& ! [W2] :
( ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) )
| W2 != sdtsldt0(W1,W0) ) )
| ~ doDivides0(W0,W1)
| W0 = sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f133,plain,
! [X0,X1,X2] :
( X1 = sdtasdt0(X0,X2)
| X2 != sdtsldt0(X1,X0)
| ~ doDivides0(X0,X1)
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f139,plain,
aNaturalNumber0(xl),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f140,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f142,plain,
( doDivides0(xl,sdtpldt0(xm,xn))
& sdtpldt0(xm,xn) = sdtasdt0(xl,sK3_skl)
& aNaturalNumber0(sK3_skl)
& doDivides0(xl,xm)
& xm = sdtasdt0(xl,sK2_skl)
& aNaturalNumber0(sK2_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(W0,sK2_skl),skolemize(W0,sK3_skl)],[f35]) ).
fof(f146,plain,
aNaturalNumber0(sK3_skl),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f148,plain,
doDivides0(xl,sdtpldt0(xm,xn)),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f149,plain,
xl != sz00,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f150,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f151,plain,
xm = sdtasdt0(xl,xp),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f152,plain,
xp = sdtsldt0(xm,xl),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f153,plain,
aNaturalNumber0(xq),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f154,plain,
sdtpldt0(xm,xn) = sdtasdt0(xl,xq),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f155,plain,
xq = sdtsldt0(sdtpldt0(xm,xn),xl),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f156,plain,
( sdtlseqdt0(xm,sdtpldt0(xm,xn))
& sdtpldt0(xm,sK4_skl) = sdtpldt0(xm,xn)
& aNaturalNumber0(sK4_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(W0,sK4_skl)],[f39]) ).
fof(f157,plain,
aNaturalNumber0(sK4_skl),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f159,plain,
sdtlseqdt0(xm,sdtpldt0(xm,xn)),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f160,plain,
( ~ sdtlseqdt0(xp,xq)
& ! [W0] :
( sdtpldt0(xp,W0) != xq
| ~ aNaturalNumber0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f162,plain,
~ sdtlseqdt0(xp,xq),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f163,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f102]) ).
fof(f164,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f163]) ).
fof(f200,definition,
( sQ4_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( sQ4_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f200]) ).
fof(f206,definition,
( sQ6_spl
<=> aNaturalNumber0(xq) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f208,plain,
( sQ6_spl
| ~ aNaturalNumber0(xq) ),
inference(component_clause,[status(thm)],[f206]) ).
fof(f212,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f208,f153]) ).
fof(f213,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f212]) ).
fof(f214,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f202,f150]) ).
fof(f215,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f214]) ).
fof(f216,plain,
( sdtlseqdt0(xq,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xq) ),
inference(resolution,[status(thm)],[f103,f162]) ).
fof(f219,definition,
( sQ7_spl
<=> sdtlseqdt0(xq,xp) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f222,plain,
( sQ7_spl
| ~ sQ4_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f216,f206,f200,f219]) ).
fof(f235,definition,
( sQ10_spl
<=> xp = xq ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f254,definition,
( sQ13_spl
<=> aNaturalNumber0(xl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( sQ13_spl
| ~ aNaturalNumber0(xl) ),
inference(component_clause,[status(thm)],[f254]) ).
fof(f261,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f256,f139]) ).
fof(f262,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f261]) ).
fof(f391,definition,
( sQ36_spl
<=> xl = sz00 ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f392,plain,
( ~ sQ36_spl
| xl = sz00 ),
inference(component_clause,[status(thm)],[f391]) ).
fof(f408,plain,
( ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f392,f149]) ).
fof(f409,plain,
~ sQ36_spl,
inference(contradiction_clause,[status(thm)],[f408]) ).
fof(f507,definition,
( sQ51_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f509,plain,
( sQ51_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f727,plain,
! [X0] :
( sdtlseqdt0(sdtasdt0(xl,X0),xm)
| ~ sdtlseqdt0(X0,xp)
| X0 = xp
| xl = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xl) ),
inference(paramodulation,[status(thm)],[f151,f111]) ).
fof(f736,definition,
! [X0] :
( sQ77_spl
<=> ( sdtlseqdt0(sdtasdt0(xl,X0),xm)
| ~ sdtlseqdt0(X0,xp)
| X0 = xp
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f737,plain,
! [X0] :
( ~ sQ77_spl
| sdtlseqdt0(sdtasdt0(xl,X0),xm)
| ~ sdtlseqdt0(X0,xp)
| X0 = xp
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f736]) ).
fof(f739,plain,
( sQ36_spl
| ~ sQ4_spl
| sQ77_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f727,f254,f736,f200,f391]) ).
fof(f961,plain,
( ~ aNaturalNumber0(xp)
| doDivides0(xl,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xl) ),
inference(resolution,[status(thm)],[f128,f151]) ).
fof(f981,definition,
( sQ100_spl
<=> doDivides0(xl,xm) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f984,plain,
( ~ sQ4_spl
| sQ100_spl
| ~ sQ51_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f961,f254,f507,f981,f200]) ).
fof(f988,definition,
! [X0] :
( sQ102_spl
<=> ( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f989,plain,
! [X0] :
( ~ sQ102_spl
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f988]) ).
fof(f1016,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f509,f140]) ).
fof(f1017,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f1016]) ).
fof(f1059,definition,
( sQ111_spl
<=> aNaturalNumber0(sdtpldt0(xm,xn)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1062,definition,
( sQ112_spl
<=> doDivides0(xl,sdtpldt0(xm,xn)) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1064,plain,
( sQ112_spl
| ~ doDivides0(xl,sdtpldt0(xm,xn)) ),
inference(component_clause,[status(thm)],[f1062]) ).
fof(f1138,plain,
! [X0] :
( xm = sdtasdt0(xl,X0)
| X0 != xp
| ~ doDivides0(xl,xm)
| xl = sz00
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xl) ),
inference(paramodulation,[status(thm)],[f152,f133]) ).
fof(f1152,definition,
! [X0] :
( sQ127_spl
<=> ( xm = sdtasdt0(xl,X0)
| X0 != xp ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1153,plain,
! [X0] :
( ~ sQ127_spl
| xm = sdtasdt0(xl,X0)
| X0 != xp ),
inference(component_clause,[status(thm)],[f1152]) ).
fof(f1155,plain,
( sQ127_spl
| ~ sQ100_spl
| sQ36_spl
| ~ sQ51_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1138,f254,f507,f391,f981,f1152]) ).
fof(f1187,plain,
! [X0] :
( ~ sQ102_spl
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f989]) ).
fof(f1220,plain,
( ~ sQ102_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f150,f1187]) ).
fof(f1229,plain,
~ sQ102_spl,
inference(contradiction_clause,[status(thm)],[f1220]) ).
fof(f1234,definition,
( sQ135_spl
<=> aNaturalNumber0(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f1236,plain,
( sQ135_spl
| ~ aNaturalNumber0(sK4_skl) ),
inference(component_clause,[status(thm)],[f1234]) ).
fof(f1242,plain,
( sQ135_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1236,f157]) ).
fof(f1243,plain,
sQ135_spl,
inference(contradiction_clause,[status(thm)],[f1242]) ).
fof(f1244,plain,
( aNaturalNumber0(sdtpldt0(xm,xn))
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xl) ),
inference(paramodulation,[status(thm)],[f154,f51]) ).
fof(f1247,plain,
( sQ111_spl
| ~ sQ6_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1244,f254,f206,f1059]) ).
fof(f1248,definition,
( sQ136_spl
<=> aNaturalNumber0(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1250,plain,
( sQ136_spl
| ~ aNaturalNumber0(sK3_skl) ),
inference(component_clause,[status(thm)],[f1248]) ).
fof(f1269,plain,
( sQ136_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1250,f146]) ).
fof(f1270,plain,
sQ136_spl,
inference(contradiction_clause,[status(thm)],[f1269]) ).
fof(f1315,plain,
( sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1064,f148]) ).
fof(f1316,plain,
sQ112_spl,
inference(contradiction_clause,[status(thm)],[f1315]) ).
fof(f1414,plain,
( sdtpldt0(xm,xn) = xm
| ~ sdtlseqdt0(sdtpldt0(xm,xn),xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(sdtpldt0(xm,xn)) ),
inference(resolution,[status(thm)],[f98,f159]) ).
fof(f1432,definition,
( sQ148_spl
<=> sdtlseqdt0(sdtpldt0(xm,xn),xm) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1435,definition,
( sQ149_spl
<=> sdtpldt0(xm,xn) = xm ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1436,plain,
( ~ sQ149_spl
| sdtpldt0(xm,xn) = xm ),
inference(component_clause,[status(thm)],[f1435]) ).
fof(f1438,plain,
( sQ149_spl
| ~ sQ148_spl
| ~ sQ51_spl
| ~ sQ111_spl ),
inference(split_clause,[status(thm)],[f1414,f1059,f507,f1432,f1435]) ).
fof(f1568,definition,
( sQ160_spl
<=> xp = xp ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1570,plain,
( sQ160_spl
| xp != xp ),
inference(component_clause,[status(thm)],[f1568]) ).
fof(f1575,plain,
( sQ160_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1570]) ).
fof(f1576,plain,
sQ160_spl,
inference(contradiction_clause,[status(thm)],[f1575]) ).
fof(f1590,plain,
( ~ sQ127_spl
| xm = sdtpldt0(xm,xn)
| xq != xp ),
inference(paramodulation,[status(thm)],[f154,f1153]) ).
fof(f1602,plain,
( ~ sQ127_spl
| sQ149_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1590,f235,f1435,f1152]) ).
fof(f1819,plain,
( ~ sQ149_spl
| xq = sdtsldt0(xm,xl) ),
inference(forward_demodulation,[status(thm)],[f1436,f155]) ).
fof(f1827,plain,
( ~ sQ149_spl
| ~ sdtlseqdt0(xp,xp) ),
inference(backward_demodulation,[status(thm)],[f1833,f162]) ).
fof(f1833,plain,
( ~ sQ149_spl
| xq = xp ),
inference(forward_demodulation,[status(thm)],[f152,f1819]) ).
fof(f1851,plain,
( ~ sQ149_spl
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f1827,f164]) ).
fof(f1861,plain,
( ~ sQ149_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1851,f200,f1435]) ).
fof(f3690,definition,
( sQ349_spl
<=> aNaturalNumber0(sdtasdt0(xl,xp)) ),
introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition]) ).
fof(f3692,plain,
( sQ349_spl
| ~ aNaturalNumber0(sdtasdt0(xl,xp)) ),
inference(component_clause,[status(thm)],[f3690]) ).
fof(f3919,plain,
( sQ349_spl
| ~ aNaturalNumber0(xm) ),
inference(forward_demodulation,[status(thm)],[f151,f3692]) ).
fof(f3920,plain,
( sQ349_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3919,f140]) ).
fof(f3921,plain,
sQ349_spl,
inference(contradiction_clause,[status(thm)],[f3920]) ).
fof(f6397,plain,
( ~ sQ77_spl
| sdtlseqdt0(sdtpldt0(xm,xn),xm)
| ~ sdtlseqdt0(xq,xp)
| xq = xp
| ~ aNaturalNumber0(xq) ),
inference(paramodulation,[status(thm)],[f154,f737]) ).
fof(f6427,plain,
( ~ sQ77_spl
| sQ148_spl
| ~ sQ7_spl
| sQ10_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f6397,f206,f235,f219,f1432,f736]) ).
fof(f6428,plain,
$false,
inference(sat_refutation,[status(thm)],[f213,f215,f222,f262,f409,f739,f984,f1017,f1155,f1229,f1243,f1247,f1270,f1316,f1438,f1576,f1602,f1861,f3921,f6427]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM473+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 02:36:22 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 21.34/3.17 % Refutation found
% 21.34/3.17 % SZS status Theorem for theBenchmark: Theorem is valid
% 21.34/3.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.34/3.21 % Elapsed time: 2.824710 seconds
% 21.34/3.21 % CPU time: 21.925615 seconds
% 21.34/3.21 % Total memory used: 193.325 MB
% 21.34/3.21 % Net memory used: 184.505 MB
%------------------------------------------------------------------------------