%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM452+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 257.33s 43.03s
% Output : CNFRefutation 127.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 17
% Syntax : Number of formulae : 128 ( 35 unt; 2 def)
% Number of atoms : 717 ( 196 equ)
% Maximal formula atoms : 38 ( 5 avg)
% Number of connectives : 879 ( 290 ~; 261 |; 298 &)
% ( 10 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 2 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 7 con; 0-3 aty)
% Number of variables : 211 ( 178 !; 33 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aInteger0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
aInteger0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [W0] :
( aInteger0(W0)
=> aInteger0(smndt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> aInteger0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [W0,W1,W2] :
( ( aInteger0(W2)
& aInteger0(W1)
& aInteger0(W0) )
=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0] :
( aInteger0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [W0] :
( aInteger0(W0)
=> ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [W0] :
( aInteger0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [W0] :
( aInteger0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [W0] :
( aInteger0(W0)
=> ( smndt0(W0) = sdtasdt0(W0,smndt0(sz10))
& sdtasdt0(smndt0(sz10),W0) = smndt0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,definition,
! [W0] :
( aInteger0(W0)
=> ! [W1] :
( aDivisorOf0(W1,W0)
<=> ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
( xS = cS2043
& ! [W0] :
( ( ? [W1] :
( ( ( ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
| ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
=> ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
=> szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0 )
& isPrime0(W1)
& W1 != sz00
& aInteger0(W1) )
=> aElementOf0(W0,xS) )
& ( aElementOf0(W0,xS)
=> ? [W1] :
( szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0
& ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
| ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
=> ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))
& isPrime0(W1)
& W1 != sz00
& aInteger0(W1) ) ) )
& aSet0(xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
( 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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,sz10,xp)
| aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
| ? [W1] :
( sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> ( sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ? [W1] :
( sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& xp != sz00
& aInteger0(xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,conjecture,
( ( aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
| aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
| ? [W0] :
( sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
& aInteger0(W0) ) )
& ( aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
| aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
| ? [W0] :
( sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
& aInteger0(W0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,negated_conjecture,
~ ( ( aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
| aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
| ? [W0] :
( sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
& aInteger0(W0) ) )
& ( aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
| aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
| ? [W0] :
( sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
& aInteger0(W0) ) ) ),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f52,plain,
aInteger0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f53,plain,
aInteger0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f54,plain,
! [W0] :
( aInteger0(smndt0(W0))
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f55,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f58,plain,
! [W0,W1] :
( aInteger0(sdtasdt0(W0,W1))
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f59,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [W0,W1,W2] :
( sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2)
| ~ aInteger0(W2)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f61,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [W0,W1] :
( sdtpldt0(W0,W1) = sdtpldt0(W1,W0)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f63,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f65,plain,
! [X0] :
( sdtpldt0(X0,sz00) = X0
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X0] :
( X0 = sdtpldt0(sz00,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f67,plain,
! [W0] :
( ( sz00 = sdtpldt0(smndt0(W0),W0)
& sdtpldt0(W0,smndt0(W0)) = sz00 )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f68,plain,
! [X0] :
( sdtpldt0(X0,smndt0(X0)) = sz00
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f74,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f75,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f80,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f81,plain,
! [X0] :
( sdtasdt0(X0,sz00) = sz00
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f83,plain,
! [W0] :
( ( smndt0(W0) = sdtasdt0(W0,smndt0(sz10))
& sdtasdt0(smndt0(sz10),W0) = smndt0(W0) )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f85,plain,
! [X0] :
( smndt0(X0) = sdtasdt0(X0,smndt0(sz10))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f88,plain,
! [W0] :
( ! [W1] :
( aDivisorOf0(W1,W0)
<=> ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) ) )
| ~ aInteger0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f89,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1)
| aDivisorOf0(W1,W0) )
& ( ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(NNF_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [W0] :
( ( ! [W1] :
( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1)
| aDivisorOf0(W1,W0) )
& ! [W1] :
( ( ? [W2] :
( sdtasdt0(W1,W2) = W0
& aInteger0(W2) )
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(miniscoping,[status(thm)],[f89]) ).
fof(f91,plain,
! [W0] :
( ( ! [W1] :
( ! [W2] :
( sdtasdt0(W1,W2) != W0
| ~ aInteger0(W2) )
| W1 = sz00
| ~ aInteger0(W1)
| aDivisorOf0(W1,W0) )
& ! [W1] :
( ( sdtasdt0(W1,sK0_skl(W1,W0)) = W0
& aInteger0(sK0_skl(W1,W0))
& W1 != sz00
& aInteger0(W1) )
| ~ aDivisorOf0(W1,W0) ) )
| ~ aInteger0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f90]) ).
fof(f92,plain,
! [X0,X1] :
( aInteger0(X1)
| ~ aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f94,plain,
! [X0,X1] :
( aInteger0(sK0_skl(X1,X0))
| ~ aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f95,plain,
! [X0,X1] :
( sdtasdt0(X1,sK0_skl(X1,X0)) = X0
| ~ aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f96,plain,
! [X0,X1,X2] :
( sdtasdt0(X1,X2) != X0
| ~ aInteger0(X2)
| X1 = sz00
| ~ aInteger0(X1)
| aDivisorOf0(X1,X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f223,plain,
( xS = cS2043
& ! [W0] :
( ( aElementOf0(W0,xS)
| ! [W1] :
( ( szAzrzSzezqlpdtcmdtrp0(sz00,W1) != W0
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
| ~ isPrime0(W1)
| W1 = sz00
| ~ aInteger0(W1) ) )
& ( ? [W1] :
( szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))
& isPrime0(W1)
& W1 != sz00
& aInteger0(W1) )
| ~ aElementOf0(W0,xS) ) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f224,plain,
( xS = cS2043
& ! [W0] :
( aElementOf0(W0,xS)
| ! [W1] :
( ( szAzrzSzezqlpdtcmdtrp0(sz00,W1) != W0
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
| ~ isPrime0(W1)
| W1 = sz00
| ~ aInteger0(W1) ) )
& ! [W0] :
( ? [W1] :
( szAzrzSzezqlpdtcmdtrp0(sz00,W1) = W0
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1))
& isPrime0(W1)
& W1 != sz00
& aInteger0(W1) )
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(miniscoping,[status(thm)],[f223]) ).
fof(f225,plain,
( xS = cS2043
& ! [W0] :
( aElementOf0(W0,xS)
| ! [W1] :
( ( szAzrzSzezqlpdtcmdtrp0(sz00,W1) != W0
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,sz00,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sz00)))
& sdtasdt0(W1,sK17_skl(W2,W1,W0)) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(sK17_skl(W2,W1,W0))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,W1)) )
| ~ isPrime0(W1)
| W1 = sz00
| ~ aInteger0(W1) ) )
& ! [W0] :
( ( szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(W0)) = W0
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(W0)))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sz00,sK15_skl(W0))
& ~ aDivisorOf0(sK15_skl(W0),sdtpldt0(W2,smndt0(sz00)))
& ! [W3] :
( sdtasdt0(sK15_skl(W0),W3) != sdtpldt0(W2,smndt0(sz00))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,sz00,sK15_skl(W0))
& aDivisorOf0(sK15_skl(W0),sdtpldt0(W2,smndt0(sz00)))
& sdtasdt0(sK15_skl(W0),sK16_skl(W2,W0)) = sdtpldt0(W2,smndt0(sz00))
& aInteger0(sK16_skl(W2,W0))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(W0))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK15_skl(W0)))
& isPrime0(sK15_skl(W0))
& sK15_skl(W0) != sz00
& aInteger0(sK15_skl(W0)) )
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(W1,sK15_skl(W0)),skolemize(W3,sK16_skl(W2,W0)),skolemize(W3,sK17_skl(W2,W1,W0))],[f224]) ).
fof(f250,plain,
xS = cS2043,
inference(cnf_transformation,[status(thm)],[f225]) ).
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)) ),
inference(NNF_transformation,[status(thm)],[f43]) ).
fof(f252,plain,
( stldt0(sbsmnsldt0(xS)) = cS2076
& ! [W0] :
( ( W0 != smndt0(sz10)
& W0 != sz10 )
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( 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)) ),
inference(miniscoping,[status(thm)],[f251]) ).
fof(f253,plain,
( stldt0(sbsmnsldt0(xS)) = cS2076
& ! [W0] :
( ( W0 != smndt0(sz10)
& W0 != sz10 )
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( 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] :
( ( aElementOf0(W0,sK18_skl(W0))
& aElementOf0(sK18_skl(W0),xS)
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(W1,sK18_skl(W0))],[f252]) ).
fof(f260,plain,
! [X0] :
( aInteger0(X0)
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f265,plain,
! [X0] :
( X0 != smndt0(sz10)
| aElementOf0(X0,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f266,plain,
stldt0(sbsmnsldt0(xS)) = cS2076,
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f316,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
<=> ( ? [W1] :
( aElementOf0(W0,W1)
& aElementOf0(W1,xS) )
& aInteger0(W0) ) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ( ~ sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ! [W1] :
( sdtasdt0(xp,W1) != sdtpldt0(W0,smndt0(sz10))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ? [W1] :
( sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& xp != sz00
& aInteger0(xp) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f317,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ! [W0] :
( ( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,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,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ( ~ sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ! [W1] :
( sdtasdt0(xp,W1) != sdtpldt0(W0,smndt0(sz10))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ? [W1] :
( sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& xp != sz00
& aInteger0(xp) ),
inference(NNF_transformation,[status(thm)],[f316]) ).
fof(f318,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,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,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ( ~ sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ! [W1] :
( sdtasdt0(xp,W1) != sdtpldt0(W0,smndt0(sz10))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ! [W0] :
( ( sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ? [W1] :
( sdtasdt0(xp,W1) = sdtpldt0(W0,smndt0(sz10))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& xp != sz00
& aInteger0(xp) ),
inference(miniscoping,[status(thm)],[f317]) ).
fof(f319,plain,
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))
& ! [W0] :
( aElementOf0(W0,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ! [W0] :
( aElementOf0(W0,sbsmnsldt0(xS))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ( ~ aElementOf0(W0,sbsmnsldt0(xS))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sbsmnsldt0(xS))) )
& ! [W0] :
( ! [W1] :
( ~ aElementOf0(W0,W1)
| ~ aElementOf0(W1,xS) )
| ~ aInteger0(W0)
| aElementOf0(W0,sbsmnsldt0(xS)) )
& ! [W0] :
( ( aElementOf0(W0,sK26_skl(W0))
& aElementOf0(sK26_skl(W0),xS)
& aInteger0(W0) )
| ~ aElementOf0(W0,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ( ~ sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& ! [W1] :
( sdtasdt0(xp,W1) != sdtpldt0(W0,smndt0(sz10))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ! [W0] :
( ( sdteqdtlpzmzozddtrp0(W0,sz10,xp)
& aDivisorOf0(xp,sdtpldt0(W0,smndt0(sz10)))
& sdtasdt0(xp,sK25_skl(W0)) = sdtpldt0(W0,smndt0(sz10))
& aInteger0(sK25_skl(W0))
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& xp != sz00
& aInteger0(xp) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(W1,sK25_skl(W0)),skolemize(W1,sK26_skl(W0))],[f318]) ).
fof(f320,plain,
aInteger0(xp),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f321,plain,
xp != sz00,
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f341,plain,
( ( ~ aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ~ sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
& ! [W0] :
( sdtasdt0(xp,W0) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| ~ aInteger0(W0) ) )
| ( ~ aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ~ sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& ! [W0] :
( sdtasdt0(xp,W0) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
| ~ aInteger0(W0) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f342,definition,
( sP2_prd
<=> ( ~ aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ~ sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& ! [W0] :
( sdtasdt0(xp,W0) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
| ~ aInteger0(W0) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f343,plain,
( ( ~ aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ~ sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
& ! [W0] :
( sdtasdt0(xp,W0) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| ~ aInteger0(W0) ) )
| sP2_prd ),
inference(formula_renaming,[status(thm)],[f341,f342]) ).
fof(f344,plain,
! [X0] :
( sdtasdt0(xp,X0) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| ~ aInteger0(X0)
| sP2_prd ),
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f359,plain,
( ( aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
| aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
| ? [W0] :
( sdtasdt0(xp,W0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
& aInteger0(W0) )
| sP2_prd )
& ( ( ~ aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ~ sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& ! [W0] :
( sdtasdt0(xp,W0) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
| ~ aInteger0(W0) ) )
| ~ sP2_prd ) ),
inference(NNF_transformation,[status(thm)],[f342]) ).
fof(f360,plain,
( ( aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
| aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
| ( sdtasdt0(xp,sK27_skl) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
& aInteger0(sK27_skl) )
| sP2_prd )
& ( ( ~ aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ~ sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& ~ aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& ! [W0] :
( sdtasdt0(xp,W0) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
| ~ aInteger0(W0) ) )
| ~ sP2_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(W0,sK27_skl)],[f359]) ).
fof(f361,plain,
! [X0] :
( sdtasdt0(xp,X0) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
| ~ aInteger0(X0)
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f368,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| X0 = sz00
| ~ aInteger0(X0)
| aDivisorOf0(X0,sdtasdt0(X0,X1))
| ~ aInteger0(sdtasdt0(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f96]) ).
fof(f394,plain,
aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(xS))),
inference(destructive_equality_resolution,[status(thm)],[f265]) ).
fof(f401,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| sdtpldt0(X0,smndt0(X1)) = sdtpldt0(smndt0(X1),X0)
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f63,f55]) ).
fof(f402,plain,
! [X0] :
( sdtpldt0(X0,xp) = sdtpldt0(xp,X0)
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f63,f320]) ).
fof(f407,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(smndt0(X0),sz00) = smndt0(X0) ),
inference(resolution,[status(thm)],[f65,f55]) ).
fof(f408,plain,
sdtpldt0(xp,sz00) = xp,
inference(resolution,[status(thm)],[f65,f320]) ).
fof(f424,plain,
sz10 = sdtpldt0(sz00,sz10),
inference(resolution,[status(thm)],[f66,f53]) ).
fof(f430,plain,
sdtpldt0(sz10,smndt0(sz10)) = sz00,
inference(resolution,[status(thm)],[f68,f53]) ).
fof(f437,plain,
stldt0(sbsmnsldt0(cS2043)) = cS2076,
inference(forward_demodulation,[status(thm)],[f250,f266]) ).
fof(f451,plain,
! [X0,X1] :
( sdtasdt0(xp,X1) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| ~ aInteger0(X1)
| sdtasdt0(xp,X0) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f361,f344]) ).
fof(f467,plain,
sdtasdt0(xp,sz10) = xp,
inference(resolution,[status(thm)],[f75,f320]) ).
fof(f523,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(smndt0(X0),sz00) = sz00 ),
inference(resolution,[status(thm)],[f81,f55]) ).
fof(f561,plain,
smndt0(xp) = sdtasdt0(xp,smndt0(sz10)),
inference(resolution,[status(thm)],[f85,f320]) ).
fof(f605,plain,
! [X0] :
( sdtpldt0(X0,sz00) = sdtpldt0(sdtpldt0(X0,sz10),smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz10)
| ~ aInteger0(X0) ),
inference(paramodulation,[status(thm)],[f430,f61]) ).
fof(f607,plain,
! [X0] :
( sdtpldt0(X0,sz00) = sdtpldt0(sdtpldt0(X0,sz10),smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f605,f53]) ).
fof(f613,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| X0 = sz00
| ~ aInteger0(X0)
| aDivisorOf0(X0,sdtasdt0(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f368,f59]) ).
fof(f614,plain,
! [X0] :
( X0 = sz00
| ~ aInteger0(X0)
| aDivisorOf0(X0,sdtasdt0(X0,sz00)) ),
inference(resolution,[status(thm)],[f613,f52]) ).
fof(f619,plain,
! [X0] :
( X0 = sz00
| ~ aInteger0(X0)
| aDivisorOf0(X0,sdtasdt0(X0,sz10)) ),
inference(resolution,[status(thm)],[f613,f53]) ).
fof(f645,plain,
aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(cS2043))),
inference(forward_demodulation,[status(thm)],[f250,f394]) ).
fof(f646,plain,
aElementOf0(smndt0(sz10),cS2076),
inference(forward_demodulation,[status(thm)],[f437,f645]) ).
fof(f693,plain,
sdtasdt0(smndt0(xp),sz00) = sz00,
inference(resolution,[status(thm)],[f523,f320]) ).
fof(f717,plain,
! [X0] :
( aInteger0(X0)
| ~ aElementOf0(X0,stldt0(sbsmnsldt0(cS2043))) ),
inference(forward_demodulation,[status(thm)],[f250,f260]) ).
fof(f718,plain,
! [X0] :
( aInteger0(X0)
| ~ aElementOf0(X0,cS2076) ),
inference(forward_demodulation,[status(thm)],[f437,f717]) ).
fof(f720,plain,
aInteger0(smndt0(sz10)),
inference(resolution,[status(thm)],[f718,f646]) ).
fof(f728,plain,
! [X0] :
( sdtasdt0(xp,smndt0(sz10)) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| sdtasdt0(xp,X0) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f720,f451]) ).
fof(f877,plain,
sdtpldt0(sz10,xp) = sdtpldt0(xp,sz10),
inference(resolution,[status(thm)],[f402,f53]) ).
fof(f943,plain,
sdtpldt0(smndt0(xp),sz00) = smndt0(xp),
inference(resolution,[status(thm)],[f407,f320]) ).
fof(f1067,plain,
! [X0] :
( ~ aInteger0(X0)
| smndt0(X0) = sz00
| aDivisorOf0(smndt0(X0),sdtasdt0(smndt0(X0),sz00)) ),
inference(resolution,[status(thm)],[f614,f55]) ).
fof(f1274,plain,
( xp = sz00
| aDivisorOf0(xp,sdtasdt0(xp,sz10)) ),
inference(resolution,[status(thm)],[f619,f320]) ).
fof(f1277,plain,
( xp = sz00
| aDivisorOf0(xp,xp) ),
inference(forward_demodulation,[status(thm)],[f467,f1274]) ).
fof(f1278,plain,
aDivisorOf0(xp,xp),
inference(forward_subsumption_resolution,[status(thm)],[f1277,f321]) ).
fof(f1320,plain,
! [X0] :
( sdtpldt0(X0,smndt0(xp)) = sdtpldt0(smndt0(xp),X0)
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f401,f320]) ).
fof(f1324,plain,
( sdtasdt0(xp,sK0_skl(xp,xp)) = xp
| ~ aInteger0(xp) ),
inference(resolution,[status(thm)],[f1278,f95]) ).
fof(f1325,plain,
( aInteger0(sK0_skl(xp,xp))
| ~ aInteger0(xp) ),
inference(resolution,[status(thm)],[f1278,f94]) ).
fof(f1327,plain,
sdtasdt0(xp,sK0_skl(xp,xp)) = xp,
inference(forward_subsumption_resolution,[status(thm)],[f1324,f320]) ).
fof(f1328,plain,
aInteger0(sK0_skl(xp,xp)),
inference(forward_subsumption_resolution,[status(thm)],[f1325,f320]) ).
fof(f5737,plain,
! [X0] :
( sdtasdt0(xp,smndt0(sz10)) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| sdtasdt0(xp,X0) != sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10))
| ~ aInteger0(X0) ),
inference(forward_demodulation,[status(thm)],[f877,f728]) ).
fof(f5738,plain,
! [X0] :
( smndt0(xp) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| sdtasdt0(xp,X0) != sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10))
| ~ aInteger0(X0) ),
inference(forward_demodulation,[status(thm)],[f561,f5737]) ).
fof(f5748,plain,
( smndt0(xp) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| sdtasdt0(xp,sK0_skl(xp,xp)) != sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10)) ),
inference(resolution,[status(thm)],[f5738,f1328]) ).
fof(f5757,plain,
( smndt0(xp) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| xp != sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10)) ),
inference(forward_demodulation,[status(thm)],[f1327,f5748]) ).
fof(f25566,plain,
! [X0] :
( sdtpldt0(X0,sz00) = sdtpldt0(sdtpldt0(X0,sz10),smndt0(sz10))
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f607,f720]) ).
fof(f25629,plain,
sdtpldt0(xp,sz00) = sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10)),
inference(resolution,[status(thm)],[f25566,f320]) ).
fof(f25641,plain,
xp = sdtpldt0(sdtpldt0(xp,sz10),smndt0(sz10)),
inference(forward_demodulation,[status(thm)],[f408,f25629]) ).
fof(f25674,plain,
( smndt0(xp) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))
| xp != xp ),
inference(backward_demodulation,[status(thm)],[f25641,f5757]) ).
fof(f25720,plain,
smndt0(xp) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)),
inference(trivial_equality_resolution,[status(thm)],[f25674]) ).
fof(f30875,plain,
sdtpldt0(sz10,smndt0(xp)) = sdtpldt0(smndt0(xp),sz10),
inference(resolution,[status(thm)],[f1320,f53]) ).
fof(f30887,plain,
smndt0(xp) != sdtpldt0(sdtpldt0(smndt0(xp),sz10),smndt0(sz10)),
inference(backward_demodulation,[status(thm)],[f30875,f25720]) ).
fof(f32358,plain,
( ~ aInteger0(xp)
| smndt0(xp) = sz00
| aDivisorOf0(smndt0(xp),sz00) ),
inference(paramodulation,[status(thm)],[f693,f1067]) ).
fof(f32380,plain,
( smndt0(xp) = sz00
| aDivisorOf0(smndt0(xp),sz00) ),
inference(forward_subsumption_resolution,[status(thm)],[f32358,f320]) ).
fof(f32746,plain,
( aInteger0(smndt0(xp))
| ~ aInteger0(sz00)
| smndt0(xp) = sz00 ),
inference(resolution,[status(thm)],[f32380,f92]) ).
fof(f32749,plain,
( aInteger0(smndt0(xp))
| smndt0(xp) = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f32746,f52]) ).
fof(f32816,plain,
( sdtpldt0(smndt0(xp),sz00) = sdtpldt0(sdtpldt0(smndt0(xp),sz10),smndt0(sz10))
| smndt0(xp) = sz00 ),
inference(resolution,[status(thm)],[f32749,f25566]) ).
fof(f33153,plain,
( smndt0(xp) = sdtpldt0(sdtpldt0(smndt0(xp),sz10),smndt0(sz10))
| smndt0(xp) = sz00 ),
inference(forward_demodulation,[status(thm)],[f943,f32816]) ).
fof(f33154,plain,
smndt0(xp) = sz00,
inference(forward_subsumption_resolution,[status(thm)],[f33153,f30887]) ).
fof(f33324,plain,
smndt0(xp) != sdtpldt0(sdtpldt0(sz00,sz10),smndt0(sz10)),
inference(backward_demodulation,[status(thm)],[f33154,f30887]) ).
fof(f33401,plain,
sz00 != sdtpldt0(sdtpldt0(sz00,sz10),smndt0(sz10)),
inference(forward_demodulation,[status(thm)],[f33154,f33324]) ).
fof(f33402,plain,
sz00 != sdtpldt0(sz10,smndt0(sz10)),
inference(forward_demodulation,[status(thm)],[f424,f33401]) ).
fof(f33403,plain,
sz00 != sz00,
inference(forward_demodulation,[status(thm)],[f430,f33402]) ).
fof(f33404,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f33403]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM452+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/10.40 % Computer : n001.cluster.edu
% 0.13/10.40 % Model : x86_64 x86_64
% 0.13/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.40 % Memory : 8046.5625MB
% 0.13/10.40 % OS : Linux 6.8.0-71-generic
% 0.13/10.40 % CPULimit : 300
% 0.13/10.40 % WCLimit : 300
% 0.13/10.40 % DateTime : Mon Sep 21 02:37:09 UTC 2026
% 0.13/10.41 % CPUTime :
% 0.13/10.42 % Drodi V4.1.1
% 257.33/43.03 % Refutation found
% 257.33/43.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 257.33/43.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.06/43.42 % Elapsed time: 33.001006 seconds
% 19.06/43.42 % CPU time: 258.682039 seconds
% 19.06/43.42 % Total memory used: 582.441 MB
% 19.06/43.42 % Net memory used: 535.216 MB
%------------------------------------------------------------------------------