%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM441+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 08:52:15 AM UTC 2026
% Result : Theorem 121.06s 121.36s
% Output : Proof 121.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 6
% Syntax : Number of formulae : 50 ( 20 unt; 0 def)
% Number of atoms : 1223 ( 87 equ)
% Maximal formula atoms : 74 ( 24 avg)
% Number of connectives : 1654 ( 481 ~; 405 |; 725 &)
% ( 17 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 38 ( 14 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-4 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-2 aty)
% Number of variables : 356 ( 0 sgn 308 !; 42 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mInterOpen,axiom,
! [W0,W1] :
( ( isOpen0(W1)
& isOpen0(W0)
& aSubsetOf0(W1,cS1395)
& aSubsetOf0(W0,cS1395) )
=> isOpen0(sdtslmnbsdt0(W0,W1)) ),
file('theBenchmark.p',mInterOpen) ).
fof(m__1826,hypothesis,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
=> ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(xB)) )
& ! [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))
& W1 != sz00
& aInteger0(W1) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
<=> ( ~ aElementOf0(W0,xB)
& aInteger0(W0) ) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
=> ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA))
& ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(xA)) )
& ! [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))
& W1 != sz00
& aInteger0(W1) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
<=> ( ~ aElementOf0(W0,xA)
& aInteger0(W0) ) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [W0] :
( aElementOf0(W0,xB)
=> aElementOf0(W0,cS1395) )
& aSet0(xB)
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [W0] :
( aElementOf0(W0,xA)
=> aElementOf0(W0,cS1395) )
& aSet0(xA)
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395) ),
file('theBenchmark.p',m__1826) ).
fof(m__1883,hypothesis,
( stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aElementOf0(W0,stldt0(xB))
& aElementOf0(W0,stldt0(xA))
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
<=> ( ~ aElementOf0(W0,xB)
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
<=> ( ~ aElementOf0(W0,xA)
& aInteger0(W0) ) )
& ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [W0] :
( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
<=> ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) ) )
& aSet0(sdtbsmnsldt0(xA,xB))
& aSubsetOf0(stldt0(xB),cS1395)
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
=> aElementOf0(W0,cS1395) )
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& ! [W0] :
( aElementOf0(W0,stldt0(xB))
<=> ( ~ aElementOf0(W0,xB)
& aInteger0(W0) ) )
& aSet0(stldt0(xB))
& aSubsetOf0(stldt0(xA),cS1395)
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
=> aElementOf0(W0,cS1395) )
& ! [W0] :
( aElementOf0(W0,cS1395)
<=> aInteger0(W0) )
& aSet0(cS1395)
& ! [W0] :
( aElementOf0(W0,stldt0(xA))
<=> ( ~ aElementOf0(W0,xA)
& aInteger0(W0) ) )
& aSet0(stldt0(xA)) ),
file('theBenchmark.p',m__1883) ).
fof(m__,conjecture,
( ( ! [W0] :
( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
<=> ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) ) )
& aSet0(sdtbsmnsldt0(xA,xB)) )
=> ( isClosed0(sdtbsmnsldt0(xA,xB))
| ( ( ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB))) )
=> ( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
=> ? [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(sdtbsmnsldt0(xA,xB)))
| ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(sdtbsmnsldt0(xA,xB))) ) ) )
& W1 != sz00
& aInteger0(W1) ) ) ) ) ) ),
file('theBenchmark.p',m__) ).
fof(f_38_1,plain,
! [W0,W1] :
( isOpen0(sdtslmnbsdt0(W0,W1))
| ~ isOpen0(W1)
| ~ isOpen0(W0)
| ~ aSubsetOf0(W1,cS1395)
| ~ aSubsetOf0(W0,cS1395) ),
inference(fof_nnf,[status(thm)],[mInterOpen]) ).
fof(f_38_2,plain,
! [U_129,U_128] :
( isOpen0(sdtslmnbsdt0(U_129,U_128))
| ~ isOpen0(U_128)
| ~ isOpen0(U_129)
| ~ aSubsetOf0(U_128,cS1395)
| ~ aSubsetOf0(U_129,cS1395) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
cnf(f_38_3,plain,
( isOpen0(sdtslmnbsdt0(U_129,U_128))
| ~ isOpen0(U_128)
| ~ isOpen0(U_129)
| ~ aSubsetOf0(U_128,cS1395)
| ~ aSubsetOf0(U_129,cS1395) ),
inference(clausify,[status(thm)],[f_38_2]) ).
fof(f_39_1,plain,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [W0] :
( ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xB))
& ! [W2] :
( aElementOf0(W2,stldt0(xB))
| ~ 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(xB)) )
& ! [W0] :
( ( aElementOf0(W0,stldt0(xB))
| aElementOf0(W0,xB)
| ~ aInteger0(W0) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) ) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [W0] :
( ? [W1] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(xA))
& ! [W2] :
( aElementOf0(W2,stldt0(xA))
| ~ 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(xA)) )
& ! [W0] :
( ( aElementOf0(W0,stldt0(xA))
| aElementOf0(W0,xA)
| ~ aInteger0(W0) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) ) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,xB) )
& aSet0(xB)
& ! [W0] :
( ( aElementOf0(W0,cS1395)
| ~ aInteger0(W0) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,xA) )
& aSet0(xA)
& ! [W0] :
( ( aElementOf0(W0,cS1395)
| ~ aInteger0(W0) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395) ),
inference(fof_nnf,[status(thm)],[m__1826]) ).
fof(f_39_2,plain,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [U_147] :
( ? [U_146] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_147,U_146),stldt0(xB))
& ! [U_145] :
( aElementOf0(U_145,stldt0(xB))
| ~ aElementOf0(U_145,szAzrzSzezqlpdtcmdtrp0(U_147,U_146)) )
& ! [U_144] :
( ( aElementOf0(U_144,szAzrzSzezqlpdtcmdtrp0(U_147,U_146))
| ( ~ sdteqdtlpzmzozddtrp0(U_144,U_147,U_146)
& ~ aDivisorOf0(U_146,sdtpldt0(U_144,smndt0(U_147)))
& ! [U_143] :
( sdtasdt0(U_146,U_143) != sdtpldt0(U_144,smndt0(U_147))
| ~ aInteger0(U_143) ) )
| ~ aInteger0(U_144) )
& ( ( sdteqdtlpzmzozddtrp0(U_144,U_147,U_146)
& aDivisorOf0(U_146,sdtpldt0(U_144,smndt0(U_147)))
& ? [U_142] :
( sdtasdt0(U_146,U_142) = sdtpldt0(U_144,smndt0(U_147))
& aInteger0(U_142) )
& aInteger0(U_144) )
| ~ aElementOf0(U_144,szAzrzSzezqlpdtcmdtrp0(U_147,U_146)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_147,U_146))
& U_146 != sz00
& aInteger0(U_146) )
| ~ aElementOf0(U_147,stldt0(xB)) )
& ! [U_141] :
( ( aElementOf0(U_141,stldt0(xB))
| aElementOf0(U_141,xB)
| ~ aInteger0(U_141) )
& ( ( ~ aElementOf0(U_141,xB)
& aInteger0(U_141) )
| ~ aElementOf0(U_141,stldt0(xB)) ) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [U_140] :
( ? [U_139] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_140,U_139),stldt0(xA))
& ! [U_138] :
( aElementOf0(U_138,stldt0(xA))
| ~ aElementOf0(U_138,szAzrzSzezqlpdtcmdtrp0(U_140,U_139)) )
& ! [U_137] :
( ( aElementOf0(U_137,szAzrzSzezqlpdtcmdtrp0(U_140,U_139))
| ( ~ sdteqdtlpzmzozddtrp0(U_137,U_140,U_139)
& ~ aDivisorOf0(U_139,sdtpldt0(U_137,smndt0(U_140)))
& ! [U_136] :
( sdtasdt0(U_139,U_136) != sdtpldt0(U_137,smndt0(U_140))
| ~ aInteger0(U_136) ) )
| ~ aInteger0(U_137) )
& ( ( sdteqdtlpzmzozddtrp0(U_137,U_140,U_139)
& aDivisorOf0(U_139,sdtpldt0(U_137,smndt0(U_140)))
& ? [U_135] :
( sdtasdt0(U_139,U_135) = sdtpldt0(U_137,smndt0(U_140))
& aInteger0(U_135) )
& aInteger0(U_137) )
| ~ aElementOf0(U_137,szAzrzSzezqlpdtcmdtrp0(U_140,U_139)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_140,U_139))
& U_139 != sz00
& aInteger0(U_139) )
| ~ aElementOf0(U_140,stldt0(xA)) )
& ! [U_134] :
( ( aElementOf0(U_134,stldt0(xA))
| aElementOf0(U_134,xA)
| ~ aInteger0(U_134) )
& ( ( ~ aElementOf0(U_134,xA)
& aInteger0(U_134) )
| ~ aElementOf0(U_134,stldt0(xA)) ) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [U_133] :
( aElementOf0(U_133,cS1395)
| ~ aElementOf0(U_133,xB) )
& aSet0(xB)
& ! [U_132] :
( ( aElementOf0(U_132,cS1395)
| ~ aInteger0(U_132) )
& ( aInteger0(U_132)
| ~ aElementOf0(U_132,cS1395) ) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [U_131] :
( aElementOf0(U_131,cS1395)
| ~ aElementOf0(U_131,xA) )
& aSet0(xA)
& ! [U_130] :
( ( aElementOf0(U_130,cS1395)
| ~ aInteger0(U_130) )
& ( aInteger0(U_130)
| ~ aElementOf0(U_130,cS1395) ) )
& aSet0(cS1395) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [U_147] :
( ? [U_146] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_147,U_146),stldt0(xB))
& ! [U_145] :
( aElementOf0(U_145,stldt0(xB))
| ~ aElementOf0(U_145,szAzrzSzezqlpdtcmdtrp0(U_147,U_146)) )
& ! [U_159] :
( aElementOf0(U_159,szAzrzSzezqlpdtcmdtrp0(U_147,U_146))
| ( ~ sdteqdtlpzmzozddtrp0(U_159,U_147,U_146)
& ~ aDivisorOf0(U_146,sdtpldt0(U_159,smndt0(U_147)))
& ! [U_143] :
( sdtasdt0(U_146,U_143) != sdtpldt0(U_159,smndt0(U_147))
| ~ aInteger0(U_143) ) )
| ~ aInteger0(U_159) )
& ! [U_158] :
( ( sdteqdtlpzmzozddtrp0(U_158,U_147,U_146)
& aDivisorOf0(U_146,sdtpldt0(U_158,smndt0(U_147)))
& ? [U_142] :
( sdtasdt0(U_146,U_142) = sdtpldt0(U_158,smndt0(U_147))
& aInteger0(U_142) )
& aInteger0(U_158) )
| ~ aElementOf0(U_158,szAzrzSzezqlpdtcmdtrp0(U_147,U_146)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_147,U_146))
& U_146 != sz00
& aInteger0(U_146) )
| ~ aElementOf0(U_147,stldt0(xB)) )
& ! [U_157] :
( aElementOf0(U_157,stldt0(xB))
| aElementOf0(U_157,xB)
| ~ aInteger0(U_157) )
& ! [U_156] :
( ( ~ aElementOf0(U_156,xB)
& aInteger0(U_156) )
| ~ aElementOf0(U_156,stldt0(xB)) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [U_140] :
( ? [U_139] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_140,U_139),stldt0(xA))
& ! [U_138] :
( aElementOf0(U_138,stldt0(xA))
| ~ aElementOf0(U_138,szAzrzSzezqlpdtcmdtrp0(U_140,U_139)) )
& ! [U_155] :
( aElementOf0(U_155,szAzrzSzezqlpdtcmdtrp0(U_140,U_139))
| ( ~ sdteqdtlpzmzozddtrp0(U_155,U_140,U_139)
& ~ aDivisorOf0(U_139,sdtpldt0(U_155,smndt0(U_140)))
& ! [U_136] :
( sdtasdt0(U_139,U_136) != sdtpldt0(U_155,smndt0(U_140))
| ~ aInteger0(U_136) ) )
| ~ aInteger0(U_155) )
& ! [U_154] :
( ( sdteqdtlpzmzozddtrp0(U_154,U_140,U_139)
& aDivisorOf0(U_139,sdtpldt0(U_154,smndt0(U_140)))
& ? [U_135] :
( sdtasdt0(U_139,U_135) = sdtpldt0(U_154,smndt0(U_140))
& aInteger0(U_135) )
& aInteger0(U_154) )
| ~ aElementOf0(U_154,szAzrzSzezqlpdtcmdtrp0(U_140,U_139)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_140,U_139))
& U_139 != sz00
& aInteger0(U_139) )
| ~ aElementOf0(U_140,stldt0(xA)) )
& ! [U_153] :
( aElementOf0(U_153,stldt0(xA))
| aElementOf0(U_153,xA)
| ~ aInteger0(U_153) )
& ! [U_152] :
( ( ~ aElementOf0(U_152,xA)
& aInteger0(U_152) )
| ~ aElementOf0(U_152,stldt0(xA)) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [U_133] :
( aElementOf0(U_133,cS1395)
| ~ aElementOf0(U_133,xB) )
& aSet0(xB)
& ! [U_151] :
( aElementOf0(U_151,cS1395)
| ~ aInteger0(U_151) )
& ! [U_150] :
( aInteger0(U_150)
| ~ aElementOf0(U_150,cS1395) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [U_131] :
( aElementOf0(U_131,cS1395)
| ~ aElementOf0(U_131,xA) )
& aSet0(xA)
& ! [U_149] :
( aElementOf0(U_149,cS1395)
| ~ aInteger0(U_149) )
& ! [U_148] :
( aInteger0(U_148)
| ~ aElementOf0(U_148,cS1395) )
& aSet0(cS1395) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
fof(f_39_4,plain,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [U_147] :
( ? [U_146] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_147,U_146),stldt0(xB))
& ! [U_145] :
( aElementOf0(U_145,stldt0(xB))
| ~ aElementOf0(U_145,szAzrzSzezqlpdtcmdtrp0(U_147,U_146)) )
& ! [U_159] :
( aElementOf0(U_159,szAzrzSzezqlpdtcmdtrp0(U_147,U_146))
| ( ~ sdteqdtlpzmzozddtrp0(U_159,U_147,U_146)
& ~ aDivisorOf0(U_146,sdtpldt0(U_159,smndt0(U_147)))
& ! [U_143] :
( sdtasdt0(U_146,U_143) != sdtpldt0(U_159,smndt0(U_147))
| ~ aInteger0(U_143) ) )
| ~ aInteger0(U_159) )
& ! [U_158] :
( ( sdteqdtlpzmzozddtrp0(U_158,U_147,U_146)
& aDivisorOf0(U_146,sdtpldt0(U_158,smndt0(U_147)))
& ? [U_142] :
( sdtasdt0(U_146,U_142) = sdtpldt0(U_158,smndt0(U_147))
& aInteger0(U_142) )
& aInteger0(U_158) )
| ~ aElementOf0(U_158,szAzrzSzezqlpdtcmdtrp0(U_147,U_146)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_147,U_146))
& U_146 != sz00
& aInteger0(U_146) )
| ~ aElementOf0(U_147,stldt0(xB)) )
& ! [U_157] :
( aElementOf0(U_157,stldt0(xB))
| aElementOf0(U_157,xB)
| ~ aInteger0(U_157) )
& ! [U_156] :
( ( ~ aElementOf0(U_156,xB)
& aInteger0(U_156) )
| ~ aElementOf0(U_156,stldt0(xB)) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [U_140] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)),stldt0(xA))
& ! [U_138] :
( aElementOf0(U_138,stldt0(xA))
| ~ aElementOf0(U_138,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140))) )
& ! [U_155] :
( aElementOf0(U_155,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)))
| ( ~ sdteqdtlpzmzozddtrp0(U_155,U_140,sK20(U_140))
& ~ aDivisorOf0(sK20(U_140),sdtpldt0(U_155,smndt0(U_140)))
& ! [U_136] :
( sdtasdt0(sK20(U_140),U_136) != sdtpldt0(U_155,smndt0(U_140))
| ~ aInteger0(U_136) ) )
| ~ aInteger0(U_155) )
& ! [U_154] :
( ( sdteqdtlpzmzozddtrp0(U_154,U_140,sK20(U_140))
& aDivisorOf0(sK20(U_140),sdtpldt0(U_154,smndt0(U_140)))
& ? [U_135] :
( sdtasdt0(sK20(U_140),U_135) = sdtpldt0(U_154,smndt0(U_140))
& aInteger0(U_135) )
& aInteger0(U_154) )
| ~ aElementOf0(U_154,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)))
& sK20(U_140) != sz00
& aInteger0(sK20(U_140)) )
| ~ aElementOf0(U_140,stldt0(xA)) )
& ! [U_153] :
( aElementOf0(U_153,stldt0(xA))
| aElementOf0(U_153,xA)
| ~ aInteger0(U_153) )
& ! [U_152] :
( ( ~ aElementOf0(U_152,xA)
& aInteger0(U_152) )
| ~ aElementOf0(U_152,stldt0(xA)) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [U_133] :
( aElementOf0(U_133,cS1395)
| ~ aElementOf0(U_133,xB) )
& aSet0(xB)
& ! [U_151] :
( aElementOf0(U_151,cS1395)
| ~ aInteger0(U_151) )
& ! [U_150] :
( aInteger0(U_150)
| ~ aElementOf0(U_150,cS1395) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [U_131] :
( aElementOf0(U_131,cS1395)
| ~ aElementOf0(U_131,xA) )
& aSet0(xA)
& ! [U_149] :
( aElementOf0(U_149,cS1395)
| ~ aInteger0(U_149) )
& ! [U_148] :
( aInteger0(U_148)
| ~ aElementOf0(U_148,cS1395) )
& aSet0(cS1395) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_139,sK20(U_140))],[f_39_3]) ).
fof(f_39_5,plain,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [U_147] :
( ? [U_146] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_147,U_146),stldt0(xB))
& ! [U_145] :
( aElementOf0(U_145,stldt0(xB))
| ~ aElementOf0(U_145,szAzrzSzezqlpdtcmdtrp0(U_147,U_146)) )
& ! [U_159] :
( aElementOf0(U_159,szAzrzSzezqlpdtcmdtrp0(U_147,U_146))
| ( ~ sdteqdtlpzmzozddtrp0(U_159,U_147,U_146)
& ~ aDivisorOf0(U_146,sdtpldt0(U_159,smndt0(U_147)))
& ! [U_143] :
( sdtasdt0(U_146,U_143) != sdtpldt0(U_159,smndt0(U_147))
| ~ aInteger0(U_143) ) )
| ~ aInteger0(U_159) )
& ! [U_158] :
( ( sdteqdtlpzmzozddtrp0(U_158,U_147,U_146)
& aDivisorOf0(U_146,sdtpldt0(U_158,smndt0(U_147)))
& ? [U_142] :
( sdtasdt0(U_146,U_142) = sdtpldt0(U_158,smndt0(U_147))
& aInteger0(U_142) )
& aInteger0(U_158) )
| ~ aElementOf0(U_158,szAzrzSzezqlpdtcmdtrp0(U_147,U_146)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_147,U_146))
& U_146 != sz00
& aInteger0(U_146) )
| ~ aElementOf0(U_147,stldt0(xB)) )
& ! [U_157] :
( aElementOf0(U_157,stldt0(xB))
| aElementOf0(U_157,xB)
| ~ aInteger0(U_157) )
& ! [U_156] :
( ( ~ aElementOf0(U_156,xB)
& aInteger0(U_156) )
| ~ aElementOf0(U_156,stldt0(xB)) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [U_140] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)),stldt0(xA))
& ! [U_138] :
( aElementOf0(U_138,stldt0(xA))
| ~ aElementOf0(U_138,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140))) )
& ! [U_155] :
( aElementOf0(U_155,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)))
| ( ~ sdteqdtlpzmzozddtrp0(U_155,U_140,sK20(U_140))
& ~ aDivisorOf0(sK20(U_140),sdtpldt0(U_155,smndt0(U_140)))
& ! [U_136] :
( sdtasdt0(sK20(U_140),U_136) != sdtpldt0(U_155,smndt0(U_140))
| ~ aInteger0(U_136) ) )
| ~ aInteger0(U_155) )
& ! [U_154] :
( ( sdteqdtlpzmzozddtrp0(U_154,U_140,sK20(U_140))
& aDivisorOf0(sK20(U_140),sdtpldt0(U_154,smndt0(U_140)))
& sdtasdt0(sK20(U_140),sK21(U_140,U_154)) = sdtpldt0(U_154,smndt0(U_140))
& aInteger0(sK21(U_140,U_154))
& aInteger0(U_154) )
| ~ aElementOf0(U_154,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)))
& sK20(U_140) != sz00
& aInteger0(sK20(U_140)) )
| ~ aElementOf0(U_140,stldt0(xA)) )
& ! [U_153] :
( aElementOf0(U_153,stldt0(xA))
| aElementOf0(U_153,xA)
| ~ aInteger0(U_153) )
& ! [U_152] :
( ( ~ aElementOf0(U_152,xA)
& aInteger0(U_152) )
| ~ aElementOf0(U_152,stldt0(xA)) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [U_133] :
( aElementOf0(U_133,cS1395)
| ~ aElementOf0(U_133,xB) )
& aSet0(xB)
& ! [U_151] :
( aElementOf0(U_151,cS1395)
| ~ aInteger0(U_151) )
& ! [U_150] :
( aInteger0(U_150)
| ~ aElementOf0(U_150,cS1395) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [U_131] :
( aElementOf0(U_131,cS1395)
| ~ aElementOf0(U_131,xA) )
& aSet0(xA)
& ! [U_149] :
( aElementOf0(U_149,cS1395)
| ~ aInteger0(U_149) )
& ! [U_148] :
( aInteger0(U_148)
| ~ aElementOf0(U_148,cS1395) )
& aSet0(cS1395) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_135,sK21(U_140,U_154))],[f_39_4]) ).
fof(f_39_6,plain,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [U_147] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147)),stldt0(xB))
& ! [U_145] :
( aElementOf0(U_145,stldt0(xB))
| ~ aElementOf0(U_145,szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147))) )
& ! [U_159] :
( aElementOf0(U_159,szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147)))
| ( ~ sdteqdtlpzmzozddtrp0(U_159,U_147,sK22(U_147))
& ~ aDivisorOf0(sK22(U_147),sdtpldt0(U_159,smndt0(U_147)))
& ! [U_143] :
( sdtasdt0(sK22(U_147),U_143) != sdtpldt0(U_159,smndt0(U_147))
| ~ aInteger0(U_143) ) )
| ~ aInteger0(U_159) )
& ! [U_158] :
( ( sdteqdtlpzmzozddtrp0(U_158,U_147,sK22(U_147))
& aDivisorOf0(sK22(U_147),sdtpldt0(U_158,smndt0(U_147)))
& ? [U_142] :
( sdtasdt0(sK22(U_147),U_142) = sdtpldt0(U_158,smndt0(U_147))
& aInteger0(U_142) )
& aInteger0(U_158) )
| ~ aElementOf0(U_158,szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147)))
& sK22(U_147) != sz00
& aInteger0(sK22(U_147)) )
| ~ aElementOf0(U_147,stldt0(xB)) )
& ! [U_157] :
( aElementOf0(U_157,stldt0(xB))
| aElementOf0(U_157,xB)
| ~ aInteger0(U_157) )
& ! [U_156] :
( ( ~ aElementOf0(U_156,xB)
& aInteger0(U_156) )
| ~ aElementOf0(U_156,stldt0(xB)) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [U_140] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)),stldt0(xA))
& ! [U_138] :
( aElementOf0(U_138,stldt0(xA))
| ~ aElementOf0(U_138,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140))) )
& ! [U_155] :
( aElementOf0(U_155,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)))
| ( ~ sdteqdtlpzmzozddtrp0(U_155,U_140,sK20(U_140))
& ~ aDivisorOf0(sK20(U_140),sdtpldt0(U_155,smndt0(U_140)))
& ! [U_136] :
( sdtasdt0(sK20(U_140),U_136) != sdtpldt0(U_155,smndt0(U_140))
| ~ aInteger0(U_136) ) )
| ~ aInteger0(U_155) )
& ! [U_154] :
( ( sdteqdtlpzmzozddtrp0(U_154,U_140,sK20(U_140))
& aDivisorOf0(sK20(U_140),sdtpldt0(U_154,smndt0(U_140)))
& sdtasdt0(sK20(U_140),sK21(U_140,U_154)) = sdtpldt0(U_154,smndt0(U_140))
& aInteger0(sK21(U_140,U_154))
& aInteger0(U_154) )
| ~ aElementOf0(U_154,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)))
& sK20(U_140) != sz00
& aInteger0(sK20(U_140)) )
| ~ aElementOf0(U_140,stldt0(xA)) )
& ! [U_153] :
( aElementOf0(U_153,stldt0(xA))
| aElementOf0(U_153,xA)
| ~ aInteger0(U_153) )
& ! [U_152] :
( ( ~ aElementOf0(U_152,xA)
& aInteger0(U_152) )
| ~ aElementOf0(U_152,stldt0(xA)) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [U_133] :
( aElementOf0(U_133,cS1395)
| ~ aElementOf0(U_133,xB) )
& aSet0(xB)
& ! [U_151] :
( aElementOf0(U_151,cS1395)
| ~ aInteger0(U_151) )
& ! [U_150] :
( aInteger0(U_150)
| ~ aElementOf0(U_150,cS1395) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [U_131] :
( aElementOf0(U_131,cS1395)
| ~ aElementOf0(U_131,xA) )
& aSet0(xA)
& ! [U_149] :
( aElementOf0(U_149,cS1395)
| ~ aInteger0(U_149) )
& ! [U_148] :
( aInteger0(U_148)
| ~ aElementOf0(U_148,cS1395) )
& aSet0(cS1395) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_146,sK22(U_147))],[f_39_5]) ).
fof(f_39_7,plain,
( isClosed0(xB)
& isOpen0(stldt0(xB))
& ! [U_147] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147)),stldt0(xB))
& ! [U_145] :
( aElementOf0(U_145,stldt0(xB))
| ~ aElementOf0(U_145,szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147))) )
& ! [U_159] :
( aElementOf0(U_159,szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147)))
| ( ~ sdteqdtlpzmzozddtrp0(U_159,U_147,sK22(U_147))
& ~ aDivisorOf0(sK22(U_147),sdtpldt0(U_159,smndt0(U_147)))
& ! [U_143] :
( sdtasdt0(sK22(U_147),U_143) != sdtpldt0(U_159,smndt0(U_147))
| ~ aInteger0(U_143) ) )
| ~ aInteger0(U_159) )
& ! [U_158] :
( ( sdteqdtlpzmzozddtrp0(U_158,U_147,sK22(U_147))
& aDivisorOf0(sK22(U_147),sdtpldt0(U_158,smndt0(U_147)))
& sdtasdt0(sK22(U_147),sK23(U_147,U_158)) = sdtpldt0(U_158,smndt0(U_147))
& aInteger0(sK23(U_147,U_158))
& aInteger0(U_158) )
| ~ aElementOf0(U_158,szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_147,sK22(U_147)))
& sK22(U_147) != sz00
& aInteger0(sK22(U_147)) )
| ~ aElementOf0(U_147,stldt0(xB)) )
& ! [U_157] :
( aElementOf0(U_157,stldt0(xB))
| aElementOf0(U_157,xB)
| ~ aInteger0(U_157) )
& ! [U_156] :
( ( ~ aElementOf0(U_156,xB)
& aInteger0(U_156) )
| ~ aElementOf0(U_156,stldt0(xB)) )
& aSet0(stldt0(xB))
& isClosed0(xA)
& isOpen0(stldt0(xA))
& ! [U_140] :
( ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)),stldt0(xA))
& ! [U_138] :
( aElementOf0(U_138,stldt0(xA))
| ~ aElementOf0(U_138,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140))) )
& ! [U_155] :
( aElementOf0(U_155,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)))
| ( ~ sdteqdtlpzmzozddtrp0(U_155,U_140,sK20(U_140))
& ~ aDivisorOf0(sK20(U_140),sdtpldt0(U_155,smndt0(U_140)))
& ! [U_136] :
( sdtasdt0(sK20(U_140),U_136) != sdtpldt0(U_155,smndt0(U_140))
| ~ aInteger0(U_136) ) )
| ~ aInteger0(U_155) )
& ! [U_154] :
( ( sdteqdtlpzmzozddtrp0(U_154,U_140,sK20(U_140))
& aDivisorOf0(sK20(U_140),sdtpldt0(U_154,smndt0(U_140)))
& sdtasdt0(sK20(U_140),sK21(U_140,U_154)) = sdtpldt0(U_154,smndt0(U_140))
& aInteger0(sK21(U_140,U_154))
& aInteger0(U_154) )
| ~ aElementOf0(U_154,szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140))) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_140,sK20(U_140)))
& sK20(U_140) != sz00
& aInteger0(sK20(U_140)) )
| ~ aElementOf0(U_140,stldt0(xA)) )
& ! [U_153] :
( aElementOf0(U_153,stldt0(xA))
| aElementOf0(U_153,xA)
| ~ aInteger0(U_153) )
& ! [U_152] :
( ( ~ aElementOf0(U_152,xA)
& aInteger0(U_152) )
| ~ aElementOf0(U_152,stldt0(xA)) )
& aSet0(stldt0(xA))
& aSubsetOf0(xB,cS1395)
& ! [U_133] :
( aElementOf0(U_133,cS1395)
| ~ aElementOf0(U_133,xB) )
& aSet0(xB)
& ! [U_151] :
( aElementOf0(U_151,cS1395)
| ~ aInteger0(U_151) )
& ! [U_150] :
( aInteger0(U_150)
| ~ aElementOf0(U_150,cS1395) )
& aSet0(cS1395)
& aSubsetOf0(xA,cS1395)
& ! [U_131] :
( aElementOf0(U_131,cS1395)
| ~ aElementOf0(U_131,xA) )
& aSet0(xA)
& ! [U_149] :
( aElementOf0(U_149,cS1395)
| ~ aInteger0(U_149) )
& ! [U_148] :
( aInteger0(U_148)
| ~ aElementOf0(U_148,cS1395) )
& aSet0(cS1395) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_142,sK23(U_147,U_158))],[f_39_6]) ).
cnf(f_39_37,plain,
isOpen0(stldt0(xA)),
inference(clausify,[status(thm)],[f_39_7]) ).
cnf(f_39_56,plain,
isOpen0(stldt0(xB)),
inference(clausify,[status(thm)],[f_39_7]) ).
fof(f_40_1,plain,
( stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ! [W0] :
( ( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ aElementOf0(W0,stldt0(xB))
| ~ aElementOf0(W0,stldt0(xA))
| ~ aInteger0(W0) )
& ( ( aElementOf0(W0,stldt0(xB))
& aElementOf0(W0,stldt0(xA))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& ! [W0] :
( ( aElementOf0(W0,stldt0(xB))
| aElementOf0(W0,xB)
| ~ aInteger0(W0) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) ) )
& ! [W0] :
( ( aElementOf0(W0,stldt0(xA))
| aElementOf0(W0,xA)
| ~ aInteger0(W0) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) ) )
& ! [W0] :
( ( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(W0,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(W0) )
& ( ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [W0] :
( ( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(W0,xB)
& ~ aElementOf0(W0,xA) )
| ~ aInteger0(W0) )
& ( ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(sdtbsmnsldt0(xA,xB))
& aSubsetOf0(stldt0(xB),cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,stldt0(xB)) )
& ! [W0] :
( ( aElementOf0(W0,cS1395)
| ~ aInteger0(W0) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395)
& ! [W0] :
( ( aElementOf0(W0,stldt0(xB))
| aElementOf0(W0,xB)
| ~ aInteger0(W0) )
& ( ( ~ aElementOf0(W0,xB)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xB)) ) )
& aSet0(stldt0(xB))
& aSubsetOf0(stldt0(xA),cS1395)
& ! [W0] :
( aElementOf0(W0,cS1395)
| ~ aElementOf0(W0,stldt0(xA)) )
& ! [W0] :
( ( aElementOf0(W0,cS1395)
| ~ aInteger0(W0) )
& ( aInteger0(W0)
| ~ aElementOf0(W0,cS1395) ) )
& aSet0(cS1395)
& ! [W0] :
( ( aElementOf0(W0,stldt0(xA))
| aElementOf0(W0,xA)
| ~ aInteger0(W0) )
& ( ( ~ aElementOf0(W0,xA)
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(xA)) ) )
& aSet0(stldt0(xA)) ),
inference(fof_nnf,[status(thm)],[m__1883]) ).
fof(f_40_2,plain,
( stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ! [U_170] :
( ( aElementOf0(U_170,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ aElementOf0(U_170,stldt0(xB))
| ~ aElementOf0(U_170,stldt0(xA))
| ~ aInteger0(U_170) )
& ( ( aElementOf0(U_170,stldt0(xB))
& aElementOf0(U_170,stldt0(xA))
& aInteger0(U_170) )
| ~ aElementOf0(U_170,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& ! [U_169] :
( ( aElementOf0(U_169,stldt0(xB))
| aElementOf0(U_169,xB)
| ~ aInteger0(U_169) )
& ( ( ~ aElementOf0(U_169,xB)
& aInteger0(U_169) )
| ~ aElementOf0(U_169,stldt0(xB)) ) )
& ! [U_168] :
( ( aElementOf0(U_168,stldt0(xA))
| aElementOf0(U_168,xA)
| ~ aInteger0(U_168) )
& ( ( ~ aElementOf0(U_168,xA)
& aInteger0(U_168) )
| ~ aElementOf0(U_168,stldt0(xA)) ) )
& ! [U_167] :
( ( aElementOf0(U_167,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(U_167,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(U_167) )
& ( ( ~ aElementOf0(U_167,sdtbsmnsldt0(xA,xB))
& aInteger0(U_167) )
| ~ aElementOf0(U_167,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_166] :
( ( aElementOf0(U_166,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(U_166,xB)
& ~ aElementOf0(U_166,xA) )
| ~ aInteger0(U_166) )
& ( ( ( aElementOf0(U_166,xB)
| aElementOf0(U_166,xA) )
& aInteger0(U_166) )
| ~ aElementOf0(U_166,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(sdtbsmnsldt0(xA,xB))
& aSubsetOf0(stldt0(xB),cS1395)
& ! [U_165] :
( aElementOf0(U_165,cS1395)
| ~ aElementOf0(U_165,stldt0(xB)) )
& ! [U_164] :
( ( aElementOf0(U_164,cS1395)
| ~ aInteger0(U_164) )
& ( aInteger0(U_164)
| ~ aElementOf0(U_164,cS1395) ) )
& aSet0(cS1395)
& ! [U_163] :
( ( aElementOf0(U_163,stldt0(xB))
| aElementOf0(U_163,xB)
| ~ aInteger0(U_163) )
& ( ( ~ aElementOf0(U_163,xB)
& aInteger0(U_163) )
| ~ aElementOf0(U_163,stldt0(xB)) ) )
& aSet0(stldt0(xB))
& aSubsetOf0(stldt0(xA),cS1395)
& ! [U_162] :
( aElementOf0(U_162,cS1395)
| ~ aElementOf0(U_162,stldt0(xA)) )
& ! [U_161] :
( ( aElementOf0(U_161,cS1395)
| ~ aInteger0(U_161) )
& ( aInteger0(U_161)
| ~ aElementOf0(U_161,cS1395) ) )
& aSet0(cS1395)
& ! [U_160] :
( ( aElementOf0(U_160,stldt0(xA))
| aElementOf0(U_160,xA)
| ~ aInteger0(U_160) )
& ( ( ~ aElementOf0(U_160,xA)
& aInteger0(U_160) )
| ~ aElementOf0(U_160,stldt0(xA)) ) )
& aSet0(stldt0(xA)) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB))
& ! [U_188] :
( aElementOf0(U_188,stldt0(sdtbsmnsldt0(xA,xB)))
| ~ aElementOf0(U_188,stldt0(xB))
| ~ aElementOf0(U_188,stldt0(xA))
| ~ aInteger0(U_188) )
& ! [U_187] :
( ( aElementOf0(U_187,stldt0(xB))
& aElementOf0(U_187,stldt0(xA))
& aInteger0(U_187) )
| ~ aElementOf0(U_187,stldt0(sdtbsmnsldt0(xA,xB))) )
& ! [U_186] :
( aElementOf0(U_186,stldt0(xB))
| aElementOf0(U_186,xB)
| ~ aInteger0(U_186) )
& ! [U_185] :
( ( ~ aElementOf0(U_185,xB)
& aInteger0(U_185) )
| ~ aElementOf0(U_185,stldt0(xB)) )
& ! [U_184] :
( aElementOf0(U_184,stldt0(xA))
| aElementOf0(U_184,xA)
| ~ aInteger0(U_184) )
& ! [U_183] :
( ( ~ aElementOf0(U_183,xA)
& aInteger0(U_183) )
| ~ aElementOf0(U_183,stldt0(xA)) )
& ! [U_182] :
( aElementOf0(U_182,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(U_182,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(U_182) )
& ! [U_181] :
( ( ~ aElementOf0(U_181,sdtbsmnsldt0(xA,xB))
& aInteger0(U_181) )
| ~ aElementOf0(U_181,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_180] :
( aElementOf0(U_180,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(U_180,xB)
& ~ aElementOf0(U_180,xA) )
| ~ aInteger0(U_180) )
& ! [U_179] :
( ( ( aElementOf0(U_179,xB)
| aElementOf0(U_179,xA) )
& aInteger0(U_179) )
| ~ aElementOf0(U_179,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB))
& aSubsetOf0(stldt0(xB),cS1395)
& ! [U_165] :
( aElementOf0(U_165,cS1395)
| ~ aElementOf0(U_165,stldt0(xB)) )
& ! [U_178] :
( aElementOf0(U_178,cS1395)
| ~ aInteger0(U_178) )
& ! [U_177] :
( aInteger0(U_177)
| ~ aElementOf0(U_177,cS1395) )
& aSet0(cS1395)
& ! [U_176] :
( aElementOf0(U_176,stldt0(xB))
| aElementOf0(U_176,xB)
| ~ aInteger0(U_176) )
& ! [U_175] :
( ( ~ aElementOf0(U_175,xB)
& aInteger0(U_175) )
| ~ aElementOf0(U_175,stldt0(xB)) )
& aSet0(stldt0(xB))
& aSubsetOf0(stldt0(xA),cS1395)
& ! [U_162] :
( aElementOf0(U_162,cS1395)
| ~ aElementOf0(U_162,stldt0(xA)) )
& ! [U_174] :
( aElementOf0(U_174,cS1395)
| ~ aInteger0(U_174) )
& ! [U_173] :
( aInteger0(U_173)
| ~ aElementOf0(U_173,cS1395) )
& aSet0(cS1395)
& ! [U_172] :
( aElementOf0(U_172,stldt0(xA))
| aElementOf0(U_172,xA)
| ~ aInteger0(U_172) )
& ! [U_171] :
( ( ~ aElementOf0(U_171,xA)
& aInteger0(U_171) )
| ~ aElementOf0(U_171,stldt0(xA)) )
& aSet0(stldt0(xA)) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
cnf(f_40_12,plain,
aSubsetOf0(stldt0(xA),cS1395),
inference(clausify,[status(thm)],[f_40_3]) ).
cnf(f_40_21,plain,
aSubsetOf0(stldt0(xB),cS1395),
inference(clausify,[status(thm)],[f_40_3]) ).
cnf(f_40_41,plain,
stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)),
inference(clausify,[status(thm)],[f_40_3]) ).
fof(f_41_1,negated_conjecture,
( ~ ( isClosed0(sdtbsmnsldt0(xA,xB))
| ( ( ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB))) )
=> ( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| ! [W0] :
( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
=> ? [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(sdtbsmnsldt0(xA,xB)))
| ! [W2] :
( aElementOf0(W2,szAzrzSzezqlpdtcmdtrp0(W0,W1))
=> aElementOf0(W2,stldt0(sdtbsmnsldt0(xA,xB))) ) ) )
& W1 != sz00
& aInteger0(W1) ) ) ) ) )
& ! [W0] :
( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
<=> ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) ) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(negate,[status(cth)],[m__]) ).
fof(f_41_2,negated_conjecture,
( ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ? [W0] :
( ! [W1] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(W0,W1),stldt0(sdtbsmnsldt0(xA,xB)))
& ? [W2] :
( ~ aElementOf0(W2,stldt0(sdtbsmnsldt0(xA,xB)))
& 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(sdtbsmnsldt0(xA,xB))) )
& ! [W0] :
( ( aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(W0,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(W0) )
& ( ( ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB))
& aInteger0(W0) )
| ~ aElementOf0(W0,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [W0] :
( ( aElementOf0(W0,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(W0,xB)
& ~ aElementOf0(W0,xA) )
| ~ aInteger0(W0) )
& ( ( ( aElementOf0(W0,xB)
| aElementOf0(W0,xA) )
& aInteger0(W0) )
| ~ aElementOf0(W0,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(fof_nnf,[status(thm)],[f_41_1]) ).
fof(f_41_3,negated_conjecture,
( ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ? [U_196] :
( ! [U_195] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_196,U_195),stldt0(sdtbsmnsldt0(xA,xB)))
& ? [U_194] :
( ~ aElementOf0(U_194,stldt0(sdtbsmnsldt0(xA,xB)))
& aElementOf0(U_194,szAzrzSzezqlpdtcmdtrp0(U_196,U_195)) )
& ! [U_193] :
( ( aElementOf0(U_193,szAzrzSzezqlpdtcmdtrp0(U_196,U_195))
| ( ~ sdteqdtlpzmzozddtrp0(U_193,U_196,U_195)
& ~ aDivisorOf0(U_195,sdtpldt0(U_193,smndt0(U_196)))
& ! [U_192] :
( sdtasdt0(U_195,U_192) != sdtpldt0(U_193,smndt0(U_196))
| ~ aInteger0(U_192) ) )
| ~ aInteger0(U_193) )
& ( ( sdteqdtlpzmzozddtrp0(U_193,U_196,U_195)
& aDivisorOf0(U_195,sdtpldt0(U_193,smndt0(U_196)))
& ? [U_191] :
( sdtasdt0(U_195,U_191) = sdtpldt0(U_193,smndt0(U_196))
& aInteger0(U_191) )
& aInteger0(U_193) )
| ~ aElementOf0(U_193,szAzrzSzezqlpdtcmdtrp0(U_196,U_195)) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_196,U_195)) )
| U_195 = sz00
| ~ aInteger0(U_195) )
& aElementOf0(U_196,stldt0(sdtbsmnsldt0(xA,xB))) )
& ! [U_190] :
( ( aElementOf0(U_190,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(U_190,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(U_190) )
& ( ( ~ aElementOf0(U_190,sdtbsmnsldt0(xA,xB))
& aInteger0(U_190) )
| ~ aElementOf0(U_190,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_189] :
( ( aElementOf0(U_189,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(U_189,xB)
& ~ aElementOf0(U_189,xA) )
| ~ aInteger0(U_189) )
& ( ( ( aElementOf0(U_189,xB)
| aElementOf0(U_189,xA) )
& aInteger0(U_189) )
| ~ aElementOf0(U_189,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(variable_rename,[status(thm)],[f_41_2]) ).
fof(f_41_4,negated_conjecture,
( ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ? [U_196] :
( ! [U_195] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(U_196,U_195),stldt0(sdtbsmnsldt0(xA,xB)))
& ? [U_194] :
( ~ aElementOf0(U_194,stldt0(sdtbsmnsldt0(xA,xB)))
& aElementOf0(U_194,szAzrzSzezqlpdtcmdtrp0(U_196,U_195)) )
& ! [U_202] :
( aElementOf0(U_202,szAzrzSzezqlpdtcmdtrp0(U_196,U_195))
| ( ~ sdteqdtlpzmzozddtrp0(U_202,U_196,U_195)
& ~ aDivisorOf0(U_195,sdtpldt0(U_202,smndt0(U_196)))
& ! [U_192] :
( sdtasdt0(U_195,U_192) != sdtpldt0(U_202,smndt0(U_196))
| ~ aInteger0(U_192) ) )
| ~ aInteger0(U_202) )
& ! [U_201] :
( ( sdteqdtlpzmzozddtrp0(U_201,U_196,U_195)
& aDivisorOf0(U_195,sdtpldt0(U_201,smndt0(U_196)))
& ? [U_191] :
( sdtasdt0(U_195,U_191) = sdtpldt0(U_201,smndt0(U_196))
& aInteger0(U_191) )
& aInteger0(U_201) )
| ~ aElementOf0(U_201,szAzrzSzezqlpdtcmdtrp0(U_196,U_195)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(U_196,U_195)) )
| U_195 = sz00
| ~ aInteger0(U_195) )
& aElementOf0(U_196,stldt0(sdtbsmnsldt0(xA,xB))) )
& ! [U_200] :
( aElementOf0(U_200,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(U_200,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(U_200) )
& ! [U_199] :
( ( ~ aElementOf0(U_199,sdtbsmnsldt0(xA,xB))
& aInteger0(U_199) )
| ~ aElementOf0(U_199,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_198] :
( aElementOf0(U_198,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(U_198,xB)
& ~ aElementOf0(U_198,xA) )
| ~ aInteger0(U_198) )
& ! [U_197] :
( ( ( aElementOf0(U_197,xB)
| aElementOf0(U_197,xA) )
& aInteger0(U_197) )
| ~ aElementOf0(U_197,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(miniscope,[status(thm)],[f_41_3]) ).
fof(f_41_5,negated_conjecture,
( ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_195] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sK24,U_195),stldt0(sdtbsmnsldt0(xA,xB)))
& ? [U_194] :
( ~ aElementOf0(U_194,stldt0(sdtbsmnsldt0(xA,xB)))
& aElementOf0(U_194,szAzrzSzezqlpdtcmdtrp0(sK24,U_195)) )
& ! [U_202] :
( aElementOf0(U_202,szAzrzSzezqlpdtcmdtrp0(sK24,U_195))
| ( ~ sdteqdtlpzmzozddtrp0(U_202,sK24,U_195)
& ~ aDivisorOf0(U_195,sdtpldt0(U_202,smndt0(sK24)))
& ! [U_192] :
( sdtasdt0(U_195,U_192) != sdtpldt0(U_202,smndt0(sK24))
| ~ aInteger0(U_192) ) )
| ~ aInteger0(U_202) )
& ! [U_201] :
( ( sdteqdtlpzmzozddtrp0(U_201,sK24,U_195)
& aDivisorOf0(U_195,sdtpldt0(U_201,smndt0(sK24)))
& ? [U_191] :
( sdtasdt0(U_195,U_191) = sdtpldt0(U_201,smndt0(sK24))
& aInteger0(U_191) )
& aInteger0(U_201) )
| ~ aElementOf0(U_201,szAzrzSzezqlpdtcmdtrp0(sK24,U_195)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sK24,U_195)) )
| U_195 = sz00
| ~ aInteger0(U_195) )
& aElementOf0(sK24,stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_200] :
( aElementOf0(U_200,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(U_200,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(U_200) )
& ! [U_199] :
( ( ~ aElementOf0(U_199,sdtbsmnsldt0(xA,xB))
& aInteger0(U_199) )
| ~ aElementOf0(U_199,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_198] :
( aElementOf0(U_198,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(U_198,xB)
& ~ aElementOf0(U_198,xA) )
| ~ aInteger0(U_198) )
& ! [U_197] :
( ( ( aElementOf0(U_197,xB)
| aElementOf0(U_197,xA) )
& aInteger0(U_197) )
| ~ aElementOf0(U_197,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_196,sK24)],[f_41_4]) ).
fof(f_41_6,negated_conjecture,
( ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_195] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sK24,U_195),stldt0(sdtbsmnsldt0(xA,xB)))
& ? [U_194] :
( ~ aElementOf0(U_194,stldt0(sdtbsmnsldt0(xA,xB)))
& aElementOf0(U_194,szAzrzSzezqlpdtcmdtrp0(sK24,U_195)) )
& ! [U_202] :
( aElementOf0(U_202,szAzrzSzezqlpdtcmdtrp0(sK24,U_195))
| ( ~ sdteqdtlpzmzozddtrp0(U_202,sK24,U_195)
& ~ aDivisorOf0(U_195,sdtpldt0(U_202,smndt0(sK24)))
& ! [U_192] :
( sdtasdt0(U_195,U_192) != sdtpldt0(U_202,smndt0(sK24))
| ~ aInteger0(U_192) ) )
| ~ aInteger0(U_202) )
& ! [U_201] :
( ( sdteqdtlpzmzozddtrp0(U_201,sK24,U_195)
& aDivisorOf0(U_195,sdtpldt0(U_201,smndt0(sK24)))
& sdtasdt0(U_195,sK25(U_195,U_201)) = sdtpldt0(U_201,smndt0(sK24))
& aInteger0(sK25(U_195,U_201))
& aInteger0(U_201) )
| ~ aElementOf0(U_201,szAzrzSzezqlpdtcmdtrp0(sK24,U_195)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sK24,U_195)) )
| U_195 = sz00
| ~ aInteger0(U_195) )
& aElementOf0(sK24,stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_200] :
( aElementOf0(U_200,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(U_200,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(U_200) )
& ! [U_199] :
( ( ~ aElementOf0(U_199,sdtbsmnsldt0(xA,xB))
& aInteger0(U_199) )
| ~ aElementOf0(U_199,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_198] :
( aElementOf0(U_198,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(U_198,xB)
& ~ aElementOf0(U_198,xA) )
| ~ aInteger0(U_198) )
& ! [U_197] :
( ( ( aElementOf0(U_197,xB)
| aElementOf0(U_197,xA) )
& aInteger0(U_197) )
| ~ aElementOf0(U_197,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_191,sK25(U_195,U_201))],[f_41_5]) ).
fof(f_41_7,negated_conjecture,
( ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_195] :
( ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sK24,U_195),stldt0(sdtbsmnsldt0(xA,xB)))
& ~ aElementOf0(sK26(U_195),stldt0(sdtbsmnsldt0(xA,xB)))
& aElementOf0(sK26(U_195),szAzrzSzezqlpdtcmdtrp0(sK24,U_195))
& ! [U_202] :
( aElementOf0(U_202,szAzrzSzezqlpdtcmdtrp0(sK24,U_195))
| ( ~ sdteqdtlpzmzozddtrp0(U_202,sK24,U_195)
& ~ aDivisorOf0(U_195,sdtpldt0(U_202,smndt0(sK24)))
& ! [U_192] :
( sdtasdt0(U_195,U_192) != sdtpldt0(U_202,smndt0(sK24))
| ~ aInteger0(U_192) ) )
| ~ aInteger0(U_202) )
& ! [U_201] :
( ( sdteqdtlpzmzozddtrp0(U_201,sK24,U_195)
& aDivisorOf0(U_195,sdtpldt0(U_201,smndt0(sK24)))
& sdtasdt0(U_195,sK25(U_195,U_201)) = sdtpldt0(U_201,smndt0(sK24))
& aInteger0(sK25(U_195,U_201))
& aInteger0(U_201) )
| ~ aElementOf0(U_201,szAzrzSzezqlpdtcmdtrp0(sK24,U_195)) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(sK24,U_195)) )
| U_195 = sz00
| ~ aInteger0(U_195) )
& aElementOf0(sK24,stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_200] :
( aElementOf0(U_200,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(U_200,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(U_200) )
& ! [U_199] :
( ( ~ aElementOf0(U_199,sdtbsmnsldt0(xA,xB))
& aInteger0(U_199) )
| ~ aElementOf0(U_199,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_198] :
( aElementOf0(U_198,sdtbsmnsldt0(xA,xB))
| ( ~ aElementOf0(U_198,xB)
& ~ aElementOf0(U_198,xA) )
| ~ aInteger0(U_198) )
& ! [U_197] :
( ( ( aElementOf0(U_197,xB)
| aElementOf0(U_197,xA) )
& aInteger0(U_197) )
| ~ aElementOf0(U_197,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_194,sK26(U_195))],[f_41_6]) ).
fof(f_41_8,negated_conjecture,
( ! [U_195,U_192,U_202] :
( ~ sdteqdtlpzmzozddtrp0(U_202,sK24,U_195)
| ~ sP4(U_195,U_192,U_202) )
& ! [U_195,U_192,U_202] :
( ~ aDivisorOf0(U_195,sdtpldt0(U_202,smndt0(sK24)))
| ~ sP4(U_195,U_192,U_202) )
& ! [U_195,U_192,U_202] :
( sdtasdt0(U_195,U_192) != sdtpldt0(U_202,smndt0(sK24))
| ~ aInteger0(U_192)
| ~ sP4(U_195,U_192,U_202) )
& ! [U_201,U_195] :
( sdteqdtlpzmzozddtrp0(U_201,sK24,U_195)
| ~ sP3(U_201,U_195) )
& ! [U_201,U_195] :
( aDivisorOf0(U_195,sdtpldt0(U_201,smndt0(sK24)))
| ~ sP3(U_201,U_195) )
& ! [U_201,U_195] :
( sdtasdt0(U_195,sK25(U_195,U_201)) = sdtpldt0(U_201,smndt0(sK24))
| ~ sP3(U_201,U_195) )
& ! [U_201,U_195] :
( aInteger0(sK25(U_195,U_201))
| ~ sP3(U_201,U_195) )
& ! [U_201,U_195] :
( aInteger0(U_201)
| ~ sP3(U_201,U_195) )
& ! [U_201,U_195,U_192,U_202] :
( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sK24,U_195),stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP5(U_201,U_195,U_192,U_202) )
& ! [U_201,U_195,U_192,U_202] :
( ~ aElementOf0(sK26(U_195),stldt0(sdtbsmnsldt0(xA,xB)))
| ~ sP5(U_201,U_195,U_192,U_202) )
& ! [U_201,U_195,U_192,U_202] :
( aElementOf0(sK26(U_195),szAzrzSzezqlpdtcmdtrp0(sK24,U_195))
| ~ sP5(U_201,U_195,U_192,U_202) )
& ! [U_201,U_195,U_192,U_202] :
( aElementOf0(U_202,szAzrzSzezqlpdtcmdtrp0(sK24,U_195))
| sP4(U_195,U_192,U_202)
| ~ aInteger0(U_202)
| ~ sP5(U_201,U_195,U_192,U_202) )
& ! [U_201,U_195,U_192,U_202] :
( sP3(U_201,U_195)
| ~ aElementOf0(U_201,szAzrzSzezqlpdtcmdtrp0(sK24,U_195))
| ~ sP5(U_201,U_195,U_192,U_202) )
& ! [U_201,U_195,U_192,U_202] :
( aSet0(szAzrzSzezqlpdtcmdtrp0(sK24,U_195))
| ~ sP5(U_201,U_195,U_192,U_202) )
& ! [U_199] :
( ~ aElementOf0(U_199,sdtbsmnsldt0(xA,xB))
| ~ sP2(U_199) )
& ! [U_199] :
( aInteger0(U_199)
| ~ sP2(U_199) )
& ! [U_198] :
( ~ aElementOf0(U_198,xB)
| ~ sP1(U_198) )
& ! [U_198] :
( ~ aElementOf0(U_198,xA)
| ~ sP1(U_198) )
& ! [U_197] :
( aElementOf0(U_197,xB)
| aElementOf0(U_197,xA)
| ~ sP0(U_197) )
& ! [U_197] :
( aInteger0(U_197)
| ~ sP0(U_197) )
& ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_201,U_195,U_192,U_202] :
( sP5(U_201,U_195,U_192,U_202)
| U_195 = sz00
| ~ aInteger0(U_195) )
& aElementOf0(sK24,stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_200] :
( aElementOf0(U_200,stldt0(sdtbsmnsldt0(xA,xB)))
| aElementOf0(U_200,sdtbsmnsldt0(xA,xB))
| ~ aInteger0(U_200) )
& ! [U_199] :
( sP2(U_199)
| ~ aElementOf0(U_199,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [U_198] :
( aElementOf0(U_198,sdtbsmnsldt0(xA,xB))
| sP1(U_198)
| ~ aInteger0(U_198) )
& ! [U_197] :
( sP0(U_197)
| ~ aElementOf0(U_197,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2,sP3,sP4,sP5])],[f_41_7]) ).
cnf(f_41_17,negated_conjecture,
~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),
inference(clausify,[status(thm)],[f_41_8]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_45,axiom,
( isOpen0(Eq_y_0)
| ~ isOpen0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(t1,plain,
~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),
inference(start,[status(thm),parent(0:0)],[f_41_17]) ).
cnf(t2,plain,
( ~ isOpen0(sdtslmnbsdt0(stldt0(xA),stldt0(xB)))
| sdtslmnbsdt0(stldt0(xA),stldt0(xB)) != stldt0(sdtbsmnsldt0(xA,xB))
| isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) ),
inference(extension,[status(thm),parent(t1:1)],[equality_45]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( stldt0(sdtbsmnsldt0(xA,xB)) != sdtslmnbsdt0(stldt0(xA),stldt0(xB))
| sdtslmnbsdt0(stldt0(xA),stldt0(xB)) = stldt0(sdtbsmnsldt0(xA,xB)) ),
inference(extension,[status(thm),parent(t2:2)],[equality_2]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)),
inference(extension,[status(thm),parent(t4:2)],[f_40_41]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ aSubsetOf0(stldt0(xB),cS1395)
| ~ isOpen0(stldt0(xA))
| ~ isOpen0(stldt0(xB))
| ~ aSubsetOf0(stldt0(xA),cS1395)
| isOpen0(sdtslmnbsdt0(stldt0(xA),stldt0(xB))) ),
inference(extension,[status(thm),parent(t2:3)],[f_38_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t2:3]) ).
cnf(t10,plain,
aSubsetOf0(stldt0(xA),cS1395),
inference(extension,[status(thm),parent(t8:2)],[f_40_12]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
isOpen0(stldt0(xB)),
inference(extension,[status(thm),parent(t8:3)],[f_39_56]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t8:3]) ).
cnf(t14,plain,
isOpen0(stldt0(xA)),
inference(extension,[status(thm),parent(t8:4)],[f_39_37]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t8:4]) ).
cnf(t16,plain,
aSubsetOf0(stldt0(xB),cS1395),
inference(extension,[status(thm),parent(t8:5)],[f_40_21]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t8:5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM441+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n007.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 19 18:24:19 UTC 2026
% 0.12/0.38 % CPUTime :
% 121.06/121.36 % SZS status Theorem for theBenchmark
% 121.06/121.36 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------