%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM444+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:33 PM UTC 2026
% Result : Theorem 183.53s 28.67s
% Output : CNFRefutation 183.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 7
% Syntax : Number of formulae : 76 ( 10 unt; 5 def)
% Number of atoms : 979 ( 117 equ)
% Maximal formula atoms : 92 ( 12 avg)
% Number of connectives : 1318 ( 415 ~; 364 |; 478 &)
% ( 17 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 2 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 10 con; 0-3 aty)
% Number of variables : 260 ( 188 !; 72 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f41,hypothesis,
( xq != sz00
& aInteger0(xq)
& aInteger0(xa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,conjecture,
( ! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> ( ( ( sdteqdtlpzmzozddtrp0(W1,W0,xq)
| aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
| ? [W2] :
( sdtasdt0(xq,W2) = sdtpldt0(W1,smndt0(W0))
& aInteger0(W2) ) )
& ( ( ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
| ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
=> ( aElementOf0(W1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
| ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
=> ( ( ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
=> ( isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ( ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
<=> ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& aInteger0(W0) ) )
& aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
=> ( isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
=> ? [W1] :
( ( ( ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
| ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) )
& W1 != sz00
& aInteger0(W1) ) ) ) ) ) )
& ( ( ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( ( ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
| ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> aElementOf0(W0,cS1395) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
~ ( ! [W0,W1] :
( ( aInteger0(W1)
& aInteger0(W0) )
=> ( ( ( sdteqdtlpzmzozddtrp0(W1,W0,xq)
| aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
| ? [W2] :
( sdtasdt0(xq,W2) = sdtpldt0(W1,smndt0(W0))
& aInteger0(W2) ) )
& ( ( ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
| ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
=> ( aElementOf0(W1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
| ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
=> ( ( ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
=> ( isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ( ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
<=> ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& aInteger0(W0) ) )
& aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
=> ( isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
=> ? [W1] :
( ( ( ! [W2] :
( ( ( ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
| aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
| ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) ) )
& aInteger0(W2) )
=> aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) )
& aInteger0(W2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) ) )
& W1 != sz00
& aInteger0(W1) ) ) ) ) ) )
& ( ( ! [W0] :
( ( ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
=> aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
=> ( ( ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
| ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
=> aElementOf0(W0,cS1395) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f42]) ).
fof(f216,plain,
aInteger0(xq),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f217,plain,
xq != sz00,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f218,plain,
( ( ( ~ isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ~ isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ? [W0] :
( ! [W1] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ? [W2] :
( ~ aElementOf0(W2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,W0,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
| W1 = sz00
| ~ aInteger0(W1) )
& aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
<=> ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& aInteger0(W0) ) )
& aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
| ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
& ? [W0] :
( ~ aElementOf0(W0,cS1395)
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& ! [W0,W1] :
( ( aElementOf0(W1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ( ~ sdteqdtlpzmzozddtrp0(W1,W0,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
& ! [W2] :
( sdtasdt0(xq,W2) != sdtpldt0(W1,smndt0(W0))
| ~ aInteger0(W2) ) )
| ( ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ~ aInteger0(W1)
| ~ aInteger0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f219,definition,
! [W0,W1] :
( sP2_prd(W1,W0)
<=> ( ( ~ sdteqdtlpzmzozddtrp0(W1,W0,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
& ! [W2] :
( sdtasdt0(xq,W2) != sdtpldt0(W1,smndt0(W0))
| ~ aInteger0(W2) ) )
| ( ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f220,definition,
( sP3_prd
<=> ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
& ? [W0] :
( ~ aElementOf0(W0,cS1395)
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f221,plain,
( ( ( ~ isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ~ isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ? [W0] :
( ! [W1] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ? [W2] :
( ~ aElementOf0(W2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,W0,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
| W1 = sz00
| ~ aInteger0(W1) )
& aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
<=> ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& aInteger0(W0) ) )
& aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
| sP3_prd )
& ! [W0,W1] :
( ( aElementOf0(W1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| sP2_prd(W1,W0)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ) ),
inference(formula_renaming,[status(thm)],[f218,f220,f219]) ).
fof(f222,plain,
( ( ( ~ isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ~ isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ? [W0] :
( ! [W1] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ? [W2] :
( ~ aElementOf0(W2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,W0,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
| W1 = sz00
| ~ aInteger0(W1) )
& aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& ( ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ) )
& aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ) )
| sP3_prd )
& ! [W0,W1] :
( ( aElementOf0(W1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| sP2_prd(W1,W0)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ) ),
inference(NNF_transformation,[status(thm)],[f221]) ).
fof(f223,plain,
( ( ( ~ isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ~ isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ? [W0] :
( ! [W1] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ? [W2] :
( ~ aElementOf0(W2,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,W0,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(W0))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,W0,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(W0)))
& ? [W3] :
( sdtasdt0(W1,W3) = sdtpldt0(W2,smndt0(W0))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(W0,W1)) )
| W1 = sz00
| ~ aInteger0(W1) )
& aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& ! [W0] :
( ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ! [W0] :
( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
| sP3_prd )
& ! [W0,W1] :
( ( aElementOf0(W1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| sP2_prd(W1,W0)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ) ),
inference(miniscoping,[status(thm)],[f222]) ).
fof(f224,plain,
( ( ( ~ isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ~ isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ! [W1] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sK17_skl,W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(sK19_skl(W1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(sK19_skl(W1),szAzrzSzezqlpdtcmdtrp0(sK17_skl,W1))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sK17_skl,W1))
| ( ~ sdteqdtlpzmzozddtrp0(W2,sK17_skl,W1)
& ~ aDivisorOf0(W1,sdtpldt0(W2,smndt0(sK17_skl)))
& ! [W3] :
( sdtasdt0(W1,W3) != sdtpldt0(W2,smndt0(sK17_skl))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,sK17_skl,W1)
& aDivisorOf0(W1,sdtpldt0(W2,smndt0(sK17_skl)))
& sdtasdt0(W1,sK18_skl(W2,W1)) = sdtpldt0(W2,smndt0(sK17_skl))
& aInteger0(sK18_skl(W2,W1))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(sK17_skl,W1)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sK17_skl,W1)) )
| W1 = sz00
| ~ aInteger0(W1) )
& aElementOf0(sK17_skl,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ aInteger0(W0)
| aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& ! [W0] :
( ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) )
& aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ! [W0] :
( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& sdtasdt0(xq,sK16_skl(W0)) = sdtpldt0(W0,smndt0(xa))
& aInteger0(sK16_skl(W0))
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
| sP3_prd )
& ! [W0,W1] :
( ( aElementOf0(W1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& ~ aElementOf0(W1,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] :
( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& sdtasdt0(xq,sK15_skl(W2,W1,W0)) = sdtpldt0(W2,smndt0(xa))
& aInteger0(sK15_skl(W2,W1,W0))
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| sP2_prd(W1,W0)
| ~ aInteger0(W1)
| ~ aInteger0(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl]),skolemize(W3,sK15_skl(W2,W1,W0)),skolemize(W1,sK16_skl(W0)),skolemize(W0,sK17_skl),skolemize(W3,sK18_skl(W2,W1)),skolemize(W2,sK19_skl(W1))],[f223]) ).
fof(f235,plain,
! [X0,X1] :
( aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| sP2_prd(X1,X0)
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f245,plain,
! [X0] :
( aInteger0(X0)
| ~ aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f248,plain,
( aElementOf0(sK17_skl,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f250,plain,
! [X0,X1] :
( aInteger0(X1)
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sK17_skl,X0))
| X0 = sz00
| ~ aInteger0(X0)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f253,plain,
! [X0,X1] :
( aDivisorOf0(X0,sdtpldt0(X1,smndt0(sK17_skl)))
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sK17_skl,X0))
| X0 = sz00
| ~ aInteger0(X0)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f258,plain,
! [X0] :
( aElementOf0(sK19_skl(X0),szAzrzSzezqlpdtcmdtrp0(sK17_skl,X0))
| X0 = sz00
| ~ aInteger0(X0)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f259,plain,
! [X0] :
( ~ aElementOf0(sK19_skl(X0),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| X0 = sz00
| ~ aInteger0(X0)
| sP3_prd ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f274,definition,
! [W0] :
( sP4_prd(W0)
<=> ( ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f275,plain,
! [W0,W1] :
( sP2_prd(W1,W0)
<=> ( ( ~ sdteqdtlpzmzozddtrp0(W1,W0,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
& ! [W2] :
( sdtasdt0(xq,W2) != sdtpldt0(W1,smndt0(W0))
| ~ aInteger0(W2) ) )
| sP4_prd(W0) ) ),
inference(formula_renaming,[status(thm)],[f219,f274]) ).
fof(f276,plain,
! [W0,W1] :
( ( ( ( sdteqdtlpzmzozddtrp0(W1,W0,xq)
| aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
| ? [W2] :
( sdtasdt0(xq,W2) = sdtpldt0(W1,smndt0(W0))
& aInteger0(W2) ) )
& ~ sP4_prd(W0) )
| sP2_prd(W1,W0) )
& ( ( ~ sdteqdtlpzmzozddtrp0(W1,W0,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
& ! [W2] :
( sdtasdt0(xq,W2) != sdtpldt0(W1,smndt0(W0))
| ~ aInteger0(W2) ) )
| sP4_prd(W0)
| ~ sP2_prd(W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f275]) ).
fof(f277,plain,
( ! [W0,W1] :
( ( ( sdteqdtlpzmzozddtrp0(W1,W0,xq)
| aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
| ? [W2] :
( sdtasdt0(xq,W2) = sdtpldt0(W1,smndt0(W0))
& aInteger0(W2) ) )
& ~ sP4_prd(W0) )
| sP2_prd(W1,W0) )
& ! [W0,W1] :
( ( ~ sdteqdtlpzmzozddtrp0(W1,W0,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
& ! [W2] :
( sdtasdt0(xq,W2) != sdtpldt0(W1,smndt0(W0))
| ~ aInteger0(W2) ) )
| sP4_prd(W0)
| ~ sP2_prd(W1,W0) ) ),
inference(miniscoping,[status(thm)],[f276]) ).
fof(f278,plain,
( ! [W0,W1] :
( ( ( sdteqdtlpzmzozddtrp0(W1,W0,xq)
| aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
| ( sdtasdt0(xq,sK20_skl(W1,W0)) = sdtpldt0(W1,smndt0(W0))
& aInteger0(sK20_skl(W1,W0)) ) )
& ~ sP4_prd(W0) )
| sP2_prd(W1,W0) )
& ! [W0,W1] :
( ( ~ sdteqdtlpzmzozddtrp0(W1,W0,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W1,smndt0(W0)))
& ! [W2] :
( sdtasdt0(xq,W2) != sdtpldt0(W1,smndt0(W0))
| ~ aInteger0(W2) ) )
| sP4_prd(W0)
| ~ sP2_prd(W1,W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(W2,sK20_skl(W1,W0))],[f277]) ).
fof(f280,plain,
! [X0,X1] :
( ~ aDivisorOf0(xq,sdtpldt0(X0,smndt0(X1)))
| sP4_prd(X1)
| ~ sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f285,definition,
! [W0] :
( sP5_prd(W0)
<=> ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f286,plain,
( sP3_prd
<=> ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
& ? [W0] :
( ~ aElementOf0(W0,cS1395)
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& sP5_prd(W0) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ),
inference(formula_renaming,[status(thm)],[f220,f285]) ).
fof(f287,plain,
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
| ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ? [W0] :
( ( aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( ~ aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
| ~ aSet0(cS1395)
| ? [W0] :
( ( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
| ~ sP5_prd(W0) )
| ~ aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
| sP3_prd )
& ( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
& ? [W0] :
( ~ aElementOf0(W0,cS1395)
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ! [W0] :
( ( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395)
& ! [W0] :
( ( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& sP5_prd(W0) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ~ sP3_prd ) ),
inference(NNF_transformation,[status(thm)],[f286]) ).
fof(f288,plain,
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
| ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ? [W0] :
( ( aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ( ~ aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
| ~ aSet0(cS1395)
| ? [W0] :
( ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) ) )
& aInteger0(W0) )
| ? [W0] : ~ sP5_prd(W0)
| ~ aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
| sP3_prd )
& ( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
& ? [W0] :
( ~ aElementOf0(W0,cS1395)
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
& ! [W0] :
( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ! [W0] :
( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) )
& aSet0(cS1395)
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ! [W0] : sP5_prd(W0)
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ~ sP3_prd ) ),
inference(miniscoping,[status(thm)],[f287]) ).
fof(f289,plain,
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
| ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ( ( aInteger0(sK25_skl)
| aElementOf0(sK25_skl,cS1395) )
& ( ~ aInteger0(sK25_skl)
| ~ aElementOf0(sK25_skl,cS1395) ) )
| ~ aSet0(cS1395)
| ( ~ aElementOf0(sK23_skl,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ( sdteqdtlpzmzozddtrp0(sK23_skl,xa,xq)
| aDivisorOf0(xq,sdtpldt0(sK23_skl,smndt0(xa)))
| ( sdtasdt0(xq,sK24_skl) = sdtpldt0(sK23_skl,smndt0(xa))
& aInteger0(sK24_skl) ) )
& aInteger0(sK23_skl) )
| ~ sP5_prd(sK22_skl)
| ~ aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
| sP3_prd )
& ( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)
& ~ aElementOf0(sK21_skl,cS1395)
& aElementOf0(sK21_skl,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W0] :
( ~ aInteger0(W0)
| aElementOf0(W0,cS1395) )
& ! [W0] :
( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) )
& aSet0(cS1395)
& ! [W0] :
( aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) ) )
| ~ aInteger0(W0) )
& ! [W0] : sP5_prd(W0)
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ~ sP3_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl]),skolemize(W0,sK21_skl),skolemize(W0,sK22_skl),skolemize(W0,sK23_skl),skolemize(W1,sK24_skl),skolemize(W0,sK25_skl)],[f288]) ).
fof(f291,plain,
! [X0] :
( sP5_prd(X0)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f297,plain,
! [X0] :
( ~ aInteger0(X0)
| aElementOf0(X0,cS1395)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f298,plain,
( aElementOf0(sK21_skl,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f299,plain,
( ~ aElementOf0(sK21_skl,cS1395)
| ~ sP3_prd ),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f309,definition,
! [W2] :
( sP6_prd(W2)
<=> ( ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) )
& aInteger0(W2) )
| ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f310,plain,
! [W0] :
( sP4_prd(W0)
<=> ( ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& sP6_prd(W2) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) ) ),
inference(formula_renaming,[status(thm)],[f274,f309]) ).
fof(f311,plain,
! [W0] :
( ( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ? [W2] :
( ( ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
| ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) ) )
& aInteger0(W2) )
| ~ sP6_prd(W2) )
| ~ aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
| sP4_prd(W0) )
& ( ( ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( ( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& sP6_prd(W2) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ~ sP4_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f310]) ).
fof(f312,plain,
( ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ? [W2] :
( ~ aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ( sdteqdtlpzmzozddtrp0(W2,xa,xq)
| aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
| ? [W3] :
( sdtasdt0(xq,W3) = sdtpldt0(W2,smndt0(xa))
& aInteger0(W3) ) )
& aInteger0(W2) )
| ? [W2] : ~ sP6_prd(W2)
| ~ aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
| sP4_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] : sP6_prd(W2)
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ~ sP4_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f311]) ).
fof(f313,plain,
( ! [W0] :
( aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ aElementOf0(sK27_skl(W0),szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ( sdteqdtlpzmzozddtrp0(sK27_skl(W0),xa,xq)
| aDivisorOf0(xq,sdtpldt0(sK27_skl(W0),smndt0(xa)))
| ( sdtasdt0(xq,sK28_skl(W0)) = sdtpldt0(sK27_skl(W0),smndt0(xa))
& aInteger0(sK28_skl(W0)) ) )
& aInteger0(sK27_skl(W0)) )
| ~ sP6_prd(sK26_skl(W0))
| ~ aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq))
| sP4_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ( ~ sdteqdtlpzmzozddtrp0(W2,xa,xq)
& ~ aDivisorOf0(xq,sdtpldt0(W2,smndt0(xa)))
& ! [W3] :
( sdtasdt0(xq,W3) != sdtpldt0(W2,smndt0(xa))
| ~ aInteger0(W3) ) )
| ~ aInteger0(W2) )
& ! [W2] : sP6_prd(W2)
& aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| ~ sP4_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl]),skolemize(W2,sK26_skl(W0)),skolemize(W2,sK27_skl(W0)),skolemize(W3,sK28_skl(W0))],[f312]) ).
fof(f320,plain,
! [X0] :
( ~ aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f313]) ).
fof(f325,plain,
! [W0] :
( ( ( ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
| ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) )
| ~ aInteger0(W0) )
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| sP5_prd(W0) )
& ( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sP5_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f285]) ).
fof(f326,plain,
( ! [W0] :
( ( ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
| ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) )
| ~ aInteger0(W0) )
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| sP5_prd(W0) )
& ! [W0] :
( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& ? [W1] :
( sdtasdt0(xq,W1) = sdtpldt0(W0,smndt0(xa))
& aInteger0(W1) )
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sP5_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f325]) ).
fof(f327,plain,
( ! [W0] :
( ( ( ~ sdteqdtlpzmzozddtrp0(W0,xa,xq)
| ~ aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
| ! [W1] :
( sdtasdt0(xq,W1) != sdtpldt0(W0,smndt0(xa))
| ~ aInteger0(W1) )
| ~ aInteger0(W0) )
& aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) )
| sP5_prd(W0) )
& ! [W0] :
( ( sdteqdtlpzmzozddtrp0(W0,xa,xq)
& aDivisorOf0(xq,sdtpldt0(W0,smndt0(xa)))
& sdtasdt0(xq,sK29_skl(W0)) = sdtpldt0(W0,smndt0(xa))
& aInteger0(sK29_skl(W0))
& aInteger0(W0) )
| ~ aElementOf0(W0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sP5_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(W1,sK29_skl(W0))],[f326]) ).
fof(f328,plain,
! [X0] :
( aInteger0(X0)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f393,plain,
( ~ sP3_prd
| ~ aInteger0(sK21_skl)
| ~ sP3_prd ),
inference(resolution,[status(thm)],[f297,f299]) ).
fof(f394,plain,
( ~ aInteger0(sK21_skl)
| ~ sP3_prd ),
inference(duplicate_literals_removal,[status(thm)],[f393]) ).
fof(f421,plain,
( sP3_prd
| ~ sP4_prd(sK17_skl) ),
inference(resolution,[status(thm)],[f320,f248]) ).
fof(f455,plain,
( ~ sP3_prd
| ~ aElementOf0(sK21_skl,szAzrzSzezqlpdtcmdtrp0(xa,xq))
| ~ sP5_prd(sK21_skl) ),
inference(resolution,[status(thm)],[f328,f394]) ).
fof(f456,plain,
( ~ sP3_prd
| ~ aElementOf0(sK21_skl,szAzrzSzezqlpdtcmdtrp0(xa,xq)) ),
inference(forward_subsumption_resolution,[status(thm)],[f455,f291]) ).
fof(f458,plain,
aElementOf0(sK17_skl,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
inference(backward_subsumption_resolution,[status(thm)],[f248,f464]) ).
fof(f461,plain,
~ sP4_prd(sK17_skl),
inference(backward_subsumption_resolution,[status(thm)],[f421,f464]) ).
fof(f464,plain,
~ sP3_prd,
inference(forward_subsumption_resolution,[status(thm)],[f456,f298]) ).
fof(f509,plain,
! [X0] :
( aInteger0(X0)
| ~ aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) ),
inference(forward_subsumption_resolution,[status(thm)],[f245,f464]) ).
fof(f518,plain,
! [X0] :
( ~ aDivisorOf0(xq,sdtpldt0(X0,smndt0(sK17_skl)))
| ~ sP2_prd(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f280,f461]) ).
fof(f531,plain,
! [X0] :
( aElementOf0(sK19_skl(X0),szAzrzSzezqlpdtcmdtrp0(sK17_skl,X0))
| X0 = sz00
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f258,f464]) ).
fof(f569,plain,
! [X0,X1] :
( aInteger0(X1)
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sK17_skl,X0))
| X0 = sz00
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f250,f464]) ).
fof(f1143,plain,
! [X0,X1] :
( aDivisorOf0(X0,sdtpldt0(X1,smndt0(sK17_skl)))
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sK17_skl,X0))
| X0 = sz00
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f253,f464]) ).
fof(f1144,plain,
! [X0] :
( ~ sP2_prd(X0,sK17_skl)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sK17_skl,xq))
| xq = sz00
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[f1143,f518]) ).
fof(f1146,plain,
! [X0] :
( ~ sP2_prd(X0,sK17_skl)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sK17_skl,xq))
| xq = sz00 ),
inference(forward_subsumption_resolution,[status(thm)],[f1144,f216]) ).
fof(f1147,plain,
! [X0] :
( ~ sP2_prd(X0,sK17_skl)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sK17_skl,xq)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1146,f217]) ).
fof(f1157,plain,
( xq = sz00
| ~ aInteger0(xq)
| ~ sP2_prd(sK19_skl(xq),sK17_skl) ),
inference(resolution,[status(thm)],[f1147,f531]) ).
fof(f1174,plain,
( xq = sz00
| ~ sP2_prd(sK19_skl(xq),sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1157,f216]) ).
fof(f1177,plain,
~ sP2_prd(sK19_skl(xq),sK17_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1174,f217]) ).
fof(f1442,plain,
! [X0] :
( ~ aElementOf0(sK19_skl(X0),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| X0 = sz00
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f259,f464]) ).
fof(f1445,plain,
( ~ aElementOf0(sK19_skl(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))
| ~ aInteger0(xq) ),
inference(resolution,[status(thm)],[f1442,f217]) ).
fof(f1446,plain,
~ aElementOf0(sK19_skl(xq),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
inference(forward_subsumption_resolution,[status(thm)],[f1445,f216]) ).
fof(f1453,plain,
! [X0] :
( sP2_prd(sK19_skl(xq),X0)
| ~ aInteger0(sK19_skl(xq))
| ~ aInteger0(X0) ),
inference(resolution,[status(thm)],[f1446,f235]) ).
fof(f1474,plain,
( ~ aInteger0(sK19_skl(xq))
| ~ aInteger0(sK17_skl) ),
inference(resolution,[status(thm)],[f1453,f1177]) ).
fof(f1532,plain,
! [X0] :
( ~ aElementOf0(sK19_skl(xq),szAzrzSzezqlpdtcmdtrp0(sK17_skl,X0))
| X0 = sz00
| ~ aInteger0(X0)
| ~ aInteger0(sK17_skl) ),
inference(resolution,[status(thm)],[f1474,f569]) ).
fof(f2883,plain,
( ~ aElementOf0(sK19_skl(xq),szAzrzSzezqlpdtcmdtrp0(sK17_skl,xq))
| ~ aInteger0(xq)
| ~ aInteger0(sK17_skl) ),
inference(resolution,[status(thm)],[f1532,f217]) ).
fof(f2884,plain,
( ~ aElementOf0(sK19_skl(xq),szAzrzSzezqlpdtcmdtrp0(sK17_skl,xq))
| ~ aInteger0(sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2883,f216]) ).
fof(f2885,plain,
( xq = sz00
| ~ aInteger0(xq)
| ~ aInteger0(sK17_skl) ),
inference(resolution,[status(thm)],[f2884,f531]) ).
fof(f2898,plain,
( xq = sz00
| ~ aInteger0(sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2885,f216]) ).
fof(f2984,plain,
~ aInteger0(sK17_skl),
inference(forward_subsumption_resolution,[status(thm)],[f2898,f217]) ).
fof(f2988,plain,
~ aElementOf0(sK17_skl,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))),
inference(resolution,[status(thm)],[f2984,f509]) ).
fof(f2995,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2988,f458]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM444+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n008.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 02:31:02 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 183.53/28.67 % Refutation found
% 183.53/28.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 183.53/28.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 183.53/28.78 % Elapsed time: 23.404105 seconds
% 183.53/28.78 % CPU time: 184.552084 seconds
% 183.53/28.78 % Total memory used: 486.877 MB
% 183.53/28.78 % Net memory used: 450.564 MB
%------------------------------------------------------------------------------