%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM448+5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:34 PM UTC 2026
% Result : Theorem 0.17s 10.62s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 6
% Syntax : Number of formulae : 83 ( 6 unt; 2 def)
% Number of atoms : 512 ( 123 equ)
% Maximal formula atoms : 35 ( 6 avg)
% Number of connectives : 647 ( 218 ~; 225 |; 174 &)
% ( 14 <=>; 14 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-2 aty)
% Number of variables : 142 ( 101 !; 41 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
aInteger0(sz10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [W0] :
( aInteger0(W0)
=> aInteger0(smndt0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0] :
( aInteger0(W0)
=> ( ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0) )
<=> ( W0 != smndt0(sz10)
& W0 != sz10 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,conjecture,
( ! [W0] :
( aInteger0(W0)
=> ( ( ? [W1] :
( isPrime0(W1)
& ( aDivisorOf0(W1,W0)
| ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) )
=> ( aElementOf0(W0,sbsmnsldt0(xS))
& ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) ) )
& ( ( aElementOf0(W0,sbsmnsldt0(xS))
| ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) )
=> ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0)
& ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ) )
=> ( ( ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( ( ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& aSet0(stldt0(sbsmnsldt0(xS))) )
=> ( stldt0(sbsmnsldt0(xS)) = cS2076
| ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( W0 = smndt0(sz10)
| W0 = sz10 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
~ ( ! [W0] :
( aInteger0(W0)
=> ( ( ? [W1] :
( isPrime0(W1)
& ( aDivisorOf0(W1,W0)
| ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) )
=> ( aElementOf0(W0,sbsmnsldt0(xS))
& ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) ) )
& ( ( aElementOf0(W0,sbsmnsldt0(xS))
| ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) )
=> ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0)
& ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ) )
=> ( ( ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( ( ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& aSet0(stldt0(sbsmnsldt0(xS))) )
=> ( stldt0(sbsmnsldt0(xS)) = cS2076
| ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( W0 = smndt0(sz10)
| W0 = sz10 ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f43]) ).
fof(f49,plain,
aInteger0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f50,plain,
! [W0] :
( aInteger0(smndt0(W0))
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f51,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f108,plain,
! [W0] :
( ( ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0) )
<=> ( W0 != smndt0(sz10)
& W0 != sz10 ) )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f109,plain,
! [W0] :
( ( ( W0 = smndt0(sz10)
| W0 = sz10
| ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0) ) )
& ( ( W0 != smndt0(sz10)
& W0 != sz10 )
| ! [W1] :
( ~ isPrime0(W1)
| ~ aDivisorOf0(W1,W0) ) ) )
| ~ aInteger0(W0) ),
inference(NNF_transformation,[status(thm)],[f108]) ).
fof(f110,plain,
! [W0] :
( ( ( W0 = smndt0(sz10)
| W0 = sz10
| ( isPrime0(sK1_skl(W0))
& aDivisorOf0(sK1_skl(W0),W0) ) )
& ( ( W0 != smndt0(sz10)
& W0 != sz10 )
| ! [W1] :
( ~ isPrime0(W1)
| ~ aDivisorOf0(W1,W0) ) ) )
| ~ aInteger0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W1,sK1_skl(W0))],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( X0 != sz10
| ~ isPrime0(X1)
| ~ aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( X0 != smndt0(sz10)
| ~ isPrime0(X1)
| ~ aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f113,plain,
! [X0] :
( X0 = smndt0(sz10)
| X0 = sz10
| aDivisorOf0(sK1_skl(X0),X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f114,plain,
! [X0] :
( X0 = smndt0(sz10)
| X0 = sz10
| isPrime0(sK1_skl(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f247,plain,
( stldt0(sbsmnsldt0(xS)) != cS2076
& ? [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<~> ( W0 = smndt0(sz10)
| W0 = sz10 ) )
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( ( ( ( aElementOf0(W0,sbsmnsldt0(xS))
& ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) )
| ! [W1] :
( ~ isPrime0(W1)
| ( ~ aDivisorOf0(W1,W0)
& ( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1) ) ) ) )
& ( ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0)
& ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) ) ) ) )
| ~ aInteger0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f248,definition,
! [W0] :
( sP2_prd(W0)
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f249,definition,
! [W0,W1] :
( sP3_prd(W1,W0)
<=> ( ~ isPrime0(W1)
| ( ~ aDivisorOf0(W1,W0)
& ( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f250,plain,
( stldt0(sbsmnsldt0(xS)) != cS2076
& ? [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<~> ( W0 = smndt0(sz10)
| W0 = sz10 ) )
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( ( ( ( aElementOf0(W0,sbsmnsldt0(xS))
& ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) )
| ! [W1] : sP3_prd(W1,W0) )
& ( ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0)
& ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| sP2_prd(W0) ) )
| ~ aInteger0(W0) ) ),
inference(formula_renaming,[status(thm)],[f247,f249,f248]) ).
fof(f251,plain,
( stldt0(sbsmnsldt0(xS)) != cS2076
& ? [W0] :
( ( ( W0 != smndt0(sz10)
& W0 != sz10 )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( W0 = smndt0(sz10)
| W0 = sz10
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ) )
& ! [W0] :
( ( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( ( ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) )
| ~ aInteger0(W0)
| aElementOf0(W0,sbsmnsldt0(xS)) )
& ( ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( ( ( ( aElementOf0(W0,sbsmnsldt0(xS))
& ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) )
| ! [W1] : sP3_prd(W1,W0) )
& ( ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0)
& ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| sP2_prd(W0) ) )
| ~ aInteger0(W0) ) ),
inference(NNF_transformation,[status(thm)],[f250]) ).
fof(f252,plain,
( stldt0(sbsmnsldt0(xS)) != cS2076
& ? [W0] :
( ( ( W0 != smndt0(sz10)
& W0 != sz10 )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( W0 = smndt0(sz10)
| W0 = sz10
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) ) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) )
| ~ aInteger0(W0)
| aElementOf0(W0,sbsmnsldt0(xS)) )
& ! [W0] :
( ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( ( ( ( aElementOf0(W0,sbsmnsldt0(xS))
& ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) ) )
| ! [W1] : sP3_prd(W1,W0) )
& ( ? [W1] :
( isPrime0(W1)
& aDivisorOf0(W1,W0)
& ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| sP2_prd(W0) ) )
| ~ aInteger0(W0) ) ),
inference(miniscoping,[status(thm)],[f251]) ).
fof(f253,plain,
( stldt0(sbsmnsldt0(xS)) != cS2076
& ( ( sK22_skl != smndt0(sz10)
& sK22_skl != sz10 )
| ~ aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS))) )
& ( sK22_skl = smndt0(sz10)
| sK22_skl = sz10
| aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) )
| ~ aInteger0(W0)
| aElementOf0(W0,sbsmnsldt0(xS)) )
& ! [W0] :
( ( aElementOf0(W0,sK21_skl(W0))
& aElementOf0(sK21_skl(W0),xS)
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( ( ( ( aElementOf0(W0,sbsmnsldt0(xS))
& aElementOf0(W0,sK20_skl(W0))
& aElementOf0(sK20_skl(W0),xS) )
| ! [W1] : sP3_prd(W1,W0) )
& ( ( isPrime0(sK18_skl(W0))
& aDivisorOf0(sK18_skl(W0),W0)
& sdtasdt0(sK18_skl(W0),sK19_skl(W0)) = W0
& aInteger0(sK19_skl(W0))
& sK18_skl(W0) != sz00
& aInteger0(sK18_skl(W0)) )
| sP2_prd(W0) ) )
| ~ aInteger0(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl]),skolemize(W1,sK18_skl(W0)),skolemize(W2,sK19_skl(W0)),skolemize(W1,sK20_skl(W0)),skolemize(W1,sK21_skl(W0)),skolemize(W0,sK22_skl)],[f252]) ).
fof(f258,plain,
! [X0] :
( aDivisorOf0(sK18_skl(X0),X0)
| sP2_prd(X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f259,plain,
! [X0] :
( isPrime0(sK18_skl(X0))
| sP2_prd(X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f262,plain,
! [X0,X1] :
( aElementOf0(X0,sbsmnsldt0(xS))
| sP3_prd(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f269,plain,
! [X0] :
( aInteger0(X0)
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f270,plain,
! [X0] :
( ~ aElementOf0(X0,sbsmnsldt0(xS))
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f271,plain,
! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
| ~ aInteger0(X0)
| aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f272,plain,
( sK22_skl = smndt0(sz10)
| sK22_skl = sz10
| aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f273,plain,
( sK22_skl != sz10
| ~ aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f274,plain,
( sK22_skl != smndt0(sz10)
| ~ aElementOf0(sK22_skl,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f287,plain,
! [W0] :
( ( aElementOf0(W0,sbsmnsldt0(xS))
| ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
| sP2_prd(W0) )
& ( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) ) )
| ~ sP2_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f248]) ).
fof(f288,plain,
( ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
| sP2_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) ) )
| ~ sP2_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f287]) ).
fof(f289,plain,
( ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ( aElementOf0(W0,sK23_skl(W0))
& aElementOf0(sK23_skl(W0),xS) )
| sP2_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) ) )
| ~ sP2_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W1,sK23_skl(W0))],[f288]) ).
fof(f291,plain,
! [X0] :
( ~ aElementOf0(X0,sbsmnsldt0(xS))
| ~ sP2_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f294,plain,
! [W0,W1] :
( ( ( isPrime0(W1)
& ( aDivisorOf0(W1,W0)
| ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) )
| sP3_prd(W1,W0) )
& ( ~ isPrime0(W1)
| ( ~ aDivisorOf0(W1,W0)
& ( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1) ) )
| ~ sP3_prd(W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f249]) ).
fof(f295,plain,
( ! [W0,W1] :
( ( isPrime0(W1)
& ( aDivisorOf0(W1,W0)
| ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) )
| sP3_prd(W1,W0) )
& ! [W0,W1] :
( ~ isPrime0(W1)
| ( ~ aDivisorOf0(W1,W0)
& ( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1) ) )
| ~ sP3_prd(W1,W0) ) ),
inference(miniscoping,[status(thm)],[f294]) ).
fof(f296,plain,
( ! [W0,W1] :
( ( isPrime0(W1)
& ( aDivisorOf0(W1,W0)
| ( sdtasdt0(W1,sK24_skl(W1,W0)) = W0
& aInteger0(sK24_skl(W1,W0))
& W1 != sz00
& aInteger0(W1) ) ) )
| sP3_prd(W1,W0) )
& ! [W0,W1] :
( ~ isPrime0(W1)
| ( ~ aDivisorOf0(W1,W0)
& ( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1) ) )
| ~ sP3_prd(W1,W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W2,sK24_skl(W1,W0))],[f295]) ).
fof(f298,plain,
! [X0,X1] :
( ~ isPrime0(X0)
| ~ aDivisorOf0(X0,X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f306,plain,
! [X0] :
( ~ isPrime0(X0)
| ~ aDivisorOf0(X0,sz10)
| ~ aInteger0(sz10) ),
inference(destructive_equality_resolution,[status(thm)],[f111]) ).
fof(f307,plain,
! [X0] :
( ~ isPrime0(X0)
| ~ aDivisorOf0(X0,smndt0(sz10))
| ~ aInteger0(smndt0(sz10)) ),
inference(destructive_equality_resolution,[status(thm)],[f112]) ).
fof(f335,plain,
! [X0] :
( ~ isPrime0(X0)
| ~ aDivisorOf0(X0,sz10) ),
inference(forward_subsumption_resolution,[status(thm)],[f306,f49]) ).
fof(f336,plain,
( ~ isPrime0(sK18_skl(sz10))
| sP2_prd(sz10)
| ~ aInteger0(sz10) ),
inference(resolution,[status(thm)],[f258,f335]) ).
fof(f338,plain,
( ~ isPrime0(sK18_skl(sz10))
| sP2_prd(sz10) ),
inference(forward_subsumption_resolution,[status(thm)],[f336,f49]) ).
fof(f340,plain,
( sP2_prd(sz10)
| ~ aInteger0(sz10)
| sP2_prd(sz10) ),
inference(resolution,[status(thm)],[f338,f259]) ).
fof(f341,plain,
( ~ aInteger0(sz10)
| sP2_prd(sz10) ),
inference(duplicate_literals_removal,[status(thm)],[f340]) ).
fof(f342,plain,
sP2_prd(sz10),
inference(forward_subsumption_resolution,[status(thm)],[f341,f49]) ).
fof(f388,plain,
! [X0,X1] :
( ~ sP2_prd(X0)
| sP3_prd(X1,X0)
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f262,f291]) ).
fof(f390,plain,
! [X0,X1] :
( ~ isPrime0(X1)
| ~ aDivisorOf0(X1,X0)
| ~ sP2_prd(X0)
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f388,f298]) ).
fof(f398,plain,
( sP2_prd(smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ isPrime0(sK18_skl(smndt0(sz10)))
| ~ aInteger0(smndt0(sz10)) ),
inference(resolution,[status(thm)],[f307,f258]) ).
fof(f399,plain,
( sP2_prd(smndt0(sz10))
| ~ isPrime0(sK18_skl(smndt0(sz10)))
| ~ aInteger0(smndt0(sz10)) ),
inference(duplicate_literals_removal,[status(thm)],[f398]) ).
fof(f400,plain,
( sP2_prd(smndt0(sz10))
| ~ aInteger0(smndt0(sz10)) ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f259]) ).
fof(f517,plain,
! [X0] :
( ~ isPrime0(sK1_skl(X0))
| ~ sP2_prd(X0)
| ~ aInteger0(X0)
| X0 = smndt0(sz10)
| X0 = sz10
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f113,f390]) ).
fof(f519,plain,
! [X0] :
( ~ isPrime0(sK1_skl(X0))
| ~ sP2_prd(X0)
| X0 = smndt0(sz10)
| X0 = sz10
| ~ aInteger0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f517]) ).
fof(f520,plain,
! [X0] :
( ~ sP2_prd(X0)
| X0 = smndt0(sz10)
| X0 = sz10
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f519,f114]) ).
fof(f553,plain,
( sK22_skl != smndt0(sz10)
| aElementOf0(sK22_skl,sbsmnsldt0(xS))
| ~ aInteger0(sK22_skl) ),
inference(resolution,[status(thm)],[f271,f274]) ).
fof(f554,plain,
( sK22_skl != sz10
| aElementOf0(sK22_skl,sbsmnsldt0(xS))
| ~ aInteger0(sK22_skl) ),
inference(resolution,[status(thm)],[f271,f273]) ).
fof(f590,plain,
( ~ sP2_prd(sK22_skl)
| sK22_skl != sz10
| ~ aInteger0(sK22_skl) ),
inference(resolution,[status(thm)],[f554,f291]) ).
fof(f690,plain,
( ~ aElementOf0(sK22_skl,sbsmnsldt0(xS))
| sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(resolution,[status(thm)],[f272,f270]) ).
fof(f691,plain,
( aInteger0(sK22_skl)
| sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(resolution,[status(thm)],[f272,f269]) ).
fof(f704,plain,
( aInteger0(sK22_skl)
| sK22_skl = sz10
| aInteger0(sK22_skl)
| ~ aInteger0(sz10) ),
inference(paramodulation,[status(thm)],[f691,f51]) ).
fof(f709,plain,
( sK22_skl = sz10
| aInteger0(sK22_skl)
| ~ aInteger0(sz10) ),
inference(duplicate_literals_removal,[status(thm)],[f704]) ).
fof(f710,plain,
( sK22_skl = sz10
| aInteger0(sK22_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f709,f49]) ).
fof(f802,plain,
( ~ sP2_prd(sK22_skl)
| sK22_skl != smndt0(sz10)
| ~ aInteger0(sK22_skl) ),
inference(resolution,[status(thm)],[f553,f291]) ).
fof(f804,plain,
( ~ sP2_prd(sK22_skl)
| sK22_skl = sz10
| ~ aInteger0(sK22_skl)
| ~ sP2_prd(sK22_skl)
| ~ aInteger0(sK22_skl) ),
inference(resolution,[status(thm)],[f802,f520]) ).
fof(f805,plain,
( sK22_skl = sz10
| ~ sP2_prd(sK22_skl)
| ~ aInteger0(sK22_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f804]) ).
fof(f806,plain,
( sK22_skl = sz10
| ~ sP2_prd(sK22_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f805,f710]) ).
fof(f816,plain,
( ~ sP2_prd(sK22_skl)
| ~ aInteger0(sK22_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f590,f806]) ).
fof(f822,plain,
! [X0] :
( sP3_prd(X0,sK22_skl)
| ~ aInteger0(sK22_skl)
| sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(resolution,[status(thm)],[f690,f262]) ).
fof(f826,plain,
! [X0] :
( sP3_prd(X0,sK22_skl)
| sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(forward_subsumption_resolution,[status(thm)],[f822,f710]) ).
fof(f846,plain,
! [X0] :
( ~ isPrime0(X0)
| ~ aDivisorOf0(X0,sK22_skl)
| sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(resolution,[status(thm)],[f826,f298]) ).
fof(f973,plain,
( sK22_skl = smndt0(sz10)
| sK22_skl = sz10
| ~ aInteger0(sK22_skl)
| ~ isPrime0(sK1_skl(sK22_skl))
| sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(resolution,[status(thm)],[f846,f113]) ).
fof(f975,plain,
( ~ aInteger0(sK22_skl)
| ~ isPrime0(sK1_skl(sK22_skl))
| sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(duplicate_literals_removal,[status(thm)],[f973]) ).
fof(f976,plain,
( ~ aInteger0(sK22_skl)
| sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(forward_subsumption_resolution,[status(thm)],[f975,f114]) ).
fof(f979,plain,
( sK22_skl = smndt0(sz10)
| sK22_skl = sz10 ),
inference(forward_subsumption_resolution,[status(thm)],[f976,f710]) ).
fof(f982,plain,
( sK22_skl = sz10
| sP2_prd(sK22_skl)
| ~ aInteger0(smndt0(sz10)) ),
inference(paramodulation,[status(thm)],[f979,f400]) ).
fof(f991,plain,
( sK22_skl = sz10
| ~ aInteger0(smndt0(sz10)) ),
inference(forward_subsumption_resolution,[status(thm)],[f982,f806]) ).
fof(f996,plain,
( ~ aInteger0(sz10)
| sK22_skl = sz10 ),
inference(resolution,[status(thm)],[f991,f51]) ).
fof(f998,plain,
sK22_skl = sz10,
inference(forward_subsumption_resolution,[status(thm)],[f996,f49]) ).
fof(f1005,plain,
( ~ sP2_prd(sz10)
| ~ aInteger0(sK22_skl) ),
inference(backward_demodulation,[status(thm)],[f998,f816]) ).
fof(f1020,plain,
( ~ sP2_prd(sz10)
| ~ aInteger0(sz10) ),
inference(forward_demodulation,[status(thm)],[f998,f1005]) ).
fof(f1021,plain,
~ sP2_prd(sz10),
inference(forward_subsumption_resolution,[status(thm)],[f1020,f49]) ).
fof(f1040,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1021,f342]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM448+5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/10.39 % Computer : n017.cluster.edu
% 0.11/10.39 % Model : x86_64 x86_64
% 0.11/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.39 % Memory : 8046.5625MB
% 0.11/10.39 % OS : Linux 6.8.0-71-generic
% 0.11/10.40 % CPULimit : 300
% 0.11/10.40 % WCLimit : 300
% 0.11/10.40 % DateTime : Mon Sep 21 02:26:08 UTC 2026
% 0.17/10.40 % CPUTime :
% 0.17/10.42 % Drodi V4.1.1
% 0.17/10.62 % Refutation found
% 0.17/10.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/10.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.17/10.66 % Elapsed time: 0.246039 seconds
% 0.17/10.66 % CPU time: 1.608298 seconds
% 0.17/10.66 % Total memory used: 121.232 MB
% 0.17/10.66 % Net memory used: 119.723 MB
%------------------------------------------------------------------------------