%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM441+6 : TPTP v7.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n072.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.625MB
% OS : Linux 3.10.0-693.2.2.el7.x86_64
% CPULimit : 300s
% DateTime : Mon Jan 8 15:21:21 EST 2018
% Result : Theorem 0.06s
% Output : CNFRefutation 0.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 4
% Syntax : Number of formulae : 39 ( 9 unt; 0 def)
% Number of atoms : 1261 ( 1 equ)
% Maximal formula atoms : 116 ( 32 avg)
% Number of connectives : 1694 ( 472 ~; 447 |; 697 &)
% ( 32 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 18 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-2 aty)
% Number of variables : 243 ( 0 sgn 206 !; 35 ?)
% Comments :
%------------------------------------------------------------------------------
fof(4,axiom,
! [X1,X2] :
( ( aSubsetOf0(X1,cS1395)
& aSubsetOf0(X2,cS1395)
& isOpen0(X1)
& isOpen0(X2) )
=> isOpen0(sdtslmnbsdt0(X1,X2)) ),
file('/export/starexec/sandbox/tmp/tmpyW_fKY/sel_theBenchmark.p_1',mInterOpen) ).
fof(5,axiom,
( aSet0(stldt0(xA))
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(stldt0(xA),cS1395)
& aSet0(stldt0(xB))
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(stldt0(xB),cS1395)
& aSet0(sdtbsmnsldt0(xA,xB))
& ! [X1] :
( aElementOf0(X1,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X1)
& ( aElementOf0(X1,xA)
| aElementOf0(X1,xB) ) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X1)
& aElementOf0(X1,stldt0(xA))
& aElementOf0(X1,stldt0(xB)) ) )
& equal(stldt0(sdtbsmnsldt0(xA,xB)),sdtslmnbsdt0(stldt0(xA),stldt0(xB))) ),
file('/export/starexec/sandbox/tmp/tmpyW_fKY/sel_theBenchmark.p_1',m__1883) ).
fof(17,axiom,
( aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(xA)
& ! [X1] :
( aElementOf0(X1,xA)
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(xB)
& ! [X1] :
( aElementOf0(X1,xB)
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
=> ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ( aInteger0(X3)
& ( ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
| aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
=> aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) )
& ! [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> aElementOf0(X3,stldt0(xA)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(xA)) ) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
=> ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ( aInteger0(X3)
& ( ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
| aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
=> aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) )
& ! [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> aElementOf0(X3,stldt0(xB)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(xB)) ) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
file('/export/starexec/sandbox/tmp/tmpyW_fKY/sel_theBenchmark.p_1',m__1826) ).
fof(26,conjecture,
( ( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X1] :
( aElementOf0(X1,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X1)
& ( aElementOf0(X1,xA)
| aElementOf0(X1,xB) ) ) ) )
=> ( ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) ) )
=> ( ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
=> ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ( aInteger0(X3)
& ( ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
| aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
=> aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) ) )
=> ( ! [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> aElementOf0(X3,stldt0(sdtbsmnsldt0(xA,xB))) )
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sdtbsmnsldt0(xA,xB))) ) ) ) )
| isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) ) )
| isClosed0(sdtbsmnsldt0(xA,xB)) ) ),
file('/export/starexec/sandbox/tmp/tmpyW_fKY/sel_theBenchmark.p_1',m__) ).
fof(42,negated_conjecture,
~ ( ( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X1] :
( aElementOf0(X1,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X1)
& ( aElementOf0(X1,xA)
| aElementOf0(X1,xB) ) ) ) )
=> ( ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) ) )
=> ( ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
=> ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ( aInteger0(X3)
& ( ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
| aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
=> aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) ) )
=> ( ! [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> aElementOf0(X3,stldt0(sdtbsmnsldt0(xA,xB))) )
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sdtbsmnsldt0(xA,xB))) ) ) ) )
| isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) ) )
| isClosed0(sdtbsmnsldt0(xA,xB)) ) ),
inference(assume_negation,[status(cth)],[26]) ).
fof(44,plain,
( aSet0(stldt0(xA))
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(stldt0(xA),cS1395)
& aSet0(stldt0(xB))
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(stldt0(xB),cS1395)
& aSet0(sdtbsmnsldt0(xA,xB))
& ! [X1] :
( aElementOf0(X1,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X1)
& ( aElementOf0(X1,xA)
| aElementOf0(X1,xB) ) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X1)
& aElementOf0(X1,stldt0(xA))
& aElementOf0(X1,stldt0(xB)) ) )
& equal(stldt0(sdtbsmnsldt0(xA,xB)),sdtslmnbsdt0(stldt0(xA),stldt0(xB))) ),
inference(fof_simplification,[status(thm)],[5,theory(equality)]) ).
fof(45,plain,
( aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(xA)
& ! [X1] :
( aElementOf0(X1,xA)
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X1] :
( aElementOf0(X1,cS1395)
<=> aInteger0(X1) )
& aSet0(xB)
& ! [X1] :
( aElementOf0(X1,xB)
=> aElementOf0(X1,cS1395) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(xA))
=> ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ( aInteger0(X3)
& ( ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
| aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
=> aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) )
& ! [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> aElementOf0(X3,stldt0(xA)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(xA)) ) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(xB))
=> ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ( aInteger0(X3)
& ( ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
| aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
=> aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) )
& ! [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> aElementOf0(X3,stldt0(xB)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(xB)) ) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(fof_simplification,[status(thm)],[17,theory(equality)]) ).
fof(46,negated_conjecture,
~ ( ( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X1] :
( aElementOf0(X1,sdtbsmnsldt0(xA,xB))
<=> ( aInteger0(X1)
& ( aElementOf0(X1,xA)
| aElementOf0(X1,xB) ) ) ) )
=> ( ( ( aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) ) )
=> ( ! [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
=> ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ( aInteger0(X3)
& ( ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
| aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
=> aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) ) )
=> ( ! [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
=> aElementOf0(X3,stldt0(sdtbsmnsldt0(xA,xB))) )
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sdtbsmnsldt0(xA,xB))) ) ) ) )
| isOpen0(stldt0(sdtbsmnsldt0(xA,xB))) ) )
| isClosed0(sdtbsmnsldt0(xA,xB)) ) ),
inference(fof_simplification,[status(thm)],[42,theory(equality)]) ).
fof(69,plain,
! [X1,X2] :
( ~ aSubsetOf0(X1,cS1395)
| ~ aSubsetOf0(X2,cS1395)
| ~ isOpen0(X1)
| ~ isOpen0(X2)
| isOpen0(sdtslmnbsdt0(X1,X2)) ),
inference(fof_nnf,[status(thm)],[4]) ).
fof(70,plain,
! [X3,X4] :
( ~ aSubsetOf0(X3,cS1395)
| ~ aSubsetOf0(X4,cS1395)
| ~ isOpen0(X3)
| ~ isOpen0(X4)
| isOpen0(sdtslmnbsdt0(X3,X4)) ),
inference(variable_rename,[status(thm)],[69]) ).
cnf(71,plain,
( isOpen0(sdtslmnbsdt0(X1,X2))
| ~ isOpen0(X2)
| ~ isOpen0(X1)
| ~ aSubsetOf0(X2,cS1395)
| ~ aSubsetOf0(X1,cS1395) ),
inference(split_conjunct,[status(thm)],[70]) ).
fof(72,plain,
( aSet0(stldt0(xA))
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(xA))
| ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,xA)
| aElementOf0(X1,stldt0(xA)) ) )
& aSet0(cS1395)
& ! [X1] :
( ( ~ aElementOf0(X1,cS1395)
| aInteger0(X1) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,cS1395) ) )
& ! [X1] :
( ~ aElementOf0(X1,stldt0(xA))
| aElementOf0(X1,cS1395) )
& aSubsetOf0(stldt0(xA),cS1395)
& aSet0(stldt0(xB))
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(xB))
| ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,xB)
| aElementOf0(X1,stldt0(xB)) ) )
& aSet0(cS1395)
& ! [X1] :
( ( ~ aElementOf0(X1,cS1395)
| aInteger0(X1) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,cS1395) ) )
& ! [X1] :
( ~ aElementOf0(X1,stldt0(xB))
| aElementOf0(X1,cS1395) )
& aSubsetOf0(stldt0(xB),cS1395)
& aSet0(sdtbsmnsldt0(xA,xB))
& ! [X1] :
( ( ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB))
| ( aInteger0(X1)
& ( aElementOf0(X1,xA)
| aElementOf0(X1,xB) ) ) )
& ( ~ aInteger0(X1)
| ( ~ aElementOf0(X1,xA)
& ~ aElementOf0(X1,xB) )
| aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X1)
& ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,sdtbsmnsldt0(xA,xB))
| aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(xA))
| ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,xA)
| aElementOf0(X1,stldt0(xA)) ) )
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(xB))
| ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,xB)
| aElementOf0(X1,stldt0(xB)) ) )
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X1)
& aElementOf0(X1,stldt0(xA))
& aElementOf0(X1,stldt0(xB)) ) )
& ( ~ aInteger0(X1)
| ~ aElementOf0(X1,stldt0(xA))
| ~ aElementOf0(X1,stldt0(xB))
| aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& equal(stldt0(sdtbsmnsldt0(xA,xB)),sdtslmnbsdt0(stldt0(xA),stldt0(xB))) ),
inference(fof_nnf,[status(thm)],[44]) ).
fof(73,plain,
( aSet0(stldt0(xA))
& ! [X2] :
( ( ~ aElementOf0(X2,stldt0(xA))
| ( aInteger0(X2)
& ~ aElementOf0(X2,xA) ) )
& ( ~ aInteger0(X2)
| aElementOf0(X2,xA)
| aElementOf0(X2,stldt0(xA)) ) )
& aSet0(cS1395)
& ! [X3] :
( ( ~ aElementOf0(X3,cS1395)
| aInteger0(X3) )
& ( ~ aInteger0(X3)
| aElementOf0(X3,cS1395) ) )
& ! [X4] :
( ~ aElementOf0(X4,stldt0(xA))
| aElementOf0(X4,cS1395) )
& aSubsetOf0(stldt0(xA),cS1395)
& aSet0(stldt0(xB))
& ! [X5] :
( ( ~ aElementOf0(X5,stldt0(xB))
| ( aInteger0(X5)
& ~ aElementOf0(X5,xB) ) )
& ( ~ aInteger0(X5)
| aElementOf0(X5,xB)
| aElementOf0(X5,stldt0(xB)) ) )
& aSet0(cS1395)
& ! [X6] :
( ( ~ aElementOf0(X6,cS1395)
| aInteger0(X6) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,cS1395) ) )
& ! [X7] :
( ~ aElementOf0(X7,stldt0(xB))
| aElementOf0(X7,cS1395) )
& aSubsetOf0(stldt0(xB),cS1395)
& aSet0(sdtbsmnsldt0(xA,xB))
& ! [X8] :
( ( ~ aElementOf0(X8,sdtbsmnsldt0(xA,xB))
| ( aInteger0(X8)
& ( aElementOf0(X8,xA)
| aElementOf0(X8,xB) ) ) )
& ( ~ aInteger0(X8)
| ( ~ aElementOf0(X8,xA)
& ~ aElementOf0(X8,xB) )
| aElementOf0(X8,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X9] :
( ( ~ aElementOf0(X9,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X9)
& ~ aElementOf0(X9,sdtbsmnsldt0(xA,xB)) ) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,sdtbsmnsldt0(xA,xB))
| aElementOf0(X9,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& ! [X10] :
( ( ~ aElementOf0(X10,stldt0(xA))
| ( aInteger0(X10)
& ~ aElementOf0(X10,xA) ) )
& ( ~ aInteger0(X10)
| aElementOf0(X10,xA)
| aElementOf0(X10,stldt0(xA)) ) )
& ! [X11] :
( ( ~ aElementOf0(X11,stldt0(xB))
| ( aInteger0(X11)
& ~ aElementOf0(X11,xB) ) )
& ( ~ aInteger0(X11)
| aElementOf0(X11,xB)
| aElementOf0(X11,stldt0(xB)) ) )
& ! [X12] :
( ( ~ aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X12)
& aElementOf0(X12,stldt0(xA))
& aElementOf0(X12,stldt0(xB)) ) )
& ( ~ aInteger0(X12)
| ~ aElementOf0(X12,stldt0(xA))
| ~ aElementOf0(X12,stldt0(xB))
| aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& equal(stldt0(sdtbsmnsldt0(xA,xB)),sdtslmnbsdt0(stldt0(xA),stldt0(xB))) ),
inference(variable_rename,[status(thm)],[72]) ).
fof(74,plain,
! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ( ~ aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X12)
& aElementOf0(X12,stldt0(xA))
& aElementOf0(X12,stldt0(xB)) ) )
& ( ~ aInteger0(X12)
| ~ aElementOf0(X12,stldt0(xA))
| ~ aElementOf0(X12,stldt0(xB))
| aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ~ aElementOf0(X11,stldt0(xB))
| ( aInteger0(X11)
& ~ aElementOf0(X11,xB) ) )
& ( ~ aInteger0(X11)
| aElementOf0(X11,xB)
| aElementOf0(X11,stldt0(xB)) )
& ( ~ aElementOf0(X10,stldt0(xA))
| ( aInteger0(X10)
& ~ aElementOf0(X10,xA) ) )
& ( ~ aInteger0(X10)
| aElementOf0(X10,xA)
| aElementOf0(X10,stldt0(xA)) )
& ( ~ aElementOf0(X9,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X9)
& ~ aElementOf0(X9,sdtbsmnsldt0(xA,xB)) ) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,sdtbsmnsldt0(xA,xB))
| aElementOf0(X9,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ~ aElementOf0(X8,sdtbsmnsldt0(xA,xB))
| ( aInteger0(X8)
& ( aElementOf0(X8,xA)
| aElementOf0(X8,xB) ) ) )
& ( ~ aInteger0(X8)
| ( ~ aElementOf0(X8,xA)
& ~ aElementOf0(X8,xB) )
| aElementOf0(X8,sdtbsmnsldt0(xA,xB)) )
& ( ~ aElementOf0(X7,stldt0(xB))
| aElementOf0(X7,cS1395) )
& ( ~ aElementOf0(X6,cS1395)
| aInteger0(X6) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,cS1395) )
& ( ~ aElementOf0(X5,stldt0(xB))
| ( aInteger0(X5)
& ~ aElementOf0(X5,xB) ) )
& ( ~ aInteger0(X5)
| aElementOf0(X5,xB)
| aElementOf0(X5,stldt0(xB)) )
& ( ~ aElementOf0(X4,stldt0(xA))
| aElementOf0(X4,cS1395) )
& ( ~ aElementOf0(X3,cS1395)
| aInteger0(X3) )
& ( ~ aInteger0(X3)
| aElementOf0(X3,cS1395) )
& ( ~ aElementOf0(X2,stldt0(xA))
| ( aInteger0(X2)
& ~ aElementOf0(X2,xA) ) )
& ( ~ aInteger0(X2)
| aElementOf0(X2,xA)
| aElementOf0(X2,stldt0(xA)) )
& aSet0(stldt0(xA))
& aSet0(cS1395)
& aSubsetOf0(stldt0(xA),cS1395)
& aSet0(stldt0(xB))
& aSet0(cS1395)
& aSubsetOf0(stldt0(xB),cS1395)
& aSet0(sdtbsmnsldt0(xA,xB))
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& equal(stldt0(sdtbsmnsldt0(xA,xB)),sdtslmnbsdt0(stldt0(xA),stldt0(xB))) ),
inference(shift_quantors,[status(thm)],[73]) ).
fof(75,plain,
! [X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ( aInteger0(X12)
| ~ aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( aElementOf0(X12,stldt0(xA))
| ~ aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( aElementOf0(X12,stldt0(xB))
| ~ aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ~ aInteger0(X12)
| ~ aElementOf0(X12,stldt0(xA))
| ~ aElementOf0(X12,stldt0(xB))
| aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( aInteger0(X11)
| ~ aElementOf0(X11,stldt0(xB)) )
& ( ~ aElementOf0(X11,xB)
| ~ aElementOf0(X11,stldt0(xB)) )
& ( ~ aInteger0(X11)
| aElementOf0(X11,xB)
| aElementOf0(X11,stldt0(xB)) )
& ( aInteger0(X10)
| ~ aElementOf0(X10,stldt0(xA)) )
& ( ~ aElementOf0(X10,xA)
| ~ aElementOf0(X10,stldt0(xA)) )
& ( ~ aInteger0(X10)
| aElementOf0(X10,xA)
| aElementOf0(X10,stldt0(xA)) )
& ( aInteger0(X9)
| ~ aElementOf0(X9,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ~ aElementOf0(X9,sdtbsmnsldt0(xA,xB))
| ~ aElementOf0(X9,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,sdtbsmnsldt0(xA,xB))
| aElementOf0(X9,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( aInteger0(X8)
| ~ aElementOf0(X8,sdtbsmnsldt0(xA,xB)) )
& ( aElementOf0(X8,xA)
| aElementOf0(X8,xB)
| ~ aElementOf0(X8,sdtbsmnsldt0(xA,xB)) )
& ( ~ aElementOf0(X8,xA)
| ~ aInteger0(X8)
| aElementOf0(X8,sdtbsmnsldt0(xA,xB)) )
& ( ~ aElementOf0(X8,xB)
| ~ aInteger0(X8)
| aElementOf0(X8,sdtbsmnsldt0(xA,xB)) )
& ( ~ aElementOf0(X7,stldt0(xB))
| aElementOf0(X7,cS1395) )
& ( ~ aElementOf0(X6,cS1395)
| aInteger0(X6) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,cS1395) )
& ( aInteger0(X5)
| ~ aElementOf0(X5,stldt0(xB)) )
& ( ~ aElementOf0(X5,xB)
| ~ aElementOf0(X5,stldt0(xB)) )
& ( ~ aInteger0(X5)
| aElementOf0(X5,xB)
| aElementOf0(X5,stldt0(xB)) )
& ( ~ aElementOf0(X4,stldt0(xA))
| aElementOf0(X4,cS1395) )
& ( ~ aElementOf0(X3,cS1395)
| aInteger0(X3) )
& ( ~ aInteger0(X3)
| aElementOf0(X3,cS1395) )
& ( aInteger0(X2)
| ~ aElementOf0(X2,stldt0(xA)) )
& ( ~ aElementOf0(X2,xA)
| ~ aElementOf0(X2,stldt0(xA)) )
& ( ~ aInteger0(X2)
| aElementOf0(X2,xA)
| aElementOf0(X2,stldt0(xA)) )
& aSet0(stldt0(xA))
& aSet0(cS1395)
& aSubsetOf0(stldt0(xA),cS1395)
& aSet0(stldt0(xB))
& aSet0(cS1395)
& aSubsetOf0(stldt0(xB),cS1395)
& aSet0(sdtbsmnsldt0(xA,xB))
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& equal(stldt0(sdtbsmnsldt0(xA,xB)),sdtslmnbsdt0(stldt0(xA),stldt0(xB))) ),
inference(distribute,[status(thm)],[74]) ).
cnf(76,plain,
stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(79,plain,
aSubsetOf0(stldt0(xB),cS1395),
inference(split_conjunct,[status(thm)],[75]) ).
cnf(82,plain,
aSubsetOf0(stldt0(xA),cS1395),
inference(split_conjunct,[status(thm)],[75]) ).
fof(172,plain,
( aSet0(cS1395)
& ! [X1] :
( ( ~ aElementOf0(X1,cS1395)
| aInteger0(X1) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,cS1395) ) )
& aSet0(xA)
& ! [X1] :
( ~ aElementOf0(X1,xA)
| aElementOf0(X1,cS1395) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X1] :
( ( ~ aElementOf0(X1,cS1395)
| aInteger0(X1) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,cS1395) ) )
& aSet0(xB)
& ! [X1] :
( ~ aElementOf0(X1,xB)
| aElementOf0(X1,cS1395) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(xA))
| ( aInteger0(X1)
& ~ aElementOf0(X1,xA) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,xA)
| aElementOf0(X1,stldt0(xA)) ) )
& ! [X1] :
( ~ aElementOf0(X1,stldt0(xA))
| ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
| ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ~ aInteger0(X3)
| ( ! [X4] :
( ~ aInteger0(X4)
| ~ equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& ~ aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& ~ sdteqdtlpzmzozddtrp0(X3,X1,X2) )
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) )
& ! [X3] :
( ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
| aElementOf0(X3,stldt0(xA)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(xA)) ) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(xB))
| ( aInteger0(X1)
& ~ aElementOf0(X1,xB) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,xB)
| aElementOf0(X1,stldt0(xB)) ) )
& ! [X1] :
( ~ aElementOf0(X1,stldt0(xB))
| ? [X2] :
( aInteger0(X2)
& ~ equal(X2,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
| ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ~ aInteger0(X3)
| ( ! [X4] :
( ~ aInteger0(X4)
| ~ equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& ~ aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& ~ sdteqdtlpzmzozddtrp0(X3,X1,X2) )
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) )
& ! [X3] :
( ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
| aElementOf0(X3,stldt0(xB)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(xB)) ) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(fof_nnf,[status(thm)],[45]) ).
fof(173,plain,
( aSet0(cS1395)
& ! [X5] :
( ( ~ aElementOf0(X5,cS1395)
| aInteger0(X5) )
& ( ~ aInteger0(X5)
| aElementOf0(X5,cS1395) ) )
& aSet0(xA)
& ! [X6] :
( ~ aElementOf0(X6,xA)
| aElementOf0(X6,cS1395) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X7] :
( ( ~ aElementOf0(X7,cS1395)
| aInteger0(X7) )
& ( ~ aInteger0(X7)
| aElementOf0(X7,cS1395) ) )
& aSet0(xB)
& ! [X8] :
( ~ aElementOf0(X8,xB)
| aElementOf0(X8,cS1395) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X9] :
( ( ~ aElementOf0(X9,stldt0(xA))
| ( aInteger0(X9)
& ~ aElementOf0(X9,xA) ) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,xA)
| aElementOf0(X9,stldt0(xA)) ) )
& ! [X10] :
( ~ aElementOf0(X10,stldt0(xA))
| ? [X11] :
( aInteger0(X11)
& ~ equal(X11,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X10,X11))
& ! [X12] :
( ( ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,X11))
| ( aInteger0(X12)
& ? [X13] :
( aInteger0(X13)
& equal(sdtasdt0(X11,X13),sdtpldt0(X12,smndt0(X10))) )
& aDivisorOf0(X11,sdtpldt0(X12,smndt0(X10)))
& sdteqdtlpzmzozddtrp0(X12,X10,X11) ) )
& ( ~ aInteger0(X12)
| ( ! [X14] :
( ~ aInteger0(X14)
| ~ equal(sdtasdt0(X11,X14),sdtpldt0(X12,smndt0(X10))) )
& ~ aDivisorOf0(X11,sdtpldt0(X12,smndt0(X10)))
& ~ sdteqdtlpzmzozddtrp0(X12,X10,X11) )
| aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,X11)) ) )
& ! [X15] :
( ~ aElementOf0(X15,szAzrzSzezqlpdtcmdtrp0(X10,X11))
| aElementOf0(X15,stldt0(xA)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X10,X11),stldt0(xA)) ) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X16] :
( ( ~ aElementOf0(X16,stldt0(xB))
| ( aInteger0(X16)
& ~ aElementOf0(X16,xB) ) )
& ( ~ aInteger0(X16)
| aElementOf0(X16,xB)
| aElementOf0(X16,stldt0(xB)) ) )
& ! [X17] :
( ~ aElementOf0(X17,stldt0(xB))
| ? [X18] :
( aInteger0(X18)
& ~ equal(X18,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X17,X18))
& ! [X19] :
( ( ~ aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,X18))
| ( aInteger0(X19)
& ? [X20] :
( aInteger0(X20)
& equal(sdtasdt0(X18,X20),sdtpldt0(X19,smndt0(X17))) )
& aDivisorOf0(X18,sdtpldt0(X19,smndt0(X17)))
& sdteqdtlpzmzozddtrp0(X19,X17,X18) ) )
& ( ~ aInteger0(X19)
| ( ! [X21] :
( ~ aInteger0(X21)
| ~ equal(sdtasdt0(X18,X21),sdtpldt0(X19,smndt0(X17))) )
& ~ aDivisorOf0(X18,sdtpldt0(X19,smndt0(X17)))
& ~ sdteqdtlpzmzozddtrp0(X19,X17,X18) )
| aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,X18)) ) )
& ! [X22] :
( ~ aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X17,X18))
| aElementOf0(X22,stldt0(xB)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X17,X18),stldt0(xB)) ) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(variable_rename,[status(thm)],[172]) ).
fof(174,plain,
( aSet0(cS1395)
& ! [X5] :
( ( ~ aElementOf0(X5,cS1395)
| aInteger0(X5) )
& ( ~ aInteger0(X5)
| aElementOf0(X5,cS1395) ) )
& aSet0(xA)
& ! [X6] :
( ~ aElementOf0(X6,xA)
| aElementOf0(X6,cS1395) )
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& ! [X7] :
( ( ~ aElementOf0(X7,cS1395)
| aInteger0(X7) )
& ( ~ aInteger0(X7)
| aElementOf0(X7,cS1395) ) )
& aSet0(xB)
& ! [X8] :
( ~ aElementOf0(X8,xB)
| aElementOf0(X8,cS1395) )
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& ! [X9] :
( ( ~ aElementOf0(X9,stldt0(xA))
| ( aInteger0(X9)
& ~ aElementOf0(X9,xA) ) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,xA)
| aElementOf0(X9,stldt0(xA)) ) )
& ! [X10] :
( ~ aElementOf0(X10,stldt0(xA))
| ( aInteger0(esk5_1(X10))
& ~ equal(esk5_1(X10),sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
& ! [X12] :
( ( ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ( aInteger0(X12)
& aInteger0(esk6_2(X10,X12))
& equal(sdtasdt0(esk5_1(X10),esk6_2(X10,X12)),sdtpldt0(X12,smndt0(X10)))
& aDivisorOf0(esk5_1(X10),sdtpldt0(X12,smndt0(X10)))
& sdteqdtlpzmzozddtrp0(X12,X10,esk5_1(X10)) ) )
& ( ~ aInteger0(X12)
| ( ! [X14] :
( ~ aInteger0(X14)
| ~ equal(sdtasdt0(esk5_1(X10),X14),sdtpldt0(X12,smndt0(X10))) )
& ~ aDivisorOf0(esk5_1(X10),sdtpldt0(X12,smndt0(X10)))
& ~ sdteqdtlpzmzozddtrp0(X12,X10,esk5_1(X10)) )
| aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10))) ) )
& ! [X15] :
( ~ aElementOf0(X15,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| aElementOf0(X15,stldt0(xA)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)),stldt0(xA)) ) )
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& ! [X16] :
( ( ~ aElementOf0(X16,stldt0(xB))
| ( aInteger0(X16)
& ~ aElementOf0(X16,xB) ) )
& ( ~ aInteger0(X16)
| aElementOf0(X16,xB)
| aElementOf0(X16,stldt0(xB)) ) )
& ! [X17] :
( ~ aElementOf0(X17,stldt0(xB))
| ( aInteger0(esk7_1(X17))
& ~ equal(esk7_1(X17),sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
& ! [X19] :
( ( ~ aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ( aInteger0(X19)
& aInteger0(esk8_2(X17,X19))
& equal(sdtasdt0(esk7_1(X17),esk8_2(X17,X19)),sdtpldt0(X19,smndt0(X17)))
& aDivisorOf0(esk7_1(X17),sdtpldt0(X19,smndt0(X17)))
& sdteqdtlpzmzozddtrp0(X19,X17,esk7_1(X17)) ) )
& ( ~ aInteger0(X19)
| ( ! [X21] :
( ~ aInteger0(X21)
| ~ equal(sdtasdt0(esk7_1(X17),X21),sdtpldt0(X19,smndt0(X17))) )
& ~ aDivisorOf0(esk7_1(X17),sdtpldt0(X19,smndt0(X17)))
& ~ sdteqdtlpzmzozddtrp0(X19,X17,esk7_1(X17)) )
| aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17))) ) )
& ! [X22] :
( ~ aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| aElementOf0(X22,stldt0(xB)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)),stldt0(xB)) ) )
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(skolemize,[status(esa)],[173]) ).
fof(175,plain,
! [X5,X6,X7,X8,X9,X10,X12,X14,X15,X16,X17,X19,X21,X22] :
( ( ( ( ~ aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| aElementOf0(X22,stldt0(xB)) )
& ( ( ( ~ aInteger0(X21)
| ~ equal(sdtasdt0(esk7_1(X17),X21),sdtpldt0(X19,smndt0(X17))) )
& ~ aDivisorOf0(esk7_1(X17),sdtpldt0(X19,smndt0(X17)))
& ~ sdteqdtlpzmzozddtrp0(X19,X17,esk7_1(X17)) )
| ~ aInteger0(X19)
| aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17))) )
& ( ~ aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ( aInteger0(X19)
& aInteger0(esk8_2(X17,X19))
& equal(sdtasdt0(esk7_1(X17),esk8_2(X17,X19)),sdtpldt0(X19,smndt0(X17)))
& aDivisorOf0(esk7_1(X17),sdtpldt0(X19,smndt0(X17)))
& sdteqdtlpzmzozddtrp0(X19,X17,esk7_1(X17)) ) )
& aInteger0(esk7_1(X17))
& ~ equal(esk7_1(X17),sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)),stldt0(xB)) )
| ~ aElementOf0(X17,stldt0(xB)) )
& ( ~ aElementOf0(X16,stldt0(xB))
| ( aInteger0(X16)
& ~ aElementOf0(X16,xB) ) )
& ( ~ aInteger0(X16)
| aElementOf0(X16,xB)
| aElementOf0(X16,stldt0(xB)) )
& ( ( ( ~ aElementOf0(X15,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| aElementOf0(X15,stldt0(xA)) )
& ( ( ( ~ aInteger0(X14)
| ~ equal(sdtasdt0(esk5_1(X10),X14),sdtpldt0(X12,smndt0(X10))) )
& ~ aDivisorOf0(esk5_1(X10),sdtpldt0(X12,smndt0(X10)))
& ~ sdteqdtlpzmzozddtrp0(X12,X10,esk5_1(X10)) )
| ~ aInteger0(X12)
| aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10))) )
& ( ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ( aInteger0(X12)
& aInteger0(esk6_2(X10,X12))
& equal(sdtasdt0(esk5_1(X10),esk6_2(X10,X12)),sdtpldt0(X12,smndt0(X10)))
& aDivisorOf0(esk5_1(X10),sdtpldt0(X12,smndt0(X10)))
& sdteqdtlpzmzozddtrp0(X12,X10,esk5_1(X10)) ) )
& aInteger0(esk5_1(X10))
& ~ equal(esk5_1(X10),sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)),stldt0(xA)) )
| ~ aElementOf0(X10,stldt0(xA)) )
& ( ~ aElementOf0(X9,stldt0(xA))
| ( aInteger0(X9)
& ~ aElementOf0(X9,xA) ) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,xA)
| aElementOf0(X9,stldt0(xA)) )
& ( ~ aElementOf0(X8,xB)
| aElementOf0(X8,cS1395) )
& ( ~ aElementOf0(X7,cS1395)
| aInteger0(X7) )
& ( ~ aInteger0(X7)
| aElementOf0(X7,cS1395) )
& ( ~ aElementOf0(X6,xA)
| aElementOf0(X6,cS1395) )
& ( ~ aElementOf0(X5,cS1395)
| aInteger0(X5) )
& ( ~ aInteger0(X5)
| aElementOf0(X5,cS1395) )
& aSet0(cS1395)
& aSet0(xA)
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& aSet0(xB)
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(shift_quantors,[status(thm)],[174]) ).
fof(176,plain,
! [X5,X6,X7,X8,X9,X10,X12,X14,X15,X16,X17,X19,X21,X22] :
( ( ~ aElementOf0(X22,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| aElementOf0(X22,stldt0(xB))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( ~ aInteger0(X21)
| ~ equal(sdtasdt0(esk7_1(X17),X21),sdtpldt0(X19,smndt0(X17)))
| ~ aInteger0(X19)
| aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( ~ aDivisorOf0(esk7_1(X17),sdtpldt0(X19,smndt0(X17)))
| ~ aInteger0(X19)
| aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( ~ sdteqdtlpzmzozddtrp0(X19,X17,esk7_1(X17))
| ~ aInteger0(X19)
| aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( aInteger0(X19)
| ~ aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( aInteger0(esk8_2(X17,X19))
| ~ aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( equal(sdtasdt0(esk7_1(X17),esk8_2(X17,X19)),sdtpldt0(X19,smndt0(X17)))
| ~ aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( aDivisorOf0(esk7_1(X17),sdtpldt0(X19,smndt0(X17)))
| ~ aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( sdteqdtlpzmzozddtrp0(X19,X17,esk7_1(X17))
| ~ aElementOf0(X19,szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( aInteger0(esk7_1(X17))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( ~ equal(esk7_1(X17),sz00)
| ~ aElementOf0(X17,stldt0(xB)) )
& ( aSet0(szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X17,esk7_1(X17)),stldt0(xB))
| ~ aElementOf0(X17,stldt0(xB)) )
& ( aInteger0(X16)
| ~ aElementOf0(X16,stldt0(xB)) )
& ( ~ aElementOf0(X16,xB)
| ~ aElementOf0(X16,stldt0(xB)) )
& ( ~ aInteger0(X16)
| aElementOf0(X16,xB)
| aElementOf0(X16,stldt0(xB)) )
& ( ~ aElementOf0(X15,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| aElementOf0(X15,stldt0(xA))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( ~ aInteger0(X14)
| ~ equal(sdtasdt0(esk5_1(X10),X14),sdtpldt0(X12,smndt0(X10)))
| ~ aInteger0(X12)
| aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( ~ aDivisorOf0(esk5_1(X10),sdtpldt0(X12,smndt0(X10)))
| ~ aInteger0(X12)
| aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( ~ sdteqdtlpzmzozddtrp0(X12,X10,esk5_1(X10))
| ~ aInteger0(X12)
| aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( aInteger0(X12)
| ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( aInteger0(esk6_2(X10,X12))
| ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( equal(sdtasdt0(esk5_1(X10),esk6_2(X10,X12)),sdtpldt0(X12,smndt0(X10)))
| ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( aDivisorOf0(esk5_1(X10),sdtpldt0(X12,smndt0(X10)))
| ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( sdteqdtlpzmzozddtrp0(X12,X10,esk5_1(X10))
| ~ aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( aInteger0(esk5_1(X10))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( ~ equal(esk5_1(X10),sz00)
| ~ aElementOf0(X10,stldt0(xA)) )
& ( aSet0(szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X10,esk5_1(X10)),stldt0(xA))
| ~ aElementOf0(X10,stldt0(xA)) )
& ( aInteger0(X9)
| ~ aElementOf0(X9,stldt0(xA)) )
& ( ~ aElementOf0(X9,xA)
| ~ aElementOf0(X9,stldt0(xA)) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,xA)
| aElementOf0(X9,stldt0(xA)) )
& ( ~ aElementOf0(X8,xB)
| aElementOf0(X8,cS1395) )
& ( ~ aElementOf0(X7,cS1395)
| aInteger0(X7) )
& ( ~ aInteger0(X7)
| aElementOf0(X7,cS1395) )
& ( ~ aElementOf0(X6,xA)
| aElementOf0(X6,cS1395) )
& ( ~ aElementOf0(X5,cS1395)
| aInteger0(X5) )
& ( ~ aInteger0(X5)
| aElementOf0(X5,cS1395) )
& aSet0(cS1395)
& aSet0(xA)
& aSubsetOf0(xA,cS1395)
& aSet0(cS1395)
& aSet0(xB)
& aSubsetOf0(xB,cS1395)
& aSet0(stldt0(xA))
& isOpen0(stldt0(xA))
& isClosed0(xA)
& aSet0(stldt0(xB))
& isOpen0(stldt0(xB))
& isClosed0(xB) ),
inference(distribute,[status(thm)],[175]) ).
cnf(178,plain,
isOpen0(stldt0(xB)),
inference(split_conjunct,[status(thm)],[176]) ).
cnf(181,plain,
isOpen0(stldt0(xA)),
inference(split_conjunct,[status(thm)],[176]) ).
fof(303,negated_conjecture,
( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X1] :
( ( ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB))
| ( aInteger0(X1)
& ( aElementOf0(X1,xA)
| aElementOf0(X1,xB) ) ) )
& ( ~ aInteger0(X1)
| ( ~ aElementOf0(X1,xA)
& ~ aElementOf0(X1,xB) )
| aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X1)
& ~ aElementOf0(X1,sdtbsmnsldt0(xA,xB)) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,sdtbsmnsldt0(xA,xB))
| aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& ? [X1] :
( aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X2] :
( ~ aInteger0(X2)
| equal(X2,sz00)
| ( aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ! [X3] :
( ( ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
| ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& sdteqdtlpzmzozddtrp0(X3,X1,X2) ) )
& ( ~ aInteger0(X3)
| ( ! [X4] :
( ~ aInteger0(X4)
| ~ equal(sdtasdt0(X2,X4),sdtpldt0(X3,smndt0(X1))) )
& ~ aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1)))
& ~ sdteqdtlpzmzozddtrp0(X3,X1,X2) )
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ) )
& ? [X3] :
( aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))
& ~ aElementOf0(X3,stldt0(sdtbsmnsldt0(xA,xB))) )
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sdtbsmnsldt0(xA,xB))) ) ) )
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ~ isClosed0(sdtbsmnsldt0(xA,xB)) ),
inference(fof_nnf,[status(thm)],[46]) ).
fof(304,negated_conjecture,
( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X5] :
( ( ~ aElementOf0(X5,sdtbsmnsldt0(xA,xB))
| ( aInteger0(X5)
& ( aElementOf0(X5,xA)
| aElementOf0(X5,xB) ) ) )
& ( ~ aInteger0(X5)
| ( ~ aElementOf0(X5,xA)
& ~ aElementOf0(X5,xB) )
| aElementOf0(X5,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X6] :
( ( ~ aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X6)
& ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB)) ) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& ? [X7] :
( aElementOf0(X7,stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X8] :
( ~ aInteger0(X8)
| equal(X8,sz00)
| ( aSet0(szAzrzSzezqlpdtcmdtrp0(X7,X8))
& ! [X9] :
( ( ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(X7,X8))
| ( aInteger0(X9)
& ? [X10] :
( aInteger0(X10)
& equal(sdtasdt0(X8,X10),sdtpldt0(X9,smndt0(X7))) )
& aDivisorOf0(X8,sdtpldt0(X9,smndt0(X7)))
& sdteqdtlpzmzozddtrp0(X9,X7,X8) ) )
& ( ~ aInteger0(X9)
| ( ! [X11] :
( ~ aInteger0(X11)
| ~ equal(sdtasdt0(X8,X11),sdtpldt0(X9,smndt0(X7))) )
& ~ aDivisorOf0(X8,sdtpldt0(X9,smndt0(X7)))
& ~ sdteqdtlpzmzozddtrp0(X9,X7,X8) )
| aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(X7,X8)) ) )
& ? [X12] :
( aElementOf0(X12,szAzrzSzezqlpdtcmdtrp0(X7,X8))
& ~ aElementOf0(X12,stldt0(sdtbsmnsldt0(xA,xB))) )
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X7,X8),stldt0(sdtbsmnsldt0(xA,xB))) ) ) )
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ~ isClosed0(sdtbsmnsldt0(xA,xB)) ),
inference(variable_rename,[status(thm)],[303]) ).
fof(305,negated_conjecture,
( aSet0(sdtbsmnsldt0(xA,xB))
& ! [X5] :
( ( ~ aElementOf0(X5,sdtbsmnsldt0(xA,xB))
| ( aInteger0(X5)
& ( aElementOf0(X5,xA)
| aElementOf0(X5,xB) ) ) )
& ( ~ aInteger0(X5)
| ( ~ aElementOf0(X5,xA)
& ~ aElementOf0(X5,xB) )
| aElementOf0(X5,sdtbsmnsldt0(xA,xB)) ) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X6] :
( ( ~ aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X6)
& ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB)) ) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB))) ) )
& aElementOf0(esk17_0,stldt0(sdtbsmnsldt0(xA,xB)))
& ! [X8] :
( ~ aInteger0(X8)
| equal(X8,sz00)
| ( aSet0(szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
& ! [X9] :
( ( ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ( aInteger0(X9)
& aInteger0(esk18_2(X8,X9))
& equal(sdtasdt0(X8,esk18_2(X8,X9)),sdtpldt0(X9,smndt0(esk17_0)))
& aDivisorOf0(X8,sdtpldt0(X9,smndt0(esk17_0)))
& sdteqdtlpzmzozddtrp0(X9,esk17_0,X8) ) )
& ( ~ aInteger0(X9)
| ( ! [X11] :
( ~ aInteger0(X11)
| ~ equal(sdtasdt0(X8,X11),sdtpldt0(X9,smndt0(esk17_0))) )
& ~ aDivisorOf0(X8,sdtpldt0(X9,smndt0(esk17_0)))
& ~ sdteqdtlpzmzozddtrp0(X9,esk17_0,X8) )
| aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8)) ) )
& aElementOf0(esk19_1(X8),szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
& ~ aElementOf0(esk19_1(X8),stldt0(sdtbsmnsldt0(xA,xB)))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk17_0,X8),stldt0(sdtbsmnsldt0(xA,xB))) ) )
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ~ isClosed0(sdtbsmnsldt0(xA,xB)) ),
inference(skolemize,[status(esa)],[304]) ).
fof(306,negated_conjecture,
! [X5,X6,X8,X9,X11] :
( ( ( ( ( ( ~ aInteger0(X11)
| ~ equal(sdtasdt0(X8,X11),sdtpldt0(X9,smndt0(esk17_0))) )
& ~ aDivisorOf0(X8,sdtpldt0(X9,smndt0(esk17_0)))
& ~ sdteqdtlpzmzozddtrp0(X9,esk17_0,X8) )
| ~ aInteger0(X9)
| aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8)) )
& ( ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ( aInteger0(X9)
& aInteger0(esk18_2(X8,X9))
& equal(sdtasdt0(X8,esk18_2(X8,X9)),sdtpldt0(X9,smndt0(esk17_0)))
& aDivisorOf0(X8,sdtpldt0(X9,smndt0(esk17_0)))
& sdteqdtlpzmzozddtrp0(X9,esk17_0,X8) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
& aElementOf0(esk19_1(X8),szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
& ~ aElementOf0(esk19_1(X8),stldt0(sdtbsmnsldt0(xA,xB)))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk17_0,X8),stldt0(sdtbsmnsldt0(xA,xB))) )
| ~ aInteger0(X8)
| equal(X8,sz00) )
& aElementOf0(esk17_0,stldt0(sdtbsmnsldt0(xA,xB)))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ( ~ aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB)))
| ( aInteger0(X6)
& ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB)) ) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ( ~ aElementOf0(X5,sdtbsmnsldt0(xA,xB))
| ( aInteger0(X5)
& ( aElementOf0(X5,xA)
| aElementOf0(X5,xB) ) ) )
& ( ~ aInteger0(X5)
| ( ~ aElementOf0(X5,xA)
& ~ aElementOf0(X5,xB) )
| aElementOf0(X5,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(shift_quantors,[status(thm)],[305]) ).
fof(307,negated_conjecture,
! [X5,X6,X8,X9,X11] :
( ( ~ aInteger0(X11)
| ~ equal(sdtasdt0(X8,X11),sdtpldt0(X9,smndt0(esk17_0)))
| ~ aInteger0(X9)
| aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( ~ aDivisorOf0(X8,sdtpldt0(X9,smndt0(esk17_0)))
| ~ aInteger0(X9)
| aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( ~ sdteqdtlpzmzozddtrp0(X9,esk17_0,X8)
| ~ aInteger0(X9)
| aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( aInteger0(X9)
| ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( aInteger0(esk18_2(X8,X9))
| ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( equal(sdtasdt0(X8,esk18_2(X8,X9)),sdtpldt0(X9,smndt0(esk17_0)))
| ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( aDivisorOf0(X8,sdtpldt0(X9,smndt0(esk17_0)))
| ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( sdteqdtlpzmzozddtrp0(X9,esk17_0,X8)
| ~ aElementOf0(X9,szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( aSet0(szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( aElementOf0(esk19_1(X8),szAzrzSzezqlpdtcmdtrp0(esk17_0,X8))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( ~ aElementOf0(esk19_1(X8),stldt0(sdtbsmnsldt0(xA,xB)))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(esk17_0,X8),stldt0(sdtbsmnsldt0(xA,xB)))
| ~ aInteger0(X8)
| equal(X8,sz00) )
& aElementOf0(esk17_0,stldt0(sdtbsmnsldt0(xA,xB)))
& ~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
& ( aInteger0(X6)
| ~ aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ~ aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| ~ aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB))) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,sdtbsmnsldt0(xA,xB))
| aElementOf0(X6,stldt0(sdtbsmnsldt0(xA,xB))) )
& aSet0(stldt0(sdtbsmnsldt0(xA,xB)))
& ~ isClosed0(sdtbsmnsldt0(xA,xB))
& ( aInteger0(X5)
| ~ aElementOf0(X5,sdtbsmnsldt0(xA,xB)) )
& ( aElementOf0(X5,xA)
| aElementOf0(X5,xB)
| ~ aElementOf0(X5,sdtbsmnsldt0(xA,xB)) )
& ( ~ aElementOf0(X5,xA)
| ~ aInteger0(X5)
| aElementOf0(X5,sdtbsmnsldt0(xA,xB)) )
& ( ~ aElementOf0(X5,xB)
| ~ aInteger0(X5)
| aElementOf0(X5,sdtbsmnsldt0(xA,xB)) )
& aSet0(sdtbsmnsldt0(xA,xB)) ),
inference(distribute,[status(thm)],[306]) ).
cnf(318,negated_conjecture,
~ isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),
inference(split_conjunct,[status(thm)],[307]) ).
cnf(876,plain,
( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| ~ isOpen0(stldt0(xB))
| ~ isOpen0(stldt0(xA))
| ~ aSubsetOf0(stldt0(xB),cS1395)
| ~ aSubsetOf0(stldt0(xA),cS1395) ),
inference(spm,[status(thm)],[71,76,theory(equality)]) ).
cnf(877,plain,
( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| $false
| ~ isOpen0(stldt0(xA))
| ~ aSubsetOf0(stldt0(xB),cS1395)
| ~ aSubsetOf0(stldt0(xA),cS1395) ),
inference(rw,[status(thm)],[876,178,theory(equality)]) ).
cnf(878,plain,
( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| $false
| $false
| ~ aSubsetOf0(stldt0(xB),cS1395)
| ~ aSubsetOf0(stldt0(xA),cS1395) ),
inference(rw,[status(thm)],[877,181,theory(equality)]) ).
cnf(879,plain,
( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| $false
| $false
| $false
| ~ aSubsetOf0(stldt0(xA),cS1395) ),
inference(rw,[status(thm)],[878,79,theory(equality)]) ).
cnf(880,plain,
( isOpen0(stldt0(sdtbsmnsldt0(xA,xB)))
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[879,82,theory(equality)]) ).
cnf(881,plain,
isOpen0(stldt0(sdtbsmnsldt0(xA,xB))),
inference(cn,[status(thm)],[880,theory(equality)]) ).
cnf(882,plain,
$false,
inference(sr,[status(thm)],[881,318,theory(equality)]) ).
cnf(883,plain,
$false,
882,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM441+6 : TPTP v7.0.0. Released v4.0.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n072.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.625MB
% 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Fri Jan 5 05:17:59 CST 2018
% 0.02/0.24 % CPUTime :
% 0.06/0.28 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.28 --creating new selector for []
% 0.06/0.38 -running prover on /export/starexec/sandbox/tmp/tmpyW_fKY/sel_theBenchmark.p_1 with time limit 29
% 0.06/0.38 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox/tmp/tmpyW_fKY/sel_theBenchmark.p_1']
% 0.06/0.38 -prover status Theorem
% 0.06/0.38 Problem theBenchmark.p solved in phase 0.
% 0.06/0.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.38 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.38 Solved 1 out of 1.
% 0.06/0.38 # Problem is unsatisfiable (or provable), constructing proof object
% 0.06/0.38 # SZS status Theorem
% 0.06/0.38 # SZS output start CNFRefutation.
% See solution above
% 0.06/0.39 # SZS output end CNFRefutation
%------------------------------------------------------------------------------