%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM487+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n019.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:47 EDT 2022
% Result : Theorem 23.59s 23.98s
% Output : Refutation 23.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM487+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : bliksem %s
% 0.12/0.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Wed Jul 6 13:36:38 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.72/1.11 *** allocated 10000 integers for termspace/termends
% 0.72/1.11 *** allocated 10000 integers for clauses
% 0.72/1.11 *** allocated 10000 integers for justifications
% 0.72/1.11 Bliksem 1.12
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Automatic Strategy Selection
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Clauses:
% 0.72/1.11
% 0.72/1.11 { && }.
% 0.72/1.11 { aNaturalNumber0( sz00 ) }.
% 0.72/1.11 { aNaturalNumber0( sz10 ) }.
% 0.72/1.11 { ! sz10 = sz00 }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0
% 0.72/1.11 ( X, Y ) ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0
% 0.72/1.11 ( X, Y ) ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtpldt0( X, Y ) =
% 0.72/1.11 sdtpldt0( Y, X ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.72/1.11 sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) = X }.
% 0.72/1.11 { ! aNaturalNumber0( X ), X = sdtpldt0( sz00, X ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtasdt0( X, Y ) =
% 0.72/1.11 sdtasdt0( Y, X ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.72/1.11 sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 ) = X }.
% 0.72/1.11 { ! aNaturalNumber0( X ), X = sdtasdt0( sz10, X ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 0.72/1.11 { ! aNaturalNumber0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.72/1.11 sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X
% 0.72/1.11 , Z ) ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.72/1.11 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z
% 0.72/1.11 , X ) ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.11 sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.11 sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z }.
% 0.72/1.11 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.72/1.11 aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ), Y = Z }.
% 0.72/1.11 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.72/1.11 aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ), Y = Z }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.72/1.11 , X = sz00 }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.72/1.11 , Y = sz00 }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sz00
% 0.72/1.11 , X = sz00, Y = sz00 }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.72/1.11 aNaturalNumber0( skol1( Z, T ) ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.72/1.11 sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.11 sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.72/1.11 = sdtmndt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.72/1.11 = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.72/1.11 aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.72/1.11 sdtlseqdt0( Y, X ), X = Y }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.11 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y =
% 0.72/1.11 X }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ),
% 0.72/1.11 sdtlseqdt0( Y, X ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.72/1.11 ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z ) }.
% 0.72/1.11 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.72/1.11 ), ! aNaturalNumber0( Z ), sdtlseqdt0( sdtpldt0( X, Z ), sdtpldt0( Y, Z
% 0.72/1.11 ) ) }.
% 0.72/1.11 { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) = sdtpldt0( Z, Y ) }.
% 0.72/1.11 { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ) }.
% 0.72/1.11 { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) = sdtpldt0( Y, Z ) }.
% 2.59/2.99 { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), ! sdtlseqdt0( sdtpldt0( Z, X ),
% 2.59/2.99 sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) = sdtpldt0( Y, Z ), alpha5( X, Y, Z
% 2.59/2.99 ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 2.59/2.99 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), alpha6( X, Y, Z ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 2.59/2.99 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), sdtlseqdt0( sdtasdt0( Y, X ),
% 2.59/2.99 sdtasdt0( Z, X ) ) }.
% 2.59/2.99 { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ) }.
% 2.59/2.99 { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 2.59/2.99 { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ) }.
% 2.59/2.99 { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), ! sdtlseqdt0( sdtasdt0( X, Y ),
% 2.59/2.99 sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) = sdtasdt0( Z, X ), alpha6( X, Y, Z
% 2.59/2.99 ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! sz10 = X }.
% 2.59/2.99 { ! aNaturalNumber0( X ), X = sz00, X = sz10, sdtlseqdt0( sz10, X ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, sdtlseqdt0( Y,
% 2.59/2.99 sdtasdt0( Y, X ) ) }.
% 2.59/2.99 { && }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 2.59/2.99 ), iLess0( X, Y ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ),
% 2.59/2.99 aNaturalNumber0( skol2( Z, T ) ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 2.59/2.99 sdtasdt0( X, skol2( X, Y ) ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 2.59/2.99 Y = sdtasdt0( X, Z ), doDivides0( X, Y ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 2.59/2.99 , Y ), ! Z = sdtsldt0( Y, X ), aNaturalNumber0( Z ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 2.59/2.99 , Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0( X, Z ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 2.59/2.99 , Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), Z = sdtsldt0( Y, X
% 2.59/2.99 ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 2.59/2.99 doDivides0( X, Y ), ! doDivides0( Y, Z ), doDivides0( X, Z ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 2.59/2.99 doDivides0( X, Y ), ! doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z
% 2.59/2.99 ) ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 2.59/2.99 doDivides0( X, Y ), ! doDivides0( X, sdtpldt0( Y, Z ) ), doDivides0( X,
% 2.59/2.99 Z ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 2.59/2.99 sz00, sdtlseqdt0( X, Y ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 2.59/2.99 , Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z, sdtsldt0( Y, X ) ) = sdtsldt0
% 2.59/2.99 ( sdtasdt0( Z, Y ), X ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X = sz00 }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! isPrime0( X ), alpha1( X ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), X = sz00, ! alpha1( X ), isPrime0( X ) }.
% 2.59/2.99 { ! alpha1( X ), ! X = sz10 }.
% 2.59/2.99 { ! alpha1( X ), alpha2( X ) }.
% 2.59/2.99 { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 2.59/2.99 { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X, Y ) }.
% 2.59/2.99 { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 2.59/2.99 { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 2.59/2.99 { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 2.59/2.99 { ! Y = sz10, alpha4( X, Y ) }.
% 2.59/2.99 { ! Y = X, alpha4( X, Y ) }.
% 2.59/2.99 { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 2.59/2.99 { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 2.59/2.99 { ! aNaturalNumber0( Y ), ! doDivides0( Y, X ), alpha3( X, Y ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), X = sz00, X = sz10, aNaturalNumber0( skol4( Y ) )
% 2.59/2.99 }.
% 2.59/2.99 { ! aNaturalNumber0( X ), X = sz00, X = sz10, isPrime0( skol4( Y ) ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), X = sz00, X = sz10, doDivides0( skol4( X ), X ) }
% 2.59/2.99 .
% 2.59/2.99 { aNaturalNumber0( xn ) }.
% 2.59/2.99 { aNaturalNumber0( xm ) }.
% 2.59/2.99 { aNaturalNumber0( xp ) }.
% 2.59/2.99 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 2.59/2.99 isPrime0( Z ), ! doDivides0( Z, sdtasdt0( X, Y ) ), ! iLess0( sdtpldt0(
% 2.59/2.99 sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0( xn, xm ), xp ) ), doDivides0(
% 2.59/2.99 Z, X ), doDivides0( Z, Y ) }.
% 2.59/2.99 { isPrime0( xp ) }.
% 2.59/2.99 { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 2.59/2.99 { sdtlseqdt0( xp, xn ) }.
% 2.59/2.99 { xr = sdtmndt0( xn, xp ) }.
% 2.59/2.99 { xr = xn, ! sdtlseqdt0( xr, xn ) }.
% 23.59/23.98
% 23.59/23.98 percentage equality = 0.278125, percentage horn = 0.700000
% 23.59/23.98 This is a problem with some equality
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Options Used:
% 23.59/23.98
% 23.59/23.98 useres = 1
% 23.59/23.98 useparamod = 1
% 23.59/23.98 useeqrefl = 1
% 23.59/23.98 useeqfact = 1
% 23.59/23.98 usefactor = 1
% 23.59/23.98 usesimpsplitting = 0
% 23.59/23.98 usesimpdemod = 5
% 23.59/23.98 usesimpres = 3
% 23.59/23.98
% 23.59/23.98 resimpinuse = 1000
% 23.59/23.98 resimpclauses = 20000
% 23.59/23.98 substype = eqrewr
% 23.59/23.98 backwardsubs = 1
% 23.59/23.98 selectoldest = 5
% 23.59/23.98
% 23.59/23.98 litorderings [0] = split
% 23.59/23.98 litorderings [1] = extend the termordering, first sorting on arguments
% 23.59/23.98
% 23.59/23.98 termordering = kbo
% 23.59/23.98
% 23.59/23.98 litapriori = 0
% 23.59/23.98 termapriori = 1
% 23.59/23.98 litaposteriori = 0
% 23.59/23.98 termaposteriori = 0
% 23.59/23.98 demodaposteriori = 0
% 23.59/23.98 ordereqreflfact = 0
% 23.59/23.98
% 23.59/23.98 litselect = negord
% 23.59/23.98
% 23.59/23.98 maxweight = 15
% 23.59/23.98 maxdepth = 30000
% 23.59/23.98 maxlength = 115
% 23.59/23.98 maxnrvars = 195
% 23.59/23.98 excuselevel = 1
% 23.59/23.98 increasemaxweight = 1
% 23.59/23.98
% 23.59/23.98 maxselected = 10000000
% 23.59/23.98 maxnrclauses = 10000000
% 23.59/23.98
% 23.59/23.98 showgenerated = 0
% 23.59/23.98 showkept = 0
% 23.59/23.98 showselected = 0
% 23.59/23.98 showdeleted = 0
% 23.59/23.98 showresimp = 1
% 23.59/23.98 showstatus = 2000
% 23.59/23.98
% 23.59/23.98 prologoutput = 0
% 23.59/23.98 nrgoals = 5000000
% 23.59/23.98 totalproof = 1
% 23.59/23.98
% 23.59/23.98 Symbols occurring in the translation:
% 23.59/23.98
% 23.59/23.98 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 23.59/23.98 . [1, 2] (w:1, o:26, a:1, s:1, b:0),
% 23.59/23.98 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 23.59/23.98 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 23.59/23.98 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 23.59/23.98 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 23.59/23.98 aNaturalNumber0 [36, 1] (w:1, o:20, a:1, s:1, b:0),
% 23.59/23.98 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 23.59/23.98 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 23.59/23.98 sdtpldt0 [40, 2] (w:1, o:50, a:1, s:1, b:0),
% 23.59/23.98 sdtasdt0 [41, 2] (w:1, o:51, a:1, s:1, b:0),
% 23.59/23.98 sdtlseqdt0 [43, 2] (w:1, o:52, a:1, s:1, b:0),
% 23.59/23.98 sdtmndt0 [44, 2] (w:1, o:53, a:1, s:1, b:0),
% 23.59/23.98 iLess0 [45, 2] (w:1, o:54, a:1, s:1, b:0),
% 23.59/23.98 doDivides0 [46, 2] (w:1, o:55, a:1, s:1, b:0),
% 23.59/23.98 sdtsldt0 [47, 2] (w:1, o:56, a:1, s:1, b:0),
% 23.59/23.98 isPrime0 [48, 1] (w:1, o:21, a:1, s:1, b:0),
% 23.59/23.98 xn [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 23.59/23.98 xm [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 23.59/23.98 xp [51, 0] (w:1, o:13, a:1, s:1, b:0),
% 23.59/23.98 xr [52, 0] (w:1, o:14, a:1, s:1, b:0),
% 23.59/23.98 alpha1 [53, 1] (w:1, o:22, a:1, s:1, b:1),
% 23.59/23.98 alpha2 [54, 1] (w:1, o:23, a:1, s:1, b:1),
% 23.59/23.98 alpha3 [55, 2] (w:1, o:57, a:1, s:1, b:1),
% 23.59/23.98 alpha4 [56, 2] (w:1, o:58, a:1, s:1, b:1),
% 23.59/23.98 alpha5 [57, 3] (w:1, o:61, a:1, s:1, b:1),
% 23.59/23.98 alpha6 [58, 3] (w:1, o:62, a:1, s:1, b:1),
% 23.59/23.98 skol1 [59, 2] (w:1, o:59, a:1, s:1, b:1),
% 23.59/23.98 skol2 [60, 2] (w:1, o:60, a:1, s:1, b:1),
% 23.59/23.98 skol3 [61, 1] (w:1, o:24, a:1, s:1, b:1),
% 23.59/23.98 skol4 [62, 1] (w:1, o:25, a:1, s:1, b:1).
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Starting Search:
% 23.59/23.98
% 23.59/23.98 *** allocated 15000 integers for clauses
% 23.59/23.98 *** allocated 22500 integers for clauses
% 23.59/23.98 *** allocated 33750 integers for clauses
% 23.59/23.98 *** allocated 15000 integers for termspace/termends
% 23.59/23.98 *** allocated 50625 integers for clauses
% 23.59/23.98 *** allocated 22500 integers for termspace/termends
% 23.59/23.98 *** allocated 75937 integers for clauses
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 33750 integers for termspace/termends
% 23.59/23.98 *** allocated 113905 integers for clauses
% 23.59/23.98 *** allocated 50625 integers for termspace/termends
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 12312
% 23.59/23.98 Kept: 2024
% 23.59/23.98 Inuse: 132
% 23.59/23.98 Deleted: 8
% 23.59/23.98 Deletedinuse: 4
% 23.59/23.98
% 23.59/23.98 *** allocated 170857 integers for clauses
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 75937 integers for termspace/termends
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 256285 integers for clauses
% 23.59/23.98 *** allocated 113905 integers for termspace/termends
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 25484
% 23.59/23.98 Kept: 4029
% 23.59/23.98 Inuse: 188
% 23.59/23.98 Deleted: 11
% 23.59/23.98 Deletedinuse: 6
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 384427 integers for clauses
% 23.59/23.98 *** allocated 170857 integers for termspace/termends
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 47907
% 23.59/23.98 Kept: 6117
% 23.59/23.98 Inuse: 231
% 23.59/23.98 Deleted: 20
% 23.59/23.98 Deletedinuse: 10
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 256285 integers for termspace/termends
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 62601
% 23.59/23.98 Kept: 8134
% 23.59/23.98 Inuse: 260
% 23.59/23.98 Deleted: 23
% 23.59/23.98 Deletedinuse: 12
% 23.59/23.98
% 23.59/23.98 *** allocated 576640 integers for clauses
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 83019
% 23.59/23.98 Kept: 10136
% 23.59/23.98 Inuse: 318
% 23.59/23.98 Deleted: 32
% 23.59/23.98 Deletedinuse: 15
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 97061
% 23.59/23.98 Kept: 12289
% 23.59/23.98 Inuse: 334
% 23.59/23.98 Deleted: 39
% 23.59/23.98 Deletedinuse: 22
% 23.59/23.98
% 23.59/23.98 *** allocated 384427 integers for termspace/termends
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 864960 integers for clauses
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 112013
% 23.59/23.98 Kept: 14290
% 23.59/23.98 Inuse: 394
% 23.59/23.98 Deleted: 40
% 23.59/23.98 Deletedinuse: 23
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 139275
% 23.59/23.98 Kept: 16308
% 23.59/23.98 Inuse: 490
% 23.59/23.98 Deleted: 50
% 23.59/23.98 Deletedinuse: 23
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 156127
% 23.59/23.98 Kept: 18706
% 23.59/23.98 Inuse: 570
% 23.59/23.98 Deleted: 64
% 23.59/23.98 Deletedinuse: 28
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 1297440 integers for clauses
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying clauses:
% 23.59/23.98 *** allocated 576640 integers for termspace/termends
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 173467
% 23.59/23.98 Kept: 21544
% 23.59/23.98 Inuse: 606
% 23.59/23.98 Deleted: 5053
% 23.59/23.98 Deletedinuse: 28
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 202595
% 23.59/23.98 Kept: 23602
% 23.59/23.98 Inuse: 668
% 23.59/23.98 Deleted: 5059
% 23.59/23.98 Deletedinuse: 32
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 227069
% 23.59/23.98 Kept: 25632
% 23.59/23.98 Inuse: 725
% 23.59/23.98 Deleted: 5065
% 23.59/23.98 Deletedinuse: 35
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 239064
% 23.59/23.98 Kept: 27637
% 23.59/23.98 Inuse: 756
% 23.59/23.98 Deleted: 5065
% 23.59/23.98 Deletedinuse: 35
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 1946160 integers for clauses
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 254710
% 23.59/23.98 Kept: 29742
% 23.59/23.98 Inuse: 800
% 23.59/23.98 Deleted: 5065
% 23.59/23.98 Deletedinuse: 35
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 265603
% 23.59/23.98 Kept: 32119
% 23.59/23.98 Inuse: 830
% 23.59/23.98 Deleted: 5065
% 23.59/23.98 Deletedinuse: 35
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 273003
% 23.59/23.98 Kept: 34229
% 23.59/23.98 Inuse: 845
% 23.59/23.98 Deleted: 5065
% 23.59/23.98 Deletedinuse: 35
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 864960 integers for termspace/termends
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 281681
% 23.59/23.98 Kept: 36239
% 23.59/23.98 Inuse: 870
% 23.59/23.98 Deleted: 5065
% 23.59/23.98 Deletedinuse: 35
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 297988
% 23.59/23.98 Kept: 38296
% 23.59/23.98 Inuse: 910
% 23.59/23.98 Deleted: 5065
% 23.59/23.98 Deletedinuse: 35
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Intermediate Status:
% 23.59/23.98 Generated: 317569
% 23.59/23.98 Kept: 40398
% 23.59/23.98 Inuse: 965
% 23.59/23.98 Deleted: 5065
% 23.59/23.98 Deletedinuse: 35
% 23.59/23.98
% 23.59/23.98 Resimplifying inuse:
% 23.59/23.98 Done
% 23.59/23.98
% 23.59/23.98 *** allocated 2919240 integers for clauses
% 23.59/23.98
% 23.59/23.98 Bliksems!, er is een bewijs:
% 23.59/23.98 % SZS status Theorem
% 23.59/23.98 % SZS output start Refutation
% 23.59/23.98
% 23.59/23.98 (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 23.59/23.98 (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 23.59/23.98 , aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 23.59/23.98 (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 23.59/23.98 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 23.59/23.98 (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) ==>
% 23.59/23.98 X }.
% 23.59/23.98 (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( sz00, X ) ==>
% 23.59/23.98 X }.
% 23.59/23.98 (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 23.59/23.98 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 23.59/23.98 }.
% 23.59/23.98 (19) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 23.59/23.98 ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z
% 23.59/23.98 }.
% 23.59/23.98 (20) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), X = sz00, !
% 23.59/23.98 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 23.59/23.98 sdtasdt0( X, Z ), Y = Z }.
% 23.59/23.98 (22) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 23.59/23.98 ), ! sdtpldt0( X, Y ) ==> sz00, X = sz00 }.
% 23.59/23.98 (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 23.59/23.98 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 23.59/23.98 }.
% 23.59/23.98 (28) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 23.59/23.98 ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 23.59/23.98 }.
% 23.59/23.98 (29) {G0,W17,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 23.59/23.98 ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 23.59/23.98 }.
% 23.59/23.98 (63) {G0,W7,D2,L3,V1,M3} I { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X =
% 23.59/23.98 sz00 }.
% 23.59/23.98 (81) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 23.59/23.98 (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 23.59/23.98 (85) {G0,W2,D2,L1,V0,M1} I { isPrime0( xp ) }.
% 23.59/23.98 (87) {G0,W3,D2,L1,V0,M1} I { sdtlseqdt0( xp, xn ) }.
% 23.59/23.98 (88) {G0,W5,D3,L1,V0,M1} I { sdtmndt0( xn, xp ) ==> xr }.
% 23.59/23.98 (89) {G0,W6,D2,L2,V0,M2} I { xr ==> xn, ! sdtlseqdt0( xr, xn ) }.
% 23.59/23.98 (125) {G1,W9,D3,L3,V2,M3} Q(27);r(4) { ! aNaturalNumber0( X ), !
% 23.59/23.98 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ) }.
% 23.59/23.98 (218) {G1,W2,D2,L1,V0,M1} Q(63);r(1) { ! isPrime0( sz00 ) }.
% 23.59/23.98 (288) {G1,W9,D3,L2,V1,M2} R(6,81) { ! aNaturalNumber0( X ), sdtpldt0( xn, X
% 23.59/23.98 ) = sdtpldt0( X, xn ) }.
% 23.59/23.98 (359) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 23.59/23.98 (870) {G1,W17,D3,L5,V2,M5} R(20,83) { ! aNaturalNumber0( X ), X = sz00, !
% 23.59/23.98 aNaturalNumber0( Y ), ! sdtasdt0( X, xp ) = sdtasdt0( X, Y ), xp = Y }.
% 23.59/23.98 (950) {G2,W15,D3,L4,V1,M4} E(870);f { ! xp ==> sz00, ! aNaturalNumber0( X )
% 23.59/23.98 , X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X ) }.
% 23.59/23.98 (953) {G3,W6,D2,L2,V0,M2} Q(950);r(83) { ! xp ==> sz00, xp ==> sz00 }.
% 23.59/23.98 (1193) {G2,W9,D3,L3,V1,M3} P(22,85);r(218) { ! aNaturalNumber0( xp ), !
% 23.59/23.98 aNaturalNumber0( X ), ! sdtpldt0( xp, X ) ==> sz00 }.
% 23.59/23.98 (1194) {G3,W5,D3,L1,V0,M1} F(1193);r(83) { ! sdtpldt0( xp, xp ) ==> sz00
% 23.59/23.98 }.
% 23.59/23.98 (1445) {G4,W3,D2,L1,V0,M1} P(953,1194);d(359);q { ! xp ==> sz00 }.
% 23.59/23.98 (1446) {G5,W14,D3,L4,V2,M4} P(19,1445);r(83) { ! X = sz00, !
% 23.59/23.98 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtpldt0( xp, Y ) =
% 23.59/23.98 sdtpldt0( X, Y ) }.
% 23.59/23.98 (1451) {G6,W7,D3,L2,V1,M2} Q(1446);d(9);r(1) { ! aNaturalNumber0( X ), !
% 23.59/23.98 sdtpldt0( xp, X ) ==> X }.
% 23.59/23.98 (1921) {G1,W7,D2,L3,V1,M3} R(28,87);d(88);r(83) { ! aNaturalNumber0( xn ),
% 23.59/23.98 aNaturalNumber0( X ), ! X = xr }.
% 23.59/23.98 (1950) {G2,W2,D2,L1,V0,M1} Q(1921);r(81) { aNaturalNumber0( xr ) }.
% 23.59/23.98 (2130) {G1,W10,D3,L3,V1,M3} R(29,87);d(88);r(83) { ! aNaturalNumber0( xn )
% 23.59/23.98 , sdtpldt0( xp, X ) ==> xn, ! X = xr }.
% 23.59/23.98 (2236) {G2,W5,D3,L1,V0,M1} Q(2130);r(81) { sdtpldt0( xp, xr ) ==> xn }.
% 23.59/23.98 (3053) {G3,W7,D3,L2,V0,M2} P(2236,6);r(83) { ! aNaturalNumber0( xr ),
% 23.59/23.98 sdtpldt0( xr, xp ) ==> xn }.
% 23.59/23.98 (21401) {G4,W5,D3,L1,V0,M1} S(3053);r(1950) { sdtpldt0( xr, xp ) ==> xn }.
% 23.59/23.98 (40350) {G2,W7,D3,L1,V0,M1} R(288,83) { sdtpldt0( xn, xp ) ==> sdtpldt0( xp
% 23.59/23.98 , xn ) }.
% 23.59/23.98 (40461) {G5,W5,D2,L2,V0,M2} P(21401,125);r(1950) { ! aNaturalNumber0( xp )
% 23.59/23.98 , sdtlseqdt0( xr, xn ) }.
% 23.59/23.98 (40625) {G6,W3,D2,L1,V0,M1} S(40461);r(83) { sdtlseqdt0( xr, xn ) }.
% 23.59/23.98 (40647) {G7,W3,D2,L1,V0,M1} R(40625,89) { xr ==> xn }.
% 23.59/23.98 (40657) {G8,W5,D3,L1,V0,M1} P(40647,21401);d(40350) { sdtpldt0( xp, xn )
% 23.59/23.98 ==> xn }.
% 23.59/23.98 (41149) {G9,W13,D3,L4,V2,M4} P(18,40657);r(1451) { ! aNaturalNumber0( Y ),
% 23.59/23.98 ! aNaturalNumber0( xn ), ! aNaturalNumber0( X ), ! sdtpldt0( Y, xn ) =
% 23.59/23.98 sdtpldt0( Y, X ) }.
% 23.59/23.98 (41151) {G10,W9,D3,L2,V1,M2} F(41149);r(81) { ! aNaturalNumber0( X ), !
% 23.59/23.98 sdtpldt0( X, xn ) = sdtpldt0( X, X ) }.
% 23.59/23.98 (41153) {G11,W0,D0,L0,V0,M0} Q(41151);r(81) { }.
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 % SZS output end Refutation
% 23.59/23.98 found a proof!
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Unprocessed initial clauses:
% 23.59/23.98
% 23.59/23.98 (41155) {G0,W1,D1,L1,V0,M1} { && }.
% 23.59/23.98 (41156) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 23.59/23.98 (41157) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 23.59/23.98 (41158) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 23.59/23.98 (41159) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 23.59/23.98 ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 23.59/23.98 (41160) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 23.59/23.98 ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 23.59/23.98 (41161) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 23.59/23.98 (41162) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0(
% 23.59/23.98 X, sdtpldt0( Y, Z ) ) }.
% 23.59/23.98 (41163) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 )
% 23.59/23.98 = X }.
% 23.59/23.98 (41164) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtpldt0( sz00,
% 23.59/23.98 X ) }.
% 23.59/23.98 (41165) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 23.59/23.98 (41166) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0(
% 23.59/23.98 X, sdtasdt0( Y, Z ) ) }.
% 23.59/23.98 (41167) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 23.59/23.98 = X }.
% 23.59/23.98 (41168) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtasdt0( sz10,
% 23.59/23.98 X ) }.
% 23.59/23.98 (41169) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 )
% 23.59/23.98 = sz00 }.
% 23.59/23.98 (41170) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sz00 = sdtasdt0(
% 23.59/23.98 sz00, X ) }.
% 23.59/23.98 (41171) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0(
% 23.59/23.98 sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 23.59/23.98 (41172) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0(
% 23.59/23.98 sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 23.59/23.98 (41173) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 23.59/23.98 }.
% 23.59/23.98 (41174) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z
% 23.59/23.98 }.
% 23.59/23.98 (41175) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 23.59/23.98 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 23.59/23.98 sdtasdt0( X, Z ), Y = Z }.
% 23.59/23.98 (41176) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 23.59/23.98 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) =
% 23.59/23.98 sdtasdt0( Z, X ), Y = Z }.
% 23.59/23.98 (41177) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 23.59/23.98 (41178) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 23.59/23.98 (41179) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 23.59/23.98 (41180) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtlseqdt0( X, Y ), aNaturalNumber0( skol1( Z, T ) ) }.
% 23.59/23.98 (41181) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtlseqdt0( X, Y ), sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 23.59/23.98 (41182) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 23.59/23.98 }.
% 23.59/23.98 (41183) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 23.59/23.98 }.
% 23.59/23.98 (41184) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 23.59/23.98 }.
% 23.59/23.98 (41185) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y
% 23.59/23.98 , Z = sdtmndt0( Y, X ) }.
% 23.59/23.98 (41186) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0( X, X )
% 23.59/23.98 }.
% 23.59/23.98 (41187) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 23.59/23.98 (41188) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ),
% 23.59/23.98 sdtlseqdt0( X, Z ) }.
% 23.59/23.98 (41189) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 23.59/23.98 (41190) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), sdtlseqdt0( X, Y ), sdtlseqdt0( Y, X ) }.
% 23.59/23.98 (41191) {G0,W16,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z
% 23.59/23.98 ) }.
% 23.59/23.98 (41192) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), sdtlseqdt0(
% 23.59/23.98 sdtpldt0( X, Z ), sdtpldt0( Y, Z ) ) }.
% 23.59/23.98 (41193) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) =
% 23.59/23.98 sdtpldt0( Z, Y ) }.
% 23.59/23.98 (41194) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0(
% 23.59/23.98 Z, X ), sdtpldt0( Z, Y ) ) }.
% 23.59/23.98 (41195) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) =
% 23.59/23.98 sdtpldt0( Y, Z ) }.
% 23.59/23.98 (41196) {G0,W25,D3,L4,V3,M4} { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), !
% 23.59/23.98 sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) =
% 23.59/23.98 sdtpldt0( Y, Z ), alpha5( X, Y, Z ) }.
% 23.59/23.98 (41197) {G0,W19,D2,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 23.59/23.98 alpha6( X, Y, Z ) }.
% 23.59/23.98 (41198) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 23.59/23.98 sdtlseqdt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 23.59/23.98 (41199) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) =
% 23.59/23.98 sdtasdt0( X, Z ) }.
% 23.59/23.98 (41200) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0(
% 23.59/23.98 X, Y ), sdtasdt0( X, Z ) ) }.
% 23.59/23.98 (41201) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) =
% 23.59/23.98 sdtasdt0( Z, X ) }.
% 23.59/23.98 (41202) {G0,W25,D3,L4,V3,M4} { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), !
% 23.59/23.98 sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) =
% 23.59/23.98 sdtasdt0( Z, X ), alpha6( X, Y, Z ) }.
% 23.59/23.98 (41203) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 23.59/23.98 , ! sz10 = X }.
% 23.59/23.98 (41204) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 23.59/23.98 , sdtlseqdt0( sz10, X ) }.
% 23.59/23.98 (41205) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), X = sz00, sdtlseqdt0( Y, sdtasdt0( Y, X ) ) }.
% 23.59/23.98 (41206) {G0,W1,D1,L1,V0,M1} { && }.
% 23.59/23.98 (41207) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), X = Y, ! sdtlseqdt0( X, Y ), iLess0( X, Y ) }.
% 23.59/23.98 (41208) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! doDivides0( X, Y ), aNaturalNumber0( skol2( Z, T ) ) }.
% 23.59/23.98 (41209) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! doDivides0( X, Y ), Y = sdtasdt0( X, skol2( X, Y ) ) }.
% 23.59/23.98 (41210) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 23.59/23.98 }.
% 23.59/23.98 (41211) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 23.59/23.98 aNaturalNumber0( Z ) }.
% 23.59/23.98 (41212) {G0,W20,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0
% 23.59/23.98 ( X, Z ) }.
% 23.59/23.98 (41213) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), ! Y =
% 23.59/23.98 sdtasdt0( X, Z ), Z = sdtsldt0( Y, X ) }.
% 23.59/23.98 (41214) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( Y, Z ),
% 23.59/23.98 doDivides0( X, Z ) }.
% 23.59/23.98 (41215) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X, Z ),
% 23.59/23.98 doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 23.59/23.98 (41216) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X,
% 23.59/23.98 sdtpldt0( Y, Z ) ), doDivides0( X, Z ) }.
% 23.59/23.98 (41217) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! doDivides0( X, Y ), Y = sz00, sdtlseqdt0( X, Y ) }.
% 23.59/23.98 (41218) {G0,W23,D4,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z
% 23.59/23.98 , sdtsldt0( Y, X ) ) = sdtsldt0( sdtasdt0( Z, Y ), X ) }.
% 23.59/23.98 (41219) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X
% 23.59/23.98 = sz00 }.
% 23.59/23.98 (41220) {G0,W6,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ),
% 23.59/23.98 alpha1( X ) }.
% 23.59/23.98 (41221) {G0,W9,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, ! alpha1(
% 23.59/23.98 X ), isPrime0( X ) }.
% 23.59/23.98 (41222) {G0,W5,D2,L2,V1,M2} { ! alpha1( X ), ! X = sz10 }.
% 23.59/23.98 (41223) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), alpha2( X ) }.
% 23.59/23.98 (41224) {G0,W7,D2,L3,V1,M3} { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 23.59/23.98 (41225) {G0,W8,D2,L3,V2,M3} { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X,
% 23.59/23.98 Y ) }.
% 23.59/23.98 (41226) {G0,W6,D3,L2,V1,M2} { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 23.59/23.98 (41227) {G0,W6,D3,L2,V1,M2} { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 23.59/23.98 (41228) {G0,W9,D2,L3,V2,M3} { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 23.59/23.98 (41229) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha4( X, Y ) }.
% 23.59/23.98 (41230) {G0,W6,D2,L2,V2,M2} { ! Y = X, alpha4( X, Y ) }.
% 23.59/23.98 (41231) {G0,W5,D2,L2,V2,M2} { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 23.59/23.98 (41232) {G0,W6,D2,L2,V2,M2} { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 23.59/23.98 (41233) {G0,W8,D2,L3,V2,M3} { ! aNaturalNumber0( Y ), ! doDivides0( Y, X )
% 23.59/23.98 , alpha3( X, Y ) }.
% 23.59/23.98 (41234) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 23.59/23.98 , aNaturalNumber0( skol4( Y ) ) }.
% 23.59/23.98 (41235) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 23.59/23.98 , isPrime0( skol4( Y ) ) }.
% 23.59/23.98 (41236) {G0,W12,D3,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 23.59/23.98 , doDivides0( skol4( X ), X ) }.
% 23.59/23.98 (41237) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 23.59/23.98 (41238) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 23.59/23.98 (41239) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 23.59/23.98 (41240) {G0,W30,D4,L8,V3,M8} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 23.59/23.98 Y ), ! aNaturalNumber0( Z ), ! isPrime0( Z ), ! doDivides0( Z, sdtasdt0(
% 23.59/23.98 X, Y ) ), ! iLess0( sdtpldt0( sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0(
% 23.59/23.98 xn, xm ), xp ) ), doDivides0( Z, X ), doDivides0( Z, Y ) }.
% 23.59/23.98 (41241) {G0,W2,D2,L1,V0,M1} { isPrime0( xp ) }.
% 23.59/23.98 (41242) {G0,W5,D3,L1,V0,M1} { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 23.59/23.98 (41243) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xp, xn ) }.
% 23.59/23.98 (41244) {G0,W5,D3,L1,V0,M1} { xr = sdtmndt0( xn, xp ) }.
% 23.59/23.98 (41245) {G0,W6,D2,L2,V0,M2} { xr = xn, ! sdtlseqdt0( xr, xn ) }.
% 23.59/23.98
% 23.59/23.98
% 23.59/23.98 Total Proof:
% 23.59/23.98
% 23.59/23.98 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 23.59/23.98 parent0: (41156) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 23.59/23.98 substitution0:
% 23.59/23.98 end
% 23.59/23.98 permutation0:
% 23.59/23.98 0 ==> 0
% 23.59/23.98 end
% 23.59/23.98
% 23.59/23.98 subsumption: (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 23.59/23.98 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 23.59/23.98 parent0: (41159) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 23.59/23.98 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 23.59/23.98 substitution0:
% 23.59/23.98 X := X
% 23.59/23.98 Y := Y
% 23.59/23.98 end
% 23.59/23.98 permutation0:
% 23.59/23.98 0 ==> 0
% 23.59/23.98 1 ==> 1
% 23.59/23.98 2 ==> 2
% 23.59/23.98 end
% 23.59/23.98
% 23.59/23.98 subsumption: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 23.59/23.98 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 23.59/23.98 parent0: (41161) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 23.59/23.98 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 23.59/23.98 substitution0:
% 23.59/23.98 X := X
% 23.59/23.98 Y := Y
% 23.59/23.98 end
% 23.59/23.98 permutation0:
% 23.59/23.98 0 ==> 0
% 23.59/23.98 1 ==> 1
% 23.59/23.98 2 ==> 2
% 23.59/23.98 end
% 23.59/23.98
% 23.59/23.98 subsumption: (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 23.59/23.98 X, sz00 ) ==> X }.
% 23.59/23.98 parent0: (41163) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X
% 23.59/23.99 , sz00 ) = X }.
% 23.59/23.99 substitution0:
% 23.59/23.99 X := X
% 23.59/23.99 end
% 23.59/23.99 permutation0:
% 23.59/23.99 0 ==> 0
% 23.59/23.99 1 ==> 1
% 23.59/23.99 end
% 23.59/23.99
% 23.59/23.99 eqswap: (41280) {G0,W7,D3,L2,V1,M2} { sdtpldt0( sz00, X ) = X, !
% 23.59/23.99 aNaturalNumber0( X ) }.
% 23.59/23.99 parent0[1]: (41164) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X =
% 23.59/23.99 sdtpldt0( sz00, X ) }.
% 23.59/23.99 substitution0:
% 23.59/23.99 X := X
% 23.59/23.99 end
% 23.59/23.99
% 23.59/23.99 subsumption: (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 23.59/23.99 sz00, X ) ==> X }.
% 23.59/23.99 parent0: (41280) {G0,W7,D3,L2,V1,M2} { sdtpldt0( sz00, X ) = X, !
% 23.59/23.99 aNaturalNumber0( X ) }.
% 23.59/23.99 substitution0:
% 23.59/23.99 X := X
% 23.59/23.99 end
% 23.59/23.99 permutation0:
% 23.59/23.99 0 ==> 1
% 23.59/23.99 1 ==> 0
% 23.59/23.99 end
% 23.59/23.99
% 23.59/23.99 subsumption: (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 23.59/23.99 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 23.59/23.99 sdtpldt0( X, Z ), Y = Z }.
% 23.59/23.99 parent0: (41173) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 23.59/23.99 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 23.59/23.99 sdtpldt0( X, Z ), Y = Z }.
% 23.59/23.99 substitution0:
% 23.59/23.99 X := X
% 23.59/23.99 Y := Y
% 23.59/23.99 Z := Z
% 23.59/23.99 end
% 23.59/23.99 permutation0:
% 23.59/23.99 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 3 ==> 3
% 23.59/24.00 4 ==> 4
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (19) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) =
% 23.59/24.00 sdtpldt0( Z, X ), Y = Z }.
% 23.59/24.00 parent0: (41174) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) =
% 23.59/24.00 sdtpldt0( Z, X ), Y = Z }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 Z := Z
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 3 ==> 3
% 23.59/24.00 4 ==> 4
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (20) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), X = sz00
% 23.59/24.00 , ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 23.59/24.00 sdtasdt0( X, Z ), Y = Z }.
% 23.59/24.00 parent0: (41175) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00,
% 23.59/24.00 ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 23.59/24.00 sdtasdt0( X, Z ), Y = Z }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 Z := Z
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 3 ==> 3
% 23.59/24.00 4 ==> 4
% 23.59/24.00 5 ==> 5
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (22) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, X = sz00 }.
% 23.59/24.00 parent0: (41177) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 3 ==> 3
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 23.59/24.00 sdtlseqdt0( X, Y ) }.
% 23.59/24.00 parent0: (41182) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 23.59/24.00 sdtlseqdt0( X, Y ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 Z := Z
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 3 ==> 3
% 23.59/24.00 4 ==> 4
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (28) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 23.59/24.00 aNaturalNumber0( Z ) }.
% 23.59/24.00 parent0: (41183) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 23.59/24.00 aNaturalNumber0( Z ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 Z := Z
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 3 ==> 3
% 23.59/24.00 4 ==> 4
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (29) {G0,W17,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 23.59/24.00 sdtpldt0( X, Z ) = Y }.
% 23.59/24.00 parent0: (41184) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 23.59/24.00 sdtpldt0( X, Z ) = Y }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 Z := Z
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 3 ==> 3
% 23.59/24.00 4 ==> 4
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (63) {G0,W7,D2,L3,V1,M3} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 isPrime0( X ), ! X = sz00 }.
% 23.59/24.00 parent0: (41219) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0
% 23.59/24.00 ( X ), ! X = sz00 }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (81) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 23.59/24.00 parent0: (41237) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 23.59/24.00 parent0: (41239) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (85) {G0,W2,D2,L1,V0,M1} I { isPrime0( xp ) }.
% 23.59/24.00 parent0: (41241) {G0,W2,D2,L1,V0,M1} { isPrime0( xp ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (87) {G0,W3,D2,L1,V0,M1} I { sdtlseqdt0( xp, xn ) }.
% 23.59/24.00 parent0: (41243) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xp, xn ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (44597) {G0,W5,D3,L1,V0,M1} { sdtmndt0( xn, xp ) = xr }.
% 23.59/24.00 parent0[0]: (41244) {G0,W5,D3,L1,V0,M1} { xr = sdtmndt0( xn, xp ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (88) {G0,W5,D3,L1,V0,M1} I { sdtmndt0( xn, xp ) ==> xr }.
% 23.59/24.00 parent0: (44597) {G0,W5,D3,L1,V0,M1} { sdtmndt0( xn, xp ) = xr }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (89) {G0,W6,D2,L2,V0,M2} I { xr ==> xn, ! sdtlseqdt0( xr, xn )
% 23.59/24.00 }.
% 23.59/24.00 parent0: (41245) {G0,W6,D2,L2,V0,M2} { xr = xn, ! sdtlseqdt0( xr, xn ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45026) {G0,W14,D3,L5,V3,M5} { ! Z = sdtpldt0( X, Y ), !
% 23.59/24.00 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! aNaturalNumber0( Y ),
% 23.59/24.00 sdtlseqdt0( X, Z ) }.
% 23.59/24.00 parent0[3]: (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 23.59/24.00 sdtlseqdt0( X, Y ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Z
% 23.59/24.00 Z := Y
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqrefl: (45027) {G0,W13,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( sdtpldt0( X, Y ) ), ! aNaturalNumber0( Y ), sdtlseqdt0(
% 23.59/24.00 X, sdtpldt0( X, Y ) ) }.
% 23.59/24.00 parent0[0]: (45026) {G0,W14,D3,L5,V3,M5} { ! Z = sdtpldt0( X, Y ), !
% 23.59/24.00 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! aNaturalNumber0( Y ),
% 23.59/24.00 sdtlseqdt0( X, Z ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 Z := sdtpldt0( X, Y )
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 resolution: (45032) {G1,W13,D3,L5,V2,M5} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ), !
% 23.59/24.00 aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 23.59/24.00 parent0[1]: (45027) {G0,W13,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( sdtpldt0( X, Y ) ), ! aNaturalNumber0( Y ), sdtlseqdt0(
% 23.59/24.00 X, sdtpldt0( X, Y ) ) }.
% 23.59/24.00 parent1[2]: (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 end
% 23.59/24.00 substitution1:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 factor: (45034) {G1,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ), !
% 23.59/24.00 aNaturalNumber0( Y ) }.
% 23.59/24.00 parent0[0, 3]: (45032) {G1,W13,D3,L5,V2,M5} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ), !
% 23.59/24.00 aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 factor: (45036) {G1,W9,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ) }.
% 23.59/24.00 parent0[1, 3]: (45034) {G1,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ), !
% 23.59/24.00 aNaturalNumber0( Y ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (125) {G1,W9,D3,L3,V2,M3} Q(27);r(4) { ! aNaturalNumber0( X )
% 23.59/24.00 , ! aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ) }.
% 23.59/24.00 parent0: (45036) {G1,W9,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 2
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45038) {G0,W7,D2,L3,V1,M3} { ! sz00 = X, ! aNaturalNumber0( X ),
% 23.59/24.00 ! isPrime0( X ) }.
% 23.59/24.00 parent0[2]: (63) {G0,W7,D2,L3,V1,M3} I { ! aNaturalNumber0( X ), ! isPrime0
% 23.59/24.00 ( X ), ! X = sz00 }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqrefl: (45039) {G0,W4,D2,L2,V0,M2} { ! aNaturalNumber0( sz00 ), !
% 23.59/24.00 isPrime0( sz00 ) }.
% 23.59/24.00 parent0[0]: (45038) {G0,W7,D2,L3,V1,M3} { ! sz00 = X, ! aNaturalNumber0( X
% 23.59/24.00 ), ! isPrime0( X ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := sz00
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 resolution: (45040) {G1,W2,D2,L1,V0,M1} { ! isPrime0( sz00 ) }.
% 23.59/24.00 parent0[0]: (45039) {G0,W4,D2,L2,V0,M2} { ! aNaturalNumber0( sz00 ), !
% 23.59/24.00 isPrime0( sz00 ) }.
% 23.59/24.00 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 substitution1:
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (218) {G1,W2,D2,L1,V0,M1} Q(63);r(1) { ! isPrime0( sz00 ) }.
% 23.59/24.00 parent0: (45040) {G1,W2,D2,L1,V0,M1} { ! isPrime0( sz00 ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 resolution: (45041) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0
% 23.59/24.00 ( xn, X ) = sdtpldt0( X, xn ) }.
% 23.59/24.00 parent0[0]: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 23.59/24.00 parent1[0]: (81) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := xn
% 23.59/24.00 Y := X
% 23.59/24.00 end
% 23.59/24.00 substitution1:
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (288) {G1,W9,D3,L2,V1,M2} R(6,81) { ! aNaturalNumber0( X ),
% 23.59/24.00 sdtpldt0( xn, X ) = sdtpldt0( X, xn ) }.
% 23.59/24.00 parent0: (45041) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0(
% 23.59/24.00 xn, X ) = sdtpldt0( X, xn ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 1 ==> 1
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45043) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( X, sz00 ), !
% 23.59/24.00 aNaturalNumber0( X ) }.
% 23.59/24.00 parent0[1]: (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( X
% 23.59/24.00 , sz00 ) ==> X }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 resolution: (45044) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtpldt0( sz00, sz00 )
% 23.59/24.00 }.
% 23.59/24.00 parent0[1]: (45043) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( X, sz00 ), !
% 23.59/24.00 aNaturalNumber0( X ) }.
% 23.59/24.00 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := sz00
% 23.59/24.00 end
% 23.59/24.00 substitution1:
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45045) {G1,W5,D3,L1,V0,M1} { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 23.59/24.00 parent0[0]: (45044) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtpldt0( sz00, sz00 )
% 23.59/24.00 }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (359) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==>
% 23.59/24.00 sz00 }.
% 23.59/24.00 parent0: (45045) {G1,W5,D3,L1,V0,M1} { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 23.59/24.00 substitution0:
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 0
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45046) {G0,W19,D3,L6,V3,M6} { sz00 = X, ! aNaturalNumber0( X ), !
% 23.59/24.00 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 23.59/24.00 sdtasdt0( X, Z ), Y = Z }.
% 23.59/24.00 parent0[1]: (20) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), X = sz00
% 23.59/24.00 , ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 23.59/24.00 sdtasdt0( X, Z ), Y = Z }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 Z := Z
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 resolution: (45051) {G1,W17,D3,L5,V2,M5} { sz00 = X, ! aNaturalNumber0( X
% 23.59/24.00 ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sdtasdt0( X, xp ), Y =
% 23.59/24.00 xp }.
% 23.59/24.00 parent0[3]: (45046) {G0,W19,D3,L6,V3,M6} { sz00 = X, ! aNaturalNumber0( X
% 23.59/24.00 ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 23.59/24.00 sdtasdt0( X, Z ), Y = Z }.
% 23.59/24.00 parent1[0]: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 Z := xp
% 23.59/24.00 end
% 23.59/24.00 substitution1:
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45054) {G1,W17,D3,L5,V2,M5} { xp = X, sz00 = Y, ! aNaturalNumber0
% 23.59/24.00 ( Y ), ! aNaturalNumber0( X ), ! sdtasdt0( Y, X ) = sdtasdt0( Y, xp ) }.
% 23.59/24.00 parent0[4]: (45051) {G1,W17,D3,L5,V2,M5} { sz00 = X, ! aNaturalNumber0( X
% 23.59/24.00 ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sdtasdt0( X, xp ), Y =
% 23.59/24.00 xp }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := Y
% 23.59/24.00 Y := X
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45055) {G1,W17,D3,L5,V2,M5} { X = sz00, xp = Y, ! aNaturalNumber0
% 23.59/24.00 ( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sdtasdt0( X, xp ) }.
% 23.59/24.00 parent0[1]: (45054) {G1,W17,D3,L5,V2,M5} { xp = X, sz00 = Y, !
% 23.59/24.00 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtasdt0( Y, X ) =
% 23.59/24.00 sdtasdt0( Y, xp ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := Y
% 23.59/24.00 Y := X
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45056) {G1,W17,D3,L5,V2,M5} { ! sdtasdt0( X, xp ) = sdtasdt0( X,
% 23.59/24.00 Y ), X = sz00, xp = Y, ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 23.59/24.00 parent0[4]: (45055) {G1,W17,D3,L5,V2,M5} { X = sz00, xp = Y, !
% 23.59/24.00 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) =
% 23.59/24.00 sdtasdt0( X, xp ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 subsumption: (870) {G1,W17,D3,L5,V2,M5} R(20,83) { ! aNaturalNumber0( X ),
% 23.59/24.00 X = sz00, ! aNaturalNumber0( Y ), ! sdtasdt0( X, xp ) = sdtasdt0( X, Y )
% 23.59/24.00 , xp = Y }.
% 23.59/24.00 parent0: (45056) {G1,W17,D3,L5,V2,M5} { ! sdtasdt0( X, xp ) = sdtasdt0( X
% 23.59/24.00 , Y ), X = sz00, xp = Y, ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 23.59/24.00 }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := X
% 23.59/24.00 Y := Y
% 23.59/24.00 end
% 23.59/24.00 permutation0:
% 23.59/24.00 0 ==> 3
% 23.59/24.00 1 ==> 1
% 23.59/24.00 2 ==> 4
% 23.59/24.00 3 ==> 0
% 23.59/24.00 4 ==> 2
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45077) {G1,W17,D3,L5,V2,M5} { X = xp, ! aNaturalNumber0( Y ), Y =
% 23.59/24.00 sz00, ! aNaturalNumber0( X ), ! sdtasdt0( Y, xp ) = sdtasdt0( Y, X ) }.
% 23.59/24.00 parent0[4]: (870) {G1,W17,D3,L5,V2,M5} R(20,83) { ! aNaturalNumber0( X ), X
% 23.59/24.00 = sz00, ! aNaturalNumber0( Y ), ! sdtasdt0( X, xp ) = sdtasdt0( X, Y ),
% 23.59/24.00 xp = Y }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := Y
% 23.59/24.00 Y := X
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqswap: (45079) {G1,W17,D3,L5,V2,M5} { ! sdtasdt0( X, Y ) = sdtasdt0( X,
% 23.59/24.00 xp ), Y = xp, ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y )
% 23.59/24.00 }.
% 23.59/24.00 parent0[4]: (45077) {G1,W17,D3,L5,V2,M5} { X = xp, ! aNaturalNumber0( Y )
% 23.59/24.00 , Y = sz00, ! aNaturalNumber0( X ), ! sdtasdt0( Y, xp ) = sdtasdt0( Y, X
% 23.59/24.00 ) }.
% 23.59/24.00 substitution0:
% 23.59/24.00 X := Y
% 23.59/24.00 Y := X
% 23.59/24.00 end
% 23.59/24.00
% 23.59/24.00 eqfact: (45160) {G0,W17,D3,L5,V1,M5} { ! xp = sz00, ! sdtasdt0( X, X ) =
% 24.09/24.50 sdtasdt0( X, xp ), ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( X
% 24.09/24.50 ) }.
% 24.09/24.50 parent0[1, 3]: (45079) {G1,W17,D3,L5,V2,M5} { ! sdtasdt0( X, Y ) =
% 24.09/24.50 sdtasdt0( X, xp ), Y = xp, ! aNaturalNumber0( X ), X = sz00, !
% 24.09/24.50 aNaturalNumber0( Y ) }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := X
% 24.09/24.50 Y := X
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 factor: (45163) {G0,W15,D3,L4,V1,M4} { ! xp = sz00, ! sdtasdt0( X, X ) =
% 24.09/24.50 sdtasdt0( X, xp ), ! aNaturalNumber0( X ), X = sz00 }.
% 24.09/24.50 parent0[2, 4]: (45160) {G0,W17,D3,L5,V1,M5} { ! xp = sz00, ! sdtasdt0( X,
% 24.09/24.50 X ) = sdtasdt0( X, xp ), ! aNaturalNumber0( X ), X = sz00, !
% 24.09/24.50 aNaturalNumber0( X ) }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := X
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 eqswap: (45165) {G0,W15,D3,L4,V1,M4} { ! sdtasdt0( X, xp ) = sdtasdt0( X,
% 24.09/24.50 X ), ! xp = sz00, ! aNaturalNumber0( X ), X = sz00 }.
% 24.09/24.50 parent0[1]: (45163) {G0,W15,D3,L4,V1,M4} { ! xp = sz00, ! sdtasdt0( X, X )
% 24.09/24.50 = sdtasdt0( X, xp ), ! aNaturalNumber0( X ), X = sz00 }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := X
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 subsumption: (950) {G2,W15,D3,L4,V1,M4} E(870);f { ! xp ==> sz00, !
% 24.09/24.50 aNaturalNumber0( X ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X )
% 24.09/24.50 }.
% 24.09/24.50 parent0: (45165) {G0,W15,D3,L4,V1,M4} { ! sdtasdt0( X, xp ) = sdtasdt0( X
% 24.09/24.50 , X ), ! xp = sz00, ! aNaturalNumber0( X ), X = sz00 }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := X
% 24.09/24.50 end
% 24.09/24.50 permutation0:
% 24.09/24.50 0 ==> 3
% 24.09/24.50 1 ==> 0
% 24.09/24.50 2 ==> 1
% 24.09/24.50 3 ==> 2
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 eqswap: (45192) {G2,W15,D3,L4,V1,M4} { ! sz00 ==> xp, ! aNaturalNumber0( X
% 24.09/24.50 ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X ) }.
% 24.09/24.50 parent0[0]: (950) {G2,W15,D3,L4,V1,M4} E(870);f { ! xp ==> sz00, !
% 24.09/24.50 aNaturalNumber0( X ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X )
% 24.09/24.50 }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := X
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 eqrefl: (45199) {G0,W8,D2,L3,V0,M3} { ! sz00 ==> xp, ! aNaturalNumber0( xp
% 24.09/24.50 ), xp = sz00 }.
% 24.09/24.50 parent0[3]: (45192) {G2,W15,D3,L4,V1,M4} { ! sz00 ==> xp, !
% 24.09/24.50 aNaturalNumber0( X ), X = sz00, ! sdtasdt0( X, xp ) = sdtasdt0( X, X )
% 24.09/24.50 }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := xp
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 resolution: (45200) {G1,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp = sz00 }.
% 24.09/24.50 parent0[1]: (45199) {G0,W8,D2,L3,V0,M3} { ! sz00 ==> xp, ! aNaturalNumber0
% 24.09/24.50 ( xp ), xp = sz00 }.
% 24.09/24.50 parent1[0]: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 24.09/24.50 substitution0:
% 24.09/24.50 end
% 24.09/24.50 substitution1:
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 eqswap: (45201) {G1,W6,D2,L2,V0,M2} { ! xp ==> sz00, xp = sz00 }.
% 24.09/24.50 parent0[0]: (45200) {G1,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp = sz00 }.
% 24.09/24.50 substitution0:
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 subsumption: (953) {G3,W6,D2,L2,V0,M2} Q(950);r(83) { ! xp ==> sz00, xp ==>
% 24.09/24.50 sz00 }.
% 24.09/24.50 parent0: (45201) {G1,W6,D2,L2,V0,M2} { ! xp ==> sz00, xp = sz00 }.
% 24.09/24.50 substitution0:
% 24.09/24.50 end
% 24.09/24.50 permutation0:
% 24.09/24.50 0 ==> 0
% 24.09/24.50 1 ==> 1
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 *** allocated 15000 integers for justifications
% 24.09/24.50 eqswap: (45204) {G0,W12,D3,L4,V2,M4} { ! sz00 ==> sdtpldt0( X, Y ), !
% 24.09/24.50 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00 }.
% 24.09/24.50 parent0[2]: (22) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 24.09/24.50 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, X = sz00 }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := X
% 24.09/24.50 Y := Y
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 paramod: (45207) {G1,W11,D3,L4,V1,M4} { isPrime0( sz00 ), ! sz00 ==>
% 24.09/24.50 sdtpldt0( xp, X ), ! aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 24.09/24.50 parent0[3]: (45204) {G0,W12,D3,L4,V2,M4} { ! sz00 ==> sdtpldt0( X, Y ), !
% 24.09/24.50 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00 }.
% 24.09/24.50 parent1[0; 1]: (85) {G0,W2,D2,L1,V0,M1} I { isPrime0( xp ) }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := xp
% 24.09/24.50 Y := X
% 24.09/24.50 end
% 24.09/24.50 substitution1:
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 resolution: (45747) {G2,W9,D3,L3,V1,M3} { ! sz00 ==> sdtpldt0( xp, X ), !
% 24.09/24.50 aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 24.09/24.50 parent0[0]: (218) {G1,W2,D2,L1,V0,M1} Q(63);r(1) { ! isPrime0( sz00 ) }.
% 24.09/24.50 parent1[0]: (45207) {G1,W11,D3,L4,V1,M4} { isPrime0( sz00 ), ! sz00 ==>
% 24.09/24.50 sdtpldt0( xp, X ), ! aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 24.09/24.50 substitution0:
% 24.09/24.50 end
% 24.09/24.50 substitution1:
% 24.09/24.50 X := X
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 eqswap: (45748) {G2,W9,D3,L3,V1,M3} { ! sdtpldt0( xp, X ) ==> sz00, !
% 24.09/24.50 aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 24.09/24.50 parent0[0]: (45747) {G2,W9,D3,L3,V1,M3} { ! sz00 ==> sdtpldt0( xp, X ), !
% 24.09/24.50 aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 24.09/24.50 substitution0:
% 24.09/24.50 X := X
% 24.09/24.50 end
% 24.09/24.50
% 24.09/24.50 subsumption: (1193) {G2,W9,D3,L3,V1,M3} P(22,85);r(218) { ! aNaturalNumber0
% 24.09/24.50 ( xp ), ! aNaturalNumber0( X ), ! sdtpldt0( xp, X ) ==> sz00 }.
% 64.77/65.21 parent0: (45748) {G2,W9,D3,L3,V1,M3} { ! sdtpldt0( xp, X ) ==> sz00, !
% 64.77/65.21 aNaturalNumber0( xp ), ! aNaturalNumber0( X ) }.
% 64.77/65.21 substitution0:
% 64.77/65.21 X := X
% 64.77/65.21 end
% 64.77/65.21 permutation0:
% 64.77/65.21 0 ==> 2
% 64.77/65.21 1 ==> 0
% 64.77/65.21 2 ==> 1
% 64.77/65.21 end
% 64.77/65.21
% 64.77/65.21 factor: (45753) {G2,W7,D3,L2,V0,M2} { ! aNaturalNumber0( xp ), ! sdtpldt0
% 64.77/65.21 ( xp, xp ) ==> sz00 }.
% 64.77/65.21 parent0[0, 1]: (1193) {G2,W9,D3,L3,V1,M3} P(22,85);r(218) { !
% 64.77/65.21 aNaturalNumber0( xp ), ! aNaturalNumber0( X ), ! sdtpldt0( xp, X ) ==>
% 64.77/65.21 sz00 }.
% 64.77/65.21 substitution0:
% 64.77/65.21 X := xp
% 64.77/65.21 end
% 64.77/65.21
% 64.77/65.21 resolution: (45754) {G1,W5,D3,L1,V0,M1} { ! sdtpldt0( xp, xp ) ==> sz00
% 64.77/65.21 }.
% 64.77/65.21 parent0[0]: (45753) {G2,W7,D3,L2,V0,M2} { ! aNaturalNumber0( xp ), !
% 64.77/65.21 sdtpldt0( xp, xp ) ==> sz00 }.
% 64.77/65.21 parent1[0]: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 64.77/65.21 substitution0:
% 64.77/65.21 end
% 64.77/65.21 substitution1:
% 64.77/65.21 end
% 64.77/65.21
% 64.77/65.21 subsumption: (1194) {G3,W5,D3,L1,V0,M1} F(1193);r(83) { ! sdtpldt0( xp, xp
% 64.77/65.21 ) ==> sz00 }.
% 64.77/65.21 parent0: (45754) {G1,W5,D3,L1,V0,M1} { ! sdtpldt0( xp, xp ) ==> sz00 }.
% 64.77/65.21 substitution0:
% 64.77/65.21 end
% 64.77/65.21 permutation0:
% 64.77/65.21 0 ==> 0
% 64.77/65.21 end
% 64.77/65.21
% 64.77/65.21 eqswap: (45756) {G3,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp ==> sz00 }.
% 64.77/65.22 parent0[0]: (953) {G3,W6,D2,L2,V0,M2} Q(950);r(83) { ! xp ==> sz00, xp ==>
% 64.77/65.22 sz00 }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 eqswap: (45759) {G3,W5,D3,L1,V0,M1} { ! sz00 ==> sdtpldt0( xp, xp ) }.
% 64.77/65.22 parent0[0]: (1194) {G3,W5,D3,L1,V0,M1} F(1193);r(83) { ! sdtpldt0( xp, xp )
% 64.77/65.22 ==> sz00 }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 paramod: (45762) {G4,W8,D3,L2,V0,M2} { ! sz00 ==> sdtpldt0( xp, sz00 ), !
% 64.77/65.22 sz00 ==> xp }.
% 64.77/65.22 parent0[1]: (45756) {G3,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp ==> sz00 }.
% 64.77/65.22 parent1[0; 5]: (45759) {G3,W5,D3,L1,V0,M1} { ! sz00 ==> sdtpldt0( xp, xp )
% 64.77/65.22 }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22 substitution1:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 paramod: (45764) {G4,W11,D3,L3,V0,M3} { ! sz00 ==> sz00, ! sz00 ==> xp, !
% 64.77/65.22 sz00 ==> sdtpldt0( xp, sz00 ) }.
% 64.77/65.22 parent0[1]: (45756) {G3,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp ==> sz00 }.
% 64.77/65.22 parent1[1; 3]: (45762) {G4,W8,D3,L2,V0,M2} { ! sz00 ==> sdtpldt0( xp, sz00
% 64.77/65.22 ), ! sz00 ==> xp }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22 substitution1:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 paramod: (45766) {G4,W14,D3,L4,V0,M4} { ! sz00 ==> sdtpldt0( sz00, sz00 )
% 64.77/65.22 , ! sz00 ==> xp, ! sz00 ==> sz00, ! sz00 ==> xp }.
% 64.77/65.22 parent0[1]: (45756) {G3,W6,D2,L2,V0,M2} { ! sz00 ==> xp, xp ==> sz00 }.
% 64.77/65.22 parent1[2; 4]: (45764) {G4,W11,D3,L3,V0,M3} { ! sz00 ==> sz00, ! sz00 ==>
% 64.77/65.22 xp, ! sz00 ==> sdtpldt0( xp, sz00 ) }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22 substitution1:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 paramod: (45776) {G2,W12,D2,L4,V0,M4} { ! sz00 ==> sz00, ! sz00 ==> xp, !
% 64.77/65.22 sz00 ==> sz00, ! sz00 ==> xp }.
% 64.77/65.22 parent0[0]: (359) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==>
% 64.77/65.22 sz00 }.
% 64.77/65.22 parent1[0; 3]: (45766) {G4,W14,D3,L4,V0,M4} { ! sz00 ==> sdtpldt0( sz00,
% 64.77/65.22 sz00 ), ! sz00 ==> xp, ! sz00 ==> sz00, ! sz00 ==> xp }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22 substitution1:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 factor: (45777) {G2,W9,D2,L3,V0,M3} { ! sz00 ==> sz00, ! sz00 ==> xp, !
% 64.77/65.22 sz00 ==> xp }.
% 64.77/65.22 parent0[0, 2]: (45776) {G2,W12,D2,L4,V0,M4} { ! sz00 ==> sz00, ! sz00 ==>
% 64.77/65.22 xp, ! sz00 ==> sz00, ! sz00 ==> xp }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 factor: (45778) {G2,W6,D2,L2,V0,M2} { ! sz00 ==> sz00, ! sz00 ==> xp }.
% 64.77/65.22 parent0[1, 2]: (45777) {G2,W9,D2,L3,V0,M3} { ! sz00 ==> sz00, ! sz00 ==>
% 64.77/65.22 xp, ! sz00 ==> xp }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 eqrefl: (45779) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xp }.
% 64.77/65.22 parent0[0]: (45778) {G2,W6,D2,L2,V0,M2} { ! sz00 ==> sz00, ! sz00 ==> xp
% 64.77/65.22 }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 eqswap: (45780) {G0,W3,D2,L1,V0,M1} { ! xp ==> sz00 }.
% 64.77/65.22 parent0[0]: (45779) {G0,W3,D2,L1,V0,M1} { ! sz00 ==> xp }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 subsumption: (1445) {G4,W3,D2,L1,V0,M1} P(953,1194);d(359);q { ! xp ==>
% 64.77/65.22 sz00 }.
% 64.77/65.22 parent0: (45780) {G0,W3,D2,L1,V0,M1} { ! xp ==> sz00 }.
% 64.77/65.22 substitution0:
% 64.77/65.22 end
% 64.77/65.22 permutation0:
% 64.77/65.22 0 ==> 0
% 64.77/65.22 end
% 64.77/65.22
% 64.77/65.22 *** allocated 22500 integers for justifications
% 64.77/65.22 *** allocated 33750 integers for justifications
% 64.77/65.22 *** allocated 50625 integers for justifications
% 64.77/65.22 *** allocated 75937 integers for justifications
% 64.77/65.22 *** allocated 1297440 integers for termspace/termends
% 64.77/65.22 *** allocated 113905 integers for justifications
% 64.77/65.22 *** allocated 170857 integers for justifications
% 64.77/65.22 *** allocated 256285 integers for justifications
% 64.77/65.22 *** allocated 1946160 integers for termspace/termends
% 64.77/65.22 *** allocated 384427 integers for justifications
% 64.77/65.22 *** allocated 57Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------