%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM451+6 : TPTP v7.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n079.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:22 EST 2018
% Result : Theorem 84.95s
% Output : CNFRefutation 84.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 169
% Number of leaves : 26
% Syntax : Number of formulae : 869 ( 105 unt; 0 def)
% Number of atoms : 3589 ( 781 equ)
% Maximal formula atoms : 116 ( 4 avg)
% Number of connectives : 4319 (1599 ~;2039 |; 615 &)
% ( 20 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 58 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 6 con; 0-2 aty)
% Number of variables : 809 ( 0 sgn 317 !; 49 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
! [X1] :
( aInteger0(X1)
=> ( equal(sdtasdt0(X1,sz10),X1)
& equal(X1,sdtasdt0(sz10,X1)) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mMulOne) ).
fof(3,axiom,
! [X1] :
( aInteger0(X1)
=> ( equal(sdtasdt0(smndt0(sz10),X1),smndt0(X1))
& equal(smndt0(X1),sdtasdt0(X1,smndt0(sz10))) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mMulMinOne) ).
fof(5,axiom,
! [X1] :
( aInteger0(X1)
=> ( equal(sdtasdt0(X1,sz00),sz00)
& equal(sz00,sdtasdt0(sz00,X1)) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mMulZero) ).
fof(7,axiom,
! [X1,X2] :
( ( aInteger0(X1)
& aInteger0(X2) )
=> equal(sdtpldt0(X1,X2),sdtpldt0(X2,X1)) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mAddComm) ).
fof(8,axiom,
! [X1,X2] :
( ( aInteger0(X1)
& aInteger0(X2) )
=> aInteger0(sdtpldt0(X1,X2)) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mIntPlus) ).
fof(9,axiom,
! [X1] :
( aInteger0(X1)
=> ! [X2] :
( aDivisorOf0(X2,X1)
<=> ( aInteger0(X2)
& ~ equal(X2,sz00)
& ? [X3] :
( aInteger0(X3)
& equal(sdtasdt0(X2,X3),X1) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mDivisor) ).
fof(10,axiom,
! [X1,X2,X3] :
( ( aInteger0(X1)
& aInteger0(X2)
& aInteger0(X3)
& ~ equal(X3,sz00) )
=> ( sdteqdtlpzmzozddtrp0(X1,X2,X3)
=> sdteqdtlpzmzozddtrp0(X2,X1,X3) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mEquModSym) ).
fof(11,axiom,
! [X1,X2] :
( ( aInteger0(X1)
& aInteger0(X2) )
=> ( equal(sdtasdt0(X1,X2),sz00)
=> ( equal(X1,sz00)
| equal(X2,sz00) ) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mZeroDiv) ).
fof(17,axiom,
! [X1,X2,X3,X4] :
( ( aInteger0(X1)
& aInteger0(X2)
& aInteger0(X3)
& ~ equal(X3,sz00)
& aInteger0(X4) )
=> ( ( sdteqdtlpzmzozddtrp0(X1,X2,X3)
& sdteqdtlpzmzozddtrp0(X2,X4,X3) )
=> sdteqdtlpzmzozddtrp0(X1,X4,X3) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mEquModTrn) ).
fof(18,axiom,
( aSet0(sbsmnsldt0(xS))
& ! [X1] :
( aElementOf0(X1,sbsmnsldt0(xS))
<=> ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
=> ? [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(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS))) ) )
& isOpen0(stldt0(sbsmnsldt0(xS)))
& isClosed0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS))
& ! [X1] :
( aElementOf0(X1,sbsmnsldt0(xS))
<=> ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
=> ? [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(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS))) ) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',m__2144) ).
fof(19,axiom,
aInteger0(sz10),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mIntOne) ).
fof(23,axiom,
( aSet0(sbsmnsldt0(xS))
& ! [X1] :
( aElementOf0(X1,sbsmnsldt0(xS))
<=> ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( equal(X1,sz10)
| equal(X1,smndt0(sz10)) ) )
& equal(stldt0(sbsmnsldt0(xS)),cS2076) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',m__2079) ).
fof(25,axiom,
! [X1] :
( aInteger0(X1)
=> ( equal(sdtpldt0(X1,smndt0(X1)),sz00)
& equal(sz00,sdtpldt0(smndt0(X1),X1)) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mAddNeg) ).
fof(29,conjecture,
? [X1] :
( ( ( aInteger0(X1)
& ( ? [X2] :
( aInteger0(X2)
& equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
| aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
| sdteqdtlpzmzozddtrp0(X1,sz10,xp) ) )
| aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ~ ( ( equal(X1,sz10)
| equal(X1,smndt0(sz10)) )
& aElementOf0(X1,cS2200) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',m__) ).
fof(30,axiom,
! [X1,X2,X3] :
( ( aInteger0(X1)
& aInteger0(X2)
& aInteger0(X3) )
=> equal(sdtasdt0(X1,sdtasdt0(X2,X3)),sdtasdt0(sdtasdt0(X1,X2),X3)) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mMulAsso) ).
fof(31,axiom,
! [X1,X2] :
( ( aInteger0(X1)
& aInteger0(X2)
& ~ equal(X2,sz00) )
=> sdteqdtlpzmzozddtrp0(X1,X1,X2) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mEquModRef) ).
fof(32,axiom,
! [X1,X2] :
( ( aInteger0(X1)
& aInteger0(X2) )
=> aInteger0(sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mIntMult) ).
fof(33,axiom,
! [X1,X2,X3] :
( ( aInteger0(X1)
& aInteger0(X2)
& aInteger0(X3) )
=> equal(sdtpldt0(X1,sdtpldt0(X2,X3)),sdtpldt0(sdtpldt0(X1,X2),X3)) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mAddAsso) ).
fof(35,axiom,
! [X1] :
( aInteger0(X1)
=> aInteger0(smndt0(X1)) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mIntNeg) ).
fof(36,axiom,
aInteger0(sz00),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mIntZero) ).
fof(37,axiom,
! [X1] :
( aInteger0(X1)
=> ( equal(sdtpldt0(X1,sz00),X1)
& equal(X1,sdtpldt0(sz00,X1)) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mAddZero) ).
fof(38,axiom,
! [X1,X2] :
( ( aInteger0(X1)
& aInteger0(X2) )
=> equal(sdtasdt0(X1,X2),sdtasdt0(X2,X1)) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mMulComm) ).
fof(39,axiom,
! [X1,X2,X3] :
( ( aInteger0(X1)
& aInteger0(X2)
& aInteger0(X3)
& ~ equal(X3,sz00) )
=> ( sdteqdtlpzmzozddtrp0(X1,X2,X3)
<=> aDivisorOf0(X3,sdtpldt0(X1,smndt0(X2))) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mEquMod) ).
fof(40,axiom,
! [X1,X2,X3,X4] :
( ( aInteger0(X1)
& aInteger0(X2)
& aInteger0(X3)
& ~ equal(X3,sz00)
& aInteger0(X4)
& ~ equal(X4,sz00) )
=> ( sdteqdtlpzmzozddtrp0(X1,X2,sdtasdt0(X3,X4))
=> ( sdteqdtlpzmzozddtrp0(X1,X2,X3)
& sdteqdtlpzmzozddtrp0(X1,X2,X4) ) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mEquModMul) ).
fof(42,axiom,
! [X1,X2,X3] :
( ( aInteger0(X1)
& aInteger0(X2)
& aInteger0(X3) )
=> ( equal(sdtasdt0(X1,sdtpldt0(X2,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3)))
& equal(sdtasdt0(sdtpldt0(X1,X2),X3),sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3))) ) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',mDistrib) ).
fof(46,axiom,
( aInteger0(xp)
& ~ equal(xp,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X1] :
( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> ( aInteger0(X1)
& ? [X2] :
( aInteger0(X2)
& equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
& aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X1,sz10,xp) ) )
& ( ( aInteger0(X1)
& ( ? [X2] :
( aInteger0(X2)
& equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
| aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
| sdteqdtlpzmzozddtrp0(X1,sz10,xp) ) )
=> aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X1] :
( aElementOf0(X1,sbsmnsldt0(xS))
<=> ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> aElementOf0(X1,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
file('/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2',m__2171) ).
fof(48,negated_conjecture,
~ ? [X1] :
( ( ( aInteger0(X1)
& ( ? [X2] :
( aInteger0(X2)
& equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
| aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
| sdteqdtlpzmzozddtrp0(X1,sz10,xp) ) )
| aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ~ ( ( equal(X1,sz10)
| equal(X1,smndt0(sz10)) )
& aElementOf0(X1,cS2200) ) ),
inference(assume_negation,[status(cth)],[29]) ).
fof(50,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X1] :
( aElementOf0(X1,sbsmnsldt0(xS))
<=> ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
=> ? [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(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS))) ) )
& isOpen0(stldt0(sbsmnsldt0(xS)))
& isClosed0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS))
& ! [X1] :
( aElementOf0(X1,sbsmnsldt0(xS))
<=> ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
=> ? [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(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS))) ) ) ),
inference(fof_simplification,[status(thm)],[18,theory(equality)]) ).
fof(51,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X1] :
( aElementOf0(X1,sbsmnsldt0(xS))
<=> ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( equal(X1,sz10)
| equal(X1,smndt0(sz10)) ) )
& equal(stldt0(sbsmnsldt0(xS)),cS2076) ),
inference(fof_simplification,[status(thm)],[23,theory(equality)]) ).
fof(52,plain,
( aInteger0(xp)
& ~ equal(xp,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X1] :
( ( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> ( aInteger0(X1)
& ? [X2] :
( aInteger0(X2)
& equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
& aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X1,sz10,xp) ) )
& ( ( aInteger0(X1)
& ( ? [X2] :
( aInteger0(X2)
& equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
| aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
| sdteqdtlpzmzozddtrp0(X1,sz10,xp) ) )
=> aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X1] :
( aElementOf0(X1,sbsmnsldt0(xS))
<=> ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ! [X1] :
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> aElementOf0(X1,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(fof_simplification,[status(thm)],[46,theory(equality)]) ).
fof(53,plain,
! [X1] :
( ~ aInteger0(X1)
| ( equal(sdtasdt0(X1,sz10),X1)
& equal(X1,sdtasdt0(sz10,X1)) ) ),
inference(fof_nnf,[status(thm)],[1]) ).
fof(54,plain,
! [X2] :
( ~ aInteger0(X2)
| ( equal(sdtasdt0(X2,sz10),X2)
& equal(X2,sdtasdt0(sz10,X2)) ) ),
inference(variable_rename,[status(thm)],[53]) ).
fof(55,plain,
! [X2] :
( ( equal(sdtasdt0(X2,sz10),X2)
| ~ aInteger0(X2) )
& ( equal(X2,sdtasdt0(sz10,X2))
| ~ aInteger0(X2) ) ),
inference(distribute,[status(thm)],[54]) ).
cnf(56,plain,
( X1 = sdtasdt0(sz10,X1)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[55]) ).
cnf(57,plain,
( sdtasdt0(X1,sz10) = X1
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[55]) ).
fof(70,plain,
! [X1] :
( ~ aInteger0(X1)
| ( equal(sdtasdt0(smndt0(sz10),X1),smndt0(X1))
& equal(smndt0(X1),sdtasdt0(X1,smndt0(sz10))) ) ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(71,plain,
! [X2] :
( ~ aInteger0(X2)
| ( equal(sdtasdt0(smndt0(sz10),X2),smndt0(X2))
& equal(smndt0(X2),sdtasdt0(X2,smndt0(sz10))) ) ),
inference(variable_rename,[status(thm)],[70]) ).
fof(72,plain,
! [X2] :
( ( equal(sdtasdt0(smndt0(sz10),X2),smndt0(X2))
| ~ aInteger0(X2) )
& ( equal(smndt0(X2),sdtasdt0(X2,smndt0(sz10)))
| ~ aInteger0(X2) ) ),
inference(distribute,[status(thm)],[71]) ).
cnf(73,plain,
( smndt0(X1) = sdtasdt0(X1,smndt0(sz10))
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[72]) ).
cnf(74,plain,
( sdtasdt0(smndt0(sz10),X1) = smndt0(X1)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[72]) ).
fof(78,plain,
! [X1] :
( ~ aInteger0(X1)
| ( equal(sdtasdt0(X1,sz00),sz00)
& equal(sz00,sdtasdt0(sz00,X1)) ) ),
inference(fof_nnf,[status(thm)],[5]) ).
fof(79,plain,
! [X2] :
( ~ aInteger0(X2)
| ( equal(sdtasdt0(X2,sz00),sz00)
& equal(sz00,sdtasdt0(sz00,X2)) ) ),
inference(variable_rename,[status(thm)],[78]) ).
fof(80,plain,
! [X2] :
( ( equal(sdtasdt0(X2,sz00),sz00)
| ~ aInteger0(X2) )
& ( equal(sz00,sdtasdt0(sz00,X2))
| ~ aInteger0(X2) ) ),
inference(distribute,[status(thm)],[79]) ).
cnf(81,plain,
( sz00 = sdtasdt0(sz00,X1)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[80]) ).
cnf(82,plain,
( sdtasdt0(X1,sz00) = sz00
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[80]) ).
fof(97,plain,
! [X1,X2] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| equal(sdtpldt0(X1,X2),sdtpldt0(X2,X1)) ),
inference(fof_nnf,[status(thm)],[7]) ).
fof(98,plain,
! [X3,X4] :
( ~ aInteger0(X3)
| ~ aInteger0(X4)
| equal(sdtpldt0(X3,X4),sdtpldt0(X4,X3)) ),
inference(variable_rename,[status(thm)],[97]) ).
cnf(99,plain,
( sdtpldt0(X1,X2) = sdtpldt0(X2,X1)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[98]) ).
fof(100,plain,
! [X1,X2] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| aInteger0(sdtpldt0(X1,X2)) ),
inference(fof_nnf,[status(thm)],[8]) ).
fof(101,plain,
! [X3,X4] :
( ~ aInteger0(X3)
| ~ aInteger0(X4)
| aInteger0(sdtpldt0(X3,X4)) ),
inference(variable_rename,[status(thm)],[100]) ).
cnf(102,plain,
( aInteger0(sdtpldt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[101]) ).
fof(103,plain,
! [X1] :
( ~ aInteger0(X1)
| ! [X2] :
( ( ~ aDivisorOf0(X2,X1)
| ( aInteger0(X2)
& ~ equal(X2,sz00)
& ? [X3] :
( aInteger0(X3)
& equal(sdtasdt0(X2,X3),X1) ) ) )
& ( ~ aInteger0(X2)
| equal(X2,sz00)
| ! [X3] :
( ~ aInteger0(X3)
| ~ equal(sdtasdt0(X2,X3),X1) )
| aDivisorOf0(X2,X1) ) ) ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(104,plain,
! [X4] :
( ~ aInteger0(X4)
| ! [X5] :
( ( ~ aDivisorOf0(X5,X4)
| ( aInteger0(X5)
& ~ equal(X5,sz00)
& ? [X6] :
( aInteger0(X6)
& equal(sdtasdt0(X5,X6),X4) ) ) )
& ( ~ aInteger0(X5)
| equal(X5,sz00)
| ! [X7] :
( ~ aInteger0(X7)
| ~ equal(sdtasdt0(X5,X7),X4) )
| aDivisorOf0(X5,X4) ) ) ),
inference(variable_rename,[status(thm)],[103]) ).
fof(105,plain,
! [X4] :
( ~ aInteger0(X4)
| ! [X5] :
( ( ~ aDivisorOf0(X5,X4)
| ( aInteger0(X5)
& ~ equal(X5,sz00)
& aInteger0(esk3_2(X4,X5))
& equal(sdtasdt0(X5,esk3_2(X4,X5)),X4) ) )
& ( ~ aInteger0(X5)
| equal(X5,sz00)
| ! [X7] :
( ~ aInteger0(X7)
| ~ equal(sdtasdt0(X5,X7),X4) )
| aDivisorOf0(X5,X4) ) ) ),
inference(skolemize,[status(esa)],[104]) ).
fof(106,plain,
! [X4,X5,X7] :
( ( ( ~ aInteger0(X7)
| ~ equal(sdtasdt0(X5,X7),X4)
| ~ aInteger0(X5)
| equal(X5,sz00)
| aDivisorOf0(X5,X4) )
& ( ~ aDivisorOf0(X5,X4)
| ( aInteger0(X5)
& ~ equal(X5,sz00)
& aInteger0(esk3_2(X4,X5))
& equal(sdtasdt0(X5,esk3_2(X4,X5)),X4) ) ) )
| ~ aInteger0(X4) ),
inference(shift_quantors,[status(thm)],[105]) ).
fof(107,plain,
! [X4,X5,X7] :
( ( ~ aInteger0(X7)
| ~ equal(sdtasdt0(X5,X7),X4)
| ~ aInteger0(X5)
| equal(X5,sz00)
| aDivisorOf0(X5,X4)
| ~ aInteger0(X4) )
& ( aInteger0(X5)
| ~ aDivisorOf0(X5,X4)
| ~ aInteger0(X4) )
& ( ~ equal(X5,sz00)
| ~ aDivisorOf0(X5,X4)
| ~ aInteger0(X4) )
& ( aInteger0(esk3_2(X4,X5))
| ~ aDivisorOf0(X5,X4)
| ~ aInteger0(X4) )
& ( equal(sdtasdt0(X5,esk3_2(X4,X5)),X4)
| ~ aDivisorOf0(X5,X4)
| ~ aInteger0(X4) ) ),
inference(distribute,[status(thm)],[106]) ).
cnf(108,plain,
( sdtasdt0(X2,esk3_2(X1,X2)) = X1
| ~ aInteger0(X1)
| ~ aDivisorOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[107]) ).
cnf(109,plain,
( aInteger0(esk3_2(X1,X2))
| ~ aInteger0(X1)
| ~ aDivisorOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[107]) ).
cnf(110,plain,
( ~ aInteger0(X1)
| ~ aDivisorOf0(X2,X1)
| X2 != sz00 ),
inference(split_conjunct,[status(thm)],[107]) ).
cnf(111,plain,
( aInteger0(X2)
| ~ aInteger0(X1)
| ~ aDivisorOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[107]) ).
cnf(112,plain,
( aDivisorOf0(X2,X1)
| X2 = sz00
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sdtasdt0(X2,X3) != X1
| ~ aInteger0(X3) ),
inference(split_conjunct,[status(thm)],[107]) ).
fof(113,plain,
! [X1,X2,X3] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| equal(X3,sz00)
| ~ sdteqdtlpzmzozddtrp0(X1,X2,X3)
| sdteqdtlpzmzozddtrp0(X2,X1,X3) ),
inference(fof_nnf,[status(thm)],[10]) ).
fof(114,plain,
! [X4,X5,X6] :
( ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| equal(X6,sz00)
| ~ sdteqdtlpzmzozddtrp0(X4,X5,X6)
| sdteqdtlpzmzozddtrp0(X5,X4,X6) ),
inference(variable_rename,[status(thm)],[113]) ).
cnf(115,plain,
( sdteqdtlpzmzozddtrp0(X1,X2,X3)
| X3 = sz00
| ~ sdteqdtlpzmzozddtrp0(X2,X1,X3)
| ~ aInteger0(X3)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(split_conjunct,[status(thm)],[114]) ).
fof(116,plain,
! [X1,X2] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ equal(sdtasdt0(X1,X2),sz00)
| equal(X1,sz00)
| equal(X2,sz00) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(117,plain,
! [X3,X4] :
( ~ aInteger0(X3)
| ~ aInteger0(X4)
| ~ equal(sdtasdt0(X3,X4),sz00)
| equal(X3,sz00)
| equal(X4,sz00) ),
inference(variable_rename,[status(thm)],[116]) ).
cnf(118,plain,
( X1 = sz00
| X2 = sz00
| sdtasdt0(X2,X1) != sz00
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(split_conjunct,[status(thm)],[117]) ).
fof(139,plain,
! [X1,X2,X3,X4] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| equal(X3,sz00)
| ~ aInteger0(X4)
| ~ sdteqdtlpzmzozddtrp0(X1,X2,X3)
| ~ sdteqdtlpzmzozddtrp0(X2,X4,X3)
| sdteqdtlpzmzozddtrp0(X1,X4,X3) ),
inference(fof_nnf,[status(thm)],[17]) ).
fof(140,plain,
! [X5,X6,X7,X8] :
( ~ aInteger0(X5)
| ~ aInteger0(X6)
| ~ aInteger0(X7)
| equal(X7,sz00)
| ~ aInteger0(X8)
| ~ sdteqdtlpzmzozddtrp0(X5,X6,X7)
| ~ sdteqdtlpzmzozddtrp0(X6,X8,X7)
| sdteqdtlpzmzozddtrp0(X5,X8,X7) ),
inference(variable_rename,[status(thm)],[139]) ).
cnf(141,plain,
( sdteqdtlpzmzozddtrp0(X1,X2,X3)
| X3 = sz00
| ~ sdteqdtlpzmzozddtrp0(X4,X2,X3)
| ~ sdteqdtlpzmzozddtrp0(X1,X4,X3)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| ~ aInteger0(X4)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[140]) ).
fof(142,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X1] :
( ( ~ aElementOf0(X1,sbsmnsldt0(xS))
| ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ( ~ aInteger0(X1)
| ! [X2] :
( ~ aElementOf0(X2,xS)
| ~ aElementOf0(X1,X2) )
| aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,sbsmnsldt0(xS))
| aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ) )
& ! [X1] :
( ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| ? [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(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS))) ) )
& isOpen0(stldt0(sbsmnsldt0(xS)))
& isClosed0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS))
& ! [X1] :
( ( ~ aElementOf0(X1,sbsmnsldt0(xS))
| ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ( ~ aInteger0(X1)
| ! [X2] :
( ~ aElementOf0(X2,xS)
| ~ aElementOf0(X1,X2) )
| aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,sbsmnsldt0(xS))
| aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ) )
& ! [X1] :
( ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| ? [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(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),stldt0(sbsmnsldt0(xS))) ) ) ),
inference(fof_nnf,[status(thm)],[50]) ).
fof(143,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X5] :
( ( ~ aElementOf0(X5,sbsmnsldt0(xS))
| ( aInteger0(X5)
& ? [X6] :
( aElementOf0(X6,xS)
& aElementOf0(X5,X6) ) ) )
& ( ~ aInteger0(X5)
| ! [X7] :
( ~ aElementOf0(X7,xS)
| ~ aElementOf0(X5,X7) )
| aElementOf0(X5,sbsmnsldt0(xS)) ) )
& ! [X8] :
( ( ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X8)
& ~ aElementOf0(X8,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X8)
| aElementOf0(X8,sbsmnsldt0(xS))
| aElementOf0(X8,stldt0(sbsmnsldt0(xS))) ) )
& ! [X9] :
( ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS)))
| ? [X10] :
( aInteger0(X10)
& ~ equal(X10,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X9,X10))
& ! [X11] :
( ( ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,X10))
| ( aInteger0(X11)
& ? [X12] :
( aInteger0(X12)
& equal(sdtasdt0(X10,X12),sdtpldt0(X11,smndt0(X9))) )
& aDivisorOf0(X10,sdtpldt0(X11,smndt0(X9)))
& sdteqdtlpzmzozddtrp0(X11,X9,X10) ) )
& ( ~ aInteger0(X11)
| ( ! [X13] :
( ~ aInteger0(X13)
| ~ equal(sdtasdt0(X10,X13),sdtpldt0(X11,smndt0(X9))) )
& ~ aDivisorOf0(X10,sdtpldt0(X11,smndt0(X9)))
& ~ sdteqdtlpzmzozddtrp0(X11,X9,X10) )
| aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,X10)) ) )
& ! [X14] :
( ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X9,X10))
| aElementOf0(X14,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X9,X10),stldt0(sbsmnsldt0(xS))) ) )
& isOpen0(stldt0(sbsmnsldt0(xS)))
& isClosed0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS))
& ! [X15] :
( ( ~ aElementOf0(X15,sbsmnsldt0(xS))
| ( aInteger0(X15)
& ? [X16] :
( aElementOf0(X16,xS)
& aElementOf0(X15,X16) ) ) )
& ( ~ aInteger0(X15)
| ! [X17] :
( ~ aElementOf0(X17,xS)
| ~ aElementOf0(X15,X17) )
| aElementOf0(X15,sbsmnsldt0(xS)) ) )
& ! [X18] :
( ( ~ aElementOf0(X18,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X18)
& ~ aElementOf0(X18,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X18)
| aElementOf0(X18,sbsmnsldt0(xS))
| aElementOf0(X18,stldt0(sbsmnsldt0(xS))) ) )
& ! [X19] :
( ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS)))
| ? [X20] :
( aInteger0(X20)
& ~ equal(X20,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X19,X20))
& ! [X21] :
( ( ~ aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,X20))
| ( aInteger0(X21)
& ? [X22] :
( aInteger0(X22)
& equal(sdtasdt0(X20,X22),sdtpldt0(X21,smndt0(X19))) )
& aDivisorOf0(X20,sdtpldt0(X21,smndt0(X19)))
& sdteqdtlpzmzozddtrp0(X21,X19,X20) ) )
& ( ~ aInteger0(X21)
| ( ! [X23] :
( ~ aInteger0(X23)
| ~ equal(sdtasdt0(X20,X23),sdtpldt0(X21,smndt0(X19))) )
& ~ aDivisorOf0(X20,sdtpldt0(X21,smndt0(X19)))
& ~ sdteqdtlpzmzozddtrp0(X21,X19,X20) )
| aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,X20)) ) )
& ! [X24] :
( ~ aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X19,X20))
| aElementOf0(X24,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X19,X20),stldt0(sbsmnsldt0(xS))) ) ) ),
inference(variable_rename,[status(thm)],[142]) ).
fof(144,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X5] :
( ( ~ aElementOf0(X5,sbsmnsldt0(xS))
| ( aInteger0(X5)
& aElementOf0(esk5_1(X5),xS)
& aElementOf0(X5,esk5_1(X5)) ) )
& ( ~ aInteger0(X5)
| ! [X7] :
( ~ aElementOf0(X7,xS)
| ~ aElementOf0(X5,X7) )
| aElementOf0(X5,sbsmnsldt0(xS)) ) )
& ! [X8] :
( ( ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X8)
& ~ aElementOf0(X8,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X8)
| aElementOf0(X8,sbsmnsldt0(xS))
| aElementOf0(X8,stldt0(sbsmnsldt0(xS))) ) )
& ! [X9] :
( ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(esk6_1(X9))
& ~ equal(esk6_1(X9),sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
& ! [X11] :
( ( ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ( aInteger0(X11)
& aInteger0(esk7_2(X9,X11))
& equal(sdtasdt0(esk6_1(X9),esk7_2(X9,X11)),sdtpldt0(X11,smndt0(X9)))
& aDivisorOf0(esk6_1(X9),sdtpldt0(X11,smndt0(X9)))
& sdteqdtlpzmzozddtrp0(X11,X9,esk6_1(X9)) ) )
& ( ~ aInteger0(X11)
| ( ! [X13] :
( ~ aInteger0(X13)
| ~ equal(sdtasdt0(esk6_1(X9),X13),sdtpldt0(X11,smndt0(X9))) )
& ~ aDivisorOf0(esk6_1(X9),sdtpldt0(X11,smndt0(X9)))
& ~ sdteqdtlpzmzozddtrp0(X11,X9,esk6_1(X9)) )
| aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9))) ) )
& ! [X14] :
( ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| aElementOf0(X14,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)),stldt0(sbsmnsldt0(xS))) ) )
& isOpen0(stldt0(sbsmnsldt0(xS)))
& isClosed0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS))
& ! [X15] :
( ( ~ aElementOf0(X15,sbsmnsldt0(xS))
| ( aInteger0(X15)
& aElementOf0(esk8_1(X15),xS)
& aElementOf0(X15,esk8_1(X15)) ) )
& ( ~ aInteger0(X15)
| ! [X17] :
( ~ aElementOf0(X17,xS)
| ~ aElementOf0(X15,X17) )
| aElementOf0(X15,sbsmnsldt0(xS)) ) )
& ! [X18] :
( ( ~ aElementOf0(X18,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X18)
& ~ aElementOf0(X18,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X18)
| aElementOf0(X18,sbsmnsldt0(xS))
| aElementOf0(X18,stldt0(sbsmnsldt0(xS))) ) )
& ! [X19] :
( ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(esk9_1(X19))
& ~ equal(esk9_1(X19),sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
& ! [X21] :
( ( ~ aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ( aInteger0(X21)
& aInteger0(esk10_2(X19,X21))
& equal(sdtasdt0(esk9_1(X19),esk10_2(X19,X21)),sdtpldt0(X21,smndt0(X19)))
& aDivisorOf0(esk9_1(X19),sdtpldt0(X21,smndt0(X19)))
& sdteqdtlpzmzozddtrp0(X21,X19,esk9_1(X19)) ) )
& ( ~ aInteger0(X21)
| ( ! [X23] :
( ~ aInteger0(X23)
| ~ equal(sdtasdt0(esk9_1(X19),X23),sdtpldt0(X21,smndt0(X19))) )
& ~ aDivisorOf0(esk9_1(X19),sdtpldt0(X21,smndt0(X19)))
& ~ sdteqdtlpzmzozddtrp0(X21,X19,esk9_1(X19)) )
| aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19))) ) )
& ! [X24] :
( ~ aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| aElementOf0(X24,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)),stldt0(sbsmnsldt0(xS))) ) ) ),
inference(skolemize,[status(esa)],[143]) ).
fof(145,plain,
! [X5,X7,X8,X9,X11,X13,X14,X15,X17,X18,X19,X21,X23,X24] :
( ( ( ( ~ aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| aElementOf0(X24,stldt0(sbsmnsldt0(xS))) )
& ( ( ( ~ aInteger0(X23)
| ~ equal(sdtasdt0(esk9_1(X19),X23),sdtpldt0(X21,smndt0(X19))) )
& ~ aDivisorOf0(esk9_1(X19),sdtpldt0(X21,smndt0(X19)))
& ~ sdteqdtlpzmzozddtrp0(X21,X19,esk9_1(X19)) )
| ~ aInteger0(X21)
| aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19))) )
& ( ~ aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ( aInteger0(X21)
& aInteger0(esk10_2(X19,X21))
& equal(sdtasdt0(esk9_1(X19),esk10_2(X19,X21)),sdtpldt0(X21,smndt0(X19)))
& aDivisorOf0(esk9_1(X19),sdtpldt0(X21,smndt0(X19)))
& sdteqdtlpzmzozddtrp0(X21,X19,esk9_1(X19)) ) )
& aInteger0(esk9_1(X19))
& ~ equal(esk9_1(X19),sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)),stldt0(sbsmnsldt0(xS))) )
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X18,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X18)
& ~ aElementOf0(X18,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X18)
| aElementOf0(X18,sbsmnsldt0(xS))
| aElementOf0(X18,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X17,xS)
| ~ aElementOf0(X15,X17)
| ~ aInteger0(X15)
| aElementOf0(X15,sbsmnsldt0(xS)) )
& ( ~ aElementOf0(X15,sbsmnsldt0(xS))
| ( aInteger0(X15)
& aElementOf0(esk8_1(X15),xS)
& aElementOf0(X15,esk8_1(X15)) ) )
& ( ( ( ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| aElementOf0(X14,stldt0(sbsmnsldt0(xS))) )
& ( ( ( ~ aInteger0(X13)
| ~ equal(sdtasdt0(esk6_1(X9),X13),sdtpldt0(X11,smndt0(X9))) )
& ~ aDivisorOf0(esk6_1(X9),sdtpldt0(X11,smndt0(X9)))
& ~ sdteqdtlpzmzozddtrp0(X11,X9,esk6_1(X9)) )
| ~ aInteger0(X11)
| aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9))) )
& ( ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ( aInteger0(X11)
& aInteger0(esk7_2(X9,X11))
& equal(sdtasdt0(esk6_1(X9),esk7_2(X9,X11)),sdtpldt0(X11,smndt0(X9)))
& aDivisorOf0(esk6_1(X9),sdtpldt0(X11,smndt0(X9)))
& sdteqdtlpzmzozddtrp0(X11,X9,esk6_1(X9)) ) )
& aInteger0(esk6_1(X9))
& ~ equal(esk6_1(X9),sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)),stldt0(sbsmnsldt0(xS))) )
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X8)
& ~ aElementOf0(X8,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X8)
| aElementOf0(X8,sbsmnsldt0(xS))
| aElementOf0(X8,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X7,xS)
| ~ aElementOf0(X5,X7)
| ~ aInteger0(X5)
| aElementOf0(X5,sbsmnsldt0(xS)) )
& ( ~ aElementOf0(X5,sbsmnsldt0(xS))
| ( aInteger0(X5)
& aElementOf0(esk5_1(X5),xS)
& aElementOf0(X5,esk5_1(X5)) ) )
& aSet0(sbsmnsldt0(xS))
& isOpen0(stldt0(sbsmnsldt0(xS)))
& isClosed0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS)) ),
inference(shift_quantors,[status(thm)],[144]) ).
fof(146,plain,
! [X5,X7,X8,X9,X11,X13,X14,X15,X17,X18,X19,X21,X23,X24] :
( ( ~ aElementOf0(X24,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| aElementOf0(X24,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( ~ aInteger0(X23)
| ~ equal(sdtasdt0(esk9_1(X19),X23),sdtpldt0(X21,smndt0(X19)))
| ~ aInteger0(X21)
| aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( ~ aDivisorOf0(esk9_1(X19),sdtpldt0(X21,smndt0(X19)))
| ~ aInteger0(X21)
| aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( ~ sdteqdtlpzmzozddtrp0(X21,X19,esk9_1(X19))
| ~ aInteger0(X21)
| aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(X21)
| ~ aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(esk10_2(X19,X21))
| ~ aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( equal(sdtasdt0(esk9_1(X19),esk10_2(X19,X21)),sdtpldt0(X21,smndt0(X19)))
| ~ aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( aDivisorOf0(esk9_1(X19),sdtpldt0(X21,smndt0(X19)))
| ~ aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( sdteqdtlpzmzozddtrp0(X21,X19,esk9_1(X19))
| ~ aElementOf0(X21,szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(esk9_1(X19))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( ~ equal(esk9_1(X19),sz00)
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( aSet0(szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X19,esk9_1(X19)),stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X19,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(X18)
| ~ aElementOf0(X18,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X18,sbsmnsldt0(xS))
| ~ aElementOf0(X18,stldt0(sbsmnsldt0(xS))) )
& ( ~ aInteger0(X18)
| aElementOf0(X18,sbsmnsldt0(xS))
| aElementOf0(X18,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X17,xS)
| ~ aElementOf0(X15,X17)
| ~ aInteger0(X15)
| aElementOf0(X15,sbsmnsldt0(xS)) )
& ( aInteger0(X15)
| ~ aElementOf0(X15,sbsmnsldt0(xS)) )
& ( aElementOf0(esk8_1(X15),xS)
| ~ aElementOf0(X15,sbsmnsldt0(xS)) )
& ( aElementOf0(X15,esk8_1(X15))
| ~ aElementOf0(X15,sbsmnsldt0(xS)) )
& ( ~ aElementOf0(X14,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| aElementOf0(X14,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ aInteger0(X13)
| ~ equal(sdtasdt0(esk6_1(X9),X13),sdtpldt0(X11,smndt0(X9)))
| ~ aInteger0(X11)
| aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ aDivisorOf0(esk6_1(X9),sdtpldt0(X11,smndt0(X9)))
| ~ aInteger0(X11)
| aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ sdteqdtlpzmzozddtrp0(X11,X9,esk6_1(X9))
| ~ aInteger0(X11)
| aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(X11)
| ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(esk7_2(X9,X11))
| ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( equal(sdtasdt0(esk6_1(X9),esk7_2(X9,X11)),sdtpldt0(X11,smndt0(X9)))
| ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( aDivisorOf0(esk6_1(X9),sdtpldt0(X11,smndt0(X9)))
| ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( sdteqdtlpzmzozddtrp0(X11,X9,esk6_1(X9))
| ~ aElementOf0(X11,szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(esk6_1(X9))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ equal(esk6_1(X9),sz00)
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( aSet0(szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X9,esk6_1(X9)),stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(X8)
| ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X8,sbsmnsldt0(xS))
| ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS))) )
& ( ~ aInteger0(X8)
| aElementOf0(X8,sbsmnsldt0(xS))
| aElementOf0(X8,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X7,xS)
| ~ aElementOf0(X5,X7)
| ~ aInteger0(X5)
| aElementOf0(X5,sbsmnsldt0(xS)) )
& ( aInteger0(X5)
| ~ aElementOf0(X5,sbsmnsldt0(xS)) )
& ( aElementOf0(esk5_1(X5),xS)
| ~ aElementOf0(X5,sbsmnsldt0(xS)) )
& ( aElementOf0(X5,esk5_1(X5))
| ~ aElementOf0(X5,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& isOpen0(stldt0(sbsmnsldt0(xS)))
& isClosed0(sbsmnsldt0(xS))
& aSet0(sbsmnsldt0(xS)) ),
inference(distribute,[status(thm)],[145]) ).
cnf(157,plain,
( aInteger0(X1)
| ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[146]) ).
cnf(191,plain,
aInteger0(sz10),
inference(split_conjunct,[status(thm)],[19]) ).
fof(230,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X1] :
( ( ~ aElementOf0(X1,sbsmnsldt0(xS))
| ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ( ~ aInteger0(X1)
| ! [X2] :
( ~ aElementOf0(X2,xS)
| ~ aElementOf0(X1,X2) )
| aElementOf0(X1,sbsmnsldt0(xS)) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,sbsmnsldt0(xS))
| aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ) )
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| equal(X1,sz10)
| equal(X1,smndt0(sz10)) )
& ( ( ~ equal(X1,sz10)
& ~ equal(X1,smndt0(sz10)) )
| aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ) )
& equal(stldt0(sbsmnsldt0(xS)),cS2076) ),
inference(fof_nnf,[status(thm)],[51]) ).
fof(231,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X3] :
( ( ~ aElementOf0(X3,sbsmnsldt0(xS))
| ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,xS)
& aElementOf0(X3,X4) ) ) )
& ( ~ aInteger0(X3)
| ! [X5] :
( ~ aElementOf0(X5,xS)
| ~ aElementOf0(X3,X5) )
| aElementOf0(X3,sbsmnsldt0(xS)) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X6] :
( ( ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X6)
& ~ aElementOf0(X6,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,sbsmnsldt0(xS))
| aElementOf0(X6,stldt0(sbsmnsldt0(xS))) ) )
& ! [X7] :
( ( ~ aElementOf0(X7,stldt0(sbsmnsldt0(xS)))
| equal(X7,sz10)
| equal(X7,smndt0(sz10)) )
& ( ( ~ equal(X7,sz10)
& ~ equal(X7,smndt0(sz10)) )
| aElementOf0(X7,stldt0(sbsmnsldt0(xS))) ) )
& equal(stldt0(sbsmnsldt0(xS)),cS2076) ),
inference(variable_rename,[status(thm)],[230]) ).
fof(232,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X3] :
( ( ~ aElementOf0(X3,sbsmnsldt0(xS))
| ( aInteger0(X3)
& aElementOf0(esk17_1(X3),xS)
& aElementOf0(X3,esk17_1(X3)) ) )
& ( ~ aInteger0(X3)
| ! [X5] :
( ~ aElementOf0(X5,xS)
| ~ aElementOf0(X3,X5) )
| aElementOf0(X3,sbsmnsldt0(xS)) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X6] :
( ( ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X6)
& ~ aElementOf0(X6,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,sbsmnsldt0(xS))
| aElementOf0(X6,stldt0(sbsmnsldt0(xS))) ) )
& ! [X7] :
( ( ~ aElementOf0(X7,stldt0(sbsmnsldt0(xS)))
| equal(X7,sz10)
| equal(X7,smndt0(sz10)) )
& ( ( ~ equal(X7,sz10)
& ~ equal(X7,smndt0(sz10)) )
| aElementOf0(X7,stldt0(sbsmnsldt0(xS))) ) )
& equal(stldt0(sbsmnsldt0(xS)),cS2076) ),
inference(skolemize,[status(esa)],[231]) ).
fof(233,plain,
! [X3,X5,X6,X7] :
( ( ~ aElementOf0(X7,stldt0(sbsmnsldt0(xS)))
| equal(X7,sz10)
| equal(X7,smndt0(sz10)) )
& ( ( ~ equal(X7,sz10)
& ~ equal(X7,smndt0(sz10)) )
| aElementOf0(X7,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X6)
& ~ aElementOf0(X6,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,sbsmnsldt0(xS))
| aElementOf0(X6,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X5,xS)
| ~ aElementOf0(X3,X5)
| ~ aInteger0(X3)
| aElementOf0(X3,sbsmnsldt0(xS)) )
& ( ~ aElementOf0(X3,sbsmnsldt0(xS))
| ( aInteger0(X3)
& aElementOf0(esk17_1(X3),xS)
& aElementOf0(X3,esk17_1(X3)) ) )
& aSet0(sbsmnsldt0(xS))
& aSet0(stldt0(sbsmnsldt0(xS)))
& equal(stldt0(sbsmnsldt0(xS)),cS2076) ),
inference(shift_quantors,[status(thm)],[232]) ).
fof(234,plain,
! [X3,X5,X6,X7] :
( ( ~ aElementOf0(X7,stldt0(sbsmnsldt0(xS)))
| equal(X7,sz10)
| equal(X7,smndt0(sz10)) )
& ( ~ equal(X7,sz10)
| aElementOf0(X7,stldt0(sbsmnsldt0(xS))) )
& ( ~ equal(X7,smndt0(sz10))
| aElementOf0(X7,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(X6)
| ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X6,sbsmnsldt0(xS))
| ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS))) )
& ( ~ aInteger0(X6)
| aElementOf0(X6,sbsmnsldt0(xS))
| aElementOf0(X6,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X5,xS)
| ~ aElementOf0(X3,X5)
| ~ aInteger0(X3)
| aElementOf0(X3,sbsmnsldt0(xS)) )
& ( aInteger0(X3)
| ~ aElementOf0(X3,sbsmnsldt0(xS)) )
& ( aElementOf0(esk17_1(X3),xS)
| ~ aElementOf0(X3,sbsmnsldt0(xS)) )
& ( aElementOf0(X3,esk17_1(X3))
| ~ aElementOf0(X3,sbsmnsldt0(xS)) )
& aSet0(sbsmnsldt0(xS))
& aSet0(stldt0(sbsmnsldt0(xS)))
& equal(stldt0(sbsmnsldt0(xS)),cS2076) ),
inference(distribute,[status(thm)],[233]) ).
cnf(235,plain,
stldt0(sbsmnsldt0(xS)) = cS2076,
inference(split_conjunct,[status(thm)],[234]) ).
cnf(245,plain,
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| X1 != smndt0(sz10) ),
inference(split_conjunct,[status(thm)],[234]) ).
cnf(246,plain,
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| X1 != sz10 ),
inference(split_conjunct,[status(thm)],[234]) ).
cnf(247,plain,
( X1 = smndt0(sz10)
| X1 = sz10
| ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ),
inference(split_conjunct,[status(thm)],[234]) ).
fof(260,plain,
! [X1] :
( ~ aInteger0(X1)
| ( equal(sdtpldt0(X1,smndt0(X1)),sz00)
& equal(sz00,sdtpldt0(smndt0(X1),X1)) ) ),
inference(fof_nnf,[status(thm)],[25]) ).
fof(261,plain,
! [X2] :
( ~ aInteger0(X2)
| ( equal(sdtpldt0(X2,smndt0(X2)),sz00)
& equal(sz00,sdtpldt0(smndt0(X2),X2)) ) ),
inference(variable_rename,[status(thm)],[260]) ).
fof(262,plain,
! [X2] :
( ( equal(sdtpldt0(X2,smndt0(X2)),sz00)
| ~ aInteger0(X2) )
& ( equal(sz00,sdtpldt0(smndt0(X2),X2))
| ~ aInteger0(X2) ) ),
inference(distribute,[status(thm)],[261]) ).
cnf(263,plain,
( sz00 = sdtpldt0(smndt0(X1),X1)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[262]) ).
cnf(264,plain,
( sdtpldt0(X1,smndt0(X1)) = sz00
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[262]) ).
fof(291,negated_conjecture,
! [X1] :
( ( ( ~ aInteger0(X1)
| ( ! [X2] :
( ~ aInteger0(X2)
| ~ equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
& ~ aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X1,sz10,xp) ) )
& ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
| ( ( equal(X1,sz10)
| equal(X1,smndt0(sz10)) )
& aElementOf0(X1,cS2200) ) ),
inference(fof_nnf,[status(thm)],[48]) ).
fof(292,negated_conjecture,
! [X3] :
( ( ( ~ aInteger0(X3)
| ( ! [X4] :
( ~ aInteger0(X4)
| ~ equal(sdtasdt0(xp,X4),sdtpldt0(X3,smndt0(sz10))) )
& ~ aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X3,sz10,xp) ) )
& ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
| ( ( equal(X3,sz10)
| equal(X3,smndt0(sz10)) )
& aElementOf0(X3,cS2200) ) ),
inference(variable_rename,[status(thm)],[291]) ).
fof(293,negated_conjecture,
! [X3,X4] :
( ( ( ( ( ~ aInteger0(X4)
| ~ equal(sdtasdt0(xp,X4),sdtpldt0(X3,smndt0(sz10))) )
& ~ aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X3,sz10,xp) )
| ~ aInteger0(X3) )
& ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
| ( ( equal(X3,sz10)
| equal(X3,smndt0(sz10)) )
& aElementOf0(X3,cS2200) ) ),
inference(shift_quantors,[status(thm)],[292]) ).
fof(294,negated_conjecture,
! [X3,X4] :
( ( equal(X3,sz10)
| equal(X3,smndt0(sz10))
| ~ aInteger0(X4)
| ~ equal(sdtasdt0(xp,X4),sdtpldt0(X3,smndt0(sz10)))
| ~ aInteger0(X3) )
& ( aElementOf0(X3,cS2200)
| ~ aInteger0(X4)
| ~ equal(sdtasdt0(xp,X4),sdtpldt0(X3,smndt0(sz10)))
| ~ aInteger0(X3) )
& ( equal(X3,sz10)
| equal(X3,smndt0(sz10))
| ~ aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
| ~ aInteger0(X3) )
& ( aElementOf0(X3,cS2200)
| ~ aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
| ~ aInteger0(X3) )
& ( equal(X3,sz10)
| equal(X3,smndt0(sz10))
| ~ sdteqdtlpzmzozddtrp0(X3,sz10,xp)
| ~ aInteger0(X3) )
& ( aElementOf0(X3,cS2200)
| ~ sdteqdtlpzmzozddtrp0(X3,sz10,xp)
| ~ aInteger0(X3) )
& ( equal(X3,sz10)
| equal(X3,smndt0(sz10))
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(X3,cS2200)
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) ),
inference(distribute,[status(thm)],[293]) ).
cnf(296,negated_conjecture,
( X1 = smndt0(sz10)
| X1 = sz10
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(split_conjunct,[status(thm)],[294]) ).
cnf(298,negated_conjecture,
( X1 = smndt0(sz10)
| X1 = sz10
| ~ aInteger0(X1)
| ~ sdteqdtlpzmzozddtrp0(X1,sz10,xp) ),
inference(split_conjunct,[status(thm)],[294]) ).
cnf(300,negated_conjecture,
( X1 = smndt0(sz10)
| X1 = sz10
| ~ aInteger0(X1)
| ~ aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10))) ),
inference(split_conjunct,[status(thm)],[294]) ).
fof(303,plain,
! [X1,X2,X3] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| equal(sdtasdt0(X1,sdtasdt0(X2,X3)),sdtasdt0(sdtasdt0(X1,X2),X3)) ),
inference(fof_nnf,[status(thm)],[30]) ).
fof(304,plain,
! [X4,X5,X6] :
( ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| equal(sdtasdt0(X4,sdtasdt0(X5,X6)),sdtasdt0(sdtasdt0(X4,X5),X6)) ),
inference(variable_rename,[status(thm)],[303]) ).
cnf(305,plain,
( sdtasdt0(X1,sdtasdt0(X2,X3)) = sdtasdt0(sdtasdt0(X1,X2),X3)
| ~ aInteger0(X3)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[304]) ).
fof(306,plain,
! [X1,X2] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| equal(X2,sz00)
| sdteqdtlpzmzozddtrp0(X1,X1,X2) ),
inference(fof_nnf,[status(thm)],[31]) ).
fof(307,plain,
! [X3,X4] :
( ~ aInteger0(X3)
| ~ aInteger0(X4)
| equal(X4,sz00)
| sdteqdtlpzmzozddtrp0(X3,X3,X4) ),
inference(variable_rename,[status(thm)],[306]) ).
cnf(308,plain,
( sdteqdtlpzmzozddtrp0(X1,X1,X2)
| X2 = sz00
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[307]) ).
fof(309,plain,
! [X1,X2] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| aInteger0(sdtasdt0(X1,X2)) ),
inference(fof_nnf,[status(thm)],[32]) ).
fof(310,plain,
! [X3,X4] :
( ~ aInteger0(X3)
| ~ aInteger0(X4)
| aInteger0(sdtasdt0(X3,X4)) ),
inference(variable_rename,[status(thm)],[309]) ).
cnf(311,plain,
( aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[310]) ).
fof(312,plain,
! [X1,X2,X3] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| equal(sdtpldt0(X1,sdtpldt0(X2,X3)),sdtpldt0(sdtpldt0(X1,X2),X3)) ),
inference(fof_nnf,[status(thm)],[33]) ).
fof(313,plain,
! [X4,X5,X6] :
( ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| equal(sdtpldt0(X4,sdtpldt0(X5,X6)),sdtpldt0(sdtpldt0(X4,X5),X6)) ),
inference(variable_rename,[status(thm)],[312]) ).
cnf(314,plain,
( sdtpldt0(X1,sdtpldt0(X2,X3)) = sdtpldt0(sdtpldt0(X1,X2),X3)
| ~ aInteger0(X3)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[313]) ).
fof(345,plain,
! [X1] :
( ~ aInteger0(X1)
| aInteger0(smndt0(X1)) ),
inference(fof_nnf,[status(thm)],[35]) ).
fof(346,plain,
! [X2] :
( ~ aInteger0(X2)
| aInteger0(smndt0(X2)) ),
inference(variable_rename,[status(thm)],[345]) ).
cnf(347,plain,
( aInteger0(smndt0(X1))
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[346]) ).
cnf(348,plain,
aInteger0(sz00),
inference(split_conjunct,[status(thm)],[36]) ).
fof(349,plain,
! [X1] :
( ~ aInteger0(X1)
| ( equal(sdtpldt0(X1,sz00),X1)
& equal(X1,sdtpldt0(sz00,X1)) ) ),
inference(fof_nnf,[status(thm)],[37]) ).
fof(350,plain,
! [X2] :
( ~ aInteger0(X2)
| ( equal(sdtpldt0(X2,sz00),X2)
& equal(X2,sdtpldt0(sz00,X2)) ) ),
inference(variable_rename,[status(thm)],[349]) ).
fof(351,plain,
! [X2] :
( ( equal(sdtpldt0(X2,sz00),X2)
| ~ aInteger0(X2) )
& ( equal(X2,sdtpldt0(sz00,X2))
| ~ aInteger0(X2) ) ),
inference(distribute,[status(thm)],[350]) ).
cnf(352,plain,
( X1 = sdtpldt0(sz00,X1)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[351]) ).
cnf(353,plain,
( sdtpldt0(X1,sz00) = X1
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[351]) ).
fof(354,plain,
! [X1,X2] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| equal(sdtasdt0(X1,X2),sdtasdt0(X2,X1)) ),
inference(fof_nnf,[status(thm)],[38]) ).
fof(355,plain,
! [X3,X4] :
( ~ aInteger0(X3)
| ~ aInteger0(X4)
| equal(sdtasdt0(X3,X4),sdtasdt0(X4,X3)) ),
inference(variable_rename,[status(thm)],[354]) ).
cnf(356,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X2,X1)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(split_conjunct,[status(thm)],[355]) ).
fof(357,plain,
! [X1,X2,X3] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| equal(X3,sz00)
| ( ( ~ sdteqdtlpzmzozddtrp0(X1,X2,X3)
| aDivisorOf0(X3,sdtpldt0(X1,smndt0(X2))) )
& ( ~ aDivisorOf0(X3,sdtpldt0(X1,smndt0(X2)))
| sdteqdtlpzmzozddtrp0(X1,X2,X3) ) ) ),
inference(fof_nnf,[status(thm)],[39]) ).
fof(358,plain,
! [X4,X5,X6] :
( ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| equal(X6,sz00)
| ( ( ~ sdteqdtlpzmzozddtrp0(X4,X5,X6)
| aDivisorOf0(X6,sdtpldt0(X4,smndt0(X5))) )
& ( ~ aDivisorOf0(X6,sdtpldt0(X4,smndt0(X5)))
| sdteqdtlpzmzozddtrp0(X4,X5,X6) ) ) ),
inference(variable_rename,[status(thm)],[357]) ).
fof(359,plain,
! [X4,X5,X6] :
( ( ~ sdteqdtlpzmzozddtrp0(X4,X5,X6)
| aDivisorOf0(X6,sdtpldt0(X4,smndt0(X5)))
| ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| equal(X6,sz00) )
& ( ~ aDivisorOf0(X6,sdtpldt0(X4,smndt0(X5)))
| sdteqdtlpzmzozddtrp0(X4,X5,X6)
| ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| equal(X6,sz00) ) ),
inference(distribute,[status(thm)],[358]) ).
cnf(360,plain,
( X1 = sz00
| sdteqdtlpzmzozddtrp0(X3,X2,X1)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| ~ aDivisorOf0(X1,sdtpldt0(X3,smndt0(X2))) ),
inference(split_conjunct,[status(thm)],[359]) ).
fof(362,plain,
! [X1,X2,X3,X4] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| equal(X3,sz00)
| ~ aInteger0(X4)
| equal(X4,sz00)
| ~ sdteqdtlpzmzozddtrp0(X1,X2,sdtasdt0(X3,X4))
| ( sdteqdtlpzmzozddtrp0(X1,X2,X3)
& sdteqdtlpzmzozddtrp0(X1,X2,X4) ) ),
inference(fof_nnf,[status(thm)],[40]) ).
fof(363,plain,
! [X5,X6,X7,X8] :
( ~ aInteger0(X5)
| ~ aInteger0(X6)
| ~ aInteger0(X7)
| equal(X7,sz00)
| ~ aInteger0(X8)
| equal(X8,sz00)
| ~ sdteqdtlpzmzozddtrp0(X5,X6,sdtasdt0(X7,X8))
| ( sdteqdtlpzmzozddtrp0(X5,X6,X7)
& sdteqdtlpzmzozddtrp0(X5,X6,X8) ) ),
inference(variable_rename,[status(thm)],[362]) ).
fof(364,plain,
! [X5,X6,X7,X8] :
( ( sdteqdtlpzmzozddtrp0(X5,X6,X7)
| ~ sdteqdtlpzmzozddtrp0(X5,X6,sdtasdt0(X7,X8))
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| ~ aInteger0(X7)
| equal(X7,sz00)
| ~ aInteger0(X8)
| equal(X8,sz00) )
& ( sdteqdtlpzmzozddtrp0(X5,X6,X8)
| ~ sdteqdtlpzmzozddtrp0(X5,X6,sdtasdt0(X7,X8))
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| ~ aInteger0(X7)
| equal(X7,sz00)
| ~ aInteger0(X8)
| equal(X8,sz00) ) ),
inference(distribute,[status(thm)],[363]) ).
cnf(366,plain,
( X1 = sz00
| X2 = sz00
| sdteqdtlpzmzozddtrp0(X4,X3,X2)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| ~ aInteger0(X4)
| ~ sdteqdtlpzmzozddtrp0(X4,X3,sdtasdt0(X2,X1)) ),
inference(split_conjunct,[status(thm)],[364]) ).
fof(370,plain,
! [X1,X2,X3] :
( ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| ( equal(sdtasdt0(X1,sdtpldt0(X2,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3)))
& equal(sdtasdt0(sdtpldt0(X1,X2),X3),sdtpldt0(sdtasdt0(X1,X3),sdtasdt0(X2,X3))) ) ),
inference(fof_nnf,[status(thm)],[42]) ).
fof(371,plain,
! [X4,X5,X6] :
( ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6)
| ( equal(sdtasdt0(X4,sdtpldt0(X5,X6)),sdtpldt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6)))
& equal(sdtasdt0(sdtpldt0(X4,X5),X6),sdtpldt0(sdtasdt0(X4,X6),sdtasdt0(X5,X6))) ) ),
inference(variable_rename,[status(thm)],[370]) ).
fof(372,plain,
! [X4,X5,X6] :
( ( equal(sdtasdt0(X4,sdtpldt0(X5,X6)),sdtpldt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6)))
| ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6) )
& ( equal(sdtasdt0(sdtpldt0(X4,X5),X6),sdtpldt0(sdtasdt0(X4,X6),sdtasdt0(X5,X6)))
| ~ aInteger0(X4)
| ~ aInteger0(X5)
| ~ aInteger0(X6) ) ),
inference(distribute,[status(thm)],[371]) ).
cnf(373,plain,
( sdtasdt0(sdtpldt0(X3,X2),X1) = sdtpldt0(sdtasdt0(X3,X1),sdtasdt0(X2,X1))
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3) ),
inference(split_conjunct,[status(thm)],[372]) ).
cnf(374,plain,
( sdtasdt0(X3,sdtpldt0(X2,X1)) = sdtpldt0(sdtasdt0(X3,X2),sdtasdt0(X3,X1))
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3) ),
inference(split_conjunct,[status(thm)],[372]) ).
fof(385,plain,
( aInteger0(xp)
& ~ equal(xp,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X1] :
( ( ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ( aInteger0(X1)
& ? [X2] :
( aInteger0(X2)
& equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
& aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X1,sz10,xp) ) )
& ( ~ aInteger0(X1)
| ( ! [X2] :
( ~ aInteger0(X2)
| ~ equal(sdtasdt0(xp,X2),sdtpldt0(X1,smndt0(sz10))) )
& ~ aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X1,sz10,xp) )
| aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X1] :
( ( ~ aElementOf0(X1,sbsmnsldt0(xS))
| ( aInteger0(X1)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X1,X2) ) ) )
& ( ~ aInteger0(X1)
| ! [X2] :
( ~ aElementOf0(X2,xS)
| ~ aElementOf0(X1,X2) )
| aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ! [X1] :
( ( ~ aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X1)
& ~ aElementOf0(X1,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X1)
| aElementOf0(X1,sbsmnsldt0(xS))
| aElementOf0(X1,stldt0(sbsmnsldt0(xS))) ) )
& ! [X1] :
( ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| aElementOf0(X1,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(fof_nnf,[status(thm)],[52]) ).
fof(386,plain,
( aInteger0(xp)
& ~ equal(xp,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X3] :
( ( ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ( aInteger0(X3)
& ? [X4] :
( aInteger0(X4)
& equal(sdtasdt0(xp,X4),sdtpldt0(X3,smndt0(sz10))) )
& aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X3,sz10,xp) ) )
& ( ~ aInteger0(X3)
| ( ! [X5] :
( ~ aInteger0(X5)
| ~ equal(sdtasdt0(xp,X5),sdtpldt0(X3,smndt0(sz10))) )
& ~ aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X3,sz10,xp) )
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X6] :
( ( ~ aElementOf0(X6,sbsmnsldt0(xS))
| ( aInteger0(X6)
& ? [X7] :
( aElementOf0(X7,xS)
& aElementOf0(X6,X7) ) ) )
& ( ~ aInteger0(X6)
| ! [X8] :
( ~ aElementOf0(X8,xS)
| ~ aElementOf0(X6,X8) )
| aElementOf0(X6,sbsmnsldt0(xS)) ) )
& ! [X9] :
( ( ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X9)
& ~ aElementOf0(X9,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,sbsmnsldt0(xS))
| aElementOf0(X9,stldt0(sbsmnsldt0(xS))) ) )
& ! [X10] :
( ~ aElementOf0(X10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| aElementOf0(X10,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(variable_rename,[status(thm)],[385]) ).
fof(387,plain,
( aInteger0(xp)
& ~ equal(xp,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X3] :
( ( ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ( aInteger0(X3)
& aInteger0(esk24_1(X3))
& equal(sdtasdt0(xp,esk24_1(X3)),sdtpldt0(X3,smndt0(sz10)))
& aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X3,sz10,xp) ) )
& ( ~ aInteger0(X3)
| ( ! [X5] :
( ~ aInteger0(X5)
| ~ equal(sdtasdt0(xp,X5),sdtpldt0(X3,smndt0(sz10))) )
& ~ aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X3,sz10,xp) )
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X6] :
( ( ~ aElementOf0(X6,sbsmnsldt0(xS))
| ( aInteger0(X6)
& aElementOf0(esk25_1(X6),xS)
& aElementOf0(X6,esk25_1(X6)) ) )
& ( ~ aInteger0(X6)
| ! [X8] :
( ~ aElementOf0(X8,xS)
| ~ aElementOf0(X6,X8) )
| aElementOf0(X6,sbsmnsldt0(xS)) ) )
& ! [X9] :
( ( ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X9)
& ~ aElementOf0(X9,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,sbsmnsldt0(xS))
| aElementOf0(X9,stldt0(sbsmnsldt0(xS))) ) )
& ! [X10] :
( ~ aElementOf0(X10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| aElementOf0(X10,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(skolemize,[status(esa)],[386]) ).
fof(388,plain,
! [X3,X5,X6,X8,X9,X10] :
( ( ~ aElementOf0(X10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| aElementOf0(X10,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS)))
| ( aInteger0(X9)
& ~ aElementOf0(X9,sbsmnsldt0(xS)) ) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,sbsmnsldt0(xS))
| aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X8,xS)
| ~ aElementOf0(X6,X8)
| ~ aInteger0(X6)
| aElementOf0(X6,sbsmnsldt0(xS)) )
& ( ~ aElementOf0(X6,sbsmnsldt0(xS))
| ( aInteger0(X6)
& aElementOf0(esk25_1(X6),xS)
& aElementOf0(X6,esk25_1(X6)) ) )
& ( ( ( ~ aInteger0(X5)
| ~ equal(sdtasdt0(xp,X5),sdtpldt0(X3,smndt0(sz10))) )
& ~ aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X3,sz10,xp) )
| ~ aInteger0(X3)
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ( aInteger0(X3)
& aInteger0(esk24_1(X3))
& equal(sdtasdt0(xp,esk24_1(X3)),sdtpldt0(X3,smndt0(sz10)))
& aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X3,sz10,xp) ) )
& aInteger0(xp)
& ~ equal(xp,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& aSet0(sbsmnsldt0(xS))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(shift_quantors,[status(thm)],[387]) ).
fof(389,plain,
! [X3,X5,X6,X8,X9,X10] :
( ( ~ aElementOf0(X10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| aElementOf0(X10,stldt0(sbsmnsldt0(xS))) )
& ( aInteger0(X9)
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X9,sbsmnsldt0(xS))
| ~ aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ aInteger0(X9)
| aElementOf0(X9,sbsmnsldt0(xS))
| aElementOf0(X9,stldt0(sbsmnsldt0(xS))) )
& ( ~ aElementOf0(X8,xS)
| ~ aElementOf0(X6,X8)
| ~ aInteger0(X6)
| aElementOf0(X6,sbsmnsldt0(xS)) )
& ( aInteger0(X6)
| ~ aElementOf0(X6,sbsmnsldt0(xS)) )
& ( aElementOf0(esk25_1(X6),xS)
| ~ aElementOf0(X6,sbsmnsldt0(xS)) )
& ( aElementOf0(X6,esk25_1(X6))
| ~ aElementOf0(X6,sbsmnsldt0(xS)) )
& ( ~ aInteger0(X5)
| ~ equal(sdtasdt0(xp,X5),sdtpldt0(X3,smndt0(sz10)))
| ~ aInteger0(X3)
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( ~ aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
| ~ aInteger0(X3)
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( ~ sdteqdtlpzmzozddtrp0(X3,sz10,xp)
| ~ aInteger0(X3)
| aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aInteger0(X3)
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aInteger0(esk24_1(X3))
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( equal(sdtasdt0(xp,esk24_1(X3)),sdtpldt0(X3,smndt0(sz10)))
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aDivisorOf0(xp,sdtpldt0(X3,smndt0(sz10)))
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( sdteqdtlpzmzozddtrp0(X3,sz10,xp)
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aInteger0(xp)
& ~ equal(xp,sz00)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& aSet0(sbsmnsldt0(xS))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(distribute,[status(thm)],[388]) ).
cnf(393,plain,
xp != sz00,
inference(split_conjunct,[status(thm)],[389]) ).
cnf(394,plain,
aInteger0(xp),
inference(split_conjunct,[status(thm)],[389]) ).
cnf(395,plain,
( sdteqdtlpzmzozddtrp0(X1,sz10,xp)
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(split_conjunct,[status(thm)],[389]) ).
cnf(396,plain,
( aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10)))
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(split_conjunct,[status(thm)],[389]) ).
cnf(397,plain,
( sdtasdt0(xp,esk24_1(X1)) = sdtpldt0(X1,smndt0(sz10))
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(split_conjunct,[status(thm)],[389]) ).
cnf(398,plain,
( aInteger0(esk24_1(X1))
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(split_conjunct,[status(thm)],[389]) ).
cnf(400,plain,
( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X1)
| ~ sdteqdtlpzmzozddtrp0(X1,sz10,xp) ),
inference(split_conjunct,[status(thm)],[389]) ).
cnf(401,plain,
( aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X1)
| ~ aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10))) ),
inference(split_conjunct,[status(thm)],[389]) ).
cnf(410,plain,
( aElementOf0(X1,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(split_conjunct,[status(thm)],[389]) ).
cnf(457,plain,
( smndt0(sz00) = sz00
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[81,73,theory(equality)]) ).
cnf(458,plain,
( smndt0(sz00) = sz00
| ~ aInteger0(smndt0(sz10))
| $false ),
inference(rw,[status(thm)],[457,348,theory(equality)]) ).
cnf(459,plain,
( smndt0(sz00) = sz00
| ~ aInteger0(smndt0(sz10)) ),
inference(cn,[status(thm)],[458,theory(equality)]) ).
cnf(464,plain,
( aElementOf0(X1,cS2076)
| sz10 != X1 ),
inference(rw,[status(thm)],[246,235,theory(equality)]) ).
cnf(511,plain,
( aInteger0(X1)
| ~ aElementOf0(X1,cS2076) ),
inference(rw,[status(thm)],[157,235,theory(equality)]) ).
cnf(512,plain,
( aInteger0(X1)
| sz10 != X1 ),
inference(spm,[status(thm)],[511,464,theory(equality)]) ).
cnf(515,plain,
( aDivisorOf0(xp,sz00)
| ~ aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[396,264,theory(equality)]) ).
cnf(521,plain,
( aDivisorOf0(xp,sz00)
| ~ aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| $false ),
inference(rw,[status(thm)],[515,191,theory(equality)]) ).
cnf(522,plain,
( aDivisorOf0(xp,sz00)
| ~ aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(cn,[status(thm)],[521,theory(equality)]) ).
cnf(537,plain,
( aElementOf0(X1,cS2076)
| smndt0(sz10) != X1 ),
inference(rw,[status(thm)],[245,235,theory(equality)]) ).
cnf(538,plain,
( aInteger0(X1)
| smndt0(sz10) != X1 ),
inference(spm,[status(thm)],[511,537,theory(equality)]) ).
cnf(544,plain,
( aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,smndt0(sz10))
| ~ aInteger0(sz00)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[401,352,theory(equality)]) ).
cnf(545,plain,
( aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,sz00)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[401,264,theory(equality)]) ).
cnf(546,plain,
( aElementOf0(smndt0(smndt0(sz10)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,sz00)
| ~ aInteger0(smndt0(smndt0(sz10)))
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[401,263,theory(equality)]) ).
cnf(550,plain,
( aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,smndt0(sz10))
| $false
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[544,348,theory(equality)]) ).
cnf(551,plain,
( aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,smndt0(sz10))
| ~ aInteger0(smndt0(sz10)) ),
inference(cn,[status(thm)],[550,theory(equality)]) ).
cnf(552,plain,
( aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,sz00)
| $false ),
inference(rw,[status(thm)],[545,191,theory(equality)]) ).
cnf(553,plain,
( aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,sz00) ),
inference(cn,[status(thm)],[552,theory(equality)]) ).
cnf(569,negated_conjecture,
( smndt0(sz10) = X1
| sz10 = X1
| ~ aDivisorOf0(xp,sdtpldt0(smndt0(sz10),X1))
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[300,99,theory(equality)]) ).
cnf(642,plain,
( aElementOf0(X1,cS2076)
| ~ aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(rw,[status(thm)],[410,235,theory(equality)]) ).
cnf(643,plain,
( aElementOf0(X1,cS2076)
| ~ sdteqdtlpzmzozddtrp0(X1,sz10,xp)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[642,400,theory(equality)]) ).
cnf(667,plain,
( sz00 = smndt0(sz10)
| sz00 = X1
| smndt0(X1) != sz00
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[118,73,theory(equality)]) ).
cnf(671,plain,
( sz00 = esk3_2(X1,X2)
| sz00 = X2
| X1 != sz00
| ~ aInteger0(X2)
| ~ aInteger0(esk3_2(X1,X2))
| ~ aDivisorOf0(X2,X1)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[118,108,theory(equality)]) ).
cnf(679,plain,
( sz10 = X1
| smndt0(sz10) = X1
| ~ aElementOf0(X1,cS2076) ),
inference(rw,[status(thm)],[247,235,theory(equality)]) ).
cnf(817,plain,
( sz00 = X1
| aDivisorOf0(X1,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(sdtasdt0(X1,X2)) ),
inference(er,[status(thm)],[112,theory(equality)]) ).
cnf(818,plain,
( sz00 = X1
| aDivisorOf0(X1,X2)
| X1 != X2
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(spm,[status(thm)],[112,57,theory(equality)]) ).
cnf(819,plain,
( sz00 = sz10
| aDivisorOf0(sz10,X1)
| X2 != X1
| ~ aInteger0(X2)
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[112,56,theory(equality)]) ).
cnf(826,plain,
( sz00 = X1
| aDivisorOf0(X1,X2)
| X1 != X2
| $false
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(rw,[status(thm)],[818,191,theory(equality)]) ).
cnf(827,plain,
( sz00 = X1
| aDivisorOf0(X1,X2)
| X1 != X2
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cn,[status(thm)],[826,theory(equality)]) ).
cnf(828,plain,
( sz00 = X1
| aDivisorOf0(X1,X1)
| ~ aInteger0(X1) ),
inference(er,[status(thm)],[827,theory(equality)]) ).
cnf(829,plain,
( sz00 = sz10
| aDivisorOf0(sz10,X1)
| X2 != X1
| ~ aInteger0(X2)
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[819,191,theory(equality)]) ).
cnf(830,plain,
( sz00 = sz10
| aDivisorOf0(sz10,X1)
| X2 != X1
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[829,theory(equality)]) ).
cnf(831,plain,
( sz10 = sz00
| aDivisorOf0(sz10,X1)
| ~ aInteger0(X1) ),
inference(er,[status(thm)],[830,theory(equality)]) ).
cnf(849,plain,
( sdtasdt0(X1,sdtasdt0(X2,sz10)) = sdtasdt0(X1,X2)
| ~ aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(sz10)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[57,305,theory(equality)]) ).
cnf(850,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X1,sdtasdt0(sz10,X2))
| ~ aInteger0(X2)
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[305,57,theory(equality)]) ).
cnf(851,plain,
( sdtasdt0(X1,X2) = sdtasdt0(sz10,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[305,56,theory(equality)]) ).
cnf(854,plain,
( aInteger0(sdtasdt0(X1,sdtasdt0(X2,X3)))
| ~ aInteger0(X3)
| ~ aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[311,305,theory(equality)]) ).
cnf(855,plain,
( sdtasdt0(sz00,X2) = sdtasdt0(sz00,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[305,81,theory(equality)]) ).
cnf(856,plain,
( sdtasdt0(X1,sdtasdt0(X2,smndt0(sz10))) = smndt0(sdtasdt0(X1,X2))
| ~ aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[73,305,theory(equality)]) ).
cnf(857,plain,
( sdtasdt0(smndt0(X1),X2) = sdtasdt0(X1,sdtasdt0(smndt0(sz10),X2))
| ~ aInteger0(X2)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[305,73,theory(equality)]) ).
cnf(858,plain,
( sdtasdt0(smndt0(X1),X2) = sdtasdt0(smndt0(sz10),sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[305,74,theory(equality)]) ).
cnf(859,plain,
( sdtasdt0(X1,sdtasdt0(X2,X3)) = sdtasdt0(X3,sdtasdt0(X1,X2))
| ~ aInteger0(X3)
| ~ aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[356,305,theory(equality)]) ).
cnf(869,plain,
( sdtasdt0(X1,sdtasdt0(X2,sz10)) = sdtasdt0(X1,X2)
| ~ aInteger0(sdtasdt0(X1,X2))
| $false
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[849,191,theory(equality)]) ).
cnf(870,plain,
( sdtasdt0(X1,sdtasdt0(X2,sz10)) = sdtasdt0(X1,X2)
| ~ aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[869,theory(equality)]) ).
cnf(871,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X1,sdtasdt0(sz10,X2))
| ~ aInteger0(X2)
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[850,191,theory(equality)]) ).
cnf(872,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X1,sdtasdt0(sz10,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[871,theory(equality)]) ).
cnf(873,plain,
( sdtasdt0(X1,X2) = sdtasdt0(sz10,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[851,191,theory(equality)]) ).
cnf(874,plain,
( sdtasdt0(X1,X2) = sdtasdt0(sz10,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[873,theory(equality)]) ).
cnf(879,plain,
( sdtasdt0(sz00,X2) = sdtasdt0(sz00,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[855,348,theory(equality)]) ).
cnf(880,plain,
( sdtasdt0(sz00,X2) = sdtasdt0(sz00,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[879,theory(equality)]) ).
cnf(884,plain,
( aInteger0(sdtpldt0(X1,sdtpldt0(X2,X3)))
| ~ aInteger0(X3)
| ~ aInteger0(sdtpldt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[102,314,theory(equality)]) ).
cnf(885,plain,
( sdtpldt0(X1,sdtpldt0(X2,smndt0(sdtpldt0(X1,X2)))) = sz00
| ~ aInteger0(sdtpldt0(X1,X2))
| ~ aInteger0(smndt0(sdtpldt0(X1,X2)))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[264,314,theory(equality)]) ).
cnf(886,plain,
( sdtpldt0(sz00,X2) = sdtpldt0(X1,sdtpldt0(smndt0(X1),X2))
| ~ aInteger0(X2)
| ~ aInteger0(smndt0(X1))
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[314,264,theory(equality)]) ).
cnf(887,plain,
( sdtpldt0(sz00,X2) = sdtpldt0(smndt0(X1),sdtpldt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(X1)) ),
inference(spm,[status(thm)],[314,263,theory(equality)]) ).
cnf(890,plain,
( sdtpldt0(sdtpldt0(X2,X1),X3) = sdtpldt0(X1,sdtpldt0(X2,X3))
| ~ aInteger0(X3)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[314,99,theory(equality)]) ).
cnf(914,plain,
( sz00 = X1
| sdteqdtlpzmzozddtrp0(sz00,X2,X1)
| ~ aDivisorOf0(X1,smndt0(X2))
| ~ aInteger0(sz00)
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(X2)) ),
inference(spm,[status(thm)],[360,352,theory(equality)]) ).
cnf(922,plain,
( sz00 = X1
| sdteqdtlpzmzozddtrp0(sz00,X2,X1)
| ~ aDivisorOf0(X1,smndt0(X2))
| $false
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(X2)) ),
inference(rw,[status(thm)],[914,348,theory(equality)]) ).
cnf(923,plain,
( sz00 = X1
| sdteqdtlpzmzozddtrp0(sz00,X2,X1)
| ~ aDivisorOf0(X1,smndt0(X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(X2)) ),
inference(cn,[status(thm)],[922,theory(equality)]) ).
cnf(982,plain,
( sdtpldt0(X1,sdtasdt0(X1,X2)) = sdtasdt0(X1,sdtpldt0(sz10,X2))
| ~ aInteger0(X1)
| ~ aInteger0(sz10)
| ~ aInteger0(X2) ),
inference(spm,[status(thm)],[374,57,theory(equality)]) ).
cnf(984,plain,
( sdtpldt0(X1,sdtasdt0(sz10,X2)) = sdtasdt0(sz10,sdtpldt0(X1,X2))
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(spm,[status(thm)],[374,56,theory(equality)]) ).
cnf(985,plain,
( sdtpldt0(sdtasdt0(sz10,X1),X2) = sdtasdt0(sz10,sdtpldt0(X1,X2))
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(spm,[status(thm)],[374,56,theory(equality)]) ).
cnf(990,plain,
( aInteger0(sdtasdt0(X1,sdtpldt0(X2,X3)))
| ~ aInteger0(sdtasdt0(X1,X3))
| ~ aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3) ),
inference(spm,[status(thm)],[102,374,theory(equality)]) ).
cnf(991,plain,
( sdtpldt0(smndt0(X1),sdtasdt0(X1,X2)) = sdtasdt0(X1,sdtpldt0(smndt0(sz10),X2))
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X2) ),
inference(spm,[status(thm)],[374,73,theory(equality)]) ).
cnf(1006,plain,
( sdtpldt0(X1,sdtasdt0(X1,X2)) = sdtasdt0(X1,sdtpldt0(sz10,X2))
| ~ aInteger0(X1)
| $false
| ~ aInteger0(X2) ),
inference(rw,[status(thm)],[982,191,theory(equality)]) ).
cnf(1007,plain,
( sdtpldt0(X1,sdtasdt0(X1,X2)) = sdtasdt0(X1,sdtpldt0(sz10,X2))
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cn,[status(thm)],[1006,theory(equality)]) ).
cnf(1010,plain,
( sdtpldt0(X1,sdtasdt0(sz10,X2)) = sdtasdt0(sz10,sdtpldt0(X1,X2))
| $false
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(rw,[status(thm)],[984,191,theory(equality)]) ).
cnf(1011,plain,
( sdtpldt0(X1,sdtasdt0(sz10,X2)) = sdtasdt0(sz10,sdtpldt0(X1,X2))
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cn,[status(thm)],[1010,theory(equality)]) ).
cnf(1012,plain,
( sdtpldt0(sdtasdt0(sz10,X1),X2) = sdtasdt0(sz10,sdtpldt0(X1,X2))
| $false
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(rw,[status(thm)],[985,191,theory(equality)]) ).
cnf(1013,plain,
( sdtpldt0(sdtasdt0(sz10,X1),X2) = sdtasdt0(sz10,sdtpldt0(X1,X2))
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cn,[status(thm)],[1012,theory(equality)]) ).
cnf(1022,plain,
( sdtpldt0(X1,sdtasdt0(X2,sz10)) = sdtasdt0(sdtpldt0(X1,X2),sz10)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[373,57,theory(equality)]) ).
cnf(1024,plain,
( sdtpldt0(X1,sdtasdt0(X2,X1)) = sdtasdt0(sdtpldt0(sz10,X2),X1)
| ~ aInteger0(sz10)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[373,56,theory(equality)]) ).
cnf(1033,plain,
( sdtpldt0(smndt0(X1),sdtasdt0(X2,X1)) = sdtasdt0(sdtpldt0(smndt0(sz10),X2),X1)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[373,74,theory(equality)]) ).
cnf(1047,plain,
( sdtpldt0(X1,sdtasdt0(X2,sz10)) = sdtasdt0(sdtpldt0(X1,X2),sz10)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| $false ),
inference(rw,[status(thm)],[1022,191,theory(equality)]) ).
cnf(1048,plain,
( sdtpldt0(X1,sdtasdt0(X2,sz10)) = sdtasdt0(sdtpldt0(X1,X2),sz10)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cn,[status(thm)],[1047,theory(equality)]) ).
cnf(1051,plain,
( sdtpldt0(X1,sdtasdt0(X2,X1)) = sdtasdt0(sdtpldt0(sz10,X2),X1)
| $false
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[1024,191,theory(equality)]) ).
cnf(1052,plain,
( sdtpldt0(X1,sdtasdt0(X2,X1)) = sdtasdt0(sdtpldt0(sz10,X2),X1)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[1051,theory(equality)]) ).
cnf(1224,plain,
( sz00 = smndt0(sz10)
| sz00 = X1
| sdteqdtlpzmzozddtrp0(X2,X3,X1)
| ~ sdteqdtlpzmzozddtrp0(X2,X3,smndt0(X1))
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[366,73,theory(equality)]) ).
cnf(2149,plain,
( smndt0(sz00) = sz00
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[459,347,theory(equality)]) ).
cnf(2151,plain,
( smndt0(sz00) = sz00
| $false ),
inference(rw,[status(thm)],[2149,191,theory(equality)]) ).
cnf(2152,plain,
smndt0(sz00) = sz00,
inference(cn,[status(thm)],[2151,theory(equality)]) ).
cnf(2154,plain,
( sdtpldt0(sz00,sz00) = sz00
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[264,2152,theory(equality)]) ).
cnf(2176,plain,
( sdtpldt0(sz00,sz00) = sz00
| $false ),
inference(rw,[status(thm)],[2154,348,theory(equality)]) ).
cnf(2177,plain,
sdtpldt0(sz00,sz00) = sz00,
inference(cn,[status(thm)],[2176,theory(equality)]) ).
cnf(2286,plain,
aInteger0(smndt0(sz10)),
inference(er,[status(thm)],[538,theory(equality)]) ).
cnf(2319,plain,
( aDivisorOf0(xp,sz00)
| ~ sdteqdtlpzmzozddtrp0(sz10,sz10,xp)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[522,400,theory(equality)]) ).
cnf(2320,plain,
( aDivisorOf0(xp,sz00)
| ~ sdteqdtlpzmzozddtrp0(sz10,sz10,xp)
| $false ),
inference(rw,[status(thm)],[2319,191,theory(equality)]) ).
cnf(2321,plain,
( aDivisorOf0(xp,sz00)
| ~ sdteqdtlpzmzozddtrp0(sz10,sz10,xp) ),
inference(cn,[status(thm)],[2320,theory(equality)]) ).
cnf(2322,plain,
( aDivisorOf0(xp,sz00)
| sz00 = xp
| ~ aInteger0(xp)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[2321,308,theory(equality)]) ).
cnf(2323,plain,
( aDivisorOf0(xp,sz00)
| sz00 = xp
| $false
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[2322,394,theory(equality)]) ).
cnf(2324,plain,
( aDivisorOf0(xp,sz00)
| sz00 = xp
| $false
| $false ),
inference(rw,[status(thm)],[2323,191,theory(equality)]) ).
cnf(2325,plain,
( aDivisorOf0(xp,sz00)
| sz00 = xp ),
inference(cn,[status(thm)],[2324,theory(equality)]) ).
cnf(2326,plain,
aDivisorOf0(xp,sz00),
inference(sr,[status(thm)],[2325,393,theory(equality)]) ).
cnf(2413,plain,
( aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| $false ),
inference(rw,[status(thm)],[553,2326,theory(equality)]) ).
cnf(2414,plain,
aElementOf0(sz10,szAzrzSzezqlpdtcmdtrp0(sz10,xp)),
inference(cn,[status(thm)],[2413,theory(equality)]) ).
cnf(2418,plain,
aInteger0(esk24_1(sz10)),
inference(spm,[status(thm)],[398,2414,theory(equality)]) ).
cnf(2420,plain,
sdtasdt0(xp,esk24_1(sz10)) = sdtpldt0(sz10,smndt0(sz10)),
inference(spm,[status(thm)],[397,2414,theory(equality)]) ).
cnf(2484,plain,
( sz00 = esk24_1(sz10)
| sz00 = xp
| sdtpldt0(sz10,smndt0(sz10)) != sz00
| ~ aInteger0(xp)
| ~ aInteger0(esk24_1(sz10)) ),
inference(spm,[status(thm)],[118,2420,theory(equality)]) ).
cnf(2501,plain,
( sz00 = esk24_1(sz10)
| sz00 = xp
| sdtpldt0(sz10,smndt0(sz10)) != sz00
| $false
| ~ aInteger0(esk24_1(sz10)) ),
inference(rw,[status(thm)],[2484,394,theory(equality)]) ).
cnf(2502,plain,
( sz00 = esk24_1(sz10)
| sz00 = xp
| sdtpldt0(sz10,smndt0(sz10)) != sz00
| $false
| $false ),
inference(rw,[status(thm)],[2501,2418,theory(equality)]) ).
cnf(2503,plain,
( sz00 = esk24_1(sz10)
| sz00 = xp
| sdtpldt0(sz10,smndt0(sz10)) != sz00 ),
inference(cn,[status(thm)],[2502,theory(equality)]) ).
cnf(2504,plain,
( esk24_1(sz10) = sz00
| sdtpldt0(sz10,smndt0(sz10)) != sz00 ),
inference(sr,[status(thm)],[2503,393,theory(equality)]) ).
cnf(2608,plain,
( esk24_1(sz10) = sz00
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[2504,264,theory(equality)]) ).
cnf(2609,plain,
( esk24_1(sz10) = sz00
| $false ),
inference(rw,[status(thm)],[2608,191,theory(equality)]) ).
cnf(2610,plain,
esk24_1(sz10) = sz00,
inference(cn,[status(thm)],[2609,theory(equality)]) ).
cnf(2611,plain,
sdtasdt0(xp,sz00) = sdtpldt0(sz10,smndt0(sz10)),
inference(rw,[status(thm)],[2420,2610,theory(equality)]) ).
cnf(2616,plain,
( sdtasdt0(xp,sz00) = sz00
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[264,2611,theory(equality)]) ).
cnf(2633,plain,
( sdtasdt0(xp,sz00) = sz00
| $false ),
inference(rw,[status(thm)],[2616,191,theory(equality)]) ).
cnf(2634,plain,
sdtasdt0(xp,sz00) = sz00,
inference(cn,[status(thm)],[2633,theory(equality)]) ).
cnf(2685,plain,
( sz00 = sdtasdt0(sz00,xp)
| ~ aInteger0(sz00)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[356,2634,theory(equality)]) ).
cnf(2687,plain,
( sz00 = xp
| aDivisorOf0(xp,X1)
| sz00 != X1
| ~ aInteger0(sz00)
| ~ aInteger0(xp)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[112,2634,theory(equality)]) ).
cnf(2688,plain,
( sdtasdt0(sz00,X1) = sdtasdt0(xp,sdtasdt0(sz00,X1))
| ~ aInteger0(X1)
| ~ aInteger0(sz00)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[305,2634,theory(equality)]) ).
cnf(2702,plain,
( sz00 = sdtasdt0(sz00,xp)
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[2685,348,theory(equality)]) ).
cnf(2703,plain,
( sz00 = sdtasdt0(sz00,xp)
| $false
| $false ),
inference(rw,[status(thm)],[2702,394,theory(equality)]) ).
cnf(2704,plain,
sz00 = sdtasdt0(sz00,xp),
inference(cn,[status(thm)],[2703,theory(equality)]) ).
cnf(2708,plain,
( sz00 = xp
| aDivisorOf0(xp,X1)
| sz00 != X1
| $false
| ~ aInteger0(xp)
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[2687,348,theory(equality)]) ).
cnf(2709,plain,
( sz00 = xp
| aDivisorOf0(xp,X1)
| sz00 != X1
| $false
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[2708,394,theory(equality)]) ).
cnf(2710,plain,
( sz00 = xp
| aDivisorOf0(xp,X1)
| sz00 != X1
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[2709,theory(equality)]) ).
cnf(2711,plain,
( aDivisorOf0(xp,X1)
| sz00 != X1
| ~ aInteger0(X1) ),
inference(sr,[status(thm)],[2710,393,theory(equality)]) ).
cnf(2712,plain,
( sdtasdt0(sz00,X1) = sdtasdt0(xp,sdtasdt0(sz00,X1))
| ~ aInteger0(X1)
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[2688,348,theory(equality)]) ).
cnf(2713,plain,
( sdtasdt0(sz00,X1) = sdtasdt0(xp,sdtasdt0(sz00,X1))
| ~ aInteger0(X1)
| $false
| $false ),
inference(rw,[status(thm)],[2712,394,theory(equality)]) ).
cnf(2714,plain,
( sdtasdt0(sz00,X1) = sdtasdt0(xp,sdtasdt0(sz00,X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[2713,theory(equality)]) ).
cnf(2748,plain,
( sdtasdt0(sz00,X1) = sdtasdt0(sz00,sdtasdt0(xp,X1))
| ~ aInteger0(X1)
| ~ aInteger0(xp)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[305,2704,theory(equality)]) ).
cnf(2759,plain,
( sdtasdt0(sz00,X1) = sdtasdt0(sz00,sdtasdt0(xp,X1))
| ~ aInteger0(X1)
| $false
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[2748,394,theory(equality)]) ).
cnf(2760,plain,
( sdtasdt0(sz00,X1) = sdtasdt0(sz00,sdtasdt0(xp,X1))
| ~ aInteger0(X1)
| $false
| $false ),
inference(rw,[status(thm)],[2759,348,theory(equality)]) ).
cnf(2761,plain,
( sdtasdt0(sz00,X1) = sdtasdt0(sz00,sdtasdt0(xp,X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[2760,theory(equality)]) ).
cnf(2897,plain,
( sdtasdt0(xp,sdtasdt0(X1,sz00)) = sdtasdt0(X1,sz00)
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[2714,356,theory(equality)]) ).
cnf(2932,plain,
( sdtasdt0(xp,sdtasdt0(X1,sz00)) = sdtasdt0(X1,sz00)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[2897,348,theory(equality)]) ).
cnf(2933,plain,
( sdtasdt0(xp,sdtasdt0(X1,sz00)) = sdtasdt0(X1,sz00)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[2932,theory(equality)]) ).
cnf(2961,plain,
( sdtasdt0(sz00,xp) = sdtasdt0(sz00,sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[2761,57,theory(equality)]) ).
cnf(2975,plain,
( sz00 = sdtasdt0(sz00,sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[2961,2704,theory(equality)]) ).
cnf(2976,plain,
( sz00 = sdtasdt0(sz00,sz10)
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[2975,191,theory(equality)]) ).
cnf(2977,plain,
( sz00 = sdtasdt0(sz00,sz10)
| $false
| $false ),
inference(rw,[status(thm)],[2976,394,theory(equality)]) ).
cnf(2978,plain,
sz00 = sdtasdt0(sz00,sz10),
inference(cn,[status(thm)],[2977,theory(equality)]) ).
cnf(3438,plain,
( sz00 = sdtpldt0(X1,smndt0(X2))
| sdteqdtlpzmzozddtrp0(X1,X2,sdtpldt0(X1,smndt0(X2)))
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(sdtpldt0(X1,smndt0(X2))) ),
inference(spm,[status(thm)],[360,828,theory(equality)]) ).
cnf(3558,plain,
( aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,smndt0(sz10))
| $false ),
inference(rw,[status(thm)],[551,2286,theory(equality)]) ).
cnf(3559,plain,
( aElementOf0(sz00,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aDivisorOf0(xp,smndt0(sz10)) ),
inference(cn,[status(thm)],[3558,theory(equality)]) ).
cnf(3562,plain,
( sdteqdtlpzmzozddtrp0(sz00,sz10,xp)
| ~ aDivisorOf0(xp,smndt0(sz10)) ),
inference(spm,[status(thm)],[395,3559,theory(equality)]) ).
cnf(3710,plain,
( sdteqdtlpzmzozddtrp0(sz00,sz10,xp)
| sz00 != smndt0(sz10)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[3562,2711,theory(equality)]) ).
cnf(3712,plain,
( sdteqdtlpzmzozddtrp0(sz00,sz10,xp)
| sz00 != smndt0(sz10)
| $false ),
inference(rw,[status(thm)],[3710,2286,theory(equality)]) ).
cnf(3713,plain,
( sdteqdtlpzmzozddtrp0(sz00,sz10,xp)
| sz00 != smndt0(sz10) ),
inference(cn,[status(thm)],[3712,theory(equality)]) ).
cnf(3729,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(X1,sz10,xp)
| ~ sdteqdtlpzmzozddtrp0(X1,sz00,xp)
| ~ aInteger0(sz00)
| ~ aInteger0(xp)
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[141,3713,theory(equality)]) ).
cnf(3748,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(X1,sz10,xp)
| ~ sdteqdtlpzmzozddtrp0(X1,sz00,xp)
| $false
| ~ aInteger0(xp)
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[3729,348,theory(equality)]) ).
cnf(3749,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(X1,sz10,xp)
| ~ sdteqdtlpzmzozddtrp0(X1,sz00,xp)
| $false
| $false
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[3748,394,theory(equality)]) ).
cnf(3750,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(X1,sz10,xp)
| ~ sdteqdtlpzmzozddtrp0(X1,sz00,xp)
| $false
| $false
| $false
| ~ aInteger0(X1)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[3749,191,theory(equality)]) ).
cnf(3751,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(X1,sz10,xp)
| ~ sdteqdtlpzmzozddtrp0(X1,sz00,xp)
| ~ aInteger0(X1)
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[3750,theory(equality)]) ).
cnf(3752,plain,
( sdteqdtlpzmzozddtrp0(X1,sz10,xp)
| ~ sdteqdtlpzmzozddtrp0(X1,sz00,xp)
| ~ aInteger0(X1)
| smndt0(sz10) != sz00 ),
inference(sr,[status(thm)],[3751,393,theory(equality)]) ).
cnf(4043,plain,
( aElementOf0(X1,cS2076)
| ~ aInteger0(X1)
| smndt0(sz10) != sz00
| ~ sdteqdtlpzmzozddtrp0(X1,sz00,xp) ),
inference(spm,[status(thm)],[643,3752,theory(equality)]) ).
cnf(4186,plain,
( aElementOf0(smndt0(smndt0(sz10)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| $false
| ~ aInteger0(smndt0(smndt0(sz10)))
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[546,2326,theory(equality)]) ).
cnf(4187,plain,
( aElementOf0(smndt0(smndt0(sz10)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| $false
| ~ aInteger0(smndt0(smndt0(sz10)))
| $false ),
inference(rw,[status(thm)],[4186,2286,theory(equality)]) ).
cnf(4188,plain,
( aElementOf0(smndt0(smndt0(sz10)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(smndt0(smndt0(sz10))) ),
inference(cn,[status(thm)],[4187,theory(equality)]) ).
cnf(4193,plain,
( smndt0(sz10) = smndt0(smndt0(sz10))
| sz10 = smndt0(smndt0(sz10))
| ~ aInteger0(smndt0(smndt0(sz10))) ),
inference(spm,[status(thm)],[296,4188,theory(equality)]) ).
cnf(4311,plain,
( smndt0(smndt0(sz10)) = smndt0(sz10)
| smndt0(smndt0(sz10)) = sz10
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[4193,347,theory(equality)]) ).
cnf(4313,plain,
( smndt0(smndt0(sz10)) = smndt0(sz10)
| smndt0(smndt0(sz10)) = sz10
| $false ),
inference(rw,[status(thm)],[4311,2286,theory(equality)]) ).
cnf(4314,plain,
( smndt0(smndt0(sz10)) = smndt0(sz10)
| smndt0(smndt0(sz10)) = sz10 ),
inference(cn,[status(thm)],[4313,theory(equality)]) ).
cnf(4455,negated_conjecture,
( smndt0(sz10) = X1
| sz10 = X1
| ~ aDivisorOf0(xp,sdtpldt0(smndt0(sz10),X1))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[569,2286,theory(equality)]) ).
cnf(4456,negated_conjecture,
( smndt0(sz10) = X1
| sz10 = X1
| ~ aDivisorOf0(xp,sdtpldt0(smndt0(sz10),X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[4455,theory(equality)]) ).
cnf(6765,plain,
( smndt0(sz10) = sz00
| sz00 = X1
| smndt0(X1) != sz00
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[667,2286,theory(equality)]) ).
cnf(6766,plain,
( smndt0(sz10) = sz00
| sz00 = X1
| smndt0(X1) != sz00
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[6765,theory(equality)]) ).
cnf(6932,plain,
( esk3_2(X1,X2) = sz00
| sz00 = X2
| X1 != sz00
| ~ aDivisorOf0(X2,X1)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(csr,[status(thm)],[671,109]) ).
cnf(6933,plain,
( esk3_2(X1,X2) = sz00
| sz00 = X2
| X1 != sz00
| ~ aDivisorOf0(X2,X1)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[6932,111]) ).
cnf(6934,plain,
( esk3_2(X1,X2) = sz00
| X1 != sz00
| ~ aDivisorOf0(X2,X1)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[6933,110]) ).
cnf(6936,plain,
( sdtasdt0(X1,sz00) = X2
| ~ aDivisorOf0(X1,X2)
| ~ aInteger0(X2)
| X2 != sz00 ),
inference(spm,[status(thm)],[108,6934,theory(equality)]) ).
cnf(6949,plain,
( sdtasdt0(sz10,sz00) = X1
| sz10 = sz00
| X1 != sz00
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[6936,831,theory(equality)]) ).
cnf(6970,plain,
( sdtasdt0(sz10,sz00) = smndt0(sz10)
| sz10 = sz00
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[6949,2286,theory(equality)]) ).
cnf(7073,plain,
( sdtasdt0(xp,smndt0(sz10)) = smndt0(sz10)
| sz10 = sz00
| ~ aInteger0(sz10)
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[2933,6970,theory(equality)]) ).
cnf(7118,plain,
( sdtasdt0(xp,smndt0(sz10)) = smndt0(sz10)
| sz10 = sz00
| $false
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[7073,191,theory(equality)]) ).
cnf(7119,plain,
( sdtasdt0(xp,smndt0(sz10)) = smndt0(sz10)
| sz10 = sz00
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[7118,theory(equality)]) ).
cnf(7178,plain,
( smndt0(sz10) = smndt0(xp)
| sz10 = sz00
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[73,7119,theory(equality)]) ).
cnf(7199,plain,
( smndt0(sz10) = smndt0(xp)
| sz10 = sz00
| $false
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[7178,394,theory(equality)]) ).
cnf(7200,plain,
( smndt0(sz10) = smndt0(xp)
| sz10 = sz00
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[7199,theory(equality)]) ).
cnf(10110,plain,
( sz00 = X1
| aDivisorOf0(X1,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[817,311]) ).
cnf(10117,plain,
( sz00 = X1
| aDivisorOf0(X1,smndt0(X1))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[10110,73,theory(equality)]) ).
cnf(10151,plain,
( sz00 = X1
| aDivisorOf0(X1,smndt0(X1))
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[10117,2286,theory(equality)]) ).
cnf(10152,plain,
( sz00 = X1
| aDivisorOf0(X1,smndt0(X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[10151,theory(equality)]) ).
cnf(11204,plain,
( sdtasdt0(X1,sdtasdt0(X2,sz10)) = sdtasdt0(X1,X2)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[870,311]) ).
cnf(11347,plain,
( sdtasdt0(xp,sz00) = sdtasdt0(sz10,sz00)
| ~ aInteger0(sz10)
| ~ aInteger0(sz00)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[2933,872,theory(equality)]) ).
cnf(11387,plain,
( sz00 = sdtasdt0(sz10,sz00)
| ~ aInteger0(sz10)
| ~ aInteger0(sz00)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[11347,2634,theory(equality)]) ).
cnf(11388,plain,
( sz00 = sdtasdt0(sz10,sz00)
| $false
| ~ aInteger0(sz00)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[11387,191,theory(equality)]) ).
cnf(11389,plain,
( sz00 = sdtasdt0(sz10,sz00)
| $false
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[11388,348,theory(equality)]) ).
cnf(11390,plain,
( sz00 = sdtasdt0(sz10,sz00)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[11389,394,theory(equality)]) ).
cnf(11391,plain,
sz00 = sdtasdt0(sz10,sz00),
inference(cn,[status(thm)],[11390,theory(equality)]) ).
cnf(11511,plain,
( sdtasdt0(sz10,smndt0(X1)) = smndt0(X1)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[874,73,theory(equality)]) ).
cnf(11550,plain,
( sdtasdt0(X1,sz10) = sdtasdt0(sz10,X1)
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[11204,874,theory(equality)]) ).
cnf(11585,plain,
( sdtasdt0(sz10,smndt0(X1)) = smndt0(X1)
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[11511,2286,theory(equality)]) ).
cnf(11586,plain,
( sdtasdt0(sz10,smndt0(X1)) = smndt0(X1)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[11585,theory(equality)]) ).
cnf(11658,plain,
( sdtasdt0(X1,sz10) = sdtasdt0(sz10,X1)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[11550,191,theory(equality)]) ).
cnf(11659,plain,
( sdtasdt0(X1,sz10) = sdtasdt0(sz10,X1)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[11658,theory(equality)]) ).
cnf(11677,plain,
( sdtasdt0(sz10,smndt0(sz10)) = smndt0(sz10)
| smndt0(smndt0(sz10)) = sz10
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[11586,4314,theory(equality)]) ).
cnf(11711,plain,
( sdtasdt0(sz10,smndt0(sz10)) = smndt0(sz10)
| smndt0(smndt0(sz10)) = sz10
| $false ),
inference(rw,[status(thm)],[11677,2286,theory(equality)]) ).
cnf(11712,plain,
( sdtasdt0(sz10,smndt0(sz10)) = smndt0(sz10)
| smndt0(smndt0(sz10)) = sz10 ),
inference(cn,[status(thm)],[11711,theory(equality)]) ).
cnf(12123,plain,
( aInteger0(sdtasdt0(X1,sdtasdt0(X2,X3)))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(X3) ),
inference(csr,[status(thm)],[854,311]) ).
cnf(12289,plain,
( sdtasdt0(sz00,smndt0(X1)) = sdtasdt0(sz00,X1)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[880,74,theory(equality)]) ).
cnf(12359,plain,
( sdtasdt0(sz00,smndt0(X1)) = sdtasdt0(sz00,X1)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[12289,2286,theory(equality)]) ).
cnf(12360,plain,
( sdtasdt0(sz00,smndt0(X1)) = sdtasdt0(sz00,X1)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[12359,theory(equality)]) ).
cnf(12429,plain,
( sdtasdt0(X1,sdtasdt0(X2,smndt0(sz10))) = smndt0(sdtasdt0(X1,X2))
| ~ aInteger0(sdtasdt0(X1,X2))
| $false
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[856,2286,theory(equality)]) ).
cnf(12430,plain,
( sdtasdt0(X1,sdtasdt0(X2,smndt0(sz10))) = smndt0(sdtasdt0(X1,X2))
| ~ aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[12429,theory(equality)]) ).
cnf(12431,plain,
( sdtasdt0(X1,sdtasdt0(X2,smndt0(sz10))) = smndt0(sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[12430,311]) ).
cnf(12463,plain,
( smndt0(sdtasdt0(xp,sz00)) = sdtasdt0(sz00,smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz00)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[2714,12431,theory(equality)]) ).
cnf(12490,plain,
( smndt0(sdtasdt0(sz10,X1)) = sdtasdt0(X1,smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[874,12431,theory(equality)]) ).
cnf(12526,plain,
( sz00 = sdtasdt0(sz00,smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz00)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[12463,2634,theory(equality)]),2152,theory(equality)]) ).
cnf(12527,plain,
( sz00 = sdtasdt0(sz00,smndt0(sz10))
| $false
| ~ aInteger0(sz00)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[12526,2286,theory(equality)]) ).
cnf(12528,plain,
( sz00 = sdtasdt0(sz00,smndt0(sz10))
| $false
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[12527,348,theory(equality)]) ).
cnf(12529,plain,
( sz00 = sdtasdt0(sz00,smndt0(sz10))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[12528,394,theory(equality)]) ).
cnf(12530,plain,
sz00 = sdtasdt0(sz00,smndt0(sz10)),
inference(cn,[status(thm)],[12529,theory(equality)]) ).
cnf(12585,plain,
( smndt0(sdtasdt0(sz10,X1)) = sdtasdt0(X1,smndt0(sz10))
| $false
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[12490,2286,theory(equality)]) ).
cnf(12586,plain,
( smndt0(sdtasdt0(sz10,X1)) = sdtasdt0(X1,smndt0(sz10))
| $false
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[12585,191,theory(equality)]) ).
cnf(12587,plain,
( smndt0(sdtasdt0(sz10,X1)) = sdtasdt0(X1,smndt0(sz10))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[12586,theory(equality)]) ).
cnf(12693,plain,
( sdtasdt0(X1,sdtasdt0(smndt0(sz10),X2)) = sdtasdt0(smndt0(X1),X2)
| ~ aInteger0(X2)
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[857,2286,theory(equality)]) ).
cnf(12694,plain,
( sdtasdt0(X1,sdtasdt0(smndt0(sz10),X2)) = sdtasdt0(smndt0(X1),X2)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[12693,theory(equality)]) ).
cnf(12912,plain,
( sdtasdt0(smndt0(sz10),sdtasdt0(X1,X2)) = sdtasdt0(smndt0(X1),X2)
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[858,2286,theory(equality)]) ).
cnf(12913,plain,
( sdtasdt0(smndt0(sz10),sdtasdt0(X1,X2)) = sdtasdt0(smndt0(X1),X2)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[12912,theory(equality)]) ).
cnf(13202,plain,
( sdtasdt0(X1,sdtasdt0(X2,X3)) = sdtasdt0(X3,sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(X3) ),
inference(csr,[status(thm)],[859,311]) ).
cnf(14097,plain,
( aInteger0(sdtasdt0(X1,smndt0(sz10)))
| smndt0(smndt0(sz10)) = sz10
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[12123,11712,theory(equality)]) ).
cnf(14148,plain,
( aInteger0(sdtasdt0(X1,smndt0(sz10)))
| smndt0(smndt0(sz10)) = sz10
| $false
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[14097,2286,theory(equality)]) ).
cnf(14149,plain,
( aInteger0(sdtasdt0(X1,smndt0(sz10)))
| smndt0(smndt0(sz10)) = sz10
| $false
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[14148,191,theory(equality)]) ).
cnf(14150,plain,
( aInteger0(sdtasdt0(X1,smndt0(sz10)))
| smndt0(smndt0(sz10)) = sz10
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[14149,theory(equality)]) ).
cnf(14184,plain,
( smndt0(smndt0(sz10)) = sz10
| aInteger0(smndt0(smndt0(sz10)))
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[14150,74,theory(equality)]) ).
cnf(14203,plain,
( smndt0(smndt0(sz10)) = sz10
| aInteger0(smndt0(smndt0(sz10)))
| $false ),
inference(rw,[status(thm)],[14184,2286,theory(equality)]) ).
cnf(14204,plain,
( smndt0(smndt0(sz10)) = sz10
| aInteger0(smndt0(smndt0(sz10))) ),
inference(cn,[status(thm)],[14203,theory(equality)]) ).
cnf(14222,plain,
aInteger0(smndt0(smndt0(sz10))),
inference(csr,[status(thm)],[14204,512]) ).
cnf(16866,plain,
( sdtasdt0(sz10,sz10) = sz10
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[57,11659,theory(equality)]) ).
cnf(16872,plain,
( sdtasdt0(sz10,smndt0(sz10)) = smndt0(sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[74,11659,theory(equality)]) ).
cnf(16955,plain,
( sdtasdt0(sz10,sz10) = sz10
| $false ),
inference(rw,[status(thm)],[16866,191,theory(equality)]) ).
cnf(16956,plain,
sdtasdt0(sz10,sz10) = sz10,
inference(cn,[status(thm)],[16955,theory(equality)]) ).
cnf(16967,plain,
( sdtasdt0(sz10,smndt0(sz10)) = smndt0(sz10)
| $false
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[16872,191,theory(equality)]) ).
cnf(16968,plain,
( sdtasdt0(sz10,smndt0(sz10)) = smndt0(sz10)
| $false
| $false ),
inference(rw,[status(thm)],[16967,2286,theory(equality)]) ).
cnf(16969,plain,
sdtasdt0(sz10,smndt0(sz10)) = smndt0(sz10),
inference(cn,[status(thm)],[16968,theory(equality)]) ).
cnf(17146,plain,
( aInteger0(sdtpldt0(X1,sdtpldt0(X2,X3)))
| ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(X3) ),
inference(csr,[status(thm)],[884,102]) ).
cnf(17321,plain,
( sdtpldt0(X1,sdtpldt0(X2,smndt0(sdtpldt0(X1,X2)))) = sz00
| ~ aInteger0(sdtpldt0(X1,X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[885,347]) ).
cnf(17322,plain,
( sdtpldt0(X1,sdtpldt0(X2,smndt0(sdtpldt0(X1,X2)))) = sz00
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[17321,102]) ).
cnf(17331,plain,
( sdtpldt0(X1,sdtpldt0(X2,smndt0(sdtpldt0(X2,X1)))) = sz00
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[17322,99,theory(equality)]) ).
cnf(17748,plain,
( sdtpldt0(X1,sdtpldt0(smndt0(X1),X2)) = sdtpldt0(sz00,X2)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(csr,[status(thm)],[886,347]) ).
cnf(17763,negated_conjecture,
( smndt0(sz10) = sdtpldt0(smndt0(smndt0(sz10)),X1)
| sz10 = sdtpldt0(smndt0(smndt0(sz10)),X1)
| ~ aDivisorOf0(xp,sdtpldt0(sz00,X1))
| ~ aInteger0(sdtpldt0(smndt0(smndt0(sz10)),X1))
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[4456,17748,theory(equality)]) ).
cnf(17806,negated_conjecture,
( smndt0(sz10) = sdtpldt0(smndt0(smndt0(sz10)),X1)
| sz10 = sdtpldt0(smndt0(smndt0(sz10)),X1)
| ~ aDivisorOf0(xp,sdtpldt0(sz00,X1))
| ~ aInteger0(sdtpldt0(smndt0(smndt0(sz10)),X1))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[17763,2286,theory(equality)]) ).
cnf(17807,negated_conjecture,
( smndt0(sz10) = sdtpldt0(smndt0(smndt0(sz10)),X1)
| sz10 = sdtpldt0(smndt0(smndt0(sz10)),X1)
| ~ aDivisorOf0(xp,sdtpldt0(sz00,X1))
| ~ aInteger0(sdtpldt0(smndt0(smndt0(sz10)),X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[17806,theory(equality)]) ).
cnf(17910,plain,
( sdtpldt0(smndt0(X1),sdtpldt0(X1,X2)) = sdtpldt0(sz00,X2)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[887,347]) ).
cnf(20535,plain,
( sz00 = X1
| sdteqdtlpzmzozddtrp0(sz00,X2,X1)
| ~ aDivisorOf0(X1,smndt0(X2))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[923,347]) ).
cnf(20555,plain,
( sz00 = X1
| sdteqdtlpzmzozddtrp0(sz00,X1,X1)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[20535,10152,theory(equality)]) ).
cnf(23594,plain,
( sz00 = X1
| sdteqdtlpzmzozddtrp0(X1,sz00,X1)
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[115,20555,theory(equality)]) ).
cnf(23599,plain,
( sz00 = X1
| sdteqdtlpzmzozddtrp0(X1,sz00,X1)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[23594,348,theory(equality)]) ).
cnf(23600,plain,
( sz00 = X1
| sdteqdtlpzmzozddtrp0(X1,sz00,X1)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[23599,theory(equality)]) ).
cnf(24842,plain,
( aElementOf0(xp,cS2076)
| sz00 = xp
| smndt0(sz10) != sz00
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[4043,23600,theory(equality)]) ).
cnf(24865,plain,
( aElementOf0(xp,cS2076)
| sz00 = xp
| smndt0(sz10) != sz00
| $false ),
inference(rw,[status(thm)],[24842,394,theory(equality)]) ).
cnf(24866,plain,
( aElementOf0(xp,cS2076)
| sz00 = xp
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[24865,theory(equality)]) ).
cnf(24867,plain,
( aElementOf0(xp,cS2076)
| smndt0(sz10) != sz00 ),
inference(sr,[status(thm)],[24866,393,theory(equality)]) ).
cnf(25176,plain,
( smndt0(sz10) = xp
| sz10 = xp
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[679,24867,theory(equality)]) ).
cnf(25534,plain,
( sdtasdt0(sz10,X1) = sdtpldt0(X1,sdtasdt0(sz10,sz00))
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[1011,353,theory(equality)]) ).
cnf(25600,plain,
( sdtasdt0(sz10,X1) = sdtpldt0(X1,sz00)
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[25534,11391,theory(equality)]) ).
cnf(25601,plain,
( sdtasdt0(sz10,X1) = sdtpldt0(X1,sz00)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[25600,348,theory(equality)]) ).
cnf(25602,plain,
( sdtasdt0(sz10,X1) = sdtpldt0(X1,sz00)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[25601,theory(equality)]) ).
cnf(25687,plain,
( sdtpldt0(sz10,sz00) = sz10
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[16956,25602,theory(equality)]) ).
cnf(25688,plain,
( sdtpldt0(smndt0(sz10),sz00) = smndt0(sz10)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[16969,25602,theory(equality)]) ).
cnf(25695,plain,
( sdtpldt0(X1,sz00) = sdtasdt0(X1,sz10)
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[356,25602,theory(equality)]) ).
cnf(25733,plain,
( aInteger0(sdtasdt0(X1,sdtpldt0(X2,sz00)))
| ~ aInteger0(X2)
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[12123,25602,theory(equality)]) ).
cnf(25787,plain,
( sdtpldt0(sz10,sz00) = sz10
| $false ),
inference(rw,[status(thm)],[25687,191,theory(equality)]) ).
cnf(25788,plain,
sdtpldt0(sz10,sz00) = sz10,
inference(cn,[status(thm)],[25787,theory(equality)]) ).
cnf(25789,plain,
( sdtpldt0(smndt0(sz10),sz00) = smndt0(sz10)
| $false ),
inference(rw,[status(thm)],[25688,2286,theory(equality)]) ).
cnf(25790,plain,
sdtpldt0(smndt0(sz10),sz00) = smndt0(sz10),
inference(cn,[status(thm)],[25789,theory(equality)]) ).
cnf(25804,plain,
( sdtpldt0(X1,sz00) = sdtasdt0(X1,sz10)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[25695,191,theory(equality)]) ).
cnf(25805,plain,
( sdtpldt0(X1,sz00) = sdtasdt0(X1,sz10)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[25804,theory(equality)]) ).
cnf(25889,plain,
( aInteger0(sdtasdt0(X1,sdtpldt0(X2,sz00)))
| ~ aInteger0(X2)
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[25733,191,theory(equality)]) ).
cnf(25890,plain,
( aInteger0(sdtasdt0(X1,sdtpldt0(X2,sz00)))
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[25889,theory(equality)]) ).
cnf(26010,plain,
( sz10 = sdtpldt0(sz00,sz10)
| ~ aInteger0(sz00)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[99,25788,theory(equality)]) ).
cnf(26017,plain,
( aInteger0(sdtpldt0(X1,sz10))
| ~ aInteger0(sz00)
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[17146,25788,theory(equality)]) ).
cnf(26020,plain,
( sdtpldt0(smndt0(sz10),sz10) = sdtpldt0(sz00,sz00)
| ~ aInteger0(sz00)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[17910,25788,theory(equality)]) ).
cnf(26034,plain,
( sz10 = sdtpldt0(sz00,sz10)
| $false
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[26010,348,theory(equality)]) ).
cnf(26035,plain,
( sz10 = sdtpldt0(sz00,sz10)
| $false
| $false ),
inference(rw,[status(thm)],[26034,191,theory(equality)]) ).
cnf(26036,plain,
sz10 = sdtpldt0(sz00,sz10),
inference(cn,[status(thm)],[26035,theory(equality)]) ).
cnf(26050,plain,
( aInteger0(sdtpldt0(X1,sz10))
| $false
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[26017,348,theory(equality)]) ).
cnf(26051,plain,
( aInteger0(sdtpldt0(X1,sz10))
| $false
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[26050,191,theory(equality)]) ).
cnf(26052,plain,
( aInteger0(sdtpldt0(X1,sz10))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[26051,theory(equality)]) ).
cnf(26059,plain,
( sdtpldt0(smndt0(sz10),sz10) = sz00
| ~ aInteger0(sz00)
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[26020,2177,theory(equality)]) ).
cnf(26060,plain,
( sdtpldt0(smndt0(sz10),sz10) = sz00
| $false
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[26059,348,theory(equality)]) ).
cnf(26061,plain,
( sdtpldt0(smndt0(sz10),sz10) = sz00
| $false
| $false ),
inference(rw,[status(thm)],[26060,191,theory(equality)]) ).
cnf(26062,plain,
sdtpldt0(smndt0(sz10),sz10) = sz00,
inference(cn,[status(thm)],[26061,theory(equality)]) ).
cnf(26089,plain,
( sdtasdt0(sz10,X1) = sdtpldt0(sdtasdt0(sz10,sz00),X1)
| ~ aInteger0(sz00)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[1013,352,theory(equality)]) ).
cnf(26163,plain,
( sdtasdt0(sz10,X1) = sdtpldt0(sz00,X1)
| ~ aInteger0(sz00)
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[26089,11391,theory(equality)]) ).
cnf(26164,plain,
( sdtasdt0(sz10,X1) = sdtpldt0(sz00,X1)
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[26163,348,theory(equality)]) ).
cnf(26165,plain,
( sdtasdt0(sz10,X1) = sdtpldt0(sz00,X1)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[26164,theory(equality)]) ).
cnf(26250,plain,
( aInteger0(sdtpldt0(sz10,X1))
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[26052,99,theory(equality)]) ).
cnf(26265,plain,
( aInteger0(sdtpldt0(sz10,X1))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[26250,191,theory(equality)]) ).
cnf(26266,plain,
( aInteger0(sdtpldt0(sz10,X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[26265,theory(equality)]) ).
cnf(26836,plain,
( sdtpldt0(smndt0(smndt0(sz10)),sz00) = sdtpldt0(sz00,sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[17910,26062,theory(equality)]) ).
cnf(26902,plain,
( sdtpldt0(smndt0(smndt0(sz10)),sz00) = sz10
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[26836,26036,theory(equality)]) ).
cnf(26903,plain,
( sdtpldt0(smndt0(smndt0(sz10)),sz00) = sz10
| $false
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[26902,191,theory(equality)]) ).
cnf(26904,plain,
( sdtpldt0(smndt0(smndt0(sz10)),sz00) = sz10
| $false
| $false ),
inference(rw,[status(thm)],[26903,2286,theory(equality)]) ).
cnf(26905,plain,
sdtpldt0(smndt0(smndt0(sz10)),sz00) = sz10,
inference(cn,[status(thm)],[26904,theory(equality)]) ).
cnf(27149,plain,
( smndt0(sz10) = sdtpldt0(sz00,smndt0(sz10))
| ~ aInteger0(sz00)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[99,25790,theory(equality)]) ).
cnf(27189,plain,
( smndt0(sz10) = sdtpldt0(sz00,smndt0(sz10))
| $false
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[27149,348,theory(equality)]) ).
cnf(27190,plain,
( smndt0(sz10) = sdtpldt0(sz00,smndt0(sz10))
| $false
| $false ),
inference(rw,[status(thm)],[27189,2286,theory(equality)]) ).
cnf(27191,plain,
smndt0(sz10) = sdtpldt0(sz00,smndt0(sz10)),
inference(cn,[status(thm)],[27190,theory(equality)]) ).
cnf(27685,plain,
( aInteger0(sdtasdt0(X1,sdtpldt0(X2,X3)))
| ~ aInteger0(sdtasdt0(X1,X3))
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3) ),
inference(csr,[status(thm)],[990,311]) ).
cnf(27686,plain,
( aInteger0(sdtasdt0(X1,sdtpldt0(X2,X3)))
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| ~ aInteger0(X3) ),
inference(csr,[status(thm)],[27685,311]) ).
cnf(27727,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(X1,X2)))
| ~ aInteger0(X1)
| ~ aInteger0(sz10)
| ~ aInteger0(X2) ),
inference(spm,[status(thm)],[27686,1007,theory(equality)]) ).
cnf(27730,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz10,X2)))
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(spm,[status(thm)],[27686,1011,theory(equality)]) ).
cnf(27780,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(X1,X2)))
| ~ aInteger0(X1)
| $false
| ~ aInteger0(X2) ),
inference(rw,[status(thm)],[27727,191,theory(equality)]) ).
cnf(27781,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(X1,X2)))
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cn,[status(thm)],[27780,theory(equality)]) ).
cnf(27784,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz10,X2)))
| $false
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(rw,[status(thm)],[27730,191,theory(equality)]) ).
cnf(27785,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz10,X2)))
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cn,[status(thm)],[27784,theory(equality)]) ).
cnf(28099,plain,
( sdtpldt0(smndt0(X1),sdtasdt0(X1,X2)) = sdtasdt0(X1,sdtpldt0(smndt0(sz10),X2))
| ~ aInteger0(X1)
| $false
| ~ aInteger0(X2) ),
inference(rw,[status(thm)],[991,2286,theory(equality)]) ).
cnf(28100,plain,
( sdtpldt0(smndt0(X1),sdtasdt0(X1,X2)) = sdtasdt0(X1,sdtpldt0(smndt0(sz10),X2))
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cn,[status(thm)],[28099,theory(equality)]) ).
cnf(28109,plain,
( sdtpldt0(smndt0(X1),sz00) = sdtasdt0(X1,sdtpldt0(smndt0(sz10),sz00))
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[28100,82,theory(equality)]) ).
cnf(28276,plain,
( sdtpldt0(smndt0(X1),sz00) = sdtasdt0(X1,smndt0(sz10))
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[28109,25790,theory(equality)]) ).
cnf(28277,plain,
( sdtpldt0(smndt0(X1),sz00) = sdtasdt0(X1,smndt0(sz10))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[28276,348,theory(equality)]) ).
cnf(28278,plain,
( sdtpldt0(smndt0(X1),sz00) = sdtasdt0(X1,smndt0(sz10))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[28277,theory(equality)]) ).
cnf(28780,plain,
( sz10 = smndt0(smndt0(sz10))
| ~ aInteger0(smndt0(smndt0(sz10))) ),
inference(spm,[status(thm)],[353,26905,theory(equality)]) ).
cnf(28814,plain,
( sz10 = smndt0(smndt0(sz10))
| $false ),
inference(rw,[status(thm)],[28780,14222,theory(equality)]) ).
cnf(28815,plain,
sz10 = smndt0(smndt0(sz10)),
inference(cn,[status(thm)],[28814,theory(equality)]) ).
cnf(28924,plain,
( smndt0(sz10) = sz00
| sz10 != sz00
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[6766,28815,theory(equality)]) ).
cnf(29076,plain,
( smndt0(sz10) = sz00
| sz10 != sz00
| $false ),
inference(rw,[status(thm)],[28924,2286,theory(equality)]) ).
cnf(29077,plain,
( smndt0(sz10) = sz00
| sz10 != sz00 ),
inference(cn,[status(thm)],[29076,theory(equality)]) ).
cnf(29256,plain,
( sz00 = xp
| xp = sz10
| sz10 != sz00 ),
inference(spm,[status(thm)],[25176,29077,theory(equality)]) ).
cnf(29370,plain,
( xp = sz10
| sz10 != sz00 ),
inference(sr,[status(thm)],[29256,393,theory(equality)]) ).
cnf(29388,plain,
sz10 != sz00,
inference(spm,[status(thm)],[393,29370,theory(equality)]) ).
cnf(31215,plain,
( sdtasdt0(X1,sdtpldt0(smndt0(sz10),sz00)) = sdtasdt0(smndt0(X1),sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[12694,25805,theory(equality)]) ).
cnf(31375,plain,
( sdtasdt0(X1,smndt0(sz10)) = sdtasdt0(smndt0(X1),sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[31215,25790,theory(equality)]) ).
cnf(31376,plain,
( sdtasdt0(X1,smndt0(sz10)) = sdtasdt0(smndt0(X1),sz10)
| $false
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[31375,191,theory(equality)]) ).
cnf(31377,plain,
( sdtasdt0(X1,smndt0(sz10)) = sdtasdt0(smndt0(X1),sz10)
| $false
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[31376,2286,theory(equality)]) ).
cnf(31378,plain,
( sdtasdt0(X1,smndt0(sz10)) = sdtasdt0(smndt0(X1),sz10)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[31377,theory(equality)]) ).
cnf(32199,plain,
( sdtasdt0(X1,sdtpldt0(sz00,smndt0(sz10))) = smndt0(sdtasdt0(X1,sz10))
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[12431,26165,theory(equality)]) ).
cnf(32387,plain,
( sdtasdt0(X1,smndt0(sz10)) = smndt0(sdtasdt0(X1,sz10))
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[32199,27191,theory(equality)]) ).
cnf(32388,plain,
( sdtasdt0(X1,smndt0(sz10)) = smndt0(sdtasdt0(X1,sz10))
| $false
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[32387,191,theory(equality)]) ).
cnf(32389,plain,
( sdtasdt0(X1,smndt0(sz10)) = smndt0(sdtasdt0(X1,sz10))
| $false
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[32388,2286,theory(equality)]) ).
cnf(32390,plain,
( sdtasdt0(X1,smndt0(sz10)) = smndt0(sdtasdt0(X1,sz10))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[32389,theory(equality)]) ).
cnf(34669,plain,
( sdtasdt0(smndt0(sz10),sz10) = sdtpldt0(smndt0(sz10),sdtasdt0(sz00,sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[1048,25790,theory(equality)]) ).
cnf(34780,plain,
( sdtasdt0(smndt0(sz10),sz10) = smndt0(sz10)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[34669,2978,theory(equality)]),25790,theory(equality)]) ).
cnf(34781,plain,
( sdtasdt0(smndt0(sz10),sz10) = smndt0(sz10)
| $false
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[34780,2286,theory(equality)]) ).
cnf(34782,plain,
( sdtasdt0(smndt0(sz10),sz10) = smndt0(sz10)
| $false
| $false ),
inference(rw,[status(thm)],[34781,348,theory(equality)]) ).
cnf(34783,plain,
sdtasdt0(smndt0(sz10),sz10) = smndt0(sz10),
inference(cn,[status(thm)],[34782,theory(equality)]) ).
cnf(34928,plain,
( sdtasdt0(smndt0(sz10),smndt0(sz10)) = sdtasdt0(smndt0(smndt0(sz10)),sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[12913,34783,theory(equality)]) ).
cnf(34946,plain,
( sdtpldt0(smndt0(sz10),smndt0(sz10)) = sdtasdt0(smndt0(sz10),sdtpldt0(sz10,sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[1007,34783,theory(equality)]) ).
cnf(35031,plain,
( sdtasdt0(smndt0(sz10),smndt0(sz10)) = sz10
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[34928,28815,theory(equality)]),16956,theory(equality)]) ).
cnf(35032,plain,
( sdtasdt0(smndt0(sz10),smndt0(sz10)) = sz10
| $false
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[35031,191,theory(equality)]) ).
cnf(35033,plain,
( sdtasdt0(smndt0(sz10),smndt0(sz10)) = sz10
| $false
| $false ),
inference(rw,[status(thm)],[35032,2286,theory(equality)]) ).
cnf(35034,plain,
sdtasdt0(smndt0(sz10),smndt0(sz10)) = sz10,
inference(cn,[status(thm)],[35033,theory(equality)]) ).
cnf(35088,plain,
( sdtpldt0(smndt0(sz10),smndt0(sz10)) = sdtasdt0(smndt0(sz10),sdtpldt0(sz10,sz10))
| $false
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[34946,2286,theory(equality)]) ).
cnf(35089,plain,
( sdtpldt0(smndt0(sz10),smndt0(sz10)) = sdtasdt0(smndt0(sz10),sdtpldt0(sz10,sz10))
| $false
| $false ),
inference(rw,[status(thm)],[35088,191,theory(equality)]) ).
cnf(35090,plain,
sdtpldt0(smndt0(sz10),smndt0(sz10)) = sdtasdt0(smndt0(sz10),sdtpldt0(sz10,sz10)),
inference(cn,[status(thm)],[35089,theory(equality)]) ).
cnf(35199,plain,
( sdtasdt0(X1,sz10) = smndt0(sdtasdt0(X1,smndt0(sz10)))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[12431,35034,theory(equality)]) ).
cnf(35282,plain,
( sdtasdt0(X1,sz10) = smndt0(sdtasdt0(X1,smndt0(sz10)))
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[35199,2286,theory(equality)]) ).
cnf(35283,plain,
( sdtasdt0(X1,sz10) = smndt0(sdtasdt0(X1,smndt0(sz10)))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[35282,theory(equality)]) ).
cnf(38189,plain,
( sdtpldt0(smndt0(X1),sdtasdt0(X2,X1)) = sdtasdt0(sdtpldt0(smndt0(sz10),X2),X1)
| $false
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[1033,2286,theory(equality)]) ).
cnf(38190,plain,
( sdtpldt0(smndt0(X1),sdtasdt0(X2,X1)) = sdtasdt0(sdtpldt0(smndt0(sz10),X2),X1)
| ~ aInteger0(X2)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[38189,theory(equality)]) ).
cnf(44913,plain,
( sdtasdt0(smndt0(sz10),sz10) = sdtasdt0(xp,smndt0(sz10))
| sz10 = sz00
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[31378,7200,theory(equality)]) ).
cnf(45017,plain,
( smndt0(sz10) = sdtasdt0(xp,smndt0(sz10))
| sz10 = sz00
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[44913,34783,theory(equality)]) ).
cnf(45018,plain,
( smndt0(sz10) = sdtasdt0(xp,smndt0(sz10))
| sz10 = sz00
| $false
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[45017,394,theory(equality)]) ).
cnf(45019,plain,
( smndt0(sz10) = sdtasdt0(xp,smndt0(sz10))
| sz10 = sz00
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[45018,theory(equality)]) ).
cnf(45020,plain,
( sdtasdt0(xp,smndt0(sz10)) = smndt0(sz10)
| smndt0(sz10) != sz00 ),
inference(sr,[status(thm)],[45019,29388,theory(equality)]) ).
cnf(45159,plain,
( sdtasdt0(smndt0(sz10),smndt0(sz10)) = sdtasdt0(smndt0(xp),smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[12913,45020,theory(equality)]) ).
cnf(45275,plain,
( sz10 = sdtasdt0(smndt0(xp),smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[45159,35034,theory(equality)]) ).
cnf(45276,plain,
( sz10 = sdtasdt0(smndt0(xp),smndt0(sz10))
| $false
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[45275,2286,theory(equality)]) ).
cnf(45277,plain,
( sz10 = sdtasdt0(smndt0(xp),smndt0(sz10))
| $false
| $false
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[45276,394,theory(equality)]) ).
cnf(45278,plain,
( sz10 = sdtasdt0(smndt0(xp),smndt0(sz10))
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[45277,theory(equality)]) ).
cnf(45662,plain,
( sdtasdt0(sz00,smndt0(sdtasdt0(xp,sz10))) = sdtasdt0(sz00,smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[2761,32390,theory(equality)]) ).
cnf(45673,plain,
( sz00 = X1
| aDivisorOf0(X1,smndt0(sdtasdt0(X1,sz10)))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[10110,32390,theory(equality)]) ).
cnf(45828,plain,
( sdtasdt0(sz00,smndt0(sdtasdt0(xp,sz10))) = sz00
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[45662,12530,theory(equality)]) ).
cnf(45829,plain,
( sdtasdt0(sz00,smndt0(sdtasdt0(xp,sz10))) = sz00
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[45828,2286,theory(equality)]) ).
cnf(45830,plain,
( sdtasdt0(sz00,smndt0(sdtasdt0(xp,sz10))) = sz00
| $false
| $false ),
inference(rw,[status(thm)],[45829,394,theory(equality)]) ).
cnf(45831,plain,
sdtasdt0(sz00,smndt0(sdtasdt0(xp,sz10))) = sz00,
inference(cn,[status(thm)],[45830,theory(equality)]) ).
cnf(45868,plain,
( sz00 = X1
| aDivisorOf0(X1,smndt0(sdtasdt0(X1,sz10)))
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[45673,2286,theory(equality)]) ).
cnf(45869,plain,
( sz00 = X1
| aDivisorOf0(X1,smndt0(sdtasdt0(X1,sz10)))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[45868,theory(equality)]) ).
cnf(53152,plain,
( smndt0(smndt0(X1)) = sdtasdt0(X1,sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[35283,73,theory(equality)]) ).
cnf(53213,plain,
( smndt0(smndt0(sz10)) = sdtasdt0(xp,sz10)
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[35283,45020,theory(equality)]) ).
cnf(53300,plain,
( sz10 = sdtasdt0(xp,sz10)
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[53213,28815,theory(equality)]) ).
cnf(53301,plain,
( sz10 = sdtasdt0(xp,sz10)
| $false
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[53300,394,theory(equality)]) ).
cnf(53302,plain,
( sz10 = sdtasdt0(xp,sz10)
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[53301,theory(equality)]) ).
cnf(53350,plain,
( sdtasdt0(smndt0(sz10),sz10) = sdtasdt0(smndt0(xp),sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[12913,53302,theory(equality)]) ).
cnf(53472,plain,
( smndt0(sz10) = sdtasdt0(smndt0(xp),sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[53350,34783,theory(equality)]) ).
cnf(53473,plain,
( smndt0(sz10) = sdtasdt0(smndt0(xp),sz10)
| $false
| ~ aInteger0(xp)
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[53472,191,theory(equality)]) ).
cnf(53474,plain,
( smndt0(sz10) = sdtasdt0(smndt0(xp),sz10)
| $false
| $false
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[53473,394,theory(equality)]) ).
cnf(53475,plain,
( smndt0(sz10) = sdtasdt0(smndt0(xp),sz10)
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[53474,theory(equality)]) ).
cnf(53928,plain,
( smndt0(smndt0(X1)) = sdtasdt0(sz10,X1)
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[356,53152,theory(equality)]) ).
cnf(53945,plain,
( sdtasdt0(sz00,smndt0(smndt0(xp))) = sdtasdt0(sz00,sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[2761,53152,theory(equality)]) ).
cnf(53960,plain,
( sdtasdt0(sz10,smndt0(smndt0(X1))) = smndt0(smndt0(X1))
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[874,53152,theory(equality)]) ).
cnf(54007,plain,
( smndt0(smndt0(X1)) = sdtpldt0(X1,sz00)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[25805,53152,theory(equality)]) ).
cnf(54083,plain,
( smndt0(smndt0(X1)) = sdtasdt0(sz10,X1)
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[53928,191,theory(equality)]) ).
cnf(54084,plain,
( smndt0(smndt0(X1)) = sdtasdt0(sz10,X1)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[54083,theory(equality)]) ).
cnf(54123,plain,
( sdtasdt0(sz00,smndt0(smndt0(xp))) = sz00
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[53945,2978,theory(equality)]) ).
cnf(54124,plain,
( sdtasdt0(sz00,smndt0(smndt0(xp))) = sz00
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[54123,191,theory(equality)]) ).
cnf(54125,plain,
( sdtasdt0(sz00,smndt0(smndt0(xp))) = sz00
| $false
| $false ),
inference(rw,[status(thm)],[54124,394,theory(equality)]) ).
cnf(54126,plain,
sdtasdt0(sz00,smndt0(smndt0(xp))) = sz00,
inference(cn,[status(thm)],[54125,theory(equality)]) ).
cnf(54169,plain,
( sdtasdt0(sz10,smndt0(smndt0(X1))) = smndt0(smndt0(X1))
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[53960,191,theory(equality)]) ).
cnf(54170,plain,
( sdtasdt0(sz10,smndt0(smndt0(X1))) = smndt0(smndt0(X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[54169,theory(equality)]) ).
cnf(55203,plain,
( smndt0(sz10) = sz00
| sz00 = X1
| sdteqdtlpzmzozddtrp0(X2,X3,X1)
| ~ sdteqdtlpzmzozddtrp0(X2,X3,smndt0(X1))
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[1224,2286,theory(equality)]) ).
cnf(55204,plain,
( smndt0(sz10) = sz00
| sz00 = X1
| sdteqdtlpzmzozddtrp0(X2,X3,X1)
| ~ sdteqdtlpzmzozddtrp0(X2,X3,smndt0(X1))
| ~ aInteger0(X2)
| ~ aInteger0(X3)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[55203,theory(equality)]) ).
cnf(59731,plain,
( sz00 = sz10
| sz00 = smndt0(xp)
| smndt0(sz10) != sz00
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[118,53475,theory(equality)]) ).
cnf(59812,plain,
( sz00 = sz10
| sz00 = smndt0(xp)
| smndt0(sz10) != sz00
| ~ aInteger0(smndt0(xp))
| $false ),
inference(rw,[status(thm)],[59731,191,theory(equality)]) ).
cnf(59813,plain,
( sz00 = sz10
| sz00 = smndt0(xp)
| smndt0(sz10) != sz00
| ~ aInteger0(smndt0(xp)) ),
inference(cn,[status(thm)],[59812,theory(equality)]) ).
cnf(59814,plain,
( smndt0(xp) = sz00
| smndt0(sz10) != sz00
| ~ aInteger0(smndt0(xp)) ),
inference(sr,[status(thm)],[59813,29388,theory(equality)]) ).
cnf(59961,plain,
( smndt0(xp) = sz00
| smndt0(sz10) != sz00
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[59814,347,theory(equality)]) ).
cnf(59965,plain,
( smndt0(xp) = sz00
| smndt0(sz10) != sz00
| $false ),
inference(rw,[status(thm)],[59961,394,theory(equality)]) ).
cnf(59966,plain,
( smndt0(xp) = sz00
| smndt0(sz10) != sz00 ),
inference(cn,[status(thm)],[59965,theory(equality)]) ).
cnf(60020,plain,
( sdtasdt0(sz00,smndt0(sz10)) = sz10
| smndt0(sz10) != sz00 ),
inference(spm,[status(thm)],[45278,59966,theory(equality)]) ).
cnf(60134,plain,
( sz00 = sz10
| smndt0(sz10) != sz00 ),
inference(rw,[status(thm)],[60020,12530,theory(equality)]) ).
cnf(60135,plain,
smndt0(sz10) != sz00,
inference(sr,[status(thm)],[60134,29388,theory(equality)]) ).
cnf(62964,plain,
( sdtpldt0(smndt0(sz10),smndt0(sz10)) = smndt0(sdtpldt0(sz10,sz10))
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(spm,[status(thm)],[74,35090,theory(equality)]) ).
cnf(67682,plain,
( sz00 = smndt0(sz10)
| sz00 = X1
| smndt0(sdtasdt0(sz10,X1)) != sz00
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[118,12587,theory(equality)]) ).
cnf(67804,plain,
( smndt0(smndt0(sdtasdt0(sz10,X1))) = sdtasdt0(X1,sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[35283,12587,theory(equality)]) ).
cnf(67849,plain,
( sz00 = smndt0(sz10)
| sz00 = X1
| smndt0(sdtasdt0(sz10,X1)) != sz00
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[67682,2286,theory(equality)]) ).
cnf(67850,plain,
( sz00 = smndt0(sz10)
| sz00 = X1
| smndt0(sdtasdt0(sz10,X1)) != sz00
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[67849,theory(equality)]) ).
cnf(67851,plain,
( sz00 = X1
| smndt0(sdtasdt0(sz10,X1)) != sz00
| ~ aInteger0(X1) ),
inference(sr,[status(thm)],[67850,60135,theory(equality)]) ).
cnf(69182,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = sdtpldt0(sz00,smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(spm,[status(thm)],[17748,62964,theory(equality)]) ).
cnf(69292,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sz10)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(rw,[status(thm)],[69182,27191,theory(equality)]) ).
cnf(69293,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sz10)
| $false
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(rw,[status(thm)],[69292,2286,theory(equality)]) ).
cnf(69294,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sz10)
| $false
| $false
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(rw,[status(thm)],[69293,191,theory(equality)]) ).
cnf(69295,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sz10)
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(cn,[status(thm)],[69294,theory(equality)]) ).
cnf(70164,plain,
( smndt0(smndt0(smndt0(smndt0(X1)))) = sdtasdt0(X1,sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[67804,54084,theory(equality)]) ).
cnf(72953,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(X1,sz00)))
| ~ aInteger0(sz10)
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[25890,1007,theory(equality)]) ).
cnf(72961,plain,
( aInteger0(sdtpldt0(smndt0(X1),sdtasdt0(X1,sz00)))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[25890,28100,theory(equality)]) ).
cnf(73015,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(X1,sz00)))
| $false
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[72953,191,theory(equality)]) ).
cnf(73016,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(X1,sz00)))
| $false
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[73015,348,theory(equality)]) ).
cnf(73017,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(X1,sz00)))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[73016,theory(equality)]) ).
cnf(73034,plain,
( aInteger0(sdtpldt0(smndt0(X1),sdtasdt0(X1,sz00)))
| $false
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[72961,2286,theory(equality)]) ).
cnf(73035,plain,
( aInteger0(sdtpldt0(smndt0(X1),sdtasdt0(X1,sz00)))
| $false
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[73034,348,theory(equality)]) ).
cnf(73036,plain,
( aInteger0(sdtpldt0(smndt0(X1),sdtasdt0(X1,sz00)))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[73035,theory(equality)]) ).
cnf(73081,plain,
( aInteger0(sdtpldt0(xp,sz00))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[73017,2634,theory(equality)]) ).
cnf(73091,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz00,X1)))
| ~ aInteger0(X1)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[73017,356,theory(equality)]) ).
cnf(73132,plain,
( aInteger0(sdtpldt0(xp,sz00))
| $false ),
inference(rw,[status(thm)],[73081,394,theory(equality)]) ).
cnf(73133,plain,
aInteger0(sdtpldt0(xp,sz00)),
inference(cn,[status(thm)],[73132,theory(equality)]) ).
cnf(73158,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz00,X1)))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[73091,348,theory(equality)]) ).
cnf(73159,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz00,X1)))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[73158,theory(equality)]) ).
cnf(73372,plain,
( aInteger0(smndt0(smndt0(xp)))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[73133,54007,theory(equality)]) ).
cnf(73387,plain,
( aInteger0(smndt0(smndt0(xp)))
| $false ),
inference(rw,[status(thm)],[73372,394,theory(equality)]) ).
cnf(73388,plain,
aInteger0(smndt0(smndt0(xp))),
inference(cn,[status(thm)],[73387,theory(equality)]) ).
cnf(73581,plain,
( aInteger0(sdtpldt0(smndt0(smndt0(xp)),sz00))
| ~ aInteger0(smndt0(smndt0(xp))) ),
inference(spm,[status(thm)],[73159,54126,theory(equality)]) ).
cnf(73662,plain,
( aInteger0(sdtpldt0(smndt0(smndt0(xp)),sz00))
| $false ),
inference(rw,[status(thm)],[73581,73388,theory(equality)]) ).
cnf(73663,plain,
aInteger0(sdtpldt0(smndt0(smndt0(xp)),sz00)),
inference(cn,[status(thm)],[73662,theory(equality)]) ).
cnf(73781,plain,
( aInteger0(smndt0(smndt0(smndt0(smndt0(xp)))))
| ~ aInteger0(smndt0(smndt0(xp))) ),
inference(spm,[status(thm)],[73663,54007,theory(equality)]) ).
cnf(73800,plain,
( aInteger0(smndt0(smndt0(smndt0(smndt0(xp)))))
| $false ),
inference(rw,[status(thm)],[73781,73388,theory(equality)]) ).
cnf(73801,plain,
aInteger0(smndt0(smndt0(smndt0(smndt0(xp))))),
inference(cn,[status(thm)],[73800,theory(equality)]) ).
cnf(73814,plain,
( aInteger0(sdtasdt0(xp,sz10))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[73801,70164,theory(equality)]) ).
cnf(73833,plain,
( aInteger0(sdtasdt0(xp,sz10))
| $false ),
inference(rw,[status(thm)],[73814,394,theory(equality)]) ).
cnf(73834,plain,
aInteger0(sdtasdt0(xp,sz10)),
inference(cn,[status(thm)],[73833,theory(equality)]) ).
cnf(80289,plain,
( sdtpldt0(smndt0(X1),sz00) = smndt0(X1)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[73,28278,theory(equality)]) ).
cnf(83988,plain,
( aInteger0(sdtpldt0(smndt0(xp),sz00))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[73036,2634,theory(equality)]) ).
cnf(84055,plain,
( aInteger0(sdtpldt0(smndt0(xp),sz00))
| $false ),
inference(rw,[status(thm)],[83988,394,theory(equality)]) ).
cnf(84056,plain,
aInteger0(sdtpldt0(smndt0(xp),sz00)),
inference(cn,[status(thm)],[84055,theory(equality)]) ).
cnf(84170,plain,
( aInteger0(smndt0(xp))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[84056,80289,theory(equality)]) ).
cnf(84180,plain,
( aInteger0(smndt0(xp))
| $false ),
inference(rw,[status(thm)],[84170,394,theory(equality)]) ).
cnf(84181,plain,
aInteger0(smndt0(xp)),
inference(cn,[status(thm)],[84180,theory(equality)]) ).
cnf(84433,plain,
( aInteger0(sdtasdt0(sdtpldt0(sz10,sz10),X1))
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[27785,1052,theory(equality)]) ).
cnf(84536,plain,
( aInteger0(sdtasdt0(sdtpldt0(sz10,sz10),X1))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[84433,191,theory(equality)]) ).
cnf(84537,plain,
( aInteger0(sdtasdt0(sdtpldt0(sz10,sz10),X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[84536,theory(equality)]) ).
cnf(84707,plain,
( aInteger0(smndt0(sdtpldt0(sz10,sz10)))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(spm,[status(thm)],[84537,73,theory(equality)]) ).
cnf(84733,plain,
( aInteger0(sdtpldt0(sz10,sdtasdt0(sz10,sz10)))
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[84537,1048,theory(equality)]) ).
cnf(84735,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz10,X1)))
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[84537,1052,theory(equality)]) ).
cnf(84756,plain,
( aInteger0(smndt0(sdtpldt0(sz10,sz10)))
| $false
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(rw,[status(thm)],[84707,2286,theory(equality)]) ).
cnf(84757,plain,
( aInteger0(smndt0(sdtpldt0(sz10,sz10)))
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(cn,[status(thm)],[84756,theory(equality)]) ).
cnf(84771,plain,
( aInteger0(sdtpldt0(sz10,sz10))
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[84733,16956,theory(equality)]) ).
cnf(84772,plain,
( aInteger0(sdtpldt0(sz10,sz10))
| $false ),
inference(rw,[status(thm)],[84771,191,theory(equality)]) ).
cnf(84773,plain,
aInteger0(sdtpldt0(sz10,sz10)),
inference(cn,[status(thm)],[84772,theory(equality)]) ).
cnf(84777,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz10,X1)))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[84735,191,theory(equality)]) ).
cnf(84778,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(sz10,X1)))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[84777,theory(equality)]) ).
cnf(84812,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sz10)
| $false ),
inference(rw,[status(thm)],[69295,84773,theory(equality)]) ).
cnf(84813,plain,
sdtpldt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sz10),
inference(cn,[status(thm)],[84812,theory(equality)]) ).
cnf(84816,plain,
( sdtpldt0(smndt0(sz10),smndt0(sz10)) = smndt0(sdtpldt0(sz10,sz10))
| $false ),
inference(rw,[status(thm)],[62964,84773,theory(equality)]) ).
cnf(84817,plain,
sdtpldt0(smndt0(sz10),smndt0(sz10)) = smndt0(sdtpldt0(sz10,sz10)),
inference(cn,[status(thm)],[84816,theory(equality)]) ).
cnf(85104,plain,
( aInteger0(smndt0(sdtpldt0(sz10,sz10)))
| $false ),
inference(rw,[status(thm)],[84757,84773,theory(equality)]) ).
cnf(85105,plain,
aInteger0(smndt0(sdtpldt0(sz10,sz10))),
inference(cn,[status(thm)],[85104,theory(equality)]) ).
cnf(85127,plain,
( sdtpldt0(sz10,sdtpldt0(smndt0(sdtpldt0(sz10,sz10)),smndt0(smndt0(sz10)))) = sz00
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10)))
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[17322,84813,theory(equality)]) ).
cnf(85185,plain,
( sdtpldt0(sz10,sdtpldt0(smndt0(sdtpldt0(sz10,sz10)),sz10)) = sz00
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10)))
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[85127,28815,theory(equality)]) ).
cnf(85186,plain,
( sdtpldt0(sz10,sdtpldt0(smndt0(sdtpldt0(sz10,sz10)),sz10)) = sz00
| $false
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[85185,85105,theory(equality)]) ).
cnf(85187,plain,
( sdtpldt0(sz10,sdtpldt0(smndt0(sdtpldt0(sz10,sz10)),sz10)) = sz00
| $false
| $false ),
inference(rw,[status(thm)],[85186,191,theory(equality)]) ).
cnf(85188,plain,
sdtpldt0(sz10,sdtpldt0(smndt0(sdtpldt0(sz10,sz10)),sz10)) = sz00,
inference(cn,[status(thm)],[85187,theory(equality)]) ).
cnf(85583,plain,
( sdtasdt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = sdtpldt0(smndt0(sz10),sdtasdt0(sz10,smndt0(sz10)))
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[1011,84817,theory(equality)]) ).
cnf(85741,plain,
( sdtasdt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sdtpldt0(sz10,sz10))
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[85583,16969,theory(equality)]),84817,theory(equality)]) ).
cnf(85742,plain,
( sdtasdt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sdtpldt0(sz10,sz10))
| $false ),
inference(rw,[status(thm)],[85741,2286,theory(equality)]) ).
cnf(85743,plain,
sdtasdt0(sz10,smndt0(sdtpldt0(sz10,sz10))) = smndt0(sdtpldt0(sz10,sz10)),
inference(cn,[status(thm)],[85742,theory(equality)]) ).
cnf(87066,plain,
( aInteger0(sdtpldt0(X1,sdtpldt0(X1,sz00)))
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[84778,25602,theory(equality)]) ).
cnf(94310,plain,
( sz00 = X1
| smndt0(sdtasdt0(X1,sz10)) != sz00
| ~ aInteger0(X1)
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[67851,356,theory(equality)]) ).
cnf(94370,plain,
( sz00 = X1
| smndt0(sdtasdt0(X1,sz10)) != sz00
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[94310,191,theory(equality)]) ).
cnf(94371,plain,
( sz00 = X1
| smndt0(sdtasdt0(X1,sz10)) != sz00
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[94370,theory(equality)]) ).
cnf(101221,plain,
( smndt0(sdtpldt0(sz10,sz10)) = smndt0(smndt0(smndt0(sdtpldt0(sz10,sz10))))
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10))) ),
inference(spm,[status(thm)],[54084,85743,theory(equality)]) ).
cnf(101452,plain,
( smndt0(sdtpldt0(sz10,sz10)) = smndt0(smndt0(smndt0(sdtpldt0(sz10,sz10))))
| $false ),
inference(rw,[status(thm)],[101221,85105,theory(equality)]) ).
cnf(101453,plain,
smndt0(sdtpldt0(sz10,sz10)) = smndt0(smndt0(smndt0(sdtpldt0(sz10,sz10)))),
inference(cn,[status(thm)],[101452,theory(equality)]) ).
cnf(102706,plain,
( smndt0(smndt0(sdtpldt0(sz10,sz10))) = sdtasdt0(sdtpldt0(sz10,sz10),sz10)
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(spm,[status(thm)],[70164,101453,theory(equality)]) ).
cnf(103023,plain,
( smndt0(smndt0(sdtpldt0(sz10,sz10))) = sdtasdt0(sdtpldt0(sz10,sz10),sz10)
| $false ),
inference(rw,[status(thm)],[102706,84773,theory(equality)]) ).
cnf(103024,plain,
smndt0(smndt0(sdtpldt0(sz10,sz10))) = sdtasdt0(sdtpldt0(sz10,sz10),sz10),
inference(cn,[status(thm)],[103023,theory(equality)]) ).
cnf(104605,plain,
( smndt0(smndt0(sdtpldt0(sz10,sz10))) = sdtpldt0(sz10,sz10)
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(spm,[status(thm)],[57,103024,theory(equality)]) ).
cnf(104706,plain,
( smndt0(smndt0(sdtpldt0(sz10,sz10))) = sdtpldt0(sz10,sz10)
| $false ),
inference(rw,[status(thm)],[104605,84773,theory(equality)]) ).
cnf(104707,plain,
smndt0(smndt0(sdtpldt0(sz10,sz10))) = sdtpldt0(sz10,sz10),
inference(cn,[status(thm)],[104706,theory(equality)]) ).
cnf(120662,plain,
( sdtasdt0(sz00,sdtasdt0(xp,sz10)) = sz00
| ~ aInteger0(sdtasdt0(xp,sz10)) ),
inference(spm,[status(thm)],[45831,12360,theory(equality)]) ).
cnf(120802,plain,
( sdtasdt0(sz00,sdtasdt0(xp,sz10)) = sz00
| $false ),
inference(rw,[status(thm)],[120662,73834,theory(equality)]) ).
cnf(120803,plain,
sdtasdt0(sz00,sdtasdt0(xp,sz10)) = sz00,
inference(cn,[status(thm)],[120802,theory(equality)]) ).
cnf(121115,plain,
( sdtpldt0(sdtasdt0(xp,sz10),sz00) = sdtasdt0(sdtpldt0(sz10,sz00),sdtasdt0(xp,sz10))
| ~ aInteger0(sz00)
| ~ aInteger0(sdtasdt0(xp,sz10)) ),
inference(spm,[status(thm)],[1052,120803,theory(equality)]) ).
cnf(121358,plain,
( sdtpldt0(sdtasdt0(xp,sz10),sz00) = sdtasdt0(sz10,sdtasdt0(xp,sz10))
| ~ aInteger0(sz00)
| ~ aInteger0(sdtasdt0(xp,sz10)) ),
inference(rw,[status(thm)],[121115,25788,theory(equality)]) ).
cnf(121359,plain,
( sdtpldt0(sdtasdt0(xp,sz10),sz00) = sdtasdt0(sz10,sdtasdt0(xp,sz10))
| $false
| ~ aInteger0(sdtasdt0(xp,sz10)) ),
inference(rw,[status(thm)],[121358,348,theory(equality)]) ).
cnf(121360,plain,
( sdtpldt0(sdtasdt0(xp,sz10),sz00) = sdtasdt0(sz10,sdtasdt0(xp,sz10))
| $false
| $false ),
inference(rw,[status(thm)],[121359,73834,theory(equality)]) ).
cnf(121361,plain,
sdtpldt0(sdtasdt0(xp,sz10),sz00) = sdtasdt0(sz10,sdtasdt0(xp,sz10)),
inference(cn,[status(thm)],[121360,theory(equality)]) ).
cnf(123621,plain,
( sdtasdt0(sz10,xp) = sdtpldt0(xp,sz00)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[121361,57,theory(equality)]) ).
cnf(123735,plain,
( sdtasdt0(sz10,xp) = sdtpldt0(xp,sz00)
| $false ),
inference(rw,[status(thm)],[123621,394,theory(equality)]) ).
cnf(123736,plain,
sdtasdt0(sz10,xp) = sdtpldt0(xp,sz00),
inference(cn,[status(thm)],[123735,theory(equality)]) ).
cnf(124052,plain,
( sdtpldt0(xp,sz00) = xp
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[56,123736,theory(equality)]) ).
cnf(124192,plain,
( sdtpldt0(xp,sz00) = xp
| $false ),
inference(rw,[status(thm)],[124052,394,theory(equality)]) ).
cnf(124193,plain,
sdtpldt0(xp,sz00) = xp,
inference(cn,[status(thm)],[124192,theory(equality)]) ).
cnf(124482,plain,
( sdtasdt0(xp,sz10) = sdtpldt0(xp,sdtasdt0(sz00,sz10))
| ~ aInteger0(xp)
| ~ aInteger0(sz00) ),
inference(spm,[status(thm)],[1048,124193,theory(equality)]) ).
cnf(124494,plain,
( xp = smndt0(smndt0(xp))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[54007,124193,theory(equality)]) ).
cnf(124505,plain,
( aInteger0(sdtpldt0(xp,xp))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[87066,124193,theory(equality)]) ).
cnf(124640,plain,
( sdtasdt0(xp,sz10) = xp
| ~ aInteger0(xp)
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[124482,2978,theory(equality)]),124193,theory(equality)]) ).
cnf(124641,plain,
( sdtasdt0(xp,sz10) = xp
| $false
| ~ aInteger0(sz00) ),
inference(rw,[status(thm)],[124640,394,theory(equality)]) ).
cnf(124642,plain,
( sdtasdt0(xp,sz10) = xp
| $false
| $false ),
inference(rw,[status(thm)],[124641,348,theory(equality)]) ).
cnf(124643,plain,
sdtasdt0(xp,sz10) = xp,
inference(cn,[status(thm)],[124642,theory(equality)]) ).
cnf(124677,plain,
( xp = smndt0(smndt0(xp))
| $false ),
inference(rw,[status(thm)],[124494,394,theory(equality)]) ).
cnf(124678,plain,
xp = smndt0(smndt0(xp)),
inference(cn,[status(thm)],[124677,theory(equality)]) ).
cnf(124704,plain,
( aInteger0(sdtpldt0(xp,xp))
| $false ),
inference(rw,[status(thm)],[124505,394,theory(equality)]) ).
cnf(124705,plain,
aInteger0(sdtpldt0(xp,xp)),
inference(cn,[status(thm)],[124704,theory(equality)]) ).
cnf(124935,plain,
( sdtasdt0(xp,X1) = sdtasdt0(xp,sdtasdt0(sz10,X1))
| ~ aInteger0(X1)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[305,124643,theory(equality)]) ).
cnf(125012,plain,
( sz00 = xp
| aDivisorOf0(xp,smndt0(xp))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[45869,124643,theory(equality)]) ).
cnf(125014,plain,
( sz00 = xp
| smndt0(xp) != sz00
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[94371,124643,theory(equality)]) ).
cnf(125079,plain,
( sdtasdt0(xp,X1) = sdtasdt0(xp,sdtasdt0(sz10,X1))
| ~ aInteger0(X1)
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[124935,191,theory(equality)]) ).
cnf(125080,plain,
( sdtasdt0(xp,X1) = sdtasdt0(xp,sdtasdt0(sz10,X1))
| ~ aInteger0(X1)
| $false
| $false ),
inference(rw,[status(thm)],[125079,394,theory(equality)]) ).
cnf(125081,plain,
( sdtasdt0(xp,X1) = sdtasdt0(xp,sdtasdt0(sz10,X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[125080,theory(equality)]) ).
cnf(125315,plain,
( sz00 = xp
| aDivisorOf0(xp,smndt0(xp))
| $false ),
inference(rw,[status(thm)],[125012,394,theory(equality)]) ).
cnf(125316,plain,
( sz00 = xp
| aDivisorOf0(xp,smndt0(xp)) ),
inference(cn,[status(thm)],[125315,theory(equality)]) ).
cnf(125317,plain,
aDivisorOf0(xp,smndt0(xp)),
inference(sr,[status(thm)],[125316,393,theory(equality)]) ).
cnf(125320,plain,
( sz00 = xp
| smndt0(xp) != sz00
| $false ),
inference(rw,[status(thm)],[125014,394,theory(equality)]) ).
cnf(125321,plain,
( sz00 = xp
| smndt0(xp) != sz00 ),
inference(cn,[status(thm)],[125320,theory(equality)]) ).
cnf(125322,plain,
smndt0(xp) != sz00,
inference(sr,[status(thm)],[125321,393,theory(equality)]) ).
cnf(125518,plain,
( sdtasdt0(xp,sz10) = sdtasdt0(smndt0(xp),smndt0(sz10))
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[31378,124678,theory(equality)]) ).
cnf(125557,plain,
( sdtasdt0(sz10,smndt0(xp)) = smndt0(xp)
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[54170,124678,theory(equality)]) ).
cnf(125571,plain,
( smndt0(smndt0(smndt0(xp))) = sdtasdt0(smndt0(xp),sz10)
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[70164,124678,theory(equality)]) ).
cnf(125794,plain,
( xp = sdtasdt0(smndt0(xp),smndt0(sz10))
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[125518,124643,theory(equality)]) ).
cnf(125795,plain,
( xp = sdtasdt0(smndt0(xp),smndt0(sz10))
| $false ),
inference(rw,[status(thm)],[125794,84181,theory(equality)]) ).
cnf(125796,plain,
xp = sdtasdt0(smndt0(xp),smndt0(sz10)),
inference(cn,[status(thm)],[125795,theory(equality)]) ).
cnf(125897,plain,
( sdtasdt0(sz10,smndt0(xp)) = smndt0(xp)
| $false ),
inference(rw,[status(thm)],[125557,84181,theory(equality)]) ).
cnf(125898,plain,
sdtasdt0(sz10,smndt0(xp)) = smndt0(xp),
inference(cn,[status(thm)],[125897,theory(equality)]) ).
cnf(125934,plain,
( smndt0(xp) = sdtasdt0(smndt0(xp),sz10)
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[125571,124678,theory(equality)]) ).
cnf(125935,plain,
( smndt0(xp) = sdtasdt0(smndt0(xp),sz10)
| $false ),
inference(rw,[status(thm)],[125934,84181,theory(equality)]) ).
cnf(125936,plain,
smndt0(xp) = sdtasdt0(smndt0(xp),sz10),
inference(cn,[status(thm)],[125935,theory(equality)]) ).
cnf(127613,plain,
( smndt0(xp) = sdtpldt0(sz00,smndt0(xp))
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[26165,125898,theory(equality)]) ).
cnf(127620,plain,
( sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(sdtpldt0(sz10,sz10),smndt0(xp))
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[1052,125898,theory(equality)]) ).
cnf(127792,plain,
( smndt0(xp) = sdtpldt0(sz00,smndt0(xp))
| $false ),
inference(rw,[status(thm)],[127613,84181,theory(equality)]) ).
cnf(127793,plain,
smndt0(xp) = sdtpldt0(sz00,smndt0(xp)),
inference(cn,[status(thm)],[127792,theory(equality)]) ).
cnf(127812,plain,
( sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(sdtpldt0(sz10,sz10),smndt0(xp))
| $false
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[127620,191,theory(equality)]) ).
cnf(127813,plain,
( sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(sdtpldt0(sz10,sz10),smndt0(xp))
| $false
| $false ),
inference(rw,[status(thm)],[127812,84181,theory(equality)]) ).
cnf(127814,plain,
sdtpldt0(smndt0(xp),smndt0(xp)) = sdtasdt0(sdtpldt0(sz10,sz10),smndt0(xp)),
inference(cn,[status(thm)],[127813,theory(equality)]) ).
cnf(127967,plain,
( sdtasdt0(smndt0(sz10),smndt0(xp)) = sdtasdt0(smndt0(smndt0(xp)),sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[12913,125936,theory(equality)]) ).
cnf(128014,plain,
( smndt0(xp) = sdtasdt0(xp,smndt0(sz10))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[31378,125936,theory(equality)]) ).
cnf(128117,plain,
( sdtasdt0(smndt0(sz10),smndt0(xp)) = xp
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[127967,124678,theory(equality)]),124643,theory(equality)]) ).
cnf(128118,plain,
( sdtasdt0(smndt0(sz10),smndt0(xp)) = xp
| $false
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[128117,191,theory(equality)]) ).
cnf(128119,plain,
( sdtasdt0(smndt0(sz10),smndt0(xp)) = xp
| $false
| $false ),
inference(rw,[status(thm)],[128118,84181,theory(equality)]) ).
cnf(128120,plain,
sdtasdt0(smndt0(sz10),smndt0(xp)) = xp,
inference(cn,[status(thm)],[128119,theory(equality)]) ).
cnf(128262,plain,
( smndt0(xp) = sdtasdt0(xp,smndt0(sz10))
| $false ),
inference(rw,[status(thm)],[128014,394,theory(equality)]) ).
cnf(128263,plain,
smndt0(xp) = sdtasdt0(xp,smndt0(sz10)),
inference(cn,[status(thm)],[128262,theory(equality)]) ).
cnf(128764,plain,
( sdtasdt0(X1,smndt0(xp)) = smndt0(sdtasdt0(X1,xp))
| ~ aInteger0(xp)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[12431,128263,theory(equality)]) ).
cnf(128791,plain,
( sdtpldt0(smndt0(sz10),smndt0(xp)) = sdtasdt0(sdtpldt0(sz10,xp),smndt0(sz10))
| ~ aInteger0(xp)
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[1052,128263,theory(equality)]) ).
cnf(128908,plain,
( sdtasdt0(X1,smndt0(xp)) = smndt0(sdtasdt0(X1,xp))
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[128764,394,theory(equality)]) ).
cnf(128909,plain,
( sdtasdt0(X1,smndt0(xp)) = smndt0(sdtasdt0(X1,xp))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[128908,theory(equality)]) ).
cnf(128989,plain,
( sdtpldt0(smndt0(sz10),smndt0(xp)) = sdtasdt0(sdtpldt0(sz10,xp),smndt0(sz10))
| $false
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[128791,394,theory(equality)]) ).
cnf(128990,plain,
( sdtpldt0(smndt0(sz10),smndt0(xp)) = sdtasdt0(sdtpldt0(sz10,xp),smndt0(sz10))
| $false
| $false ),
inference(rw,[status(thm)],[128989,2286,theory(equality)]) ).
cnf(128991,plain,
sdtpldt0(smndt0(sz10),smndt0(xp)) = sdtasdt0(sdtpldt0(sz10,xp),smndt0(sz10)),
inference(cn,[status(thm)],[128990,theory(equality)]) ).
cnf(129135,plain,
( sdtasdt0(X1,xp) = smndt0(sdtasdt0(X1,smndt0(xp)))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[12431,125796,theory(equality)]) ).
cnf(129136,plain,
( sdtasdt0(smndt0(sz10),xp) = sdtasdt0(smndt0(smndt0(xp)),smndt0(sz10))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[12913,125796,theory(equality)]) ).
cnf(129151,plain,
( sdtpldt0(smndt0(smndt0(xp)),xp) = sdtasdt0(smndt0(xp),sdtpldt0(smndt0(sz10),smndt0(sz10)))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(smndt0(sz10)) ),
inference(spm,[status(thm)],[28100,125796,theory(equality)]) ).
cnf(129277,plain,
( sdtasdt0(X1,xp) = smndt0(sdtasdt0(X1,smndt0(xp)))
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[129135,84181,theory(equality)]) ).
cnf(129278,plain,
( sdtasdt0(X1,xp) = smndt0(sdtasdt0(X1,smndt0(xp)))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[129277,theory(equality)]) ).
cnf(129279,plain,
( sdtasdt0(smndt0(sz10),xp) = smndt0(xp)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[129136,124678,theory(equality)]),128263,theory(equality)]) ).
cnf(129280,plain,
( sdtasdt0(smndt0(sz10),xp) = smndt0(xp)
| $false
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[129279,2286,theory(equality)]) ).
cnf(129281,plain,
( sdtasdt0(smndt0(sz10),xp) = smndt0(xp)
| $false
| $false ),
inference(rw,[status(thm)],[129280,84181,theory(equality)]) ).
cnf(129282,plain,
sdtasdt0(smndt0(sz10),xp) = smndt0(xp),
inference(cn,[status(thm)],[129281,theory(equality)]) ).
cnf(129334,plain,
( sdtpldt0(xp,xp) = sdtasdt0(smndt0(xp),sdtpldt0(smndt0(sz10),smndt0(sz10)))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[129151,124678,theory(equality)]) ).
cnf(129335,plain,
( sdtpldt0(xp,xp) = sdtasdt0(smndt0(xp),smndt0(sdtpldt0(sz10,sz10)))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[129334,84817,theory(equality)]) ).
cnf(129336,plain,
( sdtpldt0(xp,xp) = sdtasdt0(smndt0(xp),smndt0(sdtpldt0(sz10,sz10)))
| $false
| ~ aInteger0(smndt0(sz10)) ),
inference(rw,[status(thm)],[129335,84181,theory(equality)]) ).
cnf(129337,plain,
( sdtpldt0(xp,xp) = sdtasdt0(smndt0(xp),smndt0(sdtpldt0(sz10,sz10)))
| $false
| $false ),
inference(rw,[status(thm)],[129336,2286,theory(equality)]) ).
cnf(129338,plain,
sdtpldt0(xp,xp) = sdtasdt0(smndt0(xp),smndt0(sdtpldt0(sz10,sz10))),
inference(cn,[status(thm)],[129337,theory(equality)]) ).
cnf(129540,plain,
( sdtasdt0(X1,smndt0(xp)) = sdtasdt0(smndt0(X1),xp)
| ~ aInteger0(xp)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[12694,129282,theory(equality)]) ).
cnf(129682,plain,
( sdtasdt0(X1,smndt0(xp)) = sdtasdt0(smndt0(X1),xp)
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[129540,394,theory(equality)]) ).
cnf(129683,plain,
( sdtasdt0(X1,smndt0(xp)) = sdtasdt0(smndt0(X1),xp)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[129682,theory(equality)]) ).
cnf(129923,plain,
( sdtpldt0(smndt0(smndt0(xp)),xp) = sdtasdt0(sdtpldt0(smndt0(sz10),smndt0(sz10)),smndt0(xp))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[38190,128120,theory(equality)]) ).
cnf(130137,plain,
( sdtpldt0(xp,xp) = sdtasdt0(sdtpldt0(smndt0(sz10),smndt0(sz10)),smndt0(xp))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[129923,124678,theory(equality)]) ).
cnf(130138,plain,
( sdtpldt0(xp,xp) = sdtasdt0(smndt0(sdtpldt0(sz10,sz10)),smndt0(xp))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[130137,84817,theory(equality)]) ).
cnf(130139,plain,
( sdtpldt0(xp,xp) = sdtasdt0(smndt0(sdtpldt0(sz10,sz10)),smndt0(xp))
| $false
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[130138,2286,theory(equality)]) ).
cnf(130140,plain,
( sdtpldt0(xp,xp) = sdtasdt0(smndt0(sdtpldt0(sz10,sz10)),smndt0(xp))
| $false
| $false ),
inference(rw,[status(thm)],[130139,84181,theory(equality)]) ).
cnf(130141,plain,
sdtpldt0(xp,xp) = sdtasdt0(smndt0(sdtpldt0(sz10,sz10)),smndt0(xp)),
inference(cn,[status(thm)],[130140,theory(equality)]) ).
cnf(138711,plain,
( aInteger0(smndt0(sdtasdt0(sdtpldt0(sz10,sz10),xp)))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(spm,[status(thm)],[84537,128909,theory(equality)]) ).
cnf(139196,plain,
( aInteger0(smndt0(sdtasdt0(sdtpldt0(sz10,sz10),xp)))
| $false
| ~ aInteger0(sdtpldt0(sz10,sz10)) ),
inference(rw,[status(thm)],[138711,84181,theory(equality)]) ).
cnf(139197,plain,
( aInteger0(smndt0(sdtasdt0(sdtpldt0(sz10,sz10),xp)))
| $false
| $false ),
inference(rw,[status(thm)],[139196,84773,theory(equality)]) ).
cnf(139198,plain,
aInteger0(smndt0(sdtasdt0(sdtpldt0(sz10,sz10),xp))),
inference(cn,[status(thm)],[139197,theory(equality)]) ).
cnf(139528,plain,
( aInteger0(smndt0(sdtpldt0(xp,sdtasdt0(sz10,xp))))
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[139198,1052,theory(equality)]) ).
cnf(139548,plain,
( aInteger0(smndt0(sdtpldt0(xp,xp)))
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[139528,123736,theory(equality)]),124193,theory(equality)]) ).
cnf(139549,plain,
( aInteger0(smndt0(sdtpldt0(xp,xp)))
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[139548,191,theory(equality)]) ).
cnf(139550,plain,
( aInteger0(smndt0(sdtpldt0(xp,xp)))
| $false
| $false ),
inference(rw,[status(thm)],[139549,394,theory(equality)]) ).
cnf(139551,plain,
aInteger0(smndt0(sdtpldt0(xp,xp))),
inference(cn,[status(thm)],[139550,theory(equality)]) ).
cnf(140471,plain,
( sdtasdt0(xp,xp) = sdtasdt0(smndt0(xp),smndt0(xp))
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[129683,124678,theory(equality)]) ).
cnf(140597,plain,
( sdtasdt0(xp,xp) = sdtasdt0(smndt0(xp),smndt0(xp))
| $false ),
inference(rw,[status(thm)],[140471,84181,theory(equality)]) ).
cnf(140598,plain,
sdtasdt0(xp,xp) = sdtasdt0(smndt0(xp),smndt0(xp)),
inference(cn,[status(thm)],[140597,theory(equality)]) ).
cnf(140996,plain,
( sz00 = smndt0(xp)
| sdtasdt0(xp,xp) != sz00
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[118,140598,theory(equality)]) ).
cnf(141075,plain,
( sz00 = smndt0(xp)
| sdtasdt0(xp,xp) != sz00
| $false ),
inference(rw,[status(thm)],[140996,84181,theory(equality)]) ).
cnf(141076,plain,
( sz00 = smndt0(xp)
| sdtasdt0(xp,xp) != sz00 ),
inference(cn,[status(thm)],[141075,theory(equality)]) ).
cnf(141077,plain,
sdtasdt0(xp,xp) != sz00,
inference(sr,[status(thm)],[141076,125322,theory(equality)]) ).
cnf(172877,plain,
( sdtasdt0(sz10,sdtpldt0(xp,xp)) = sdtpldt0(xp,xp)
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10)))
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[874,129338,theory(equality)]) ).
cnf(173002,plain,
( sdtasdt0(sz10,sdtpldt0(xp,xp)) = sdtpldt0(xp,xp)
| $false
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[172877,85105,theory(equality)]) ).
cnf(173003,plain,
( sdtasdt0(sz10,sdtpldt0(xp,xp)) = sdtpldt0(xp,xp)
| $false
| $false ),
inference(rw,[status(thm)],[173002,84181,theory(equality)]) ).
cnf(173004,plain,
sdtasdt0(sz10,sdtpldt0(xp,xp)) = sdtpldt0(xp,xp),
inference(cn,[status(thm)],[173003,theory(equality)]) ).
cnf(174193,plain,
( sdtpldt0(xp,xp) = smndt0(smndt0(sdtpldt0(xp,xp)))
| ~ aInteger0(sdtpldt0(xp,xp)) ),
inference(spm,[status(thm)],[54084,173004,theory(equality)]) ).
cnf(174434,plain,
( sdtpldt0(xp,xp) = smndt0(smndt0(sdtpldt0(xp,xp)))
| $false ),
inference(rw,[status(thm)],[174193,124705,theory(equality)]) ).
cnf(174435,plain,
sdtpldt0(xp,xp) = smndt0(smndt0(sdtpldt0(xp,xp))),
inference(cn,[status(thm)],[174434,theory(equality)]) ).
cnf(175345,plain,
( smndt0(smndt0(smndt0(sdtpldt0(xp,xp)))) = sdtasdt0(smndt0(sdtpldt0(xp,xp)),sz10)
| ~ aInteger0(smndt0(sdtpldt0(xp,xp))) ),
inference(spm,[status(thm)],[70164,174435,theory(equality)]) ).
cnf(175659,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sdtpldt0(xp,xp)),sz10)
| ~ aInteger0(smndt0(sdtpldt0(xp,xp))) ),
inference(rw,[status(thm)],[175345,174435,theory(equality)]) ).
cnf(175660,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sdtpldt0(xp,xp)),sz10)
| $false ),
inference(rw,[status(thm)],[175659,139551,theory(equality)]) ).
cnf(175661,plain,
smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sdtpldt0(xp,xp)),sz10),
inference(cn,[status(thm)],[175660,theory(equality)]) ).
cnf(205588,plain,
( sdtasdt0(xp,X1) = sdtasdt0(X1,sdtasdt0(xp,sz10))
| ~ aInteger0(X1)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[13202,125081,theory(equality)]) ).
cnf(205794,plain,
( sdtasdt0(xp,X1) = sdtasdt0(X1,xp)
| ~ aInteger0(X1)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[205588,124643,theory(equality)]) ).
cnf(205795,plain,
( sdtasdt0(xp,X1) = sdtasdt0(X1,xp)
| ~ aInteger0(X1)
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[205794,191,theory(equality)]) ).
cnf(205796,plain,
( sdtasdt0(xp,X1) = sdtasdt0(X1,xp)
| ~ aInteger0(X1)
| $false
| $false ),
inference(rw,[status(thm)],[205795,394,theory(equality)]) ).
cnf(205797,plain,
( sdtasdt0(xp,X1) = sdtasdt0(X1,xp)
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[205796,theory(equality)]) ).
cnf(220378,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(sdtpldt0(xp,xp),smndt0(sz10))
| ~ aInteger0(sdtpldt0(xp,xp)) ),
inference(spm,[status(thm)],[31378,175661,theory(equality)]) ).
cnf(220636,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(sdtpldt0(xp,xp),smndt0(sz10))
| $false ),
inference(rw,[status(thm)],[220378,124705,theory(equality)]) ).
cnf(220637,plain,
smndt0(sdtpldt0(xp,xp)) = sdtasdt0(sdtpldt0(xp,xp),smndt0(sz10)),
inference(cn,[status(thm)],[220636,theory(equality)]) ).
cnf(229667,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sz10),sdtpldt0(xp,xp))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sdtpldt0(xp,xp)) ),
inference(spm,[status(thm)],[356,220637,theory(equality)]) ).
cnf(229768,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sz10),sdtpldt0(xp,xp))
| $false
| ~ aInteger0(sdtpldt0(xp,xp)) ),
inference(rw,[status(thm)],[229667,2286,theory(equality)]) ).
cnf(229769,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sz10),sdtpldt0(xp,xp))
| $false
| $false ),
inference(rw,[status(thm)],[229768,124705,theory(equality)]) ).
cnf(229770,plain,
smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sz10),sdtpldt0(xp,xp)),
inference(cn,[status(thm)],[229769,theory(equality)]) ).
cnf(238829,plain,
( sdtasdt0(smndt0(sz10),sdtpldt0(xp,xp)) = sdtasdt0(smndt0(smndt0(sdtpldt0(sz10,sz10))),smndt0(xp))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10))) ),
inference(spm,[status(thm)],[12913,130141,theory(equality)]) ).
cnf(238902,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sdtpldt0(sz10,sz10)),xp)
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10))) ),
inference(spm,[status(thm)],[129278,130141,theory(equality)]) ).
cnf(238974,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(smndt0(sdtpldt0(sz10,sz10))),smndt0(xp))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10))) ),
inference(rw,[status(thm)],[238829,229770,theory(equality)]) ).
cnf(238975,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(sdtpldt0(sz10,sz10),smndt0(xp))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10))) ),
inference(rw,[status(thm)],[238974,104707,theory(equality)]) ).
cnf(238976,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(sdtpldt0(sz10,sz10),smndt0(xp))
| $false
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10))) ),
inference(rw,[status(thm)],[238975,84181,theory(equality)]) ).
cnf(238977,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(sdtpldt0(sz10,sz10),smndt0(xp))
| $false
| $false ),
inference(rw,[status(thm)],[238976,85105,theory(equality)]) ).
cnf(238978,plain,
smndt0(sdtpldt0(xp,xp)) = sdtasdt0(sdtpldt0(sz10,sz10),smndt0(xp)),
inference(cn,[status(thm)],[238977,theory(equality)]) ).
cnf(239192,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sdtpldt0(sz10,sz10)),xp)
| $false ),
inference(rw,[status(thm)],[238902,85105,theory(equality)]) ).
cnf(239193,plain,
smndt0(sdtpldt0(xp,xp)) = sdtasdt0(smndt0(sdtpldt0(sz10,sz10)),xp),
inference(cn,[status(thm)],[239192,theory(equality)]) ).
cnf(253536,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(xp,smndt0(sdtpldt0(sz10,sz10)))
| ~ aInteger0(xp)
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10))) ),
inference(spm,[status(thm)],[356,239193,theory(equality)]) ).
cnf(253662,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(xp,smndt0(sdtpldt0(sz10,sz10)))
| $false
| ~ aInteger0(smndt0(sdtpldt0(sz10,sz10))) ),
inference(rw,[status(thm)],[253536,394,theory(equality)]) ).
cnf(253663,plain,
( smndt0(sdtpldt0(xp,xp)) = sdtasdt0(xp,smndt0(sdtpldt0(sz10,sz10)))
| $false
| $false ),
inference(rw,[status(thm)],[253662,85105,theory(equality)]) ).
cnf(253664,plain,
smndt0(sdtpldt0(xp,xp)) = sdtasdt0(xp,smndt0(sdtpldt0(sz10,sz10))),
inference(cn,[status(thm)],[253663,theory(equality)]) ).
cnf(268554,plain,
( aInteger0(sdtpldt0(sz10,smndt0(smndt0(X1))))
| ~ aInteger0(sz10)
| ~ aInteger0(X1) ),
inference(spm,[status(thm)],[27781,54084,theory(equality)]) ).
cnf(268644,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(xp,X1)))
| ~ aInteger0(X1)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[27781,205797,theory(equality)]) ).
cnf(269019,plain,
( aInteger0(sdtpldt0(sz10,smndt0(smndt0(X1))))
| $false
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[268554,191,theory(equality)]) ).
cnf(269020,plain,
( aInteger0(sdtpldt0(sz10,smndt0(smndt0(X1))))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[269019,theory(equality)]) ).
cnf(269160,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(xp,X1)))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[268644,394,theory(equality)]) ).
cnf(269161,plain,
( aInteger0(sdtpldt0(X1,sdtasdt0(xp,X1)))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[269160,theory(equality)]) ).
cnf(269458,plain,
( aInteger0(sdtpldt0(sz10,xp))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[269020,124678,theory(equality)]) ).
cnf(269537,plain,
( aInteger0(sdtpldt0(sz10,xp))
| $false ),
inference(rw,[status(thm)],[269458,394,theory(equality)]) ).
cnf(269538,plain,
aInteger0(sdtpldt0(sz10,xp)),
inference(cn,[status(thm)],[269537,theory(equality)]) ).
cnf(269851,plain,
( aInteger0(sdtasdt0(sdtpldt0(sz10,xp),X1))
| ~ aInteger0(X1)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[269161,1052,theory(equality)]) ).
cnf(269998,plain,
( aInteger0(sdtasdt0(sdtpldt0(sz10,xp),X1))
| ~ aInteger0(X1)
| $false ),
inference(rw,[status(thm)],[269851,394,theory(equality)]) ).
cnf(269999,plain,
( aInteger0(sdtasdt0(sdtpldt0(sz10,xp),X1))
| ~ aInteger0(X1) ),
inference(cn,[status(thm)],[269998,theory(equality)]) ).
cnf(270975,plain,
( aInteger0(sdtpldt0(sdtpldt0(sz10,xp),sz00))
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(spm,[status(thm)],[269999,25805,theory(equality)]) ).
cnf(271060,plain,
( aInteger0(sdtpldt0(sdtpldt0(sz10,xp),sz00))
| $false
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(rw,[status(thm)],[270975,191,theory(equality)]) ).
cnf(271061,plain,
( aInteger0(sdtpldt0(sdtpldt0(sz10,xp),sz00))
| $false
| $false ),
inference(rw,[status(thm)],[271060,269538,theory(equality)]) ).
cnf(271062,plain,
aInteger0(sdtpldt0(sdtpldt0(sz10,xp),sz00)),
inference(cn,[status(thm)],[271061,theory(equality)]) ).
cnf(271292,plain,
( aInteger0(sdtpldt0(xp,sdtpldt0(sz10,sz00)))
| ~ aInteger0(sz00)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[271062,890,theory(equality)]) ).
cnf(271320,plain,
( aInteger0(sdtpldt0(xp,sz10))
| ~ aInteger0(sz00)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[271292,25788,theory(equality)]) ).
cnf(271321,plain,
( aInteger0(sdtpldt0(xp,sz10))
| $false
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[271320,348,theory(equality)]) ).
cnf(271322,plain,
( aInteger0(sdtpldt0(xp,sz10))
| $false
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[271321,191,theory(equality)]) ).
cnf(271323,plain,
( aInteger0(sdtpldt0(xp,sz10))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[271322,394,theory(equality)]) ).
cnf(271324,plain,
aInteger0(sdtpldt0(xp,sz10)),
inference(cn,[status(thm)],[271323,theory(equality)]) ).
cnf(351759,plain,
smndt0(sdtpldt0(xp,xp)) = sdtpldt0(smndt0(xp),smndt0(xp)),
inference(rw,[status(thm)],[127814,238978,theory(equality)]) ).
cnf(352878,plain,
( sdtpldt0(smndt0(sz10),smndt0(xp)) = smndt0(sdtpldt0(sz10,xp))
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(spm,[status(thm)],[73,128991,theory(equality)]) ).
cnf(352978,plain,
( sdtpldt0(smndt0(sz10),smndt0(xp)) = smndt0(sdtpldt0(sz10,xp))
| $false ),
inference(rw,[status(thm)],[352878,269538,theory(equality)]) ).
cnf(352979,plain,
sdtpldt0(smndt0(sz10),smndt0(xp)) = smndt0(sdtpldt0(sz10,xp)),
inference(cn,[status(thm)],[352978,theory(equality)]) ).
cnf(355645,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,xp))) = sdtpldt0(sz00,smndt0(xp))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[17748,352979,theory(equality)]) ).
cnf(355787,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,xp))) = smndt0(xp)
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[355645,127793,theory(equality)]) ).
cnf(355788,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,xp))) = smndt0(xp)
| $false
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[355787,84181,theory(equality)]) ).
cnf(355789,plain,
( sdtpldt0(sz10,smndt0(sdtpldt0(sz10,xp))) = smndt0(xp)
| $false
| $false ),
inference(rw,[status(thm)],[355788,191,theory(equality)]) ).
cnf(355790,plain,
sdtpldt0(sz10,smndt0(sdtpldt0(sz10,xp))) = smndt0(xp),
inference(cn,[status(thm)],[355789,theory(equality)]) ).
cnf(356298,plain,
( smndt0(xp) = sz00
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),smndt0(xp))
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(spm,[status(thm)],[3438,355790,theory(equality)]) ).
cnf(356458,plain,
( smndt0(xp) = sz00
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),smndt0(xp))
| $false
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(rw,[status(thm)],[356298,84181,theory(equality)]) ).
cnf(356459,plain,
( smndt0(xp) = sz00
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),smndt0(xp))
| $false
| $false
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(rw,[status(thm)],[356458,191,theory(equality)]) ).
cnf(356460,plain,
( smndt0(xp) = sz00
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),smndt0(xp))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[356459,269538,theory(equality)]) ).
cnf(356461,plain,
( smndt0(xp) = sz00
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),smndt0(xp)) ),
inference(cn,[status(thm)],[356460,theory(equality)]) ).
cnf(356462,plain,
sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),smndt0(xp)),
inference(sr,[status(thm)],[356461,125322,theory(equality)]) ).
cnf(356491,plain,
( smndt0(sz10) = sz00
| sz00 = xp
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),xp)
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,xp))
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[55204,356462,theory(equality)]) ).
cnf(356529,plain,
( smndt0(sz10) = sz00
| sz00 = xp
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),xp)
| $false
| ~ aInteger0(sdtpldt0(sz10,xp))
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[356491,191,theory(equality)]) ).
cnf(356530,plain,
( smndt0(sz10) = sz00
| sz00 = xp
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),xp)
| $false
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[356529,269538,theory(equality)]) ).
cnf(356531,plain,
( smndt0(sz10) = sz00
| sz00 = xp
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),xp)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[356530,394,theory(equality)]) ).
cnf(356532,plain,
( smndt0(sz10) = sz00
| sz00 = xp
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),xp) ),
inference(cn,[status(thm)],[356531,theory(equality)]) ).
cnf(356533,plain,
( xp = sz00
| sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),xp) ),
inference(sr,[status(thm)],[356532,60135,theory(equality)]) ).
cnf(356534,plain,
sdteqdtlpzmzozddtrp0(sz10,sdtpldt0(sz10,xp),xp),
inference(sr,[status(thm)],[356533,393,theory(equality)]) ).
cnf(356585,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
| ~ aInteger0(xp)
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(spm,[status(thm)],[115,356534,theory(equality)]) ).
cnf(356594,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
| $false
| ~ aInteger0(sz10)
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(rw,[status(thm)],[356585,394,theory(equality)]) ).
cnf(356595,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
| $false
| $false
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(rw,[status(thm)],[356594,191,theory(equality)]) ).
cnf(356596,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[356595,269538,theory(equality)]) ).
cnf(356597,plain,
( sz00 = xp
| sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp) ),
inference(cn,[status(thm)],[356596,theory(equality)]) ).
cnf(356598,plain,
sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp),
inference(sr,[status(thm)],[356597,393,theory(equality)]) ).
cnf(356674,plain,
( smndt0(sz10) = sdtpldt0(sz10,xp)
| sz10 = sdtpldt0(sz10,xp)
| ~ aInteger0(sdtpldt0(sz10,xp)) ),
inference(spm,[status(thm)],[298,356598,theory(equality)]) ).
cnf(356697,plain,
( smndt0(sz10) = sdtpldt0(sz10,xp)
| sz10 = sdtpldt0(sz10,xp)
| $false ),
inference(rw,[status(thm)],[356674,269538,theory(equality)]) ).
cnf(356698,plain,
( smndt0(sz10) = sdtpldt0(sz10,xp)
| sz10 = sdtpldt0(sz10,xp) ),
inference(cn,[status(thm)],[356697,theory(equality)]) ).
cnf(357031,plain,
( sdtpldt0(sz10,smndt0(smndt0(sz10))) = smndt0(xp)
| sdtpldt0(sz10,xp) = sz10 ),
inference(spm,[status(thm)],[355790,356698,theory(equality)]) ).
cnf(357121,plain,
( sdtpldt0(sz10,sz10) = smndt0(xp)
| sdtpldt0(sz10,xp) = sz10 ),
inference(rw,[status(thm)],[357031,28815,theory(equality)]) ).
cnf(359346,plain,
( sdtpldt0(sz10,smndt0(sz10)) = smndt0(xp)
| sdtpldt0(sz10,sz10) = smndt0(xp) ),
inference(spm,[status(thm)],[355790,357121,theory(equality)]) ).
cnf(359439,plain,
( sz00 = smndt0(xp)
| sdtpldt0(sz10,sz10) = smndt0(xp) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[359346,2611,theory(equality)]),2634,theory(equality)]) ).
cnf(359440,plain,
sdtpldt0(sz10,sz10) = smndt0(xp),
inference(sr,[status(thm)],[359439,125322,theory(equality)]) ).
cnf(359657,plain,
sdtpldt0(sz10,sdtpldt0(xp,sz10)) = sz00,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[85188,359440,theory(equality)]),124678,theory(equality)]) ).
cnf(359694,plain,
sdtasdt0(xp,xp) = smndt0(sdtpldt0(xp,xp)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[253664,359440,theory(equality)]),124678,theory(equality)]) ).
cnf(360571,plain,
( sdtpldt0(smndt0(sz10),sz00) = sdtpldt0(sz00,sdtpldt0(xp,sz10))
| ~ aInteger0(sdtpldt0(xp,sz10))
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[17910,359657,theory(equality)]) ).
cnf(360635,plain,
( smndt0(sz10) = sdtpldt0(sz00,sdtpldt0(xp,sz10))
| ~ aInteger0(sdtpldt0(xp,sz10))
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[360571,25790,theory(equality)]) ).
cnf(360636,plain,
( smndt0(sz10) = sdtpldt0(sz00,sdtpldt0(xp,sz10))
| $false
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[360635,271324,theory(equality)]) ).
cnf(360637,plain,
( smndt0(sz10) = sdtpldt0(sz00,sdtpldt0(xp,sz10))
| $false
| $false ),
inference(rw,[status(thm)],[360636,191,theory(equality)]) ).
cnf(360638,plain,
smndt0(sz10) = sdtpldt0(sz00,sdtpldt0(xp,sz10)),
inference(cn,[status(thm)],[360637,theory(equality)]) ).
cnf(367729,plain,
( smndt0(sz10) = sdtpldt0(xp,sz10)
| ~ aInteger0(sdtpldt0(xp,sz10)) ),
inference(spm,[status(thm)],[352,360638,theory(equality)]) ).
cnf(367811,plain,
( smndt0(sz10) = sdtpldt0(xp,sz10)
| $false ),
inference(rw,[status(thm)],[367729,271324,theory(equality)]) ).
cnf(367812,plain,
smndt0(sz10) = sdtpldt0(xp,sz10),
inference(cn,[status(thm)],[367811,theory(equality)]) ).
cnf(368054,plain,
( sdtpldt0(smndt0(xp),smndt0(sz10)) = sdtpldt0(sz00,sz10)
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(spm,[status(thm)],[17910,367812,theory(equality)]) ).
cnf(368171,plain,
( sdtpldt0(smndt0(xp),smndt0(sz10)) = sz10
| ~ aInteger0(sz10)
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[368054,26036,theory(equality)]) ).
cnf(368172,plain,
( sdtpldt0(smndt0(xp),smndt0(sz10)) = sz10
| $false
| ~ aInteger0(xp) ),
inference(rw,[status(thm)],[368171,191,theory(equality)]) ).
cnf(368173,plain,
( sdtpldt0(smndt0(xp),smndt0(sz10)) = sz10
| $false
| $false ),
inference(rw,[status(thm)],[368172,394,theory(equality)]) ).
cnf(368174,plain,
sdtpldt0(smndt0(xp),smndt0(sz10)) = sz10,
inference(cn,[status(thm)],[368173,theory(equality)]) ).
cnf(2510278,negated_conjecture,
( sdtpldt0(sz10,X1) = smndt0(sz10)
| sdtpldt0(smndt0(smndt0(sz10)),X1) = sz10
| ~ aDivisorOf0(xp,sdtpldt0(sz00,X1))
| ~ aInteger0(sdtpldt0(smndt0(smndt0(sz10)),X1))
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[17807,28815,theory(equality)]) ).
cnf(2510279,negated_conjecture,
( sdtpldt0(sz10,X1) = smndt0(sz10)
| sdtpldt0(sz10,X1) = sz10
| ~ aDivisorOf0(xp,sdtpldt0(sz00,X1))
| ~ aInteger0(sdtpldt0(smndt0(smndt0(sz10)),X1))
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[2510278,28815,theory(equality)]) ).
cnf(2510280,negated_conjecture,
( sdtpldt0(sz10,X1) = smndt0(sz10)
| sdtpldt0(sz10,X1) = sz10
| ~ aDivisorOf0(xp,sdtpldt0(sz00,X1))
| ~ aInteger0(sdtpldt0(sz10,X1))
| ~ aInteger0(X1) ),
inference(rw,[status(thm)],[2510279,28815,theory(equality)]) ).
cnf(2510281,negated_conjecture,
( sdtpldt0(sz10,X1) = smndt0(sz10)
| sdtpldt0(sz10,X1) = sz10
| ~ aDivisorOf0(xp,sdtpldt0(sz00,X1))
| ~ aInteger0(X1) ),
inference(csr,[status(thm)],[2510280,26266]) ).
cnf(2510286,plain,
( sdtpldt0(sz10,smndt0(xp)) = smndt0(sz10)
| sdtpldt0(sz10,smndt0(xp)) = sz10
| ~ aDivisorOf0(xp,smndt0(xp))
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[2510281,127793,theory(equality)]) ).
cnf(2510388,plain,
( sdtpldt0(sz10,smndt0(xp)) = smndt0(sz10)
| sdtpldt0(sz10,smndt0(xp)) = sz10
| $false
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[2510286,125317,theory(equality)]) ).
cnf(2510389,plain,
( sdtpldt0(sz10,smndt0(xp)) = smndt0(sz10)
| sdtpldt0(sz10,smndt0(xp)) = sz10
| $false
| $false ),
inference(rw,[status(thm)],[2510388,84181,theory(equality)]) ).
cnf(2510390,plain,
( sdtpldt0(sz10,smndt0(xp)) = smndt0(sz10)
| sdtpldt0(sz10,smndt0(xp)) = sz10 ),
inference(cn,[status(thm)],[2510389,theory(equality)]) ).
cnf(2514357,plain,
( sdtpldt0(smndt0(xp),sdtpldt0(sz10,smndt0(smndt0(sz10)))) = sz00
| sdtpldt0(sz10,smndt0(xp)) = sz10
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(xp)) ),
inference(spm,[status(thm)],[17331,2510390,theory(equality)]) ).
cnf(2514642,plain,
( sdtasdt0(xp,xp) = sz00
| sdtpldt0(sz10,smndt0(xp)) = sz10
| ~ aInteger0(sz10)
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[2514357,28815,theory(equality)]),359440,theory(equality)]),351759,theory(equality)]),359694,theory(equality)]) ).
cnf(2514643,plain,
( sdtasdt0(xp,xp) = sz00
| sdtpldt0(sz10,smndt0(xp)) = sz10
| $false
| ~ aInteger0(smndt0(xp)) ),
inference(rw,[status(thm)],[2514642,191,theory(equality)]) ).
cnf(2514644,plain,
( sdtasdt0(xp,xp) = sz00
| sdtpldt0(sz10,smndt0(xp)) = sz10
| $false
| $false ),
inference(rw,[status(thm)],[2514643,84181,theory(equality)]) ).
cnf(2514645,plain,
( sdtasdt0(xp,xp) = sz00
| sdtpldt0(sz10,smndt0(xp)) = sz10 ),
inference(cn,[status(thm)],[2514644,theory(equality)]) ).
cnf(2514646,plain,
sdtpldt0(sz10,smndt0(xp)) = sz10,
inference(sr,[status(thm)],[2514645,141077,theory(equality)]) ).
cnf(2514728,plain,
( sdtpldt0(sz10,sdtpldt0(smndt0(xp),smndt0(sz10))) = sz00
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(sz10) ),
inference(spm,[status(thm)],[17322,2514646,theory(equality)]) ).
cnf(2514901,plain,
( smndt0(xp) = sz00
| ~ aInteger0(smndt0(xp))
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[2514728,368174,theory(equality)]),359440,theory(equality)]) ).
cnf(2514902,plain,
( smndt0(xp) = sz00
| $false
| ~ aInteger0(sz10) ),
inference(rw,[status(thm)],[2514901,84181,theory(equality)]) ).
cnf(2514903,plain,
( smndt0(xp) = sz00
| $false
| $false ),
inference(rw,[status(thm)],[2514902,191,theory(equality)]) ).
cnf(2514904,plain,
smndt0(xp) = sz00,
inference(cn,[status(thm)],[2514903,theory(equality)]) ).
cnf(2514905,plain,
$false,
inference(sr,[status(thm)],[2514904,125322,theory(equality)]) ).
cnf(2514906,plain,
$false,
2514905,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM451+6 : TPTP v7.0.0. Released v4.0.0.
% 0.00/0.03 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n079.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 04:19:00 CST 2018
% 0.02/0.23 % CPUTime :
% 0.06/0.52 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.53 --creating new selector for []
% 29.10/30.29 eprover: CPU time limit exceeded, terminating
% 84.95/86.77 -running prover on /export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_1 with time limit 29
% 84.95/86.77 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_1']
% 84.95/86.77 -prover status ResourceOut
% 84.95/86.77 -running prover on /export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2 with time limit 80
% 84.95/86.77 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=80', '/export/starexec/sandbox2/tmp/tmpyIXAkO/sel_theBenchmark.p_2']
% 84.95/86.77 -prover status Theorem
% 84.95/86.77 Problem theBenchmark.p solved in phase 1.
% 84.95/86.77 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 84.95/86.77 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 84.95/86.77 Solved 1 out of 1.
% 84.95/86.77 # Problem is unsatisfiable (or provable), constructing proof object
% 84.95/86.77 # SZS status Theorem
% 84.95/86.77 # SZS output start CNFRefutation.
% See solution above
% 84.95/86.79 # SZS output end CNFRefutation
%------------------------------------------------------------------------------