%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM487+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n004.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:48 EDT 2022
% Result : Theorem 29.42s 29.80s
% Output : Refutation 29.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM487+3 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Wed Jul 6 09:19:52 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.73/1.12 *** allocated 10000 integers for termspace/termends
% 0.73/1.12 *** allocated 10000 integers for clauses
% 0.73/1.12 *** allocated 10000 integers for justifications
% 0.73/1.12 Bliksem 1.12
% 0.73/1.12
% 0.73/1.12
% 0.73/1.12 Automatic Strategy Selection
% 0.73/1.12
% 0.73/1.12
% 0.73/1.12 Clauses:
% 0.73/1.12
% 0.73/1.12 { && }.
% 0.73/1.12 { aNaturalNumber0( sz00 ) }.
% 0.73/1.12 { aNaturalNumber0( sz10 ) }.
% 0.73/1.12 { ! sz10 = sz00 }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0
% 0.73/1.12 ( X, Y ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0
% 0.73/1.12 ( X, Y ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtpldt0( X, Y ) =
% 0.73/1.12 sdtpldt0( Y, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.73/1.12 sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) = X }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sdtpldt0( sz00, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtasdt0( X, Y ) =
% 0.73/1.12 sdtasdt0( Y, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.73/1.12 sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 ) = X }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sdtasdt0( sz10, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 0.73/1.12 { ! aNaturalNumber0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.73/1.12 sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X
% 0.73/1.12 , Z ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.73/1.12 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z
% 0.73/1.12 , X ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.73/1.12 sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.73/1.12 sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.73/1.12 aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ), Y = Z }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.73/1.12 aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ), Y = Z }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.73/1.12 , X = sz00 }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.73/1.12 , Y = sz00 }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sz00
% 0.73/1.12 , X = sz00, Y = sz00 }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.73/1.12 aNaturalNumber0( skol1( Z, T ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.73/1.12 sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.73/1.12 sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.73/1.12 = sdtmndt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.73/1.12 = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.73/1.12 aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.73/1.12 sdtlseqdt0( Y, X ), X = Y }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.73/1.12 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y =
% 0.73/1.12 X }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ),
% 0.73/1.12 sdtlseqdt0( Y, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.73/1.12 ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.73/1.12 ), ! aNaturalNumber0( Z ), sdtlseqdt0( sdtpldt0( X, Z ), sdtpldt0( Y, Z
% 0.73/1.12 ) ) }.
% 0.73/1.12 { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) = sdtpldt0( Z, Y ) }.
% 0.73/1.12 { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ) }.
% 0.73/1.12 { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) = sdtpldt0( Y, Z ) }.
% 0.73/1.12 { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), ! sdtlseqdt0( sdtpldt0( Z, X ),
% 0.73/1.12 sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) = sdtpldt0( Y, Z ), alpha5( X, Y, Z
% 0.73/1.12 ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 0.73/1.12 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), alpha6( X, Y, Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 0.73/1.12 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), sdtlseqdt0( sdtasdt0( Y, X ),
% 0.73/1.12 sdtasdt0( Z, X ) ) }.
% 0.73/1.12 { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ) }.
% 0.73/1.12 { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 0.73/1.12 { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ) }.
% 0.73/1.12 { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), ! sdtlseqdt0( sdtasdt0( X, Y ),
% 0.73/1.12 sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) = sdtasdt0( Z, X ), alpha6( X, Y, Z
% 0.73/1.12 ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! sz10 = X }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sz00, X = sz10, sdtlseqdt0( sz10, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, sdtlseqdt0( Y,
% 0.73/1.12 sdtasdt0( Y, X ) ) }.
% 0.73/1.12 { && }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.73/1.12 ), iLess0( X, Y ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ),
% 0.73/1.12 aNaturalNumber0( skol2( Z, T ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 0.73/1.12 sdtasdt0( X, skol2( X, Y ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.73/1.12 Y = sdtasdt0( X, Z ), doDivides0( X, Y ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.73/1.12 , Y ), ! Z = sdtsldt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.73/1.12 , Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0( X, Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.73/1.12 , Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), Z = sdtsldt0( Y, X
% 0.73/1.12 ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.73/1.12 doDivides0( X, Y ), ! doDivides0( Y, Z ), doDivides0( X, Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.73/1.12 doDivides0( X, Y ), ! doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z
% 0.73/1.12 ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.73/1.12 doDivides0( X, Y ), ! doDivides0( X, sdtpldt0( Y, Z ) ), doDivides0( X,
% 0.73/1.12 Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 0.73/1.12 sz00, sdtlseqdt0( X, Y ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.73/1.12 , Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z, sdtsldt0( Y, X ) ) = sdtsldt0
% 0.73/1.12 ( sdtasdt0( Z, Y ), X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X = sz00 }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! isPrime0( X ), alpha1( X ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sz00, ! alpha1( X ), isPrime0( X ) }.
% 0.73/1.12 { ! alpha1( X ), ! X = sz10 }.
% 0.73/1.12 { ! alpha1( X ), alpha2( X ) }.
% 0.73/1.12 { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 0.73/1.12 { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X, Y ) }.
% 0.73/1.12 { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 0.73/1.12 { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 0.73/1.12 { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 0.73/1.12 { ! Y = sz10, alpha4( X, Y ) }.
% 0.73/1.12 { ! Y = X, alpha4( X, Y ) }.
% 0.73/1.12 { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 0.73/1.12 { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 0.73/1.12 { ! aNaturalNumber0( Y ), ! doDivides0( Y, X ), alpha3( X, Y ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sz00, X = sz10, aNaturalNumber0( skol4( Y ) )
% 0.73/1.12 }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sz00, X = sz10, isPrime0( skol4( Y ) ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), X = sz00, X = sz10, doDivides0( skol4( X ), X ) }
% 0.73/1.12 .
% 0.73/1.12 { aNaturalNumber0( xn ) }.
% 0.73/1.12 { aNaturalNumber0( xm ) }.
% 0.73/1.12 { aNaturalNumber0( xp ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.73/1.12 alpha7( Z ), ! aNaturalNumber0( T ), ! sdtasdt0( X, Y ) = sdtasdt0( Z, T
% 0.73/1.12 ), ! iLess0( sdtpldt0( sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0( xn, xm
% 0.73/1.12 ), xp ) ), alpha8( X, Z ), alpha10( Y, Z ) }.
% 0.73/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.73/1.12 alpha7( Z ), ! doDivides0( Z, sdtasdt0( X, Y ) ), ! iLess0( sdtpldt0(
% 8.99/9.44 sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0( xn, xm ), xp ) ), alpha8( X, Z
% 8.99/9.44 ), alpha10( Y, Z ) }.
% 8.99/9.44 { ! alpha10( X, Y ), aNaturalNumber0( skol5( Z, T ) ) }.
% 8.99/9.44 { ! alpha10( X, Y ), X = sdtasdt0( Y, skol5( X, Y ) ) }.
% 8.99/9.44 { ! alpha10( X, Y ), doDivides0( Y, X ) }.
% 8.99/9.44 { ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ), ! doDivides0( Y, X ),
% 8.99/9.44 alpha10( X, Y ) }.
% 8.99/9.44 { ! alpha8( X, Y ), aNaturalNumber0( skol6( Z, T ) ) }.
% 8.99/9.44 { ! alpha8( X, Y ), X = sdtasdt0( Y, skol6( X, Y ) ) }.
% 8.99/9.44 { ! alpha8( X, Y ), doDivides0( Y, X ) }.
% 8.99/9.44 { ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ), ! doDivides0( Y, X ),
% 8.99/9.44 alpha8( X, Y ) }.
% 8.99/9.44 { ! alpha7( X ), alpha9( X ) }.
% 8.99/9.44 { ! alpha7( X ), ! isPrime0( X ) }.
% 8.99/9.44 { ! alpha9( X ), isPrime0( X ), alpha7( X ) }.
% 8.99/9.44 { ! alpha9( X ), alpha11( X ), alpha12( X ) }.
% 8.99/9.44 { ! alpha11( X ), alpha9( X ) }.
% 8.99/9.44 { ! alpha12( X ), alpha9( X ) }.
% 8.99/9.44 { ! alpha12( X ), alpha13( X, skol7( X ) ) }.
% 8.99/9.44 { ! alpha12( X ), ! skol7( X ) = X }.
% 8.99/9.44 { ! alpha13( X, Y ), Y = X, alpha12( X ) }.
% 8.99/9.44 { ! alpha13( X, Y ), alpha14( X, Y ) }.
% 8.99/9.44 { ! alpha13( X, Y ), ! Y = sz10 }.
% 8.99/9.44 { ! alpha14( X, Y ), Y = sz10, alpha13( X, Y ) }.
% 8.99/9.44 { ! alpha14( X, Y ), alpha15( X, Y ) }.
% 8.99/9.44 { ! alpha14( X, Y ), doDivides0( Y, X ) }.
% 8.99/9.44 { ! alpha15( X, Y ), ! doDivides0( Y, X ), alpha14( X, Y ) }.
% 8.99/9.44 { ! alpha15( X, Y ), aNaturalNumber0( Y ) }.
% 8.99/9.44 { ! alpha15( X, Y ), aNaturalNumber0( skol8( Z, T ) ) }.
% 8.99/9.44 { ! alpha15( X, Y ), X = sdtasdt0( Y, skol8( X, Y ) ) }.
% 8.99/9.44 { ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ),
% 8.99/9.44 alpha15( X, Y ) }.
% 8.99/9.44 { ! alpha11( X ), X = sz00, X = sz10 }.
% 8.99/9.44 { ! X = sz00, alpha11( X ) }.
% 8.99/9.44 { ! X = sz10, alpha11( X ) }.
% 8.99/9.44 { ! xp = sz00 }.
% 8.99/9.44 { ! xp = sz10 }.
% 8.99/9.44 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! xp = sdtasdt0( X, Y ),
% 8.99/9.44 X = sz10, X = xp }.
% 8.99/9.44 { ! aNaturalNumber0( X ), ! doDivides0( X, xp ), X = sz10, X = xp }.
% 8.99/9.44 { isPrime0( xp ) }.
% 8.99/9.44 { aNaturalNumber0( skol9 ) }.
% 8.99/9.44 { sdtasdt0( xn, xm ) = sdtasdt0( xp, skol9 ) }.
% 8.99/9.44 { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 8.99/9.44 { aNaturalNumber0( skol10 ) }.
% 8.99/9.44 { sdtpldt0( xp, skol10 ) = xn }.
% 8.99/9.44 { sdtlseqdt0( xp, xn ) }.
% 8.99/9.44 { aNaturalNumber0( xr ) }.
% 8.99/9.44 { sdtpldt0( xp, xr ) = xn }.
% 8.99/9.44 { xr = sdtmndt0( xn, xp ) }.
% 8.99/9.44 { xr = xn, ! aNaturalNumber0( X ), ! sdtpldt0( xr, X ) = xn }.
% 8.99/9.44 { xr = xn, ! sdtlseqdt0( xr, xn ) }.
% 8.99/9.44
% 8.99/9.44 percentage equality = 0.275534, percentage horn = 0.734848
% 8.99/9.44 This is a problem with some equality
% 8.99/9.44
% 8.99/9.44
% 8.99/9.44
% 8.99/9.44 Options Used:
% 8.99/9.44
% 8.99/9.44 useres = 1
% 8.99/9.44 useparamod = 1
% 8.99/9.44 useeqrefl = 1
% 8.99/9.44 useeqfact = 1
% 8.99/9.44 usefactor = 1
% 8.99/9.44 usesimpsplitting = 0
% 8.99/9.44 usesimpdemod = 5
% 8.99/9.44 usesimpres = 3
% 8.99/9.44
% 8.99/9.44 resimpinuse = 1000
% 8.99/9.44 resimpclauses = 20000
% 8.99/9.44 substype = eqrewr
% 8.99/9.44 backwardsubs = 1
% 8.99/9.44 selectoldest = 5
% 8.99/9.44
% 8.99/9.44 litorderings [0] = split
% 8.99/9.44 litorderings [1] = extend the termordering, first sorting on arguments
% 8.99/9.44
% 8.99/9.44 termordering = kbo
% 8.99/9.44
% 8.99/9.44 litapriori = 0
% 8.99/9.44 termapriori = 1
% 8.99/9.44 litaposteriori = 0
% 8.99/9.44 termaposteriori = 0
% 8.99/9.44 demodaposteriori = 0
% 8.99/9.44 ordereqreflfact = 0
% 8.99/9.44
% 8.99/9.44 litselect = negord
% 8.99/9.44
% 8.99/9.44 maxweight = 15
% 8.99/9.44 maxdepth = 30000
% 8.99/9.44 maxlength = 115
% 8.99/9.44 maxnrvars = 195
% 8.99/9.44 excuselevel = 1
% 8.99/9.44 increasemaxweight = 1
% 8.99/9.44
% 8.99/9.44 maxselected = 10000000
% 8.99/9.44 maxnrclauses = 10000000
% 8.99/9.44
% 8.99/9.44 showgenerated = 0
% 8.99/9.44 showkept = 0
% 8.99/9.44 showselected = 0
% 8.99/9.44 showdeleted = 0
% 8.99/9.44 showresimp = 1
% 8.99/9.44 showstatus = 2000
% 8.99/9.44
% 8.99/9.44 prologoutput = 0
% 8.99/9.44 nrgoals = 5000000
% 8.99/9.44 totalproof = 1
% 8.99/9.44
% 8.99/9.44 Symbols occurring in the translation:
% 8.99/9.44
% 8.99/9.44 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 8.99/9.44 . [1, 2] (w:1, o:35, a:1, s:1, b:0),
% 8.99/9.44 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 8.99/9.44 ! [4, 1] (w:0, o:19, a:1, s:1, b:0),
% 8.99/9.44 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 8.99/9.44 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 8.99/9.44 aNaturalNumber0 [36, 1] (w:1, o:24, a:1, s:1, b:0),
% 8.99/9.44 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 8.99/9.44 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 8.99/9.44 sdtpldt0 [40, 2] (w:1, o:59, a:1, s:1, b:0),
% 8.99/9.44 sdtasdt0 [41, 2] (w:1, o:60, a:1, s:1, b:0),
% 8.99/9.44 sdtlseqdt0 [43, 2] (w:1, o:61, a:1, s:1, b:0),
% 8.99/9.44 sdtmndt0 [44, 2] (w:1, o:62, a:1, s:1, b:0),
% 8.99/9.44 iLess0 [45, 2] (w:1, o:63, a:1, s:1, b:0),
% 8.99/9.44 doDivides0 [46, 2] (w:1, o:64, a:1, s:1, b:0),
% 8.99/9.44 sdtsldt0 [47, 2] (w:1, o:65, a:1, s:1, b:0),
% 29.42/29.80 isPrime0 [48, 1] (w:1, o:25, a:1, s:1, b:0),
% 29.42/29.80 xn [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 29.42/29.80 xm [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 29.42/29.80 xp [51, 0] (w:1, o:13, a:1, s:1, b:0),
% 29.42/29.80 xr [54, 0] (w:1, o:16, a:1, s:1, b:0),
% 29.42/29.80 alpha1 [55, 1] (w:1, o:26, a:1, s:1, b:1),
% 29.42/29.80 alpha2 [56, 1] (w:1, o:29, a:1, s:1, b:1),
% 29.42/29.80 alpha3 [57, 2] (w:1, o:66, a:1, s:1, b:1),
% 29.42/29.80 alpha4 [58, 2] (w:1, o:67, a:1, s:1, b:1),
% 29.42/29.80 alpha5 [59, 3] (w:1, o:78, a:1, s:1, b:1),
% 29.42/29.80 alpha6 [60, 3] (w:1, o:79, a:1, s:1, b:1),
% 29.42/29.80 alpha7 [61, 1] (w:1, o:30, a:1, s:1, b:1),
% 29.42/29.80 alpha8 [62, 2] (w:1, o:68, a:1, s:1, b:1),
% 29.42/29.80 alpha9 [63, 1] (w:1, o:31, a:1, s:1, b:1),
% 29.42/29.80 alpha10 [64, 2] (w:1, o:69, a:1, s:1, b:1),
% 29.42/29.80 alpha11 [65, 1] (w:1, o:27, a:1, s:1, b:1),
% 29.42/29.80 alpha12 [66, 1] (w:1, o:28, a:1, s:1, b:1),
% 29.42/29.80 alpha13 [67, 2] (w:1, o:70, a:1, s:1, b:1),
% 29.42/29.80 alpha14 [68, 2] (w:1, o:71, a:1, s:1, b:1),
% 29.42/29.80 alpha15 [69, 2] (w:1, o:72, a:1, s:1, b:1),
% 29.42/29.80 skol1 [70, 2] (w:1, o:73, a:1, s:1, b:1),
% 29.42/29.80 skol2 [71, 2] (w:1, o:74, a:1, s:1, b:1),
% 29.42/29.80 skol3 [72, 1] (w:1, o:32, a:1, s:1, b:1),
% 29.42/29.80 skol4 [73, 1] (w:1, o:33, a:1, s:1, b:1),
% 29.42/29.80 skol5 [74, 2] (w:1, o:75, a:1, s:1, b:1),
% 29.42/29.80 skol6 [75, 2] (w:1, o:76, a:1, s:1, b:1),
% 29.42/29.80 skol7 [76, 1] (w:1, o:34, a:1, s:1, b:1),
% 29.42/29.80 skol8 [77, 2] (w:1, o:77, a:1, s:1, b:1),
% 29.42/29.80 skol9 [78, 0] (w:1, o:17, a:1, s:1, b:1),
% 29.42/29.80 skol10 [79, 0] (w:1, o:18, a:1, s:1, b:1).
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Starting Search:
% 29.42/29.80
% 29.42/29.80 *** allocated 15000 integers for clauses
% 29.42/29.80 *** allocated 22500 integers for clauses
% 29.42/29.80 *** allocated 33750 integers for clauses
% 29.42/29.80 *** allocated 15000 integers for termspace/termends
% 29.42/29.80 *** allocated 50625 integers for clauses
% 29.42/29.80 *** allocated 75937 integers for clauses
% 29.42/29.80 *** allocated 22500 integers for termspace/termends
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 33750 integers for termspace/termends
% 29.42/29.80 *** allocated 113905 integers for clauses
% 29.42/29.80 *** allocated 50625 integers for termspace/termends
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 11835
% 29.42/29.80 Kept: 2002
% 29.42/29.80 Inuse: 135
% 29.42/29.80 Deleted: 1
% 29.42/29.80 Deletedinuse: 0
% 29.42/29.80
% 29.42/29.80 *** allocated 170857 integers for clauses
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 75937 integers for termspace/termends
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 256285 integers for clauses
% 29.42/29.80 *** allocated 113905 integers for termspace/termends
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 24001
% 29.42/29.80 Kept: 4036
% 29.42/29.80 Inuse: 184
% 29.42/29.80 Deleted: 2
% 29.42/29.80 Deletedinuse: 0
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 384427 integers for clauses
% 29.42/29.80 *** allocated 170857 integers for termspace/termends
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 42148
% 29.42/29.80 Kept: 6036
% 29.42/29.80 Inuse: 222
% 29.42/29.80 Deleted: 4
% 29.42/29.80 Deletedinuse: 0
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 55966
% 29.42/29.80 Kept: 8192
% 29.42/29.80 Inuse: 258
% 29.42/29.80 Deleted: 9
% 29.42/29.80 Deletedinuse: 1
% 29.42/29.80
% 29.42/29.80 *** allocated 256285 integers for termspace/termends
% 29.42/29.80 *** allocated 576640 integers for clauses
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 78579
% 29.42/29.80 Kept: 10374
% 29.42/29.80 Inuse: 293
% 29.42/29.80 Deleted: 21
% 29.42/29.80 Deletedinuse: 8
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 384427 integers for termspace/termends
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 93243
% 29.42/29.80 Kept: 12750
% 29.42/29.80 Inuse: 338
% 29.42/29.80 Deleted: 31
% 29.42/29.80 Deletedinuse: 13
% 29.42/29.80
% 29.42/29.80 *** allocated 864960 integers for clauses
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 110293
% 29.42/29.80 Kept: 14784
% 29.42/29.80 Inuse: 383
% 29.42/29.80 Deleted: 35
% 29.42/29.80 Deletedinuse: 17
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 116784
% 29.42/29.80 Kept: 16784
% 29.42/29.80 Inuse: 438
% 29.42/29.80 Deleted: 37
% 29.42/29.80 Deletedinuse: 19
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 576640 integers for termspace/termends
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 132256
% 29.42/29.80 Kept: 18788
% 29.42/29.80 Inuse: 495
% 29.42/29.80 Deleted: 38
% 29.42/29.80 Deletedinuse: 20
% 29.42/29.80
% 29.42/29.80 *** allocated 1297440 integers for clauses
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying clauses:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 144707
% 29.42/29.80 Kept: 21253
% 29.42/29.80 Inuse: 560
% 29.42/29.80 Deleted: 4599
% 29.42/29.80 Deletedinuse: 20
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 162570
% 29.42/29.80 Kept: 23262
% 29.42/29.80 Inuse: 620
% 29.42/29.80 Deleted: 4642
% 29.42/29.80 Deletedinuse: 63
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 178258
% 29.42/29.80 Kept: 25266
% 29.42/29.80 Inuse: 684
% 29.42/29.80 Deleted: 4646
% 29.42/29.80 Deletedinuse: 67
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 201776
% 29.42/29.80 Kept: 27300
% 29.42/29.80 Inuse: 751
% 29.42/29.80 Deleted: 4648
% 29.42/29.80 Deletedinuse: 67
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 1946160 integers for clauses
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 228255
% 29.42/29.80 Kept: 29312
% 29.42/29.80 Inuse: 832
% 29.42/29.80 Deleted: 4658
% 29.42/29.80 Deletedinuse: 67
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 237968
% 29.42/29.80 Kept: 31363
% 29.42/29.80 Inuse: 860
% 29.42/29.80 Deleted: 4658
% 29.42/29.80 Deletedinuse: 67
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 864960 integers for termspace/termends
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 248156
% 29.42/29.80 Kept: 33369
% 29.42/29.80 Inuse: 878
% 29.42/29.80 Deleted: 4658
% 29.42/29.80 Deletedinuse: 67
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 257455
% 29.42/29.80 Kept: 35389
% 29.42/29.80 Inuse: 927
% 29.42/29.80 Deleted: 4658
% 29.42/29.80 Deletedinuse: 67
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 262737
% 29.42/29.80 Kept: 37890
% 29.42/29.80 Inuse: 938
% 29.42/29.80 Deleted: 4658
% 29.42/29.80 Deletedinuse: 67
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Intermediate Status:
% 29.42/29.80 Generated: 268762
% 29.42/29.80 Kept: 40011
% 29.42/29.80 Inuse: 953
% 29.42/29.80 Deleted: 4658
% 29.42/29.80 Deletedinuse: 67
% 29.42/29.80
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 *** allocated 2919240 integers for clauses
% 29.42/29.80 Resimplifying inuse:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80 Resimplifying clauses:
% 29.42/29.80 Done
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Bliksems!, er is een bewijs:
% 29.42/29.80 % SZS status Theorem
% 29.42/29.80 % SZS output start Refutation
% 29.42/29.80
% 29.42/29.80 (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 29.42/29.80 (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 29.42/29.80 (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 29.42/29.80 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 29.42/29.80 (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) ==>
% 29.42/29.80 X }.
% 29.42/29.80 (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( sz00, X ) ==>
% 29.42/29.80 X }.
% 29.42/29.80 (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 29.42/29.80 }.
% 29.42/29.80 (19) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z
% 29.42/29.80 }.
% 29.42/29.80 (23) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 29.42/29.80 (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 29.42/29.80 }.
% 29.42/29.80 (28) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 29.42/29.80 }.
% 29.42/29.80 (29) {G0,W17,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 29.42/29.80 }.
% 29.42/29.80 (30) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y
% 29.42/29.80 , Z = sdtmndt0( Y, X ) }.
% 29.42/29.80 (31) {G0,W5,D2,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 29.42/29.80 (34) {G0,W10,D2,L4,V2,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), sdtlseqdt0( X, Y ), ! Y = X }.
% 29.42/29.80 (72) {G0,W9,D2,L3,V2,M3} I { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 29.42/29.80 (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 29.42/29.80 (81) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 29.42/29.80 (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 29.42/29.80 (116) {G0,W3,D2,L1,V0,M1} I { ! xp ==> sz00 }.
% 29.42/29.80 (124) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol10 ) }.
% 29.42/29.80 (125) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xp, skol10 ) ==> xn }.
% 29.42/29.80 (126) {G0,W3,D2,L1,V0,M1} I { sdtlseqdt0( xp, xn ) }.
% 29.42/29.80 (127) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 29.42/29.80 (128) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xp, xr ) ==> xn }.
% 29.42/29.80 (129) {G0,W5,D3,L1,V0,M1} I { sdtmndt0( xn, xp ) ==> xr }.
% 29.42/29.80 (130) {G0,W10,D3,L3,V1,M3} I { xr ==> xn, ! aNaturalNumber0( X ), !
% 29.42/29.80 sdtpldt0( xr, X ) ==> xn }.
% 29.42/29.80 (262) {G1,W6,D2,L2,V1,M2} F(72) { ! alpha4( sz10, X ), X = sz10 }.
% 29.42/29.80 (937) {G1,W14,D3,L4,V2,M4} P(19,116);r(83) { ! X = sz00, ! aNaturalNumber0
% 29.42/29.80 ( Y ), ! aNaturalNumber0( X ), ! sdtpldt0( xp, Y ) = sdtpldt0( X, Y ) }.
% 29.42/29.80 (953) {G2,W7,D3,L2,V1,M2} Q(937);d(9);r(1) { ! aNaturalNumber0( X ), !
% 29.42/29.80 sdtpldt0( xp, X ) ==> X }.
% 29.42/29.80 (1490) {G1,W16,D3,L4,V2,M4} P(18,128);r(127) { sdtpldt0( xp, X ) ==> xn, !
% 29.42/29.80 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtpldt0( Y, xr ) =
% 29.42/29.80 sdtpldt0( Y, X ) }.
% 29.42/29.80 (1492) {G1,W7,D3,L2,V0,M2} P(128,6);r(83) { ! aNaturalNumber0( xr ),
% 29.42/29.80 sdtpldt0( xr, xp ) ==> xn }.
% 29.42/29.80 (1494) {G2,W14,D3,L3,V1,M3} F(1490) { sdtpldt0( xp, X ) ==> xn, !
% 29.42/29.80 aNaturalNumber0( X ), ! sdtpldt0( X, xr ) = sdtpldt0( X, X ) }.
% 29.42/29.80 (1914) {G1,W10,D2,L4,V2,M4} R(27,1);d(9) { ! aNaturalNumber0( X ), !
% 29.42/29.80 aNaturalNumber0( Y ), sdtlseqdt0( sz00, X ), ! Y = X }.
% 29.42/29.80 (1965) {G2,W5,D2,L2,V1,M2} F(1914);q { ! aNaturalNumber0( X ), sdtlseqdt0(
% 29.42/29.80 sz00, X ) }.
% 29.42/29.80 (2014) {G3,W3,D2,L1,V0,M1} R(1965,124) { sdtlseqdt0( sz00, skol10 ) }.
% 29.42/29.80 (2547) {G3,W12,D3,L4,V2,M4} R(30,1965);f;d(9);r(1) { ! aNaturalNumber0( X )
% 29.42/29.80 , ! aNaturalNumber0( Y ), Y = sdtmndt0( X, sz00 ), ! Y = X }.
% 29.42/29.80 (2588) {G1,W15,D3,L5,V2,M5} R(30,1);d(8) { ! aNaturalNumber0( X ), !
% 29.42/29.80 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), sdtmndt0( Y, X ) ==> sz00, !
% 29.42/29.80 X = Y }.
% 29.42/29.80 (2619) {G1,W15,D3,L5,V1,M5} P(125,30);r(83) { ! aNaturalNumber0( X ), !
% 29.42/29.80 sdtlseqdt0( xp, X ), ! aNaturalNumber0( skol10 ), ! xn = X, sdtmndt0( X,
% 29.42/29.80 xp ) ==> skol10 }.
% 29.42/29.80 (2654) {G2,W8,D2,L3,V0,M3} Q(2619);d(129);r(81) { ! sdtlseqdt0( xp, xn ), !
% 29.42/29.80 aNaturalNumber0( skol10 ), skol10 ==> xr }.
% 29.42/29.80 (2670) {G2,W7,D3,L2,V1,M2} F(2588);q;r(31) { ! aNaturalNumber0( X ),
% 29.42/29.80 sdtmndt0( X, X ) ==> sz00 }.
% 29.42/29.80 (2692) {G4,W7,D3,L2,V1,M2} F(2547);q { ! aNaturalNumber0( X ), sdtmndt0( X
% 29.42/29.80 , sz00 ) ==> X }.
% 29.42/29.80 (3676) {G2,W5,D2,L2,V1,M2} P(262,2) { aNaturalNumber0( X ), ! alpha4( sz10
% 29.42/29.80 , X ) }.
% 29.42/29.80 (4045) {G3,W5,D2,L2,V1,M2} R(3676,73) { aNaturalNumber0( X ), ! X = sz10
% 29.42/29.80 }.
% 29.42/29.80 (4064) {G4,W11,D2,L4,V2,M4} R(4045,34) { ! X = sz10, ! aNaturalNumber0( Y )
% 29.42/29.80 , sdtlseqdt0( Y, X ), ! X = Y }.
% 29.42/29.80 (4098) {G5,W6,D2,L2,V1,M2} F(4064);r(2) { ! X = sz10, sdtlseqdt0( sz10, X )
% 29.42/29.80 }.
% 29.42/29.80 (4204) {G6,W12,D3,L4,V2,M4} R(4098,28);r(2) { ! X = sz10, ! aNaturalNumber0
% 29.42/29.80 ( X ), ! Y = sdtmndt0( X, sz10 ), aNaturalNumber0( Y ) }.
% 29.42/29.80 (4214) {G7,W5,D2,L2,V1,M2} Q(4204);d(2670);r(2) { aNaturalNumber0( X ), ! X
% 29.42/29.80 = sz00 }.
% 29.42/29.80 (4227) {G8,W13,D3,L4,V2,M4} R(4214,23) { ! X = sz00, ! aNaturalNumber0( Y )
% 29.42/29.80 , ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 29.42/29.80 (4242) {G9,W6,D2,L2,V1,M2} Q(4227);d(9);r(4214) { X = sz00, ! X = sz00 }.
% 29.42/29.80 (4271) {G10,W6,D2,L2,V1,M2} P(4242,2014) { sdtlseqdt0( X, skol10 ), ! X =
% 29.42/29.80 sz00 }.
% 29.42/29.80 (5847) {G11,W15,D3,L4,V2,M4} R(4271,29);r(4214) { ! X = sz00, !
% 29.42/29.80 aNaturalNumber0( skol10 ), ! Y = sdtmndt0( skol10, X ), sdtpldt0( X, Y )
% 29.42/29.80 ==> skol10 }.
% 29.42/29.80 (5848) {G11,W12,D3,L4,V2,M4} R(4271,28);r(4214) { ! X = sz00, !
% 29.42/29.80 aNaturalNumber0( skol10 ), ! Y = sdtmndt0( skol10, X ), aNaturalNumber0(
% 29.42/29.80 Y ) }.
% 29.42/29.80 (5859) {G12,W5,D2,L2,V1,M2} Q(5848);d(2692);r(124) { aNaturalNumber0( X ),
% 29.42/29.80 ! X = skol10 }.
% 29.42/29.80 (5862) {G12,W8,D3,L2,V1,M2} Q(5847);d(2692);r(124) { sdtpldt0( sz00, X )
% 29.42/29.80 ==> skol10, ! X = skol10 }.
% 29.42/29.80 (5891) {G13,W6,D2,L2,V1,M2} R(5859,9);d(5862) { ! X = skol10, skol10 = X
% 29.42/29.80 }.
% 29.42/29.80 (6298) {G14,W8,D2,L3,V2,M3} P(5891,5859) { aNaturalNumber0( Y ), ! Y = X, !
% 29.42/29.80 X = skol10 }.
% 29.42/29.80 (18003) {G1,W8,D3,L2,V0,M2} R(130,83) { xr ==> xn, ! sdtpldt0( xr, xp ) ==>
% 29.42/29.80 xn }.
% 29.42/29.80 (21148) {G3,W3,D2,L1,V0,M1} S(2654);r(126);r(124) { skol10 ==> xr }.
% 29.42/29.80 (21158) {G2,W5,D3,L1,V0,M1} S(1492);r(127) { sdtpldt0( xr, xp ) ==> xn }.
% 29.42/29.80 (42297) {G3,W3,D2,L1,V0,M1} S(18003);d(21158);q { xr ==> xn }.
% 29.42/29.80 (42449) {G15,W8,D2,L3,V2,M3} S(6298);d(21148);d(42297) { aNaturalNumber0( Y
% 29.42/29.80 ), ! Y = X, ! X = xn }.
% 29.42/29.80 (42535) {G4,W14,D3,L3,V1,M3} S(1494);d(42297) { sdtpldt0( xp, X ) ==> xn, !
% 29.42/29.80 aNaturalNumber0( X ), ! sdtpldt0( X, xn ) = sdtpldt0( X, X ) }.
% 29.42/29.80 (42552) {G5,W2,D2,L1,V0,M1} Q(42535);r(953) { ! aNaturalNumber0( xn ) }.
% 29.42/29.80 (42555) {G16,W0,D0,L0,V0,M0} F(42449);q;r(42552) { }.
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 % SZS output end Refutation
% 29.42/29.80 found a proof!
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Unprocessed initial clauses:
% 29.42/29.80
% 29.42/29.80 (42557) {G0,W1,D1,L1,V0,M1} { && }.
% 29.42/29.80 (42558) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 29.42/29.80 (42559) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 29.42/29.80 (42560) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 29.42/29.80 (42561) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 29.42/29.80 (42562) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 29.42/29.80 ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 29.42/29.80 (42563) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 29.42/29.80 (42564) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0(
% 29.42/29.80 X, sdtpldt0( Y, Z ) ) }.
% 29.42/29.80 (42565) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 )
% 29.42/29.80 = X }.
% 29.42/29.80 (42566) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtpldt0( sz00,
% 29.42/29.80 X ) }.
% 29.42/29.80 (42567) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 29.42/29.80 (42568) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0(
% 29.42/29.80 X, sdtasdt0( Y, Z ) ) }.
% 29.42/29.80 (42569) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 29.42/29.80 = X }.
% 29.42/29.80 (42570) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtasdt0( sz10,
% 29.42/29.80 X ) }.
% 29.42/29.80 (42571) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 )
% 29.42/29.80 = sz00 }.
% 29.42/29.80 (42572) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sz00 = sdtasdt0(
% 29.42/29.80 sz00, X ) }.
% 29.42/29.80 (42573) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0(
% 29.42/29.80 sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 29.42/29.80 (42574) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0(
% 29.42/29.80 sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 29.42/29.80 (42575) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 29.42/29.80 }.
% 29.42/29.80 (42576) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z
% 29.42/29.80 }.
% 29.42/29.80 (42577) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 29.42/29.80 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 29.42/29.80 sdtasdt0( X, Z ), Y = Z }.
% 29.42/29.80 (42578) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 29.42/29.80 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) =
% 29.42/29.80 sdtasdt0( Z, X ), Y = Z }.
% 29.42/29.80 (42579) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 29.42/29.80 (42580) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 29.42/29.80 (42581) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 29.42/29.80 (42582) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtlseqdt0( X, Y ), aNaturalNumber0( skol1( Z, T ) ) }.
% 29.42/29.80 (42583) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtlseqdt0( X, Y ), sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 29.42/29.80 (42584) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 29.42/29.80 }.
% 29.42/29.80 (42585) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 29.42/29.80 }.
% 29.42/29.80 (42586) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 29.42/29.80 }.
% 29.42/29.80 (42587) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y
% 29.42/29.80 , Z = sdtmndt0( Y, X ) }.
% 29.42/29.80 (42588) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0( X, X )
% 29.42/29.80 }.
% 29.42/29.80 (42589) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 29.42/29.80 (42590) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ),
% 29.42/29.80 sdtlseqdt0( X, Z ) }.
% 29.42/29.80 (42591) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 29.42/29.80 (42592) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), sdtlseqdt0( X, Y ), sdtlseqdt0( Y, X ) }.
% 29.42/29.80 (42593) {G0,W16,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z
% 29.42/29.80 ) }.
% 29.42/29.80 (42594) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), sdtlseqdt0(
% 29.42/29.80 sdtpldt0( X, Z ), sdtpldt0( Y, Z ) ) }.
% 29.42/29.80 (42595) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) =
% 29.42/29.80 sdtpldt0( Z, Y ) }.
% 29.42/29.80 (42596) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0(
% 29.42/29.80 Z, X ), sdtpldt0( Z, Y ) ) }.
% 29.42/29.80 (42597) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) =
% 29.42/29.80 sdtpldt0( Y, Z ) }.
% 29.42/29.80 (42598) {G0,W25,D3,L4,V3,M4} { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), !
% 29.42/29.80 sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) =
% 29.42/29.80 sdtpldt0( Y, Z ), alpha5( X, Y, Z ) }.
% 29.42/29.80 (42599) {G0,W19,D2,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 29.42/29.80 alpha6( X, Y, Z ) }.
% 29.42/29.80 (42600) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 29.42/29.80 sdtlseqdt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 29.42/29.80 (42601) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) =
% 29.42/29.80 sdtasdt0( X, Z ) }.
% 29.42/29.80 (42602) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0(
% 29.42/29.80 X, Y ), sdtasdt0( X, Z ) ) }.
% 29.42/29.80 (42603) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) =
% 29.42/29.80 sdtasdt0( Z, X ) }.
% 29.42/29.80 (42604) {G0,W25,D3,L4,V3,M4} { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), !
% 29.42/29.80 sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) =
% 29.42/29.80 sdtasdt0( Z, X ), alpha6( X, Y, Z ) }.
% 29.42/29.80 (42605) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 29.42/29.80 , ! sz10 = X }.
% 29.42/29.80 (42606) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 29.42/29.80 , sdtlseqdt0( sz10, X ) }.
% 29.42/29.80 (42607) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), X = sz00, sdtlseqdt0( Y, sdtasdt0( Y, X ) ) }.
% 29.42/29.80 (42608) {G0,W1,D1,L1,V0,M1} { && }.
% 29.42/29.80 (42609) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), X = Y, ! sdtlseqdt0( X, Y ), iLess0( X, Y ) }.
% 29.42/29.80 (42610) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! doDivides0( X, Y ), aNaturalNumber0( skol2( Z, T ) ) }.
% 29.42/29.80 (42611) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! doDivides0( X, Y ), Y = sdtasdt0( X, skol2( X, Y ) ) }.
% 29.42/29.80 (42612) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 29.42/29.80 }.
% 29.42/29.80 (42613) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 29.42/29.80 aNaturalNumber0( Z ) }.
% 29.42/29.80 (42614) {G0,W20,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0
% 29.42/29.80 ( X, Z ) }.
% 29.42/29.80 (42615) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), ! Y =
% 29.42/29.80 sdtasdt0( X, Z ), Z = sdtsldt0( Y, X ) }.
% 29.42/29.80 (42616) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( Y, Z ),
% 29.42/29.80 doDivides0( X, Z ) }.
% 29.42/29.80 (42617) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X, Z ),
% 29.42/29.80 doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 29.42/29.80 (42618) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X,
% 29.42/29.80 sdtpldt0( Y, Z ) ), doDivides0( X, Z ) }.
% 29.42/29.80 (42619) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! doDivides0( X, Y ), Y = sz00, sdtlseqdt0( X, Y ) }.
% 29.42/29.80 (42620) {G0,W23,D4,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z
% 29.42/29.80 , sdtsldt0( Y, X ) ) = sdtsldt0( sdtasdt0( Z, Y ), X ) }.
% 29.42/29.80 (42621) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X
% 29.42/29.80 = sz00 }.
% 29.42/29.80 (42622) {G0,W6,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ),
% 29.42/29.80 alpha1( X ) }.
% 29.42/29.80 (42623) {G0,W9,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, ! alpha1(
% 29.42/29.80 X ), isPrime0( X ) }.
% 29.42/29.80 (42624) {G0,W5,D2,L2,V1,M2} { ! alpha1( X ), ! X = sz10 }.
% 29.42/29.80 (42625) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), alpha2( X ) }.
% 29.42/29.80 (42626) {G0,W7,D2,L3,V1,M3} { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 29.42/29.80 (42627) {G0,W8,D2,L3,V2,M3} { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X,
% 29.42/29.80 Y ) }.
% 29.42/29.80 (42628) {G0,W6,D3,L2,V1,M2} { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 29.42/29.80 (42629) {G0,W6,D3,L2,V1,M2} { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 29.42/29.80 (42630) {G0,W9,D2,L3,V2,M3} { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 29.42/29.80 (42631) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha4( X, Y ) }.
% 29.42/29.80 (42632) {G0,W6,D2,L2,V2,M2} { ! Y = X, alpha4( X, Y ) }.
% 29.42/29.80 (42633) {G0,W5,D2,L2,V2,M2} { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 29.42/29.80 (42634) {G0,W6,D2,L2,V2,M2} { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 29.42/29.80 (42635) {G0,W8,D2,L3,V2,M3} { ! aNaturalNumber0( Y ), ! doDivides0( Y, X )
% 29.42/29.80 , alpha3( X, Y ) }.
% 29.42/29.80 (42636) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 29.42/29.80 , aNaturalNumber0( skol4( Y ) ) }.
% 29.42/29.80 (42637) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 29.42/29.80 , isPrime0( skol4( Y ) ) }.
% 29.42/29.80 (42638) {G0,W12,D3,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 29.42/29.80 , doDivides0( skol4( X ), X ) }.
% 29.42/29.80 (42639) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 29.42/29.80 (42640) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 29.42/29.80 (42641) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 29.42/29.80 (42642) {G0,W34,D4,L9,V4,M9} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), alpha7( Z ), ! aNaturalNumber0( T ), !
% 29.42/29.80 sdtasdt0( X, Y ) = sdtasdt0( Z, T ), ! iLess0( sdtpldt0( sdtpldt0( X, Y )
% 29.42/29.80 , Z ), sdtpldt0( sdtpldt0( xn, xm ), xp ) ), alpha8( X, Z ), alpha10( Y,
% 29.42/29.80 Z ) }.
% 29.42/29.80 (42643) {G0,W30,D4,L8,V3,M8} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! aNaturalNumber0( Z ), alpha7( Z ), ! doDivides0( Z, sdtasdt0( X, Y
% 29.42/29.80 ) ), ! iLess0( sdtpldt0( sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0( xn,
% 29.42/29.80 xm ), xp ) ), alpha8( X, Z ), alpha10( Y, Z ) }.
% 29.42/29.80 (42644) {G0,W7,D3,L2,V4,M2} { ! alpha10( X, Y ), aNaturalNumber0( skol5( Z
% 29.42/29.80 , T ) ) }.
% 29.42/29.80 (42645) {G0,W10,D4,L2,V2,M2} { ! alpha10( X, Y ), X = sdtasdt0( Y, skol5(
% 29.42/29.80 X, Y ) ) }.
% 29.42/29.80 (42646) {G0,W6,D2,L2,V2,M2} { ! alpha10( X, Y ), doDivides0( Y, X ) }.
% 29.42/29.80 (42647) {G0,W13,D3,L4,V3,M4} { ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y,
% 29.42/29.80 Z ), ! doDivides0( Y, X ), alpha10( X, Y ) }.
% 29.42/29.80 (42648) {G0,W7,D3,L2,V4,M2} { ! alpha8( X, Y ), aNaturalNumber0( skol6( Z
% 29.42/29.80 , T ) ) }.
% 29.42/29.80 (42649) {G0,W10,D4,L2,V2,M2} { ! alpha8( X, Y ), X = sdtasdt0( Y, skol6( X
% 29.42/29.80 , Y ) ) }.
% 29.42/29.80 (42650) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), doDivides0( Y, X ) }.
% 29.42/29.80 (42651) {G0,W13,D3,L4,V3,M4} { ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y,
% 29.42/29.80 Z ), ! doDivides0( Y, X ), alpha8( X, Y ) }.
% 29.42/29.80 (42652) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), alpha9( X ) }.
% 29.42/29.80 (42653) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), ! isPrime0( X ) }.
% 29.42/29.80 (42654) {G0,W6,D2,L3,V1,M3} { ! alpha9( X ), isPrime0( X ), alpha7( X )
% 29.42/29.80 }.
% 29.42/29.80 (42655) {G0,W6,D2,L3,V1,M3} { ! alpha9( X ), alpha11( X ), alpha12( X )
% 29.42/29.80 }.
% 29.42/29.80 (42656) {G0,W4,D2,L2,V1,M2} { ! alpha11( X ), alpha9( X ) }.
% 29.42/29.80 (42657) {G0,W4,D2,L2,V1,M2} { ! alpha12( X ), alpha9( X ) }.
% 29.42/29.80 (42658) {G0,W6,D3,L2,V1,M2} { ! alpha12( X ), alpha13( X, skol7( X ) ) }.
% 29.42/29.80 (42659) {G0,W6,D3,L2,V1,M2} { ! alpha12( X ), ! skol7( X ) = X }.
% 29.42/29.80 (42660) {G0,W8,D2,L3,V2,M3} { ! alpha13( X, Y ), Y = X, alpha12( X ) }.
% 29.42/29.80 (42661) {G0,W6,D2,L2,V2,M2} { ! alpha13( X, Y ), alpha14( X, Y ) }.
% 29.42/29.80 (42662) {G0,W6,D2,L2,V2,M2} { ! alpha13( X, Y ), ! Y = sz10 }.
% 29.42/29.80 (42663) {G0,W9,D2,L3,V2,M3} { ! alpha14( X, Y ), Y = sz10, alpha13( X, Y )
% 29.42/29.80 }.
% 29.42/29.80 (42664) {G0,W6,D2,L2,V2,M2} { ! alpha14( X, Y ), alpha15( X, Y ) }.
% 29.42/29.80 (42665) {G0,W6,D2,L2,V2,M2} { ! alpha14( X, Y ), doDivides0( Y, X ) }.
% 29.42/29.80 (42666) {G0,W9,D2,L3,V2,M3} { ! alpha15( X, Y ), ! doDivides0( Y, X ),
% 29.42/29.80 alpha14( X, Y ) }.
% 29.42/29.80 (42667) {G0,W5,D2,L2,V2,M2} { ! alpha15( X, Y ), aNaturalNumber0( Y ) }.
% 29.42/29.80 (42668) {G0,W7,D3,L2,V4,M2} { ! alpha15( X, Y ), aNaturalNumber0( skol8( Z
% 29.42/29.80 , T ) ) }.
% 29.42/29.80 (42669) {G0,W10,D4,L2,V2,M2} { ! alpha15( X, Y ), X = sdtasdt0( Y, skol8(
% 29.42/29.80 X, Y ) ) }.
% 29.42/29.80 (42670) {G0,W12,D3,L4,V3,M4} { ! aNaturalNumber0( Y ), ! aNaturalNumber0(
% 29.42/29.80 Z ), ! X = sdtasdt0( Y, Z ), alpha15( X, Y ) }.
% 29.42/29.80 (42671) {G0,W8,D2,L3,V1,M3} { ! alpha11( X ), X = sz00, X = sz10 }.
% 29.42/29.80 (42672) {G0,W5,D2,L2,V1,M2} { ! X = sz00, alpha11( X ) }.
% 29.42/29.80 (42673) {G0,W5,D2,L2,V1,M2} { ! X = sz10, alpha11( X ) }.
% 29.42/29.80 (42674) {G0,W3,D2,L1,V0,M1} { ! xp = sz00 }.
% 29.42/29.80 (42675) {G0,W3,D2,L1,V0,M1} { ! xp = sz10 }.
% 29.42/29.80 (42676) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 29.42/29.80 Y ), ! xp = sdtasdt0( X, Y ), X = sz10, X = xp }.
% 29.42/29.80 (42677) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), ! doDivides0( X, xp
% 29.42/29.80 ), X = sz10, X = xp }.
% 29.42/29.80 (42678) {G0,W2,D2,L1,V0,M1} { isPrime0( xp ) }.
% 29.42/29.80 (42679) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol9 ) }.
% 29.42/29.80 (42680) {G0,W7,D3,L1,V0,M1} { sdtasdt0( xn, xm ) = sdtasdt0( xp, skol9 )
% 29.42/29.80 }.
% 29.42/29.80 (42681) {G0,W5,D3,L1,V0,M1} { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 29.42/29.80 (42682) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol10 ) }.
% 29.42/29.80 (42683) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xp, skol10 ) = xn }.
% 29.42/29.80 (42684) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xp, xn ) }.
% 29.42/29.80 (42685) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xr ) }.
% 29.42/29.80 (42686) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xp, xr ) = xn }.
% 29.42/29.80 (42687) {G0,W5,D3,L1,V0,M1} { xr = sdtmndt0( xn, xp ) }.
% 29.42/29.80 (42688) {G0,W10,D3,L3,V1,M3} { xr = xn, ! aNaturalNumber0( X ), ! sdtpldt0
% 29.42/29.80 ( xr, X ) = xn }.
% 29.42/29.80 (42689) {G0,W6,D2,L2,V0,M2} { xr = xn, ! sdtlseqdt0( xr, xn ) }.
% 29.42/29.80
% 29.42/29.80
% 29.42/29.80 Total Proof:
% 29.42/29.80
% 29.42/29.80 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 29.42/29.80 parent0: (42558) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 29.42/29.80 substitution0:
% 29.42/29.80 end
% 29.42/29.80 permutation0:
% 29.42/29.80 0 ==> 0
% 29.42/29.80 end
% 29.42/29.80
% 29.42/29.80 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 29.42/29.80 parent0: (42559) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 29.42/29.80 substitution0:
% 29.42/29.80 end
% 29.42/29.80 permutation0:
% 29.42/29.80 0 ==> 0
% 29.42/29.80 end
% 29.42/29.80
% 29.42/29.80 subsumption: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 29.42/29.80 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 29.42/29.80 parent0: (42563) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 29.42/29.80 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 29.42/29.80 substitution0:
% 29.42/29.80 X := X
% 29.42/29.80 Y := Y
% 29.42/29.80 end
% 29.42/29.80 permutation0:
% 29.42/29.80 0 ==> 0
% 29.42/29.80 1 ==> 1
% 29.42/29.80 2 ==> 2
% 29.42/29.80 end
% 29.42/29.80
% 29.42/29.80 subsumption: (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 29.42/29.80 X, sz00 ) ==> X }.
% 29.42/29.80 parent0: (42565) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X
% 29.42/29.80 , sz00 ) = X }.
% 29.42/29.80 substitution0:
% 29.42/29.80 X := X
% 29.42/29.80 end
% 29.42/29.80 permutation0:
% 29.42/29.80 0 ==> 0
% 29.42/29.80 1 ==> 1
% 29.42/29.80 end
% 29.42/29.80
% 29.42/29.80 eqswap: (42722) {G0,W7,D3,L2,V1,M2} { sdtpldt0( sz00, X ) = X, !
% 29.42/29.80 aNaturalNumber0( X ) }.
% 29.42/29.80 parent0[1]: (42566) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X =
% 29.42/29.80 sdtpldt0( sz00, X ) }.
% 29.42/29.80 substitution0:
% 29.42/29.80 X := X
% 29.42/29.80 end
% 29.42/29.80
% 29.42/29.80 subsumption: (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 29.42/29.80 sz00, X ) ==> X }.
% 29.42/29.80 parent0: (42722) {G0,W7,D3,L2,V1,M2} { sdtpldt0( sz00, X ) = X, !
% 29.42/29.80 aNaturalNumber0( X ) }.
% 29.42/29.80 substitution0:
% 29.42/29.80 X := X
% 29.42/29.80 end
% 29.42/29.80 permutation0:
% 29.42/29.80 0 ==> 1
% 29.42/29.80 1 ==> 0
% 29.42/29.80 end
% 29.42/29.80
% 29.42/29.80 subsumption: (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 29.42/29.80 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 29.42/29.80 sdtpldt0( X, Z ), Y = Z }.
% 29.42/29.80 parent0: (42575) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 29.42/29.80 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 29.42/29.80 sdtpldt0( X, Z ), Y = Z }.
% 29.42/29.80 substitution0:
% 29.42/29.80 X := X
% 29.42/29.80 Y := Y
% 29.42/29.80 Z := Z
% 29.42/29.80 end
% 29.42/29.80 permutation0:
% 29.42/29.80 0 ==> 0
% 29.42/29.80 1 ==> 1
% 29.42/29.80 2 ==> 2
% 29.42/29.80 3 ==> 3
% 29.42/29.80 4 ==> 4
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (19) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) =
% 29.42/29.81 sdtpldt0( Z, X ), Y = Z }.
% 29.42/29.81 parent0: (42576) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) =
% 29.42/29.81 sdtpldt0( Z, X ), Y = Z }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 Z := Z
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 2 ==> 2
% 29.42/29.81 3 ==> 3
% 29.42/29.81 4 ==> 4
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (23) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 29.42/29.81 parent0: (42580) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 2 ==> 2
% 29.42/29.81 3 ==> 3
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 29.42/29.81 sdtlseqdt0( X, Y ) }.
% 29.42/29.81 parent0: (42584) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 29.42/29.81 sdtlseqdt0( X, Y ) }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 Z := Z
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 2 ==> 2
% 29.42/29.81 3 ==> 3
% 29.42/29.81 4 ==> 4
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (28) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 29.42/29.81 aNaturalNumber0( Z ) }.
% 29.42/29.81 parent0: (42585) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 29.42/29.81 aNaturalNumber0( Z ) }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 Z := Z
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 2 ==> 2
% 29.42/29.81 3 ==> 3
% 29.42/29.81 4 ==> 4
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (29) {G0,W17,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 29.42/29.81 sdtpldt0( X, Z ) = Y }.
% 29.42/29.81 parent0: (42586) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 29.42/29.81 sdtpldt0( X, Z ) = Y }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 Z := Z
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 2 ==> 2
% 29.42/29.81 3 ==> 3
% 29.42/29.81 4 ==> 4
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (30) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), !
% 29.42/29.81 sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 29.42/29.81 parent0: (42587) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), !
% 29.42/29.81 sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 Z := Z
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 2 ==> 2
% 29.42/29.81 3 ==> 3
% 29.42/29.81 4 ==> 4
% 29.42/29.81 5 ==> 5
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (31) {G0,W5,D2,L2,V1,M2} I { ! aNaturalNumber0( X ),
% 29.42/29.81 sdtlseqdt0( X, X ) }.
% 29.42/29.81 parent0: (42588) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0
% 29.42/29.81 ( X, X ) }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (34) {G0,W10,D2,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 29.42/29.81 parent0: (42591) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 29.42/29.81 aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 2 ==> 2
% 29.42/29.81 3 ==> 3
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (72) {G0,W9,D2,L3,V2,M3} I { ! alpha4( X, Y ), Y = sz10, Y = X
% 29.42/29.81 }.
% 29.42/29.81 parent0: (42630) {G0,W9,D2,L3,V2,M3} { ! alpha4( X, Y ), Y = sz10, Y = X
% 29.42/29.81 }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 2 ==> 2
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 29.42/29.81 parent0: (42631) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha4( X, Y ) }.
% 29.42/29.81 substitution0:
% 29.42/29.81 X := X
% 29.42/29.81 Y := Y
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 1 ==> 1
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (81) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 29.42/29.81 parent0: (42639) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 29.42/29.81 substitution0:
% 29.42/29.81 end
% 29.42/29.81 permutation0:
% 29.42/29.81 0 ==> 0
% 29.42/29.81 end
% 29.42/29.81
% 29.42/29.81 subsumption: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 29.42/29.81 parent0: (42641) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------