%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM500+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Mon Jul 18 06:22:56 EDT 2022
% Result : Theorem 11.04s 11.43s
% Output : Refutation 11.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NUM500+1 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % DateTime : Thu Jul 7 13:51:39 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.47/1.14 *** allocated 10000 integers for termspace/termends
% 0.47/1.14 *** allocated 10000 integers for clauses
% 0.47/1.14 *** allocated 10000 integers for justifications
% 0.47/1.14 Bliksem 1.12
% 0.47/1.14
% 0.47/1.14
% 0.47/1.14 Automatic Strategy Selection
% 0.47/1.14
% 0.47/1.14
% 0.47/1.14 Clauses:
% 0.47/1.14
% 0.47/1.14 { && }.
% 0.47/1.14 { aNaturalNumber0( sz00 ) }.
% 0.47/1.14 { aNaturalNumber0( sz10 ) }.
% 0.47/1.14 { ! sz10 = sz00 }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0
% 0.47/1.14 ( X, Y ) ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0
% 0.47/1.14 ( X, Y ) ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtpldt0( X, Y ) =
% 0.47/1.14 sdtpldt0( Y, X ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.47/1.14 sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) = X }.
% 0.47/1.14 { ! aNaturalNumber0( X ), X = sdtpldt0( sz00, X ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtasdt0( X, Y ) =
% 0.47/1.14 sdtasdt0( Y, X ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.47/1.14 sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 ) = X }.
% 0.47/1.14 { ! aNaturalNumber0( X ), X = sdtasdt0( sz10, X ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 0.47/1.14 { ! aNaturalNumber0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.47/1.14 sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X
% 0.47/1.14 , Z ) ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.47/1.14 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z
% 0.47/1.14 , X ) ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.47/1.14 sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.47/1.14 sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z }.
% 0.47/1.14 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.47/1.14 aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ), Y = Z }.
% 0.47/1.14 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.47/1.14 aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ), Y = Z }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.47/1.14 , X = sz00 }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.47/1.14 , Y = sz00 }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sz00
% 0.47/1.14 , X = sz00, Y = sz00 }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.47/1.14 aNaturalNumber0( skol1( Z, T ) ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.47/1.14 sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.47/1.14 sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.47/1.14 = sdtmndt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.47/1.14 = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.47/1.14 aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.47/1.14 sdtlseqdt0( Y, X ), X = Y }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.47/1.14 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y =
% 0.47/1.14 X }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ),
% 0.47/1.14 sdtlseqdt0( Y, X ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.47/1.14 ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z ) }.
% 0.47/1.14 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.47/1.14 ), ! aNaturalNumber0( Z ), sdtlseqdt0( sdtpldt0( X, Z ), sdtpldt0( Y, Z
% 0.47/1.14 ) ) }.
% 0.47/1.14 { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) = sdtpldt0( Z, Y ) }.
% 0.47/1.14 { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ) }.
% 0.47/1.14 { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) = sdtpldt0( Y, Z ) }.
% 1.93/2.31 { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), ! sdtlseqdt0( sdtpldt0( Z, X ),
% 1.93/2.31 sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) = sdtpldt0( Y, Z ), alpha5( X, Y, Z
% 1.93/2.31 ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 1.93/2.31 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), alpha6( X, Y, Z ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 1.93/2.31 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), sdtlseqdt0( sdtasdt0( Y, X ),
% 1.93/2.31 sdtasdt0( Z, X ) ) }.
% 1.93/2.31 { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ) }.
% 1.93/2.31 { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 1.93/2.31 { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ) }.
% 1.93/2.31 { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), ! sdtlseqdt0( sdtasdt0( X, Y ),
% 1.93/2.31 sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) = sdtasdt0( Z, X ), alpha6( X, Y, Z
% 1.93/2.31 ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! sz10 = X }.
% 1.93/2.31 { ! aNaturalNumber0( X ), X = sz00, X = sz10, sdtlseqdt0( sz10, X ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, sdtlseqdt0( Y,
% 1.93/2.31 sdtasdt0( Y, X ) ) }.
% 1.93/2.31 { && }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 1.93/2.31 ), iLess0( X, Y ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ),
% 1.93/2.31 aNaturalNumber0( skol2( Z, T ) ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 1.93/2.31 sdtasdt0( X, skol2( X, Y ) ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 1.93/2.31 Y = sdtasdt0( X, Z ), doDivides0( X, Y ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 1.93/2.31 , Y ), ! Z = sdtsldt0( Y, X ), aNaturalNumber0( Z ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 1.93/2.31 , Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0( X, Z ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 1.93/2.31 , Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), Z = sdtsldt0( Y, X
% 1.93/2.31 ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 1.93/2.31 doDivides0( X, Y ), ! doDivides0( Y, Z ), doDivides0( X, Z ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 1.93/2.31 doDivides0( X, Y ), ! doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z
% 1.93/2.31 ) ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 1.93/2.31 doDivides0( X, Y ), ! doDivides0( X, sdtpldt0( Y, Z ) ), doDivides0( X,
% 1.93/2.31 Z ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 1.93/2.31 sz00, sdtlseqdt0( X, Y ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 1.93/2.31 , Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z, sdtsldt0( Y, X ) ) = sdtsldt0
% 1.93/2.31 ( sdtasdt0( Z, Y ), X ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X = sz00 }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! isPrime0( X ), alpha1( X ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), X = sz00, ! alpha1( X ), isPrime0( X ) }.
% 1.93/2.31 { ! alpha1( X ), ! X = sz10 }.
% 1.93/2.31 { ! alpha1( X ), alpha2( X ) }.
% 1.93/2.31 { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 1.93/2.31 { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X, Y ) }.
% 1.93/2.31 { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 1.93/2.31 { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 1.93/2.31 { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 1.93/2.31 { ! Y = sz10, alpha4( X, Y ) }.
% 1.93/2.31 { ! Y = X, alpha4( X, Y ) }.
% 1.93/2.31 { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 1.93/2.31 { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 1.93/2.31 { ! aNaturalNumber0( Y ), ! doDivides0( Y, X ), alpha3( X, Y ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), X = sz00, X = sz10, aNaturalNumber0( skol4( Y ) )
% 1.93/2.31 }.
% 1.93/2.31 { ! aNaturalNumber0( X ), X = sz00, X = sz10, isPrime0( skol4( Y ) ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), X = sz00, X = sz10, doDivides0( skol4( X ), X ) }
% 1.93/2.31 .
% 1.93/2.31 { aNaturalNumber0( xn ) }.
% 1.93/2.31 { aNaturalNumber0( xm ) }.
% 1.93/2.31 { aNaturalNumber0( xp ) }.
% 1.93/2.31 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 1.93/2.31 isPrime0( Z ), ! doDivides0( Z, sdtasdt0( X, Y ) ), ! iLess0( sdtpldt0(
% 1.93/2.31 sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0( xn, xm ), xp ) ), doDivides0(
% 1.93/2.31 Z, X ), doDivides0( Z, Y ) }.
% 1.93/2.31 { isPrime0( xp ) }.
% 1.93/2.31 { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 1.93/2.31 { ! sdtlseqdt0( xp, xn ) }.
% 1.93/2.31 { ! sdtlseqdt0( xp, xm ) }.
% 1.93/2.31 { ! xn = xp }.
% 1.93/2.31 { sdtlseqdt0( xn, xp ) }.
% 11.04/11.42 { ! xm = xp }.
% 11.04/11.42 { sdtlseqdt0( xm, xp ) }.
% 11.04/11.42 { xk = sdtsldt0( sdtasdt0( xn, xm ), xp ) }.
% 11.04/11.42 { ! xk = sz00 }.
% 11.04/11.42 { ! xk = sz10 }.
% 11.04/11.42 { ! xk = sz00 }.
% 11.04/11.42 { ! xk = sz10 }.
% 11.04/11.42 { ! aNaturalNumber0( X ), ! doDivides0( X, xk ), ! isPrime0( X ) }.
% 11.04/11.42
% 11.04/11.42 percentage equality = 0.280488, percentage horn = 0.721649
% 11.04/11.42 This is a problem with some equality
% 11.04/11.42
% 11.04/11.42
% 11.04/11.42
% 11.04/11.42 Options Used:
% 11.04/11.42
% 11.04/11.42 useres = 1
% 11.04/11.42 useparamod = 1
% 11.04/11.42 useeqrefl = 1
% 11.04/11.42 useeqfact = 1
% 11.04/11.42 usefactor = 1
% 11.04/11.42 usesimpsplitting = 0
% 11.04/11.42 usesimpdemod = 5
% 11.04/11.42 usesimpres = 3
% 11.04/11.42
% 11.04/11.42 resimpinuse = 1000
% 11.04/11.42 resimpclauses = 20000
% 11.04/11.42 substype = eqrewr
% 11.04/11.42 backwardsubs = 1
% 11.04/11.42 selectoldest = 5
% 11.04/11.42
% 11.04/11.42 litorderings [0] = split
% 11.04/11.42 litorderings [1] = extend the termordering, first sorting on arguments
% 11.04/11.42
% 11.04/11.42 termordering = kbo
% 11.04/11.42
% 11.04/11.42 litapriori = 0
% 11.04/11.42 termapriori = 1
% 11.04/11.42 litaposteriori = 0
% 11.04/11.42 termaposteriori = 0
% 11.04/11.42 demodaposteriori = 0
% 11.04/11.42 ordereqreflfact = 0
% 11.04/11.42
% 11.04/11.42 litselect = negord
% 11.04/11.42
% 11.04/11.42 maxweight = 15
% 11.04/11.42 maxdepth = 30000
% 11.04/11.42 maxlength = 115
% 11.04/11.42 maxnrvars = 195
% 11.04/11.42 excuselevel = 1
% 11.04/11.42 increasemaxweight = 1
% 11.04/11.42
% 11.04/11.42 maxselected = 10000000
% 11.04/11.42 maxnrclauses = 10000000
% 11.04/11.42
% 11.04/11.42 showgenerated = 0
% 11.04/11.42 showkept = 0
% 11.04/11.42 showselected = 0
% 11.04/11.42 showdeleted = 0
% 11.04/11.42 showresimp = 1
% 11.04/11.42 showstatus = 2000
% 11.04/11.42
% 11.04/11.42 prologoutput = 0
% 11.04/11.42 nrgoals = 5000000
% 11.04/11.42 totalproof = 1
% 11.04/11.42
% 11.04/11.42 Symbols occurring in the translation:
% 11.04/11.42
% 11.04/11.42 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 11.04/11.42 . [1, 2] (w:1, o:26, a:1, s:1, b:0),
% 11.04/11.42 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 11.04/11.42 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 11.04/11.42 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 11.04/11.42 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 11.04/11.42 aNaturalNumber0 [36, 1] (w:1, o:20, a:1, s:1, b:0),
% 11.04/11.42 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 11.04/11.42 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 11.04/11.42 sdtpldt0 [40, 2] (w:1, o:50, a:1, s:1, b:0),
% 11.04/11.42 sdtasdt0 [41, 2] (w:1, o:51, a:1, s:1, b:0),
% 11.04/11.42 sdtlseqdt0 [43, 2] (w:1, o:52, a:1, s:1, b:0),
% 11.04/11.42 sdtmndt0 [44, 2] (w:1, o:53, a:1, s:1, b:0),
% 11.04/11.42 iLess0 [45, 2] (w:1, o:54, a:1, s:1, b:0),
% 11.04/11.42 doDivides0 [46, 2] (w:1, o:55, a:1, s:1, b:0),
% 11.04/11.42 sdtsldt0 [47, 2] (w:1, o:56, a:1, s:1, b:0),
% 11.04/11.42 isPrime0 [48, 1] (w:1, o:21, a:1, s:1, b:0),
% 11.04/11.42 xn [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 11.04/11.42 xm [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 11.04/11.42 xp [51, 0] (w:1, o:13, a:1, s:1, b:0),
% 11.04/11.42 xk [52, 0] (w:1, o:14, a:1, s:1, b:0),
% 11.04/11.42 alpha1 [53, 1] (w:1, o:22, a:1, s:1, b:1),
% 11.04/11.42 alpha2 [54, 1] (w:1, o:23, a:1, s:1, b:1),
% 11.04/11.42 alpha3 [55, 2] (w:1, o:57, a:1, s:1, b:1),
% 11.04/11.42 alpha4 [56, 2] (w:1, o:58, a:1, s:1, b:1),
% 11.04/11.42 alpha5 [57, 3] (w:1, o:61, a:1, s:1, b:1),
% 11.04/11.42 alpha6 [58, 3] (w:1, o:62, a:1, s:1, b:1),
% 11.04/11.42 skol1 [59, 2] (w:1, o:59, a:1, s:1, b:1),
% 11.04/11.42 skol2 [60, 2] (w:1, o:60, a:1, s:1, b:1),
% 11.04/11.42 skol3 [61, 1] (w:1, o:24, a:1, s:1, b:1),
% 11.04/11.42 skol4 [62, 1] (w:1, o:25, a:1, s:1, b:1).
% 11.04/11.42
% 11.04/11.42
% 11.04/11.42 Starting Search:
% 11.04/11.42
% 11.04/11.42 *** allocated 15000 integers for clauses
% 11.04/11.42 *** allocated 22500 integers for clauses
% 11.04/11.42 *** allocated 33750 integers for clauses
% 11.04/11.42 *** allocated 15000 integers for termspace/termends
% 11.04/11.42 *** allocated 50625 integers for clauses
% 11.04/11.42 *** allocated 22500 integers for termspace/termends
% 11.04/11.42 *** allocated 75937 integers for clauses
% 11.04/11.42 Resimplifying inuse:
% 11.04/11.42 Done
% 11.04/11.42
% 11.04/11.42 *** allocated 33750 integers for termspace/termends
% 11.04/11.42 *** allocated 113905 integers for clauses
% 11.04/11.42 *** allocated 50625 integers for termspace/termends
% 11.04/11.42
% 11.04/11.42 Intermediate Status:
% 11.04/11.42 Generated: 12375
% 11.04/11.42 Kept: 2004
% 11.04/11.42 Inuse: 137
% 11.04/11.42 Deleted: 1
% 11.04/11.42 Deletedinuse: 0
% 11.04/11.42
% 11.04/11.42 Resimplifying inuse:
% 11.04/11.42 Done
% 11.04/11.42
% 11.04/11.42 *** allocated 170857 integers for clauses
% 11.04/11.42 *** allocated 75937 integers for termspace/termends
% 11.04/11.42 Resimplifying inuse:
% 11.04/11.42 Done
% 11.04/11.42
% 11.04/11.42 *** allocated 256285 integers for clauses
% 11.04/11.42 *** allocated 113905 integers for termspace/termends
% 11.04/11.42
% 11.04/11.42 Intermediate Status:
% 11.04/11.42 Generated: 25504
% 11.04/11.42 Kept: 4047
% 11.04/11.42 Inuse: 187
% 11.04/11.42 Deleted: 8
% 11.04/11.42 Deletedinuse: 5
% 11.04/11.42
% 11.04/11.42 Resimplifying inuse:
% 11.04/11.42 Done
% 11.04/11.42
% 11.04/11.42 Resimplifying inuse:
% 11.04/11.42 Done
% 11.04/11.42
% 11.04/11.42 *** allocated 170857 integers for termspace/termends
% 11.04/11.42 *** allocated 384427 integers for clauses
% 11.04/11.42
% 11.04/11.42 Intermediate Status:
% 11.04/11.42 Generated: 47787
% 11.04/11.42 Kept: 6047
% 11.04/11.42 Inuse: 231
% 11.04/11.42 Deleted: 20
% 11.04/11.43 Deletedinuse: 15
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 *** allocated 256285 integers for termspace/termends
% 11.04/11.43
% 11.04/11.43 Intermediate Status:
% 11.04/11.43 Generated: 63745
% 11.04/11.43 Kept: 8233
% 11.04/11.43 Inuse: 266
% 11.04/11.43 Deleted: 28
% 11.04/11.43 Deletedinuse: 23
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 *** allocated 576640 integers for clauses
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 Intermediate Status:
% 11.04/11.43 Generated: 87380
% 11.04/11.43 Kept: 11294
% 11.04/11.43 Inuse: 328
% 11.04/11.43 Deleted: 48
% 11.04/11.43 Deletedinuse: 35
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 *** allocated 384427 integers for termspace/termends
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 *** allocated 864960 integers for clauses
% 11.04/11.43
% 11.04/11.43 Intermediate Status:
% 11.04/11.43 Generated: 105056
% 11.04/11.43 Kept: 13300
% 11.04/11.43 Inuse: 367
% 11.04/11.43 Deleted: 55
% 11.04/11.43 Deletedinuse: 42
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 Intermediate Status:
% 11.04/11.43 Generated: 119734
% 11.04/11.43 Kept: 15304
% 11.04/11.43 Inuse: 460
% 11.04/11.43 Deleted: 58
% 11.04/11.43 Deletedinuse: 42
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 Intermediate Status:
% 11.04/11.43 Generated: 145151
% 11.04/11.43 Kept: 17337
% 11.04/11.43 Inuse: 562
% 11.04/11.43 Deleted: 71
% 11.04/11.43 Deletedinuse: 44
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 Intermediate Status:
% 11.04/11.43 Generated: 156806
% 11.04/11.43 Kept: 19371
% 11.04/11.43 Inuse: 607
% 11.04/11.43 Deleted: 80
% 11.04/11.43 Deletedinuse: 48
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 *** allocated 576640 integers for termspace/termends
% 11.04/11.43 *** allocated 1297440 integers for clauses
% 11.04/11.43 Resimplifying clauses:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 Intermediate Status:
% 11.04/11.43 Generated: 175160
% 11.04/11.43 Kept: 21540
% 11.04/11.43 Inuse: 641
% 11.04/11.43 Deleted: 5792
% 11.04/11.43 Deletedinuse: 48
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43 Resimplifying inuse:
% 11.04/11.43 Done
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 Bliksems!, er is een bewijs:
% 11.04/11.43 % SZS status Theorem
% 11.04/11.43 % SZS output start Refutation
% 11.04/11.43
% 11.04/11.43 (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 11.04/11.43 (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 11.04/11.43 (3) {G0,W3,D2,L1,V0,M1} I { ! sz10 ==> sz00 }.
% 11.04/11.43 (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 11.04/11.43 , aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 11.04/11.43 (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) ==>
% 11.04/11.43 X }.
% 11.04/11.43 (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 11.04/11.43 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 11.04/11.43 }.
% 11.04/11.43 (20) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), X = sz00, !
% 11.04/11.43 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 11.04/11.43 sdtasdt0( X, Z ), Y = Z }.
% 11.04/11.43 (22) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 11.04/11.43 ), ! sdtpldt0( X, Y ) ==> sz00, X = sz00 }.
% 11.04/11.43 (48) {G0,W11,D2,L4,V1,M4} I { ! aNaturalNumber0( X ), X = sz00, X = sz10, !
% 11.04/11.43 sz10 = X }.
% 11.04/11.43 (55) {G0,W17,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 11.04/11.43 ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 11.04/11.43 aNaturalNumber0( Z ) }.
% 11.04/11.43 (63) {G0,W7,D2,L3,V1,M3} I { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X =
% 11.04/11.43 sz00 }.
% 11.04/11.43 (72) {G0,W9,D2,L3,V2,M3} I { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 11.04/11.43 (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 11.04/11.43 (74) {G0,W6,D2,L2,V2,M2} I { ! Y = X, alpha4( X, Y ) }.
% 11.04/11.43 (78) {G0,W11,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), X = sz00, X = sz10,
% 11.04/11.43 aNaturalNumber0( skol4( Y ) ) }.
% 11.04/11.43 (79) {G0,W11,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), X = sz00, X = sz10,
% 11.04/11.43 isPrime0( skol4( Y ) ) }.
% 11.04/11.43 (80) {G0,W12,D3,L4,V1,M4} I { ! aNaturalNumber0( X ), X = sz00, X = sz10,
% 11.04/11.43 doDivides0( skol4( X ), X ) }.
% 11.04/11.43 (81) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 11.04/11.43 (82) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 11.04/11.43 (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 11.04/11.43 (85) {G0,W2,D2,L1,V0,M1} I { isPrime0( xp ) }.
% 11.04/11.43 (86) {G0,W5,D3,L1,V0,M1} I { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 11.04/11.43 (93) {G0,W7,D4,L1,V0,M1} I { sdtsldt0( sdtasdt0( xn, xm ), xp ) ==> xk }.
% 11.04/11.43 (94) {G0,W3,D2,L1,V0,M1} I { ! xk ==> sz00 }.
% 11.04/11.43 (95) {G0,W3,D2,L1,V0,M1} I { ! xk ==> sz10 }.
% 11.04/11.43 (96) {G0,W7,D2,L3,V1,M3} I { ! aNaturalNumber0( X ), ! doDivides0( X, xk )
% 11.04/11.43 , ! isPrime0( X ) }.
% 11.04/11.43 (225) {G1,W2,D2,L1,V0,M1} Q(63);r(1) { ! isPrime0( sz00 ) }.
% 11.04/11.43 (227) {G1,W6,D2,L2,V1,M2} F(72) { ! alpha4( sz10, X ), X = sz10 }.
% 11.04/11.43 (255) {G1,W6,D3,L2,V1,M2} R(5,82) { ! aNaturalNumber0( X ), aNaturalNumber0
% 11.04/11.43 ( sdtasdt0( X, xm ) ) }.
% 11.04/11.43 (345) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 11.04/11.43 (442) {G2,W6,D2,L2,V1,M2} P(227,3) { ! X = sz00, ! alpha4( sz10, X ) }.
% 11.04/11.43 (443) {G2,W5,D2,L2,V1,M2} P(227,2) { aNaturalNumber0( X ), ! alpha4( sz10,
% 11.04/11.43 X ) }.
% 11.04/11.43 (455) {G3,W5,D2,L2,V1,M2} R(443,73) { aNaturalNumber0( X ), ! X = sz10 }.
% 11.04/11.43 (735) {G3,W6,D2,L2,V1,M2} R(442,73) { ! X = sz00, ! X = sz10 }.
% 11.04/11.43 (907) {G1,W17,D3,L5,V2,M5} R(20,83) { ! aNaturalNumber0( X ), X = sz00, !
% 11.04/11.43 aNaturalNumber0( Y ), ! sdtasdt0( X, xp ) = sdtasdt0( X, Y ), xp = Y }.
% 11.04/11.43 (1008) {G2,W15,D3,L4,V1,M4} E(907);f { ! xp ==> sz00, ! aNaturalNumber0( X
% 11.04/11.43 ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X ) }.
% 11.04/11.43 (1011) {G3,W6,D2,L2,V0,M2} Q(1008);r(83) { ! xp ==> sz00, xp ==> sz00 }.
% 11.04/11.43 (1308) {G2,W9,D3,L3,V1,M3} P(22,85);r(225) { ! aNaturalNumber0( xp ), !
% 11.04/11.43 aNaturalNumber0( X ), ! sdtpldt0( xp, X ) ==> sz00 }.
% 11.04/11.43 (1309) {G3,W5,D3,L1,V0,M1} F(1308);r(83) { ! sdtpldt0( xp, xp ) ==> sz00
% 11.04/11.43 }.
% 11.04/11.43 (1375) {G4,W3,D2,L1,V0,M1} P(1011,1309);d(345);q { ! xp ==> sz00 }.
% 11.04/11.43 (5957) {G4,W6,D2,L2,V1,M2} S(48);r(455);r(735) { X = sz10, ! sz10 = X }.
% 11.04/11.43 (7717) {G1,W12,D3,L4,V1,M4} R(55,86);d(93);r(83) { ! aNaturalNumber0(
% 11.04/11.43 sdtasdt0( xn, xm ) ), xp ==> sz00, aNaturalNumber0( X ), ! X = xk }.
% 11.04/11.43 (7841) {G5,W6,D3,L2,V0,M2} Q(7717);r(1375) { ! aNaturalNumber0( sdtasdt0(
% 11.04/11.43 xn, xm ) ), aNaturalNumber0( xk ) }.
% 11.04/11.43 (10548) {G5,W12,D2,L4,V3,M4} P(72,5957) { Y = X, ! X = Y, ! alpha4( Z, X )
% 11.04/11.43 , X = Z }.
% 11.04/11.43 (11257) {G6,W6,D2,L2,V2,M2} E(10548);q;r(74) { Y = X, ! X = Y }.
% 11.04/11.43 (17334) {G7,W6,D2,L2,V1,M2} P(11257,94) { ! X = sz00, ! X = xk }.
% 11.04/11.43 (17335) {G7,W6,D2,L2,V1,M2} P(11257,95) { ! X = sz10, ! X = xk }.
% 11.04/11.43 (17847) {G8,W9,D3,L3,V1,M3} R(17334,80);r(17335) { ! X = xk, !
% 11.04/11.43 aNaturalNumber0( X ), doDivides0( skol4( X ), X ) }.
% 11.04/11.43 (17848) {G8,W8,D3,L3,V2,M3} R(17334,79);r(17335) { ! X = xk, !
% 11.04/11.43 aNaturalNumber0( X ), isPrime0( skol4( Y ) ) }.
% 11.04/11.43 (17849) {G8,W8,D3,L3,V2,M3} R(17334,78);r(17335) { ! X = xk, !
% 11.04/11.43 aNaturalNumber0( X ), aNaturalNumber0( skol4( Y ) ) }.
% 11.04/11.43 (17891) {G9,W5,D3,L2,V1,M2} Q(17849) { ! aNaturalNumber0( xk ),
% 11.04/11.43 aNaturalNumber0( skol4( X ) ) }.
% 11.04/11.43 (17892) {G9,W5,D3,L2,V1,M2} Q(17848) { ! aNaturalNumber0( xk ), isPrime0(
% 11.04/11.43 skol4( X ) ) }.
% 11.04/11.43 (17893) {G9,W6,D3,L2,V0,M2} Q(17847) { ! aNaturalNumber0( xk ), doDivides0
% 11.04/11.43 ( skol4( xk ), xk ) }.
% 11.04/11.43 (19164) {G10,W6,D3,L2,V1,M2} R(17892,96);r(17891) { ! aNaturalNumber0( xk )
% 11.04/11.43 , ! doDivides0( skol4( X ), xk ) }.
% 11.04/11.43 (20470) {G11,W2,D2,L1,V0,M1} S(17893);r(19164) { ! aNaturalNumber0( xk )
% 11.04/11.43 }.
% 11.04/11.43 (21081) {G12,W4,D3,L1,V0,M1} S(7841);r(20470) { ! aNaturalNumber0( sdtasdt0
% 11.04/11.43 ( xn, xm ) ) }.
% 11.04/11.43 (23063) {G13,W13,D3,L4,V2,M4} P(18,21081);r(255) { ! aNaturalNumber0( Y ),
% 11.04/11.43 ! aNaturalNumber0( xn ), ! aNaturalNumber0( X ), ! sdtpldt0( Y, xn ) =
% 11.04/11.43 sdtpldt0( Y, X ) }.
% 11.04/11.43 (23066) {G14,W9,D3,L2,V1,M2} F(23063);r(81) { ! aNaturalNumber0( X ), !
% 11.04/11.43 sdtpldt0( X, xn ) = sdtpldt0( X, X ) }.
% 11.04/11.43 (23068) {G15,W0,D0,L0,V0,M0} Q(23066);r(81) { }.
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 % SZS output end Refutation
% 11.04/11.43 found a proof!
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 Unprocessed initial clauses:
% 11.04/11.43
% 11.04/11.43 (23070) {G0,W1,D1,L1,V0,M1} { && }.
% 11.04/11.43 (23071) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 11.04/11.43 (23072) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 11.04/11.43 (23073) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 11.04/11.43 (23074) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 11.04/11.43 ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 11.04/11.43 (23075) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 11.04/11.43 ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 11.04/11.43 (23076) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 11.04/11.43 (23077) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0(
% 11.04/11.43 X, sdtpldt0( Y, Z ) ) }.
% 11.04/11.43 (23078) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 )
% 11.04/11.43 = X }.
% 11.04/11.43 (23079) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtpldt0( sz00,
% 11.04/11.43 X ) }.
% 11.04/11.43 (23080) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 11.04/11.43 (23081) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0(
% 11.04/11.43 X, sdtasdt0( Y, Z ) ) }.
% 11.04/11.43 (23082) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 11.04/11.43 = X }.
% 11.04/11.43 (23083) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtasdt0( sz10,
% 11.04/11.43 X ) }.
% 11.04/11.43 (23084) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 )
% 11.04/11.43 = sz00 }.
% 11.04/11.43 (23085) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sz00 = sdtasdt0(
% 11.04/11.43 sz00, X ) }.
% 11.04/11.43 (23086) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0(
% 11.04/11.43 sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 11.04/11.43 (23087) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0(
% 11.04/11.43 sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 11.04/11.43 (23088) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 11.04/11.43 }.
% 11.04/11.43 (23089) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z
% 11.04/11.43 }.
% 11.04/11.43 (23090) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 11.04/11.43 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 11.04/11.43 sdtasdt0( X, Z ), Y = Z }.
% 11.04/11.43 (23091) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 11.04/11.43 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) =
% 11.04/11.43 sdtasdt0( Z, X ), Y = Z }.
% 11.04/11.43 (23092) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 11.04/11.43 (23093) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 11.04/11.43 (23094) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 11.04/11.43 (23095) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtlseqdt0( X, Y ), aNaturalNumber0( skol1( Z, T ) ) }.
% 11.04/11.43 (23096) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtlseqdt0( X, Y ), sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 11.04/11.43 (23097) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 11.04/11.43 }.
% 11.04/11.43 (23098) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 11.04/11.43 }.
% 11.04/11.43 (23099) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 11.04/11.43 }.
% 11.04/11.43 (23100) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y
% 11.04/11.43 , Z = sdtmndt0( Y, X ) }.
% 11.04/11.43 (23101) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0( X, X )
% 11.04/11.43 }.
% 11.04/11.43 (23102) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 11.04/11.43 (23103) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ),
% 11.04/11.43 sdtlseqdt0( X, Z ) }.
% 11.04/11.43 (23104) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 11.04/11.43 (23105) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), sdtlseqdt0( X, Y ), sdtlseqdt0( Y, X ) }.
% 11.04/11.43 (23106) {G0,W16,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z
% 11.04/11.43 ) }.
% 11.04/11.43 (23107) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), sdtlseqdt0(
% 11.04/11.43 sdtpldt0( X, Z ), sdtpldt0( Y, Z ) ) }.
% 11.04/11.43 (23108) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) =
% 11.04/11.43 sdtpldt0( Z, Y ) }.
% 11.04/11.43 (23109) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0(
% 11.04/11.43 Z, X ), sdtpldt0( Z, Y ) ) }.
% 11.04/11.43 (23110) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) =
% 11.04/11.43 sdtpldt0( Y, Z ) }.
% 11.04/11.43 (23111) {G0,W25,D3,L4,V3,M4} { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), !
% 11.04/11.43 sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) =
% 11.04/11.43 sdtpldt0( Y, Z ), alpha5( X, Y, Z ) }.
% 11.04/11.43 (23112) {G0,W19,D2,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 11.04/11.43 alpha6( X, Y, Z ) }.
% 11.04/11.43 (23113) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 11.04/11.43 sdtlseqdt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 11.04/11.43 (23114) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) =
% 11.04/11.43 sdtasdt0( X, Z ) }.
% 11.04/11.43 (23115) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0(
% 11.04/11.43 X, Y ), sdtasdt0( X, Z ) ) }.
% 11.04/11.43 (23116) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) =
% 11.04/11.43 sdtasdt0( Z, X ) }.
% 11.04/11.43 (23117) {G0,W25,D3,L4,V3,M4} { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), !
% 11.04/11.43 sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) =
% 11.04/11.43 sdtasdt0( Z, X ), alpha6( X, Y, Z ) }.
% 11.04/11.43 (23118) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 11.04/11.43 , ! sz10 = X }.
% 11.04/11.43 (23119) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 11.04/11.43 , sdtlseqdt0( sz10, X ) }.
% 11.04/11.43 (23120) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), X = sz00, sdtlseqdt0( Y, sdtasdt0( Y, X ) ) }.
% 11.04/11.43 (23121) {G0,W1,D1,L1,V0,M1} { && }.
% 11.04/11.43 (23122) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), X = Y, ! sdtlseqdt0( X, Y ), iLess0( X, Y ) }.
% 11.04/11.43 (23123) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! doDivides0( X, Y ), aNaturalNumber0( skol2( Z, T ) ) }.
% 11.04/11.43 (23124) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! doDivides0( X, Y ), Y = sdtasdt0( X, skol2( X, Y ) ) }.
% 11.04/11.43 (23125) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 11.04/11.43 }.
% 11.04/11.43 (23126) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 11.04/11.43 aNaturalNumber0( Z ) }.
% 11.04/11.43 (23127) {G0,W20,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0
% 11.04/11.43 ( X, Z ) }.
% 11.04/11.43 (23128) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), ! Y =
% 11.04/11.43 sdtasdt0( X, Z ), Z = sdtsldt0( Y, X ) }.
% 11.04/11.43 (23129) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( Y, Z ),
% 11.04/11.43 doDivides0( X, Z ) }.
% 11.04/11.43 (23130) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X, Z ),
% 11.04/11.43 doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 11.04/11.43 (23131) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X,
% 11.04/11.43 sdtpldt0( Y, Z ) ), doDivides0( X, Z ) }.
% 11.04/11.43 (23132) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! doDivides0( X, Y ), Y = sz00, sdtlseqdt0( X, Y ) }.
% 11.04/11.43 (23133) {G0,W23,D4,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z
% 11.04/11.43 , sdtsldt0( Y, X ) ) = sdtsldt0( sdtasdt0( Z, Y ), X ) }.
% 11.04/11.43 (23134) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X
% 11.04/11.43 = sz00 }.
% 11.04/11.43 (23135) {G0,W6,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ),
% 11.04/11.43 alpha1( X ) }.
% 11.04/11.43 (23136) {G0,W9,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, ! alpha1(
% 11.04/11.43 X ), isPrime0( X ) }.
% 11.04/11.43 (23137) {G0,W5,D2,L2,V1,M2} { ! alpha1( X ), ! X = sz10 }.
% 11.04/11.43 (23138) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), alpha2( X ) }.
% 11.04/11.43 (23139) {G0,W7,D2,L3,V1,M3} { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 11.04/11.43 (23140) {G0,W8,D2,L3,V2,M3} { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X,
% 11.04/11.43 Y ) }.
% 11.04/11.43 (23141) {G0,W6,D3,L2,V1,M2} { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 11.04/11.43 (23142) {G0,W6,D3,L2,V1,M2} { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 11.04/11.43 (23143) {G0,W9,D2,L3,V2,M3} { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 11.04/11.43 (23144) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha4( X, Y ) }.
% 11.04/11.43 (23145) {G0,W6,D2,L2,V2,M2} { ! Y = X, alpha4( X, Y ) }.
% 11.04/11.43 (23146) {G0,W5,D2,L2,V2,M2} { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 11.04/11.43 (23147) {G0,W6,D2,L2,V2,M2} { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 11.04/11.43 (23148) {G0,W8,D2,L3,V2,M3} { ! aNaturalNumber0( Y ), ! doDivides0( Y, X )
% 11.04/11.43 , alpha3( X, Y ) }.
% 11.04/11.43 (23149) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 11.04/11.43 , aNaturalNumber0( skol4( Y ) ) }.
% 11.04/11.43 (23150) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 11.04/11.43 , isPrime0( skol4( Y ) ) }.
% 11.04/11.43 (23151) {G0,W12,D3,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 11.04/11.43 , doDivides0( skol4( X ), X ) }.
% 11.04/11.43 (23152) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 11.04/11.43 (23153) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 11.04/11.43 (23154) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 11.04/11.43 (23155) {G0,W30,D4,L8,V3,M8} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 11.04/11.43 Y ), ! aNaturalNumber0( Z ), ! isPrime0( Z ), ! doDivides0( Z, sdtasdt0(
% 11.04/11.43 X, Y ) ), ! iLess0( sdtpldt0( sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0(
% 11.04/11.43 xn, xm ), xp ) ), doDivides0( Z, X ), doDivides0( Z, Y ) }.
% 11.04/11.43 (23156) {G0,W2,D2,L1,V0,M1} { isPrime0( xp ) }.
% 11.04/11.43 (23157) {G0,W5,D3,L1,V0,M1} { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 11.04/11.43 (23158) {G0,W3,D2,L1,V0,M1} { ! sdtlseqdt0( xp, xn ) }.
% 11.04/11.43 (23159) {G0,W3,D2,L1,V0,M1} { ! sdtlseqdt0( xp, xm ) }.
% 11.04/11.43 (23160) {G0,W3,D2,L1,V0,M1} { ! xn = xp }.
% 11.04/11.43 (23161) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xn, xp ) }.
% 11.04/11.43 (23162) {G0,W3,D2,L1,V0,M1} { ! xm = xp }.
% 11.04/11.43 (23163) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xm, xp ) }.
% 11.04/11.43 (23164) {G0,W7,D4,L1,V0,M1} { xk = sdtsldt0( sdtasdt0( xn, xm ), xp ) }.
% 11.04/11.43 (23165) {G0,W3,D2,L1,V0,M1} { ! xk = sz00 }.
% 11.04/11.43 (23166) {G0,W3,D2,L1,V0,M1} { ! xk = sz10 }.
% 11.04/11.43 (23167) {G0,W3,D2,L1,V0,M1} { ! xk = sz00 }.
% 11.04/11.43 (23168) {G0,W3,D2,L1,V0,M1} { ! xk = sz10 }.
% 11.04/11.43 (23169) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! doDivides0( X, xk
% 11.04/11.43 ), ! isPrime0( X ) }.
% 11.04/11.43
% 11.04/11.43
% 11.04/11.43 Total Proof:
% 11.04/11.43
% 11.04/11.43 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 11.04/11.43 parent0: (23071) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 11.04/11.43 substitution0:
% 11.04/11.43 end
% 11.04/11.43 permutation0:
% 11.04/11.43 0 ==> 0
% 11.04/11.43 end
% 11.04/11.43
% 11.04/11.43 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 11.04/11.43 parent0: (23072) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 11.04/11.43 substitution0:
% 11.04/11.43 end
% 11.04/11.43 permutation0:
% 11.04/11.43 0 ==> 0
% 11.04/11.43 end
% 11.04/11.43
% 11.04/11.43 subsumption: (3) {G0,W3,D2,L1,V0,M1} I { ! sz10 ==> sz00 }.
% 11.04/11.43 parent0: (23073) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 11.04/11.43 substitution0:
% 11.04/11.43 end
% 11.04/11.43 permutation0:
% 11.04/11.43 0 ==> 0
% 11.04/11.43 end
% 11.04/11.43
% 11.04/11.43 subsumption: (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 11.04/11.43 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 11.04/11.43 parent0: (23075) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 11.04/11.43 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 11.04/11.43 substitution0:
% 11.04/11.43 X := X
% 11.04/11.43 Y := Y
% 11.04/11.43 end
% 11.04/11.43 permutation0:
% 11.04/11.43 0 ==> 0
% 11.04/11.43 1 ==> 1
% 11.04/11.43 2 ==> 2
% 11.04/11.43 end
% 11.04/11.43
% 11.04/11.43 subsumption: (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 11.04/11.43 X, sz00 ) ==> X }.
% 11.04/11.43 parent0: (23078) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X
% 11.04/11.43 , sz00 ) = X }.
% 11.04/11.43 substitution0:
% 11.04/11.43 X := X
% 11.04/11.43 end
% 11.04/11.43 permutation0:
% 11.04/11.43 0 ==> 0
% 11.04/11.43 1 ==> 1
% 11.04/11.43 end
% 11.04/11.43
% 11.04/11.43 subsumption: (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 11.04/11.43 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 11.04/11.43 sdtpldt0( X, Z ), Y = Z }.
% 11.04/11.43 parent0: (23088) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 11.04/11.43 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 11.04/11.43 sdtpldt0( X, Z ), Y = Z }.
% 11.04/11.43 substitution0:
% 11.04/11.43 X := X
% 11.04/11.43 Y := Y
% 11.04/11.43 Z := Z
% 11.04/11.43 end
% 11.04/11.43 permutation0:
% 11.04/11.43 0 ==> 0
% 11.04/11.43 1 ==> 1
% 11.04/11.43 2 ==> 2
% 11.04/11.43 3 ==> 3
% 11.04/11.43 4 ==> 4
% 11.04/11.43 end
% 11.04/11.43
% 11.04/11.43 subsumption: (20) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), X = sz00
% 11.04/11.43 , ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 11.04/11.43 sdtasdt0( X, Z ), Y = Z }.
% 11.04/11.43 parent0: (23090) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00,
% 11.04/11.43 ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 11.04/11.43 sdtasdt0( X, Z ), Y = Z }.
% 11.04/11.43 substitution0:
% 11.04/11.43 X := X
% 11.04/11.43 Y := Y
% 11.04/11.43 Z := Z
% 11.04/11.43 end
% 11.04/11.43 permutation0:
% 11.04/11.43 0 ==> 0
% 11.04/11.43 1 ==> 1
% 11.04/11.43 2 ==> 2
% 11.04/11.43 3 ==> 3
% 11.04/11.43 4 ==> 4
% 11.04/11.43 5 ==> 5
% 11.04/11.43 end
% 11.04/11.43
% 11.04/11.43 subsumption: (22) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 11.04/11.43 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, X = sz00 }.
% 11.04/11.45 parent0: (23092) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 11.04/11.45 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 Y := Y
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 2 ==> 2
% 11.04/11.45 3 ==> 3
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (48) {G0,W11,D2,L4,V1,M4} I { ! aNaturalNumber0( X ), X = sz00
% 11.04/11.45 , X = sz10, ! sz10 = X }.
% 11.04/11.45 parent0: (23118) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00,
% 11.04/11.45 X = sz10, ! sz10 = X }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 2 ==> 2
% 11.04/11.45 3 ==> 3
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (55) {G0,W17,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), !
% 11.04/11.45 aNaturalNumber0( Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y,
% 11.04/11.45 X ), aNaturalNumber0( Z ) }.
% 11.04/11.45 parent0: (23126) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), !
% 11.04/11.45 aNaturalNumber0( Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y,
% 11.04/11.45 X ), aNaturalNumber0( Z ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 Y := Y
% 11.04/11.45 Z := Z
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 2 ==> 2
% 11.04/11.45 3 ==> 3
% 11.04/11.45 4 ==> 4
% 11.04/11.45 5 ==> 5
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (63) {G0,W7,D2,L3,V1,M3} I { ! aNaturalNumber0( X ), !
% 11.04/11.45 isPrime0( X ), ! X = sz00 }.
% 11.04/11.45 parent0: (23134) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0
% 11.04/11.45 ( X ), ! X = sz00 }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 2 ==> 2
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (72) {G0,W9,D2,L3,V2,M3} I { ! alpha4( X, Y ), Y = sz10, Y = X
% 11.04/11.45 }.
% 11.04/11.45 parent0: (23143) {G0,W9,D2,L3,V2,M3} { ! alpha4( X, Y ), Y = sz10, Y = X
% 11.04/11.45 }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 Y := Y
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 2 ==> 2
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 11.04/11.45 parent0: (23144) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha4( X, Y ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 Y := Y
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (74) {G0,W6,D2,L2,V2,M2} I { ! Y = X, alpha4( X, Y ) }.
% 11.04/11.45 parent0: (23145) {G0,W6,D2,L2,V2,M2} { ! Y = X, alpha4( X, Y ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 Y := Y
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (78) {G0,W11,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), X = sz00
% 11.04/11.45 , X = sz10, aNaturalNumber0( skol4( Y ) ) }.
% 11.04/11.45 parent0: (23149) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00,
% 11.04/11.45 X = sz10, aNaturalNumber0( skol4( Y ) ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 Y := Y
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 2 ==> 2
% 11.04/11.45 3 ==> 3
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (79) {G0,W11,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), X = sz00
% 11.04/11.45 , X = sz10, isPrime0( skol4( Y ) ) }.
% 11.04/11.45 parent0: (23150) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00,
% 11.04/11.45 X = sz10, isPrime0( skol4( Y ) ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 Y := Y
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 2 ==> 2
% 11.04/11.45 3 ==> 3
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (80) {G0,W12,D3,L4,V1,M4} I { ! aNaturalNumber0( X ), X = sz00
% 11.04/11.45 , X = sz10, doDivides0( skol4( X ), X ) }.
% 11.04/11.45 parent0: (23151) {G0,W12,D3,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00,
% 11.04/11.45 X = sz10, doDivides0( skol4( X ), X ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 X := X
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 1 ==> 1
% 11.04/11.45 2 ==> 2
% 11.04/11.45 3 ==> 3
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (81) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 11.04/11.45 parent0: (23152) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (82) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 11.04/11.45 parent0: (23153) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 11.04/11.45 parent0: (23154) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (85) {G0,W2,D2,L1,V0,M1} I { isPrime0( xp ) }.
% 11.04/11.45 parent0: (23156) {G0,W2,D2,L1,V0,M1} { isPrime0( xp ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 subsumption: (86) {G0,W5,D3,L1,V0,M1} I { doDivides0( xp, sdtasdt0( xn, xm
% 11.04/11.45 ) ) }.
% 11.04/11.45 parent0: (23157) {G0,W5,D3,L1,V0,M1} { doDivides0( xp, sdtasdt0( xn, xm )
% 11.04/11.45 ) }.
% 11.04/11.45 substitution0:
% 11.04/11.45 end
% 11.04/11.45 permutation0:
% 11.04/11.45 0 ==> 0
% 11.04/11.45 end
% 11.04/11.45
% 11.04/11.45 eqswap: (29454) {G0,W7,D4,L1,V0,M1} { sdtsldt0( sdtasdt0( xn, xm ), xp ) =
% 11.04/11.45 xk }.
% 11.04/11.45 parent0[0]: (23164) {G0,W7,D4,L1,V0,M1} { xk = sdtsldt0( sdtasdt0( xn, xm
% 13.43/13.82 ), xp ) }.
% 13.43/13.82 substitution0:
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 subsumption: (93) {G0,W7,D4,L1,V0,M1} I { sdtsldt0( sdtasdt0( xn, xm ), xp
% 13.43/13.82 ) ==> xk }.
% 13.43/13.82 parent0: (29454) {G0,W7,D4,L1,V0,M1} { sdtsldt0( sdtasdt0( xn, xm ), xp )
% 13.43/13.82 = xk }.
% 13.43/13.82 substitution0:
% 13.43/13.82 end
% 13.43/13.82 permutation0:
% 13.43/13.82 0 ==> 0
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 subsumption: (94) {G0,W3,D2,L1,V0,M1} I { ! xk ==> sz00 }.
% 13.43/13.82 parent0: (23165) {G0,W3,D2,L1,V0,M1} { ! xk = sz00 }.
% 13.43/13.82 substitution0:
% 13.43/13.82 end
% 13.43/13.82 permutation0:
% 13.43/13.82 0 ==> 0
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 subsumption: (95) {G0,W3,D2,L1,V0,M1} I { ! xk ==> sz10 }.
% 13.43/13.82 parent0: (23166) {G0,W3,D2,L1,V0,M1} { ! xk = sz10 }.
% 13.43/13.82 substitution0:
% 13.43/13.82 end
% 13.43/13.82 permutation0:
% 13.43/13.82 0 ==> 0
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 subsumption: (96) {G0,W7,D2,L3,V1,M3} I { ! aNaturalNumber0( X ), !
% 13.43/13.82 doDivides0( X, xk ), ! isPrime0( X ) }.
% 13.43/13.82 parent0: (23169) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), !
% 13.43/13.82 doDivides0( X, xk ), ! isPrime0( X ) }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := X
% 13.43/13.82 end
% 13.43/13.82 permutation0:
% 13.43/13.82 0 ==> 0
% 13.43/13.82 1 ==> 1
% 13.43/13.82 2 ==> 2
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 eqswap: (30749) {G0,W7,D2,L3,V1,M3} { ! sz00 = X, ! aNaturalNumber0( X ),
% 13.43/13.82 ! isPrime0( X ) }.
% 13.43/13.82 parent0[2]: (63) {G0,W7,D2,L3,V1,M3} I { ! aNaturalNumber0( X ), ! isPrime0
% 13.43/13.82 ( X ), ! X = sz00 }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := X
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 eqrefl: (30750) {G0,W4,D2,L2,V0,M2} { ! aNaturalNumber0( sz00 ), !
% 13.43/13.82 isPrime0( sz00 ) }.
% 13.43/13.82 parent0[0]: (30749) {G0,W7,D2,L3,V1,M3} { ! sz00 = X, ! aNaturalNumber0( X
% 13.43/13.82 ), ! isPrime0( X ) }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := sz00
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 resolution: (30751) {G1,W2,D2,L1,V0,M1} { ! isPrime0( sz00 ) }.
% 13.43/13.82 parent0[0]: (30750) {G0,W4,D2,L2,V0,M2} { ! aNaturalNumber0( sz00 ), !
% 13.43/13.82 isPrime0( sz00 ) }.
% 13.43/13.82 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 13.43/13.82 substitution0:
% 13.43/13.82 end
% 13.43/13.82 substitution1:
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 subsumption: (225) {G1,W2,D2,L1,V0,M1} Q(63);r(1) { ! isPrime0( sz00 ) }.
% 13.43/13.82 parent0: (30751) {G1,W2,D2,L1,V0,M1} { ! isPrime0( sz00 ) }.
% 13.43/13.82 substitution0:
% 13.43/13.82 end
% 13.43/13.82 permutation0:
% 13.43/13.82 0 ==> 0
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 factor: (30755) {G0,W6,D2,L2,V1,M2} { ! alpha4( sz10, X ), X = sz10 }.
% 13.43/13.82 parent0[1, 2]: (72) {G0,W9,D2,L3,V2,M3} I { ! alpha4( X, Y ), Y = sz10, Y =
% 13.43/13.82 X }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := sz10
% 13.43/13.82 Y := X
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 subsumption: (227) {G1,W6,D2,L2,V1,M2} F(72) { ! alpha4( sz10, X ), X =
% 13.43/13.82 sz10 }.
% 13.43/13.82 parent0: (30755) {G0,W6,D2,L2,V1,M2} { ! alpha4( sz10, X ), X = sz10 }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := X
% 13.43/13.82 end
% 13.43/13.82 permutation0:
% 13.43/13.82 0 ==> 0
% 13.43/13.82 1 ==> 1
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 resolution: (30758) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 13.43/13.82 aNaturalNumber0( sdtasdt0( X, xm ) ) }.
% 13.43/13.82 parent0[1]: (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 13.43/13.82 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 13.43/13.82 parent1[0]: (82) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := X
% 13.43/13.82 Y := xm
% 13.43/13.82 end
% 13.43/13.82 substitution1:
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 subsumption: (255) {G1,W6,D3,L2,V1,M2} R(5,82) { ! aNaturalNumber0( X ),
% 13.43/13.82 aNaturalNumber0( sdtasdt0( X, xm ) ) }.
% 13.43/13.82 parent0: (30758) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 13.43/13.82 aNaturalNumber0( sdtasdt0( X, xm ) ) }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := X
% 13.43/13.82 end
% 13.43/13.82 permutation0:
% 13.43/13.82 0 ==> 0
% 13.43/13.82 1 ==> 1
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 eqswap: (30759) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( X, sz00 ), !
% 13.43/13.82 aNaturalNumber0( X ) }.
% 13.43/13.82 parent0[1]: (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( X
% 13.43/13.82 , sz00 ) ==> X }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := X
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 resolution: (30760) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtpldt0( sz00, sz00 )
% 13.43/13.82 }.
% 13.43/13.82 parent0[1]: (30759) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( X, sz00 ), !
% 13.43/13.82 aNaturalNumber0( X ) }.
% 13.43/13.82 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 13.43/13.82 substitution0:
% 13.43/13.82 X := sz00
% 13.43/13.82 end
% 13.43/13.82 substitution1:
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 eqswap: (30761) {G1,W5,D3,L1,V0,M1} { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 13.43/13.82 parent0[0]: (30760) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtpldt0( sz00, sz00 )
% 13.43/13.82 }.
% 13.43/13.82 substitution0:
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 subsumption: (345) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==>
% 13.43/13.82 sz00 }.
% 13.43/13.82 parent0: (30761) {G1,W5,D3,L1,V0,M1} { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 13.43/13.82 substitution0:
% 13.43/13.82 end
% 13.43/13.82 permutation0:
% 13.43/13.82 0 ==> 0
% 13.43/13.82 end
% 13.43/13.82
% 13.43/13.82 *** allocated 15000 integers for justifications
% 13.43/13.82 *** allocated 864960 integers for termspace/termends
% 13.43/13.82 *** allocated 22500 integers for justifications
% 13.43/13.82 *** allocated 33750 integers for justifications
% 13.43/13.82 *** allocated 50625 integers for justifications
% 13.43/13.82 eqswap: (30762) {G1,W6,D2,L2,V1,M2} { sz10 = X, ! alpha4( sz10, X ) }.
% 14.60/14.98 parent0[1]: (227) {G1,W6,D2,L2,V1,M2} F(72) { ! alpha4( sz10, X ), X = sz10
% 14.60/14.98 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (30763) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> sz10 }.
% 14.60/14.98 parent0[0]: (3) {G0,W3,D2,L1,V0,M1} I { ! sz10 ==> sz00 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 paramod: (30764) {G1,W6,D2,L2,V1,M2} { ! sz00 ==> X, ! alpha4( sz10, X )
% 14.60/14.98 }.
% 14.60/14.98 parent0[0]: (30762) {G1,W6,D2,L2,V1,M2} { sz10 = X, ! alpha4( sz10, X )
% 14.60/14.98 }.
% 14.60/14.98 parent1[0; 3]: (30763) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> sz10 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98 substitution1:
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (30785) {G1,W6,D2,L2,V1,M2} { ! X ==> sz00, ! alpha4( sz10, X )
% 14.60/14.98 }.
% 14.60/14.98 parent0[0]: (30764) {G1,W6,D2,L2,V1,M2} { ! sz00 ==> X, ! alpha4( sz10, X
% 14.60/14.98 ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 subsumption: (442) {G2,W6,D2,L2,V1,M2} P(227,3) { ! X = sz00, ! alpha4(
% 14.60/14.98 sz10, X ) }.
% 14.60/14.98 parent0: (30785) {G1,W6,D2,L2,V1,M2} { ! X ==> sz00, ! alpha4( sz10, X )
% 14.60/14.98 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98 permutation0:
% 14.60/14.98 0 ==> 0
% 14.60/14.98 1 ==> 1
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (31672) {G1,W6,D2,L2,V1,M2} { sz10 = X, ! alpha4( sz10, X ) }.
% 14.60/14.98 parent0[1]: (227) {G1,W6,D2,L2,V1,M2} F(72) { ! alpha4( sz10, X ), X = sz10
% 14.60/14.98 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 paramod: (31673) {G1,W5,D2,L2,V1,M2} { aNaturalNumber0( X ), ! alpha4(
% 14.60/14.98 sz10, X ) }.
% 14.60/14.98 parent0[0]: (31672) {G1,W6,D2,L2,V1,M2} { sz10 = X, ! alpha4( sz10, X )
% 14.60/14.98 }.
% 14.60/14.98 parent1[0; 1]: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98 substitution1:
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 subsumption: (443) {G2,W5,D2,L2,V1,M2} P(227,2) { aNaturalNumber0( X ), !
% 14.60/14.98 alpha4( sz10, X ) }.
% 14.60/14.98 parent0: (31673) {G1,W5,D2,L2,V1,M2} { aNaturalNumber0( X ), ! alpha4(
% 14.60/14.98 sz10, X ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98 permutation0:
% 14.60/14.98 0 ==> 0
% 14.60/14.98 1 ==> 1
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32127) {G0,W6,D2,L2,V2,M2} { ! sz10 = X, alpha4( Y, X ) }.
% 14.60/14.98 parent0[0]: (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := Y
% 14.60/14.98 Y := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 resolution: (32128) {G1,W5,D2,L2,V1,M2} { aNaturalNumber0( X ), ! sz10 = X
% 14.60/14.98 }.
% 14.60/14.98 parent0[1]: (443) {G2,W5,D2,L2,V1,M2} P(227,2) { aNaturalNumber0( X ), !
% 14.60/14.98 alpha4( sz10, X ) }.
% 14.60/14.98 parent1[1]: (32127) {G0,W6,D2,L2,V2,M2} { ! sz10 = X, alpha4( Y, X ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98 substitution1:
% 14.60/14.98 X := X
% 14.60/14.98 Y := sz10
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32129) {G1,W5,D2,L2,V1,M2} { ! X = sz10, aNaturalNumber0( X ) }.
% 14.60/14.98 parent0[1]: (32128) {G1,W5,D2,L2,V1,M2} { aNaturalNumber0( X ), ! sz10 = X
% 14.60/14.98 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 subsumption: (455) {G3,W5,D2,L2,V1,M2} R(443,73) { aNaturalNumber0( X ), !
% 14.60/14.98 X = sz10 }.
% 14.60/14.98 parent0: (32129) {G1,W5,D2,L2,V1,M2} { ! X = sz10, aNaturalNumber0( X )
% 14.60/14.98 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98 permutation0:
% 14.60/14.98 0 ==> 1
% 14.60/14.98 1 ==> 0
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32130) {G2,W6,D2,L2,V1,M2} { ! sz00 = X, ! alpha4( sz10, X ) }.
% 14.60/14.98 parent0[0]: (442) {G2,W6,D2,L2,V1,M2} P(227,3) { ! X = sz00, ! alpha4( sz10
% 14.60/14.98 , X ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32131) {G0,W6,D2,L2,V2,M2} { ! sz10 = X, alpha4( Y, X ) }.
% 14.60/14.98 parent0[0]: (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := Y
% 14.60/14.98 Y := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 resolution: (32132) {G1,W6,D2,L2,V1,M2} { ! sz00 = X, ! sz10 = X }.
% 14.60/14.98 parent0[1]: (32130) {G2,W6,D2,L2,V1,M2} { ! sz00 = X, ! alpha4( sz10, X )
% 14.60/14.98 }.
% 14.60/14.98 parent1[1]: (32131) {G0,W6,D2,L2,V2,M2} { ! sz10 = X, alpha4( Y, X ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98 substitution1:
% 14.60/14.98 X := X
% 14.60/14.98 Y := sz10
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32134) {G1,W6,D2,L2,V1,M2} { ! X = sz10, ! sz00 = X }.
% 14.60/14.98 parent0[1]: (32132) {G1,W6,D2,L2,V1,M2} { ! sz00 = X, ! sz10 = X }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32135) {G1,W6,D2,L2,V1,M2} { ! X = sz00, ! X = sz10 }.
% 14.60/14.98 parent0[1]: (32134) {G1,W6,D2,L2,V1,M2} { ! X = sz10, ! sz00 = X }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 subsumption: (735) {G3,W6,D2,L2,V1,M2} R(442,73) { ! X = sz00, ! X = sz10
% 14.60/14.98 }.
% 14.60/14.98 parent0: (32135) {G1,W6,D2,L2,V1,M2} { ! X = sz00, ! X = sz10 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98 permutation0:
% 14.60/14.98 0 ==> 0
% 14.60/14.98 1 ==> 1
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32136) {G0,W19,D3,L6,V3,M6} { sz00 = X, ! aNaturalNumber0( X ), !
% 14.60/14.98 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 14.60/14.98 sdtasdt0( X, Z ), Y = Z }.
% 14.60/14.98 parent0[1]: (20) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), X = sz00
% 14.60/14.98 , ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 14.60/14.98 sdtasdt0( X, Z ), Y = Z }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 Y := Y
% 14.60/14.98 Z := Z
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 resolution: (32141) {G1,W17,D3,L5,V2,M5} { sz00 = X, ! aNaturalNumber0( X
% 14.60/14.98 ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sdtasdt0( X, xp ), Y =
% 14.60/14.98 xp }.
% 14.60/14.98 parent0[3]: (32136) {G0,W19,D3,L6,V3,M6} { sz00 = X, ! aNaturalNumber0( X
% 14.60/14.98 ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 14.60/14.98 sdtasdt0( X, Z ), Y = Z }.
% 14.60/14.98 parent1[0]: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 Y := Y
% 14.60/14.98 Z := xp
% 14.60/14.98 end
% 14.60/14.98 substitution1:
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32144) {G1,W17,D3,L5,V2,M5} { xp = X, sz00 = Y, ! aNaturalNumber0
% 14.60/14.98 ( Y ), ! aNaturalNumber0( X ), ! sdtasdt0( Y, X ) = sdtasdt0( Y, xp ) }.
% 14.60/14.98 parent0[4]: (32141) {G1,W17,D3,L5,V2,M5} { sz00 = X, ! aNaturalNumber0( X
% 14.60/14.98 ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sdtasdt0( X, xp ), Y =
% 14.60/14.98 xp }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := Y
% 14.60/14.98 Y := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32145) {G1,W17,D3,L5,V2,M5} { X = sz00, xp = Y, ! aNaturalNumber0
% 14.60/14.98 ( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sdtasdt0( X, xp ) }.
% 14.60/14.98 parent0[1]: (32144) {G1,W17,D3,L5,V2,M5} { xp = X, sz00 = Y, !
% 14.60/14.98 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtasdt0( Y, X ) =
% 14.60/14.98 sdtasdt0( Y, xp ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := Y
% 14.60/14.98 Y := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32146) {G1,W17,D3,L5,V2,M5} { ! sdtasdt0( X, xp ) = sdtasdt0( X,
% 14.60/14.98 Y ), X = sz00, xp = Y, ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 14.60/14.98 parent0[4]: (32145) {G1,W17,D3,L5,V2,M5} { X = sz00, xp = Y, !
% 14.60/14.98 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) =
% 14.60/14.98 sdtasdt0( X, xp ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 Y := Y
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 subsumption: (907) {G1,W17,D3,L5,V2,M5} R(20,83) { ! aNaturalNumber0( X ),
% 14.60/14.98 X = sz00, ! aNaturalNumber0( Y ), ! sdtasdt0( X, xp ) = sdtasdt0( X, Y )
% 14.60/14.98 , xp = Y }.
% 14.60/14.98 parent0: (32146) {G1,W17,D3,L5,V2,M5} { ! sdtasdt0( X, xp ) = sdtasdt0( X
% 14.60/14.98 , Y ), X = sz00, xp = Y, ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 14.60/14.98 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 Y := Y
% 14.60/14.98 end
% 14.60/14.98 permutation0:
% 14.60/14.98 0 ==> 3
% 14.60/14.98 1 ==> 1
% 14.60/14.98 2 ==> 4
% 14.60/14.98 3 ==> 0
% 14.60/14.98 4 ==> 2
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32167) {G1,W17,D3,L5,V2,M5} { X = xp, ! aNaturalNumber0( Y ), Y =
% 14.60/14.98 sz00, ! aNaturalNumber0( X ), ! sdtasdt0( Y, xp ) = sdtasdt0( Y, X ) }.
% 14.60/14.98 parent0[4]: (907) {G1,W17,D3,L5,V2,M5} R(20,83) { ! aNaturalNumber0( X ), X
% 14.60/14.98 = sz00, ! aNaturalNumber0( Y ), ! sdtasdt0( X, xp ) = sdtasdt0( X, Y ),
% 14.60/14.98 xp = Y }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := Y
% 14.60/14.98 Y := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32169) {G1,W17,D3,L5,V2,M5} { ! sdtasdt0( X, Y ) = sdtasdt0( X,
% 14.60/14.98 xp ), Y = xp, ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y )
% 14.60/14.98 }.
% 14.60/14.98 parent0[4]: (32167) {G1,W17,D3,L5,V2,M5} { X = xp, ! aNaturalNumber0( Y )
% 14.60/14.98 , Y = sz00, ! aNaturalNumber0( X ), ! sdtasdt0( Y, xp ) = sdtasdt0( Y, X
% 14.60/14.98 ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := Y
% 14.60/14.98 Y := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqfact: (32250) {G0,W17,D3,L5,V1,M5} { ! xp = sz00, ! sdtasdt0( X, X ) =
% 14.60/14.98 sdtasdt0( X, xp ), ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( X
% 14.60/14.98 ) }.
% 14.60/14.98 parent0[1, 3]: (32169) {G1,W17,D3,L5,V2,M5} { ! sdtasdt0( X, Y ) =
% 14.60/14.98 sdtasdt0( X, xp ), Y = xp, ! aNaturalNumber0( X ), X = sz00, !
% 14.60/14.98 aNaturalNumber0( Y ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 Y := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 factor: (32253) {G0,W15,D3,L4,V1,M4} { ! xp = sz00, ! sdtasdt0( X, X ) =
% 14.60/14.98 sdtasdt0( X, xp ), ! aNaturalNumber0( X ), X = sz00 }.
% 14.60/14.98 parent0[2, 4]: (32250) {G0,W17,D3,L5,V1,M5} { ! xp = sz00, ! sdtasdt0( X,
% 14.60/14.98 X ) = sdtasdt0( X, xp ), ! aNaturalNumber0( X ), X = sz00, !
% 14.60/14.98 aNaturalNumber0( X ) }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 eqswap: (32255) {G0,W15,D3,L4,V1,M4} { ! sdtasdt0( X, xp ) = sdtasdt0( X,
% 14.60/14.98 X ), ! xp = sz00, ! aNaturalNumber0( X ), X = sz00 }.
% 14.60/14.98 parent0[1]: (32253) {G0,W15,D3,L4,V1,M4} { ! xp = sz00, ! sdtasdt0( X, X )
% 14.60/14.98 = sdtasdt0( X, xp ), ! aNaturalNumber0( X ), X = sz00 }.
% 14.60/14.98 substitution0:
% 14.60/14.98 X := X
% 14.60/14.98 end
% 14.60/14.98
% 14.60/14.98 subsumption: (1008) {G2,W15,D3,L4,V1,M4} E(907);f { ! xp ==> sz00, !
% 14.60/14.98 aNaturalNumber0( X ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X )
% 14.60/14.98 }.
% 14.60/14.98 parent0: (32255) {G0,W15,D3,L4,V1,M4} { ! sdtasdt0( X, xp ) = sdtasdt0( X
% 14.60/14.98 , X ), ! xp = sz00, ! aNaturalNumber0( X ), X = sz00 }.
% 14.60/14.98 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45 permutation0:
% 15.05/15.45 0 ==> 3
% 15.05/15.45 1 ==> 0
% 15.05/15.45 2 ==> 1
% 15.05/15.45 3 ==> 2
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32282) {G2,W15,D3,L4,V1,M4} { ! sz00 ==> xp, ! aNaturalNumber0( X
% 15.05/15.45 ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X ) }.
% 15.05/15.45 parent0[0]: (1008) {G2,W15,D3,L4,V1,M4} E(907);f { ! xp ==> sz00, !
% 15.05/15.45 aNaturalNumber0( X ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X )
% 15.05/15.45 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqrefl: (32289) {G0,W8,D2,L3,V0,M3} { ! sz00 ==> xp, ! aNaturalNumber0( xp
% 15.05/15.45 ), xp = sz00 }.
% 15.05/15.45 parent0[3]: (32282) {G2,W15,D3,L4,V1,M4} { ! sz00 ==> xp, !
% 15.05/15.45 aNaturalNumber0( X ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X )
% 15.05/15.45 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := xp
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 resolution: (32290) {G1,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp = sz00 }.
% 15.05/15.45 parent0[1]: (32289) {G0,W8,D2,L3,V0,M3} { ! sz00 ==> xp, ! aNaturalNumber0
% 15.05/15.45 ( xp ), xp = sz00 }.
% 15.05/15.45 parent1[0]: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32291) {G1,W6,D2,L2,V0,M2} { ! xp ==> sz00, xp = sz00 }.
% 15.05/15.45 parent0[0]: (32290) {G1,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp = sz00 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 subsumption: (1011) {G3,W6,D2,L2,V0,M2} Q(1008);r(83) { ! xp ==> sz00, xp
% 15.05/15.45 ==> sz00 }.
% 15.05/15.45 parent0: (32291) {G1,W6,D2,L2,V0,M2} { ! xp ==> sz00, xp = sz00 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 permutation0:
% 15.05/15.45 0 ==> 0
% 15.05/15.45 1 ==> 1
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32294) {G0,W12,D3,L4,V2,M4} { ! sz00 ==> sdtpldt0( X, Y ), !
% 15.05/15.45 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00 }.
% 15.05/15.45 parent0[2]: (22) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 15.05/15.45 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, X = sz00 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 Y := Y
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 paramod: (32297) {G1,W11,D3,L4,V1,M4} { isPrime0( sz00 ), ! sz00 ==>
% 15.05/15.45 sdtpldt0( xp, X ), ! aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 15.05/15.45 parent0[3]: (32294) {G0,W12,D3,L4,V2,M4} { ! sz00 ==> sdtpldt0( X, Y ), !
% 15.05/15.45 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00 }.
% 15.05/15.45 parent1[0; 1]: (85) {G0,W2,D2,L1,V0,M1} I { isPrime0( xp ) }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := xp
% 15.05/15.45 Y := X
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 resolution: (32837) {G2,W9,D3,L3,V1,M3} { ! sz00 ==> sdtpldt0( xp, X ), !
% 15.05/15.45 aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 15.05/15.45 parent0[0]: (225) {G1,W2,D2,L1,V0,M1} Q(63);r(1) { ! isPrime0( sz00 ) }.
% 15.05/15.45 parent1[0]: (32297) {G1,W11,D3,L4,V1,M4} { isPrime0( sz00 ), ! sz00 ==>
% 15.05/15.45 sdtpldt0( xp, X ), ! aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32838) {G2,W9,D3,L3,V1,M3} { ! sdtpldt0( xp, X ) ==> sz00, !
% 15.05/15.45 aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 15.05/15.45 parent0[0]: (32837) {G2,W9,D3,L3,V1,M3} { ! sz00 ==> sdtpldt0( xp, X ), !
% 15.05/15.45 aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 subsumption: (1308) {G2,W9,D3,L3,V1,M3} P(22,85);r(225) { ! aNaturalNumber0
% 15.05/15.45 ( xp ), ! aNaturalNumber0( X ), ! sdtpldt0( xp, X ) ==> sz00 }.
% 15.05/15.45 parent0: (32838) {G2,W9,D3,L3,V1,M3} { ! sdtpldt0( xp, X ) ==> sz00, !
% 15.05/15.45 aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45 permutation0:
% 15.05/15.45 0 ==> 2
% 15.05/15.45 1 ==> 0
% 15.05/15.45 2 ==> 1
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 factor: (32843) {G2,W7,D3,L2,V0,M2} { ! aNaturalNumber0( xp ), ! sdtpldt0
% 15.05/15.45 ( xp, xp ) ==> sz00 }.
% 15.05/15.45 parent0[0, 1]: (1308) {G2,W9,D3,L3,V1,M3} P(22,85);r(225) { !
% 15.05/15.45 aNaturalNumber0( xp ), ! aNaturalNumber0( X ), ! sdtpldt0( xp, X ) ==>
% 15.05/15.45 sz00 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := xp
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 resolution: (32844) {G1,W5,D3,L1,V0,M1} { ! sdtpldt0( xp, xp ) ==> sz00
% 15.05/15.45 }.
% 15.05/15.45 parent0[0]: (32843) {G2,W7,D3,L2,V0,M2} { ! aNaturalNumber0( xp ), !
% 15.05/15.45 sdtpldt0( xp, xp ) ==> sz00 }.
% 15.05/15.45 parent1[0]: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 subsumption: (1309) {G3,W5,D3,L1,V0,M1} F(1308);r(83) { ! sdtpldt0( xp, xp
% 15.05/15.45 ) ==> sz00 }.
% 15.05/15.45 parent0: (32844) {G1,W5,D3,L1,V0,M1} { ! sdtpldt0( xp, xp ) ==> sz00 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 permutation0:
% 15.05/15.45 0 ==> 0
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32846) {G3,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp ==> sz00 }.
% 15.05/15.45 parent0[0]: (1011) {G3,W6,D2,L2,V0,M2} Q(1008);r(83) { ! xp ==> sz00, xp
% 15.05/15.45 ==> sz00 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32849) {G3,W5,D3,L1,V0,M1} { ! sz00 ==> sdtpldt0( xp, xp ) }.
% 15.05/15.45 parent0[0]: (1309) {G3,W5,D3,L1,V0,M1} F(1308);r(83) { ! sdtpldt0( xp, xp )
% 15.05/15.45 ==> sz00 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 paramod: (32852) {G4,W8,D3,L2,V0,M2} { ! sz00 ==> sdtpldt0( xp, sz00 ), !
% 15.05/15.45 sz00 ==> xp }.
% 15.05/15.45 parent0[1]: (32846) {G3,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp ==> sz00 }.
% 15.05/15.45 parent1[0; 5]: (32849) {G3,W5,D3,L1,V0,M1} { ! sz00 ==> sdtpldt0( xp, xp )
% 15.05/15.45 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 paramod: (32854) {G4,W11,D3,L3,V0,M3} { ! sz00 ==> sz00, ! sz00 ==> xp, !
% 15.05/15.45 sz00 ==> sdtpldt0( xp, sz00 ) }.
% 15.05/15.45 parent0[1]: (32846) {G3,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp ==> sz00 }.
% 15.05/15.45 parent1[1; 3]: (32852) {G4,W8,D3,L2,V0,M2} { ! sz00 ==> sdtpldt0( xp, sz00
% 15.05/15.45 ), ! sz00 ==> xp }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 paramod: (32856) {G4,W14,D3,L4,V0,M4} { ! sz00 ==> sdtpldt0( sz00, sz00 )
% 15.05/15.45 , ! sz00 ==> xp, ! sz00 ==> sz00, ! sz00 ==> xp }.
% 15.05/15.45 parent0[1]: (32846) {G3,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp ==> sz00 }.
% 15.05/15.45 parent1[2; 4]: (32854) {G4,W11,D3,L3,V0,M3} { ! sz00 ==> sz00, ! sz00 ==>
% 15.05/15.45 xp, ! sz00 ==> sdtpldt0( xp, sz00 ) }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 paramod: (32866) {G2,W12,D2,L4,V0,M4} { ! sz00 ==> sz00, ! sz00 ==> xp, !
% 15.05/15.45 sz00 ==> sz00, ! sz00 ==> xp }.
% 15.05/15.45 parent0[0]: (345) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==>
% 15.05/15.45 sz00 }.
% 15.05/15.45 parent1[0; 3]: (32856) {G4,W14,D3,L4,V0,M4} { ! sz00 ==> sdtpldt0( sz00,
% 15.05/15.45 sz00 ), ! sz00 ==> xp, ! sz00 ==> sz00, ! sz00 ==> xp }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 factor: (32867) {G2,W9,D2,L3,V0,M3} { ! sz00 ==> sz00, ! sz00 ==> xp, !
% 15.05/15.45 sz00 ==> xp }.
% 15.05/15.45 parent0[0, 2]: (32866) {G2,W12,D2,L4,V0,M4} { ! sz00 ==> sz00, ! sz00 ==>
% 15.05/15.45 xp, ! sz00 ==> sz00, ! sz00 ==> xp }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 factor: (32868) {G2,W6,D2,L2,V0,M2} { ! sz00 ==> sz00, ! sz00 ==> xp }.
% 15.05/15.45 parent0[1, 2]: (32867) {G2,W9,D2,L3,V0,M3} { ! sz00 ==> sz00, ! sz00 ==>
% 15.05/15.45 xp, ! sz00 ==> xp }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqrefl: (32869) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xp }.
% 15.05/15.45 parent0[0]: (32868) {G2,W6,D2,L2,V0,M2} { ! sz00 ==> sz00, ! sz00 ==> xp
% 15.05/15.45 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32870) {G0,W3,D2,L1,V0,M1} { ! xp ==> sz00 }.
% 15.05/15.45 parent0[0]: (32869) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xp }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 subsumption: (1375) {G4,W3,D2,L1,V0,M1} P(1011,1309);d(345);q { ! xp ==>
% 15.05/15.45 sz00 }.
% 15.05/15.45 parent0: (32870) {G0,W3,D2,L1,V0,M1} { ! xp ==> sz00 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 end
% 15.05/15.45 permutation0:
% 15.05/15.45 0 ==> 0
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32878) {G3,W5,D2,L2,V1,M2} { ! sz10 = X, aNaturalNumber0( X ) }.
% 15.05/15.45 parent0[1]: (455) {G3,W5,D2,L2,V1,M2} R(443,73) { aNaturalNumber0( X ), ! X
% 15.05/15.45 = sz10 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32880) {G3,W6,D2,L2,V1,M2} { ! sz10 = X, ! X = sz00 }.
% 15.05/15.45 parent0[1]: (735) {G3,W6,D2,L2,V1,M2} R(442,73) { ! X = sz00, ! X = sz10
% 15.05/15.45 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 resolution: (32882) {G1,W12,D2,L4,V1,M4} { X = sz00, X = sz10, ! sz10 = X
% 15.05/15.45 , ! sz10 = X }.
% 15.05/15.45 parent0[0]: (48) {G0,W11,D2,L4,V1,M4} I { ! aNaturalNumber0( X ), X = sz00
% 15.05/15.45 , X = sz10, ! sz10 = X }.
% 15.05/15.45 parent1[1]: (32878) {G3,W5,D2,L2,V1,M2} { ! sz10 = X, aNaturalNumber0( X )
% 15.05/15.45 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 factor: (32883) {G1,W9,D2,L3,V1,M3} { X = sz00, X = sz10, ! sz10 = X }.
% 15.05/15.45 parent0[2, 3]: (32882) {G1,W12,D2,L4,V1,M4} { X = sz00, X = sz10, ! sz10 =
% 15.05/15.45 X, ! sz10 = X }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 resolution: (32892) {G2,W9,D2,L3,V1,M3} { ! sz10 = X, X = sz10, ! sz10 = X
% 15.05/15.45 }.
% 15.05/15.45 parent0[1]: (32880) {G3,W6,D2,L2,V1,M2} { ! sz10 = X, ! X = sz00 }.
% 15.05/15.45 parent1[0]: (32883) {G1,W9,D2,L3,V1,M3} { X = sz00, X = sz10, ! sz10 = X
% 15.05/15.45 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45 substitution1:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 factor: (32895) {G2,W6,D2,L2,V1,M2} { ! sz10 = X, X = sz10 }.
% 15.05/15.45 parent0[0, 2]: (32892) {G2,W9,D2,L3,V1,M3} { ! sz10 = X, X = sz10, ! sz10
% 15.05/15.45 = X }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 subsumption: (5957) {G4,W6,D2,L2,V1,M2} S(48);r(455);r(735) { X = sz10, !
% 15.05/15.45 sz10 = X }.
% 15.05/15.45 parent0: (32895) {G2,W6,D2,L2,V1,M2} { ! sz10 = X, X = sz10 }.
% 15.05/15.45 substitution0:
% 15.05/15.45 X := X
% 15.05/15.45 end
% 15.05/15.45 permutation0:
% 15.05/15.45 0 ==> 1
% 15.05/15.45 1 ==> 0
% 15.05/15.45 end
% 15.05/15.45
% 15.05/15.45 eqswap: (32896) {G0,W17,D3,L6,V3,M6} { sz00 = X, ! aNaturalNumber0( X ), !
% 15.05/15.45 aNaturalNumber0( Y ), ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 15.05/15.45 aNaturalNumber0( Z ) }.
% 15.05/15.45 pCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------