%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM482+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Mon Jul 18 06:22:45 EDT 2022
% Result : Theorem 3.40s 3.79s
% Output : Refutation 3.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUM482+3 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : bliksem %s
% 0.12/0.34 % Computer : n011.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 : Tue Jul 5 04:40:07 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.72/1.10 *** allocated 10000 integers for termspace/termends
% 0.72/1.10 *** allocated 10000 integers for clauses
% 0.72/1.10 *** allocated 10000 integers for justifications
% 0.72/1.10 Bliksem 1.12
% 0.72/1.10
% 0.72/1.10
% 0.72/1.10 Automatic Strategy Selection
% 0.72/1.10
% 0.72/1.10
% 0.72/1.10 Clauses:
% 0.72/1.10
% 0.72/1.10 { && }.
% 0.72/1.10 { aNaturalNumber0( sz00 ) }.
% 0.72/1.10 { aNaturalNumber0( sz10 ) }.
% 0.72/1.10 { ! sz10 = sz00 }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0
% 0.72/1.10 ( X, Y ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0
% 0.72/1.10 ( X, Y ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtpldt0( X, Y ) =
% 0.72/1.10 sdtpldt0( Y, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.72/1.10 sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) = X }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sdtpldt0( sz00, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtasdt0( X, Y ) =
% 0.72/1.10 sdtasdt0( Y, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.72/1.10 sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 ) = X }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sdtasdt0( sz10, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 0.72/1.10 { ! aNaturalNumber0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.72/1.10 sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X
% 0.72/1.10 , Z ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.72/1.10 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z
% 0.72/1.10 , X ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.10 sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.10 sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.72/1.10 aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ), Y = Z }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.72/1.10 aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ), Y = Z }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.72/1.10 , X = sz00 }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.72/1.10 , Y = sz00 }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sz00
% 0.72/1.10 , X = sz00, Y = sz00 }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.72/1.10 aNaturalNumber0( skol1( Z, T ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.72/1.10 sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.10 sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.72/1.10 = sdtmndt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.72/1.10 = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.72/1.10 aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.72/1.10 sdtlseqdt0( Y, X ), X = Y }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.10 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y =
% 0.72/1.10 X }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ),
% 0.72/1.10 sdtlseqdt0( Y, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.72/1.10 ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.72/1.10 ), ! aNaturalNumber0( Z ), sdtlseqdt0( sdtpldt0( X, Z ), sdtpldt0( Y, Z
% 0.72/1.10 ) ) }.
% 0.72/1.10 { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) = sdtpldt0( Z, Y ) }.
% 0.72/1.10 { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ) }.
% 0.72/1.10 { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) = sdtpldt0( Y, Z ) }.
% 0.72/1.10 { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), ! sdtlseqdt0( sdtpldt0( Z, X ),
% 0.72/1.10 sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) = sdtpldt0( Y, Z ), alpha5( X, Y, Z
% 0.72/1.10 ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 0.72/1.10 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), alpha6( X, Y, Z ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 0.72/1.10 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), sdtlseqdt0( sdtasdt0( Y, X ),
% 0.72/1.10 sdtasdt0( Z, X ) ) }.
% 0.72/1.10 { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ) }.
% 0.72/1.10 { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 0.72/1.10 { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ) }.
% 0.72/1.10 { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), ! sdtlseqdt0( sdtasdt0( X, Y ),
% 0.72/1.10 sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) = sdtasdt0( Z, X ), alpha6( X, Y, Z
% 0.72/1.10 ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! sz10 = X }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sz00, X = sz10, sdtlseqdt0( sz10, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, sdtlseqdt0( Y,
% 0.72/1.10 sdtasdt0( Y, X ) ) }.
% 0.72/1.10 { && }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.72/1.10 ), iLess0( X, Y ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ),
% 0.72/1.10 aNaturalNumber0( skol2( Z, T ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 0.72/1.10 sdtasdt0( X, skol2( X, Y ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.10 Y = sdtasdt0( X, Z ), doDivides0( X, Y ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.72/1.10 , Y ), ! Z = sdtsldt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.72/1.10 , Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0( X, Z ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.72/1.10 , Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), Z = sdtsldt0( Y, X
% 0.72/1.10 ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.10 doDivides0( X, Y ), ! doDivides0( Y, Z ), doDivides0( X, Z ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.10 doDivides0( X, Y ), ! doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z
% 0.72/1.10 ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.72/1.10 doDivides0( X, Y ), ! doDivides0( X, sdtpldt0( Y, Z ) ), doDivides0( X,
% 0.72/1.10 Z ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 0.72/1.10 sz00, sdtlseqdt0( X, Y ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.72/1.10 , Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z, sdtsldt0( Y, X ) ) = sdtsldt0
% 0.72/1.10 ( sdtasdt0( Z, Y ), X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X = sz00 }.
% 0.72/1.10 { ! aNaturalNumber0( X ), ! isPrime0( X ), alpha1( X ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sz00, ! alpha1( X ), isPrime0( X ) }.
% 0.72/1.10 { ! alpha1( X ), ! X = sz10 }.
% 0.72/1.10 { ! alpha1( X ), alpha2( X ) }.
% 0.72/1.10 { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 0.72/1.10 { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X, Y ) }.
% 0.72/1.10 { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 0.72/1.10 { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 0.72/1.10 { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 0.72/1.10 { ! Y = sz10, alpha4( X, Y ) }.
% 0.72/1.10 { ! Y = X, alpha4( X, Y ) }.
% 0.72/1.10 { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 0.72/1.10 { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 0.72/1.10 { ! aNaturalNumber0( Y ), ! doDivides0( Y, X ), alpha3( X, Y ) }.
% 0.72/1.10 { aNaturalNumber0( xk ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! iLess0( X, xk ), isPrime0(
% 0.72/1.10 skol4( Y ) ) }.
% 0.72/1.10 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! iLess0( X, xk ), alpha9( X
% 0.72/1.10 , skol4( X ) ) }.
% 0.72/1.10 { ! alpha9( X, Y ), alpha13( X, Y ) }.
% 0.72/1.10 { ! alpha9( X, Y ), alpha7( Y ) }.
% 0.72/1.10 { ! alpha13( X, Y ), ! alpha7( Y ), alpha9( X, Y ) }.
% 0.72/1.10 { ! alpha13( X, Y ), alpha18( X, Y ) }.
% 0.72/1.10 { ! alpha13( X, Y ), ! Y = sz10 }.
% 0.72/1.10 { ! alpha18( X, Y ), Y = sz10, alpha13( X, Y ) }.
% 0.72/1.10 { ! alpha18( X, Y ), alpha22( X, Y ) }.
% 0.72/1.10 { ! alpha18( X, Y ), ! Y = sz00 }.
% 0.72/1.10 { ! alpha22( X, Y ), Y = sz00, alpha18( X, Y ) }.
% 0.72/1.10 { ! alpha22( X, Y ), alpha25( X, Y ) }.
% 0.72/1.10 { ! alpha22( X, Y ), doDivides0( Y, X ) }.
% 0.72/1.10 { ! alpha25( X, Y ), ! doDivides0( Y, X ), alpha22( X, Y ) }.
% 2.54/2.95 { ! alpha25( X, Y ), aNaturalNumber0( Y ) }.
% 2.54/2.95 { ! alpha25( X, Y ), aNaturalNumber0( skol5( Z, T ) ) }.
% 2.54/2.95 { ! alpha25( X, Y ), X = sdtasdt0( Y, skol5( X, Y ) ) }.
% 2.54/2.95 { ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ),
% 2.54/2.95 alpha25( X, Y ) }.
% 2.54/2.95 { ! alpha7( X ), alpha10( X, Y ), Y = X }.
% 2.54/2.95 { ! alpha10( X, skol6( X ) ), alpha7( X ) }.
% 2.54/2.95 { ! skol6( X ) = X, alpha7( X ) }.
% 2.54/2.95 { ! alpha10( X, Y ), alpha14( X, Y ), Y = sz10 }.
% 2.54/2.95 { ! alpha14( X, Y ), alpha10( X, Y ) }.
% 2.54/2.95 { ! Y = sz10, alpha10( X, Y ) }.
% 2.54/2.95 { ! alpha14( X, Y ), ! aNaturalNumber0( Y ), alpha19( X, Y ) }.
% 2.54/2.95 { aNaturalNumber0( Y ), alpha14( X, Y ) }.
% 2.54/2.95 { ! alpha19( X, Y ), alpha14( X, Y ) }.
% 2.54/2.95 { ! alpha19( X, Y ), ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ) }.
% 2.54/2.95 { ! alpha19( X, Y ), ! doDivides0( Y, X ) }.
% 2.54/2.95 { aNaturalNumber0( skol7( Z, T ) ), doDivides0( Y, X ), alpha19( X, Y ) }.
% 2.54/2.95 { X = sdtasdt0( Y, skol7( X, Y ) ), doDivides0( Y, X ), alpha19( X, Y ) }.
% 2.54/2.95 { ! xk = sz00 }.
% 2.54/2.95 { ! xk = sz10 }.
% 2.54/2.95 { alpha8 }.
% 2.54/2.95 { alpha11( X ), X = sz00, X = sz10, alpha15( X ) }.
% 2.54/2.95 { alpha11( X ), ! isPrime0( X ) }.
% 2.54/2.95 { ! alpha15( X ), alpha20( X, skol8( X ) ) }.
% 2.54/2.95 { ! alpha15( X ), ! skol8( X ) = X }.
% 2.54/2.95 { ! alpha20( X, Y ), Y = X, alpha15( X ) }.
% 2.54/2.95 { ! alpha20( X, Y ), alpha23( X, Y ) }.
% 2.54/2.95 { ! alpha20( X, Y ), ! Y = sz10 }.
% 2.54/2.95 { ! alpha23( X, Y ), Y = sz10, alpha20( X, Y ) }.
% 2.54/2.95 { ! alpha23( X, Y ), alpha26( X, Y ) }.
% 2.54/2.95 { ! alpha23( X, Y ), doDivides0( Y, X ) }.
% 2.54/2.95 { ! alpha26( X, Y ), ! doDivides0( Y, X ), alpha23( X, Y ) }.
% 2.54/2.95 { ! alpha26( X, Y ), aNaturalNumber0( Y ) }.
% 2.54/2.95 { ! alpha26( X, Y ), aNaturalNumber0( skol9( Z, T ) ) }.
% 2.54/2.95 { ! alpha26( X, Y ), X = sdtasdt0( Y, skol9( X, Y ) ) }.
% 2.54/2.95 { ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ),
% 2.54/2.95 alpha26( X, Y ) }.
% 2.54/2.95 { ! alpha11( X ), ! aNaturalNumber0( X ), alpha16( X ) }.
% 2.54/2.95 { aNaturalNumber0( X ), alpha11( X ) }.
% 2.54/2.95 { ! alpha16( X ), alpha11( X ) }.
% 2.54/2.95 { ! alpha16( X ), ! aNaturalNumber0( Y ), ! xk = sdtasdt0( X, Y ) }.
% 2.54/2.95 { ! alpha16( X ), ! doDivides0( X, xk ) }.
% 2.54/2.95 { aNaturalNumber0( skol10( Y ) ), doDivides0( X, xk ), alpha16( X ) }.
% 2.54/2.95 { xk = sdtasdt0( X, skol10( X ) ), doDivides0( X, xk ), alpha16( X ) }.
% 2.54/2.95 { ! alpha8, alpha12 }.
% 2.54/2.95 { ! alpha8, isPrime0( xk ) }.
% 2.54/2.95 { ! alpha12, ! isPrime0( xk ), alpha8 }.
% 2.54/2.95 { ! alpha12, alpha17( X ), X = xk }.
% 2.54/2.95 { ! alpha17( skol11 ), alpha12 }.
% 2.54/2.95 { ! skol11 = xk, alpha12 }.
% 2.54/2.95 { ! alpha17( X ), alpha21( X ), X = sz10 }.
% 2.54/2.95 { ! alpha21( X ), alpha17( X ) }.
% 2.54/2.95 { ! X = sz10, alpha17( X ) }.
% 2.54/2.95 { ! alpha21( X ), ! aNaturalNumber0( X ), alpha24( X ) }.
% 2.54/2.95 { aNaturalNumber0( X ), alpha21( X ) }.
% 2.54/2.95 { ! alpha24( X ), alpha21( X ) }.
% 2.54/2.95 { ! alpha24( X ), ! aNaturalNumber0( Y ), ! xk = sdtasdt0( X, Y ) }.
% 2.54/2.95 { ! alpha24( X ), ! doDivides0( X, xk ) }.
% 2.54/2.95 { aNaturalNumber0( skol12( Y ) ), doDivides0( X, xk ), alpha24( X ) }.
% 2.54/2.95 { xk = sdtasdt0( X, skol12( X ) ), doDivides0( X, xk ), alpha24( X ) }.
% 2.54/2.95
% 2.54/2.95 percentage equality = 0.246781, percentage horn = 0.713333
% 2.54/2.95 This is a problem with some equality
% 2.54/2.95
% 2.54/2.95
% 2.54/2.95
% 2.54/2.95 Options Used:
% 2.54/2.95
% 2.54/2.95 useres = 1
% 2.54/2.95 useparamod = 1
% 2.54/2.95 useeqrefl = 1
% 2.54/2.95 useeqfact = 1
% 2.54/2.95 usefactor = 1
% 2.54/2.95 usesimpsplitting = 0
% 2.54/2.95 usesimpdemod = 5
% 2.54/2.95 usesimpres = 3
% 2.54/2.95
% 2.54/2.95 resimpinuse = 1000
% 2.54/2.95 resimpclauses = 20000
% 2.54/2.95 substype = eqrewr
% 2.54/2.95 backwardsubs = 1
% 2.54/2.95 selectoldest = 5
% 2.54/2.95
% 2.54/2.95 litorderings [0] = split
% 2.54/2.95 litorderings [1] = extend the termordering, first sorting on arguments
% 2.54/2.95
% 2.54/2.95 termordering = kbo
% 2.54/2.95
% 2.54/2.95 litapriori = 0
% 2.54/2.95 termapriori = 1
% 2.54/2.95 litaposteriori = 0
% 2.54/2.95 termaposteriori = 0
% 2.54/2.95 demodaposteriori = 0
% 2.54/2.95 ordereqreflfact = 0
% 2.54/2.95
% 2.54/2.95 litselect = negord
% 2.54/2.95
% 2.54/2.95 maxweight = 15
% 2.54/2.95 maxdepth = 30000
% 2.54/2.95 maxlength = 115
% 2.54/2.95 maxnrvars = 195
% 2.54/2.95 excuselevel = 1
% 2.54/2.95 increasemaxweight = 1
% 2.54/2.95
% 2.54/2.95 maxselected = 10000000
% 2.54/2.95 maxnrclauses = 10000000
% 2.54/2.95
% 2.54/2.95 showgenerated = 0
% 2.54/2.95 showkept = 0
% 2.54/2.95 showselected = 0
% 2.54/2.95 showdeleted = 0
% 2.54/2.95 showresimp = 1
% 2.54/2.95 showstatus = 2000
% 2.54/2.95
% 2.54/2.95 prologoutput = 0
% 2.54/2.95 nrgoals = 5000000
% 2.54/2.95 totalproof = 1
% 2.54/2.95
% 2.54/2.95 Symbols occurring in the translation:
% 2.54/2.95
% 2.54/2.95 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.54/2.95 . [1, 2] (w:1, o:38, a:1, s:1, b:0),
% 2.54/2.95 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 2.54/2.95 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 3.40/3.79 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.40/3.79 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.40/3.79 aNaturalNumber0 [36, 1] (w:1, o:21, a:1, s:1, b:0),
% 3.40/3.79 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 3.40/3.79 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 3.40/3.79 sdtpldt0 [40, 2] (w:1, o:62, a:1, s:1, b:0),
% 3.40/3.79 sdtasdt0 [41, 2] (w:1, o:63, a:1, s:1, b:0),
% 3.40/3.79 sdtlseqdt0 [43, 2] (w:1, o:64, a:1, s:1, b:0),
% 3.40/3.79 sdtmndt0 [44, 2] (w:1, o:65, a:1, s:1, b:0),
% 3.40/3.79 iLess0 [45, 2] (w:1, o:66, a:1, s:1, b:0),
% 3.40/3.79 doDivides0 [46, 2] (w:1, o:67, a:1, s:1, b:0),
% 3.40/3.79 sdtsldt0 [47, 2] (w:1, o:68, a:1, s:1, b:0),
% 3.40/3.79 isPrime0 [48, 1] (w:1, o:22, a:1, s:1, b:0),
% 3.40/3.79 xk [49, 0] (w:1, o:11, a:1, s:1, b:0),
% 3.40/3.79 alpha1 [51, 1] (w:1, o:23, a:1, s:1, b:1),
% 3.40/3.79 alpha2 [52, 1] (w:1, o:28, a:1, s:1, b:1),
% 3.40/3.79 alpha3 [53, 2] (w:1, o:74, a:1, s:1, b:1),
% 3.40/3.79 alpha4 [54, 2] (w:1, o:75, a:1, s:1, b:1),
% 3.40/3.79 alpha5 [55, 3] (w:1, o:87, a:1, s:1, b:1),
% 3.40/3.79 alpha6 [56, 3] (w:1, o:88, a:1, s:1, b:1),
% 3.40/3.79 alpha7 [57, 1] (w:1, o:29, a:1, s:1, b:1),
% 3.40/3.79 alpha8 [58, 0] (w:1, o:13, a:1, s:1, b:1),
% 3.40/3.79 alpha9 [59, 2] (w:1, o:76, a:1, s:1, b:1),
% 3.40/3.79 alpha10 [60, 2] (w:1, o:77, a:1, s:1, b:1),
% 3.40/3.79 alpha11 [61, 1] (w:1, o:24, a:1, s:1, b:1),
% 3.40/3.79 alpha12 [62, 0] (w:1, o:14, a:1, s:1, b:1),
% 3.40/3.79 alpha13 [63, 2] (w:1, o:78, a:1, s:1, b:1),
% 3.40/3.79 alpha14 [64, 2] (w:1, o:79, a:1, s:1, b:1),
% 3.40/3.79 alpha15 [65, 1] (w:1, o:25, a:1, s:1, b:1),
% 3.40/3.79 alpha16 [66, 1] (w:1, o:26, a:1, s:1, b:1),
% 3.40/3.79 alpha17 [67, 1] (w:1, o:27, a:1, s:1, b:1),
% 3.40/3.79 alpha18 [68, 2] (w:1, o:80, a:1, s:1, b:1),
% 3.40/3.79 alpha19 [69, 2] (w:1, o:81, a:1, s:1, b:1),
% 3.40/3.79 alpha20 [70, 2] (w:1, o:69, a:1, s:1, b:1),
% 3.40/3.79 alpha21 [71, 1] (w:1, o:30, a:1, s:1, b:1),
% 3.40/3.79 alpha22 [72, 2] (w:1, o:70, a:1, s:1, b:1),
% 3.40/3.79 alpha23 [73, 2] (w:1, o:71, a:1, s:1, b:1),
% 3.40/3.79 alpha24 [74, 1] (w:1, o:31, a:1, s:1, b:1),
% 3.40/3.79 alpha25 [75, 2] (w:1, o:72, a:1, s:1, b:1),
% 3.40/3.79 alpha26 [76, 2] (w:1, o:73, a:1, s:1, b:1),
% 3.40/3.79 skol1 [77, 2] (w:1, o:82, a:1, s:1, b:1),
% 3.40/3.79 skol2 [78, 2] (w:1, o:83, a:1, s:1, b:1),
% 3.40/3.79 skol3 [79, 1] (w:1, o:32, a:1, s:1, b:1),
% 3.40/3.79 skol4 [80, 1] (w:1, o:33, a:1, s:1, b:1),
% 3.40/3.79 skol5 [81, 2] (w:1, o:84, a:1, s:1, b:1),
% 3.40/3.79 skol6 [82, 1] (w:1, o:34, a:1, s:1, b:1),
% 3.40/3.79 skol7 [83, 2] (w:1, o:85, a:1, s:1, b:1),
% 3.40/3.79 skol8 [84, 1] (w:1, o:35, a:1, s:1, b:1),
% 3.40/3.79 skol9 [85, 2] (w:1, o:86, a:1, s:1, b:1),
% 3.40/3.79 skol10 [86, 1] (w:1, o:36, a:1, s:1, b:1),
% 3.40/3.79 skol11 [87, 0] (w:1, o:15, a:1, s:1, b:1),
% 3.40/3.79 skol12 [88, 1] (w:1, o:37, a:1, s:1, b:1).
% 3.40/3.79
% 3.40/3.79
% 3.40/3.79 Starting Search:
% 3.40/3.79
% 3.40/3.79 *** allocated 15000 integers for clauses
% 3.40/3.79 *** allocated 22500 integers for clauses
% 3.40/3.79 *** allocated 33750 integers for clauses
% 3.40/3.79 *** allocated 15000 integers for termspace/termends
% 3.40/3.79 *** allocated 50625 integers for clauses
% 3.40/3.79 *** allocated 22500 integers for termspace/termends
% 3.40/3.79 *** allocated 75937 integers for clauses
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 33750 integers for termspace/termends
% 3.40/3.79 *** allocated 113905 integers for clauses
% 3.40/3.79 *** allocated 50625 integers for termspace/termends
% 3.40/3.79
% 3.40/3.79 Intermediate Status:
% 3.40/3.79 Generated: 11481
% 3.40/3.79 Kept: 2133
% 3.40/3.79 Inuse: 140
% 3.40/3.79 Deleted: 1
% 3.40/3.79 Deletedinuse: 0
% 3.40/3.79
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 170857 integers for clauses
% 3.40/3.79 *** allocated 75937 integers for termspace/termends
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 113905 integers for termspace/termends
% 3.40/3.79 *** allocated 256285 integers for clauses
% 3.40/3.79
% 3.40/3.79 Intermediate Status:
% 3.40/3.79 Generated: 31165
% 3.40/3.79 Kept: 4285
% 3.40/3.79 Inuse: 204
% 3.40/3.79 Deleted: 3
% 3.40/3.79 Deletedinuse: 1
% 3.40/3.79
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 170857 integers for termspace/termends
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 384427 integers for clauses
% 3.40/3.79
% 3.40/3.79 Intermediate Status:
% 3.40/3.79 Generated: 43075
% 3.40/3.79 Kept: 6292
% 3.40/3.79 Inuse: 251
% 3.40/3.79 Deleted: 8
% 3.40/3.79 Deletedinuse: 3
% 3.40/3.79
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 256285 integers for termspace/termends
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79
% 3.40/3.79 Intermediate Status:
% 3.40/3.79 Generated: 63194
% 3.40/3.79 Kept: 8357
% 3.40/3.79 Inuse: 296
% 3.40/3.79 Deleted: 10
% 3.40/3.79 Deletedinuse: 5
% 3.40/3.79
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 576640 integers for clauses
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79
% 3.40/3.79 Intermediate Status:
% 3.40/3.79 Generated: 77561
% 3.40/3.79 Kept: 10465
% 3.40/3.79 Inuse: 358
% 3.40/3.79 Deleted: 15
% 3.40/3.79 Deletedinuse: 7
% 3.40/3.79
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 384427 integers for termspace/termends
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79
% 3.40/3.79 Intermediate Status:
% 3.40/3.79 Generated: 84608
% 3.40/3.79 Kept: 12504
% 3.40/3.79 Inuse: 418
% 3.40/3.79 Deleted: 17
% 3.40/3.79 Deletedinuse: 9
% 3.40/3.79
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79 *** allocated 864960 integers for clauses
% 3.40/3.79 Resimplifying inuse:
% 3.40/3.79 Done
% 3.40/3.79
% 3.40/3.79
% 3.40/3.79 Bliksems!, er is een bewijs:
% 3.40/3.79 % SZS status Theorem
% 3.40/3.79 % SZS output start Refutation
% 3.40/3.79
% 3.40/3.79 (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 3.40/3.79 (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 3.40/3.79 (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) ==>
% 3.40/3.79 X }.
% 3.40/3.79 (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( sz00, X ) ==>
% 3.40/3.79 X }.
% 3.40/3.79 (12) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 3.40/3.79 ==> X }.
% 3.40/3.79 (23) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 3.40/3.79 (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 3.40/3.79 }.
% 3.40/3.79 (28) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 3.40/3.79 }.
% 3.40/3.79 (29) {G0,W17,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 3.40/3.79 }.
% 3.40/3.79 (30) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y
% 3.40/3.79 , Z = sdtmndt0( Y, X ) }.
% 3.40/3.79 (31) {G0,W5,D2,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 3.40/3.79 (34) {G0,W10,D2,L4,V2,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), sdtlseqdt0( X, Y ), ! Y = X }.
% 3.40/3.79 (54) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 3.40/3.79 }.
% 3.40/3.79 (72) {G0,W9,D2,L3,V2,M3} I { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 3.40/3.79 (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 3.40/3.79 (78) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xk ) }.
% 3.40/3.79 (112) {G0,W1,D1,L1,V0,M1} I { alpha8 }.
% 3.40/3.79 (114) {G0,W4,D2,L2,V1,M2} I { alpha11( X ), ! isPrime0( X ) }.
% 3.40/3.79 (128) {G0,W6,D2,L3,V1,M3} I { ! alpha11( X ), ! aNaturalNumber0( X ),
% 3.40/3.79 alpha16( X ) }.
% 3.40/3.79 (132) {G0,W5,D2,L2,V1,M2} I { ! alpha16( X ), ! doDivides0( X, xk ) }.
% 3.40/3.79 (136) {G1,W2,D2,L1,V0,M1} I;r(112) { isPrime0( xk ) }.
% 3.40/3.79 (278) {G1,W6,D2,L2,V1,M2} F(72) { ! alpha4( sz10, X ), X = sz10 }.
% 3.40/3.79 (1570) {G1,W10,D2,L4,V2,M4} R(27,1);d(9) { ! aNaturalNumber0( X ), !
% 3.40/3.79 aNaturalNumber0( Y ), sdtlseqdt0( sz00, X ), ! Y = X }.
% 3.40/3.79 (1591) {G2,W5,D2,L2,V1,M2} F(1570);q { ! aNaturalNumber0( X ), sdtlseqdt0(
% 3.40/3.79 sz00, X ) }.
% 3.40/3.79 (1668) {G3,W3,D2,L1,V0,M1} R(1591,78) { sdtlseqdt0( sz00, xk ) }.
% 3.40/3.79 (2180) {G3,W12,D3,L4,V2,M4} R(30,1591);f;d(9);r(1) { ! aNaturalNumber0( X )
% 3.40/3.79 , ! aNaturalNumber0( Y ), Y = sdtmndt0( X, sz00 ), ! Y = X }.
% 3.40/3.79 (2223) {G1,W15,D3,L5,V2,M5} R(30,1);d(8) { ! aNaturalNumber0( X ), !
% 3.40/3.79 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), sdtmndt0( Y, X ) ==> sz00, !
% 3.40/3.79 X = Y }.
% 3.40/3.79 (2275) {G2,W7,D3,L2,V1,M2} F(2223);q;r(31) { ! aNaturalNumber0( X ),
% 3.40/3.79 sdtmndt0( X, X ) ==> sz00 }.
% 3.40/3.79 (2288) {G4,W7,D3,L2,V1,M2} F(2180);q { ! aNaturalNumber0( X ), sdtmndt0( X
% 3.40/3.79 , sz00 ) ==> X }.
% 3.40/3.79 (4512) {G2,W5,D2,L2,V1,M2} P(278,2) { aNaturalNumber0( X ), ! alpha4( sz10
% 3.40/3.79 , X ) }.
% 3.40/3.79 (4599) {G3,W5,D2,L2,V1,M2} R(4512,73) { aNaturalNumber0( X ), ! X = sz10
% 3.40/3.79 }.
% 3.40/3.79 (4716) {G4,W11,D2,L4,V2,M4} R(4599,34) { ! X = sz10, ! aNaturalNumber0( Y )
% 3.40/3.79 , sdtlseqdt0( Y, X ), ! X = Y }.
% 3.40/3.79 (4750) {G5,W6,D2,L2,V1,M2} F(4716);r(2) { ! X = sz10, sdtlseqdt0( sz10, X )
% 3.40/3.79 }.
% 3.40/3.79 (4965) {G6,W12,D3,L4,V2,M4} R(4750,28);r(2) { ! X = sz10, ! aNaturalNumber0
% 3.40/3.79 ( X ), ! Y = sdtmndt0( X, sz10 ), aNaturalNumber0( Y ) }.
% 3.40/3.79 (4975) {G7,W5,D2,L2,V1,M2} Q(4965);d(2275);r(2) { aNaturalNumber0( X ), ! X
% 3.40/3.79 = sz00 }.
% 3.40/3.79 (4988) {G8,W13,D3,L4,V2,M4} R(4975,23) { ! X = sz00, ! aNaturalNumber0( Y )
% 3.40/3.79 , ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 3.40/3.79 (5003) {G9,W6,D2,L2,V1,M2} Q(4988);d(9);r(4975) { X = sz00, ! X = sz00 }.
% 3.40/3.79 (5043) {G10,W6,D2,L2,V1,M2} P(5003,1668) { sdtlseqdt0( X, xk ), ! X = sz00
% 3.40/3.79 }.
% 3.40/3.79 (5079) {G11,W15,D3,L4,V2,M4} R(5043,29);r(4975) { ! X = sz00, !
% 3.40/3.79 aNaturalNumber0( xk ), ! Y = sdtmndt0( xk, X ), sdtpldt0( X, Y ) ==> xk
% 3.40/3.79 }.
% 3.40/3.79 (5080) {G11,W12,D3,L4,V2,M4} R(5043,28);r(4975) { ! X = sz00, !
% 3.40/3.79 aNaturalNumber0( xk ), ! Y = sdtmndt0( xk, X ), aNaturalNumber0( Y ) }.
% 3.40/3.79 (5091) {G12,W5,D2,L2,V1,M2} Q(5080);d(2288);r(78) { aNaturalNumber0( X ), !
% 3.40/3.79 X = xk }.
% 3.40/3.79 (5092) {G12,W8,D3,L2,V1,M2} Q(5079);d(2288);r(78) { sdtpldt0( sz00, X ) ==>
% 3.40/3.79 xk, ! X = xk }.
% 3.40/3.79 (5121) {G13,W6,D2,L2,V1,M2} R(5091,9);d(5092) { ! X = xk, xk = X }.
% 3.40/3.79 (5465) {G14,W5,D2,L2,V1,M2} P(5121,136) { isPrime0( X ), ! X = xk }.
% 3.40/3.79 (5468) {G15,W5,D2,L2,V1,M2} R(5465,114) { ! X = xk, alpha11( X ) }.
% 3.40/3.79 (6416) {G1,W10,D2,L4,V2,M4} R(54,2);d(12) { ! aNaturalNumber0( X ), !
% 3.40/3.79 aNaturalNumber0( Y ), doDivides0( X, Y ), ! Y = X }.
% 3.40/3.79 (6470) {G2,W5,D2,L2,V1,M2} F(6416);q { ! aNaturalNumber0( X ), doDivides0(
% 3.40/3.79 X, X ) }.
% 3.40/3.79 (8131) {G3,W2,D2,L1,V0,M1} R(6470,132);r(78) { ! alpha16( xk ) }.
% 3.40/3.79 (14377) {G16,W5,D2,L2,V1,M2} R(128,5468);r(5091) { alpha16( X ), ! X = xk
% 3.40/3.79 }.
% 3.40/3.79 (14414) {G17,W0,D0,L0,V0,M0} Q(14377);r(8131) { }.
% 3.40/3.79
% 3.40/3.79
% 3.40/3.79 % SZS output end Refutation
% 3.40/3.79 found a proof!
% 3.40/3.79
% 3.40/3.79
% 3.40/3.79 Unprocessed initial clauses:
% 3.40/3.79
% 3.40/3.79 (14416) {G0,W1,D1,L1,V0,M1} { && }.
% 3.40/3.79 (14417) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 3.40/3.79 (14418) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 3.40/3.79 (14419) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 3.40/3.79 (14420) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 3.40/3.79 (14421) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 3.40/3.79 ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 3.40/3.79 (14422) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 3.40/3.79 (14423) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0(
% 3.40/3.79 X, sdtpldt0( Y, Z ) ) }.
% 3.40/3.79 (14424) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 )
% 3.40/3.79 = X }.
% 3.40/3.79 (14425) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtpldt0( sz00,
% 3.40/3.79 X ) }.
% 3.40/3.79 (14426) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 3.40/3.79 (14427) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0(
% 3.40/3.79 X, sdtasdt0( Y, Z ) ) }.
% 3.40/3.79 (14428) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 3.40/3.79 = X }.
% 3.40/3.79 (14429) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtasdt0( sz10,
% 3.40/3.79 X ) }.
% 3.40/3.79 (14430) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 )
% 3.40/3.79 = sz00 }.
% 3.40/3.79 (14431) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sz00 = sdtasdt0(
% 3.40/3.79 sz00, X ) }.
% 3.40/3.79 (14432) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0(
% 3.40/3.79 sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 3.40/3.79 (14433) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0(
% 3.40/3.79 sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 3.40/3.79 (14434) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 3.40/3.79 }.
% 3.40/3.79 (14435) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z
% 3.40/3.79 }.
% 3.40/3.79 (14436) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 3.40/3.79 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 3.40/3.79 sdtasdt0( X, Z ), Y = Z }.
% 3.40/3.79 (14437) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 3.40/3.79 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) =
% 3.40/3.79 sdtasdt0( Z, X ), Y = Z }.
% 3.40/3.79 (14438) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 3.40/3.79 (14439) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 3.40/3.79 (14440) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 3.40/3.79 (14441) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtlseqdt0( X, Y ), aNaturalNumber0( skol1( Z, T ) ) }.
% 3.40/3.79 (14442) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtlseqdt0( X, Y ), sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 3.40/3.79 (14443) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 3.40/3.79 }.
% 3.40/3.79 (14444) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 3.40/3.79 }.
% 3.40/3.79 (14445) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 3.40/3.79 }.
% 3.40/3.79 (14446) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y
% 3.40/3.79 , Z = sdtmndt0( Y, X ) }.
% 3.40/3.79 (14447) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0( X, X )
% 3.40/3.79 }.
% 3.40/3.79 (14448) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 3.40/3.79 (14449) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ),
% 3.40/3.79 sdtlseqdt0( X, Z ) }.
% 3.40/3.79 (14450) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 3.40/3.79 (14451) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), sdtlseqdt0( X, Y ), sdtlseqdt0( Y, X ) }.
% 3.40/3.79 (14452) {G0,W16,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z
% 3.40/3.79 ) }.
% 3.40/3.79 (14453) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), sdtlseqdt0(
% 3.40/3.79 sdtpldt0( X, Z ), sdtpldt0( Y, Z ) ) }.
% 3.40/3.79 (14454) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) =
% 3.40/3.79 sdtpldt0( Z, Y ) }.
% 3.40/3.79 (14455) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0(
% 3.40/3.79 Z, X ), sdtpldt0( Z, Y ) ) }.
% 3.40/3.79 (14456) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) =
% 3.40/3.79 sdtpldt0( Y, Z ) }.
% 3.40/3.79 (14457) {G0,W25,D3,L4,V3,M4} { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), !
% 3.40/3.79 sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) =
% 3.40/3.79 sdtpldt0( Y, Z ), alpha5( X, Y, Z ) }.
% 3.40/3.79 (14458) {G0,W19,D2,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 3.40/3.79 alpha6( X, Y, Z ) }.
% 3.40/3.79 (14459) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 3.40/3.79 sdtlseqdt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 3.40/3.79 (14460) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) =
% 3.40/3.79 sdtasdt0( X, Z ) }.
% 3.40/3.79 (14461) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0(
% 3.40/3.79 X, Y ), sdtasdt0( X, Z ) ) }.
% 3.40/3.79 (14462) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) =
% 3.40/3.79 sdtasdt0( Z, X ) }.
% 3.40/3.79 (14463) {G0,W25,D3,L4,V3,M4} { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), !
% 3.40/3.79 sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) =
% 3.40/3.79 sdtasdt0( Z, X ), alpha6( X, Y, Z ) }.
% 3.40/3.79 (14464) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 3.40/3.79 , ! sz10 = X }.
% 3.40/3.79 (14465) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 3.40/3.79 , sdtlseqdt0( sz10, X ) }.
% 3.40/3.79 (14466) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), X = sz00, sdtlseqdt0( Y, sdtasdt0( Y, X ) ) }.
% 3.40/3.79 (14467) {G0,W1,D1,L1,V0,M1} { && }.
% 3.40/3.79 (14468) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), X = Y, ! sdtlseqdt0( X, Y ), iLess0( X, Y ) }.
% 3.40/3.79 (14469) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! doDivides0( X, Y ), aNaturalNumber0( skol2( Z, T ) ) }.
% 3.40/3.79 (14470) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! doDivides0( X, Y ), Y = sdtasdt0( X, skol2( X, Y ) ) }.
% 3.40/3.79 (14471) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 3.40/3.79 }.
% 3.40/3.79 (14472) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 3.40/3.79 aNaturalNumber0( Z ) }.
% 3.40/3.79 (14473) {G0,W20,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0
% 3.40/3.79 ( X, Z ) }.
% 3.40/3.79 (14474) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), ! Y =
% 3.40/3.79 sdtasdt0( X, Z ), Z = sdtsldt0( Y, X ) }.
% 3.40/3.79 (14475) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( Y, Z ),
% 3.40/3.79 doDivides0( X, Z ) }.
% 3.40/3.79 (14476) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X, Z ),
% 3.40/3.79 doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 3.40/3.79 (14477) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X,
% 3.40/3.79 sdtpldt0( Y, Z ) ), doDivides0( X, Z ) }.
% 3.40/3.79 (14478) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), ! doDivides0( X, Y ), Y = sz00, sdtlseqdt0( X, Y ) }.
% 3.40/3.79 (14479) {G0,W23,D4,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 3.40/3.79 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z
% 3.40/3.79 , sdtsldt0( Y, X ) ) = sdtsldt0( sdtasdt0( Z, Y ), X ) }.
% 3.40/3.79 (14480) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X
% 3.40/3.79 = sz00 }.
% 3.40/3.79 (14481) {G0,W6,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ),
% 3.40/3.79 alpha1( X ) }.
% 3.40/3.79 (14482) {G0,W9,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, ! alpha1(
% 3.40/3.79 X ), isPrime0( X ) }.
% 3.40/3.79 (14483) {G0,W5,D2,L2,V1,M2} { ! alpha1( X ), ! X = sz10 }.
% 3.40/3.79 (14484) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), alpha2( X ) }.
% 3.40/3.79 (14485) {G0,W7,D2,L3,V1,M3} { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 3.40/3.79 (14486) {G0,W8,D2,L3,V2,M3} { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X,
% 3.40/3.79 Y ) }.
% 3.40/3.79 (14487) {G0,W6,D3,L2,V1,M2} { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 3.40/3.79 (14488) {G0,W6,D3,L2,V1,M2} { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 3.40/3.79 (14489) {G0,W9,D2,L3,V2,M3} { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 3.40/3.79 (14490) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha4( X, Y ) }.
% 3.40/3.79 (14491) {G0,W6,D2,L2,V2,M2} { ! Y = X, alpha4( X, Y ) }.
% 3.40/3.79 (14492) {G0,W5,D2,L2,V2,M2} { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 3.40/3.79 (14493) {G0,W6,D2,L2,V2,M2} { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 3.40/3.79 (14494) {G0,W8,D2,L3,V2,M3} { ! aNaturalNumber0( Y ), ! doDivides0( Y, X )
% 3.40/3.79 , alpha3( X, Y ) }.
% 3.40/3.79 (14495) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xk ) }.
% 3.40/3.79 (14496) {G0,W14,D3,L5,V2,M5} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 3.40/3.79 , ! iLess0( X, xk ), isPrime0( skol4( Y ) ) }.
% 3.40/3.79 (14497) {G0,W15,D3,L5,V1,M5} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 3.40/3.79 , ! iLess0( X, xk ), alpha9( X, skol4( X ) ) }.
% 3.40/3.79 (14498) {G0,W6,D2,L2,V2,M2} { ! alpha9( X, Y ), alpha13( X, Y ) }.
% 3.40/3.79 (14499) {G0,W5,D2,L2,V2,M2} { ! alpha9( X, Y ), alpha7( Y ) }.
% 3.40/3.79 (14500) {G0,W8,D2,L3,V2,M3} { ! alpha13( X, Y ), ! alpha7( Y ), alpha9( X
% 3.40/3.79 , Y ) }.
% 3.40/3.79 (14501) {G0,W6,D2,L2,V2,M2} { ! alpha13( X, Y ), alpha18( X, Y ) }.
% 3.40/3.79 (14502) {G0,W6,D2,L2,V2,M2} { ! alpha13( X, Y ), ! Y = sz10 }.
% 3.40/3.79 (14503) {G0,W9,D2,L3,V2,M3} { ! alpha18( X, Y ), Y = sz10, alpha13( X, Y )
% 3.40/3.79 }.
% 3.40/3.79 (14504) {G0,W6,D2,L2,V2,M2} { ! alpha18( X, Y ), alpha22( X, Y ) }.
% 3.40/3.79 (14505) {G0,W6,D2,L2,V2,M2} { ! alpha18( X, Y ), ! Y = sz00 }.
% 3.40/3.79 (14506) {G0,W9,D2,L3,V2,M3} { ! alpha22( X, Y ), Y = sz00, alpha18( X, Y )
% 3.40/3.79 }.
% 3.40/3.79 (14507) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), alpha25( X, Y ) }.
% 3.40/3.79 (14508) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), doDivides0( Y, X ) }.
% 3.40/3.79 (14509) {G0,W9,D2,L3,V2,M3} { ! alpha25( X, Y ), ! doDivides0( Y, X ),
% 3.40/3.79 alpha22( X, Y ) }.
% 3.40/3.79 (14510) {G0,W5,D2,L2,V2,M2} { ! alpha25( X, Y ), aNaturalNumber0( Y ) }.
% 3.40/3.79 (14511) {G0,W7,D3,L2,V4,M2} { ! alpha25( X, Y ), aNaturalNumber0( skol5( Z
% 3.40/3.79 , T ) ) }.
% 3.40/3.79 (14512) {G0,W10,D4,L2,V2,M2} { ! alpha25( X, Y ), X = sdtasdt0( Y, skol5(
% 3.40/3.79 X, Y ) ) }.
% 3.40/3.79 (14513) {G0,W12,D3,L4,V3,M4} { ! aNaturalNumber0( Y ), ! aNaturalNumber0(
% 3.40/3.79 Z ), ! X = sdtasdt0( Y, Z ), alpha25( X, Y ) }.
% 3.40/3.79 (14514) {G0,W8,D2,L3,V2,M3} { ! alpha7( X ), alpha10( X, Y ), Y = X }.
% 3.40/3.79 (14515) {G0,W6,D3,L2,V1,M2} { ! alpha10( X, skol6( X ) ), alpha7( X ) }.
% 3.40/3.79 (14516) {G0,W6,D3,L2,V1,M2} { ! skol6( X ) = X, alpha7( X ) }.
% 3.40/3.79 (14517) {G0,W9,D2,L3,V2,M3} { ! alpha10( X, Y ), alpha14( X, Y ), Y = sz10
% 3.40/3.79 }.
% 3.40/3.79 (14518) {G0,W6,D2,L2,V2,M2} { ! alpha14( X, Y ), alpha10( X, Y ) }.
% 3.40/3.79 (14519) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha10( X, Y ) }.
% 3.40/3.79 (14520) {G0,W8,D2,L3,V2,M3} { ! alpha14( X, Y ), ! aNaturalNumber0( Y ),
% 3.40/3.79 alpha19( X, Y ) }.
% 3.40/3.79 (14521) {G0,W5,D2,L2,V2,M2} { aNaturalNumber0( Y ), alpha14( X, Y ) }.
% 3.40/3.79 (14522) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), alpha14( X, Y ) }.
% 3.40/3.79 (14523) {G0,W10,D3,L3,V3,M3} { ! alpha19( X, Y ), ! aNaturalNumber0( Z ),
% 3.40/3.79 ! X = sdtasdt0( Y, Z ) }.
% 3.40/3.79 (14524) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), ! doDivides0( Y, X ) }.
% 3.40/3.79 (14525) {G0,W10,D3,L3,V4,M3} { aNaturalNumber0( skol7( Z, T ) ),
% 3.40/3.79 doDivides0( Y, X ), alpha19( X, Y ) }.
% 3.40/3.79 (14526) {G0,W13,D4,L3,V2,M3} { X = sdtasdt0( Y, skol7( X, Y ) ),
% 3.40/3.79 doDivides0( Y, X ), alpha19( X, Y ) }.
% 3.40/3.79 (14527) {G0,W3,D2,L1,V0,M1} { ! xk = sz00 }.
% 3.40/3.79 (14528) {G0,W3,D2,L1,V0,M1} { ! xk = sz10 }.
% 3.40/3.79 (14529) {G0,W1,D1,L1,V0,M1} { alpha8 }.
% 3.40/3.79 (14530) {G0,W10,D2,L4,V1,M4} { alpha11( X ), X = sz00, X = sz10, alpha15(
% 3.40/3.79 X ) }.
% 3.40/3.79 (14531) {G0,W4,D2,L2,V1,M2} { alpha11( X ), ! isPrime0( X ) }.
% 3.40/3.79 (14532) {G0,W6,D3,L2,V1,M2} { ! alpha15( X ), alpha20( X, skol8( X ) ) }.
% 3.40/3.79 (14533) {G0,W6,D3,L2,V1,M2} { ! alpha15( X ), ! skol8( X ) = X }.
% 3.40/3.79 (14534) {G0,W8,D2,L3,V2,M3} { ! alpha20( X, Y ), Y = X, alpha15( X ) }.
% 3.40/3.79 (14535) {G0,W6,D2,L2,V2,M2} { ! alpha20( X, Y ), alpha23( X, Y ) }.
% 3.40/3.79 (14536) {G0,W6,D2,L2,V2,M2} { ! alpha20( X, Y ), ! Y = sz10 }.
% 3.40/3.79 (14537) {G0,W9,D2,L3,V2,M3} { ! alpha23( X, Y ), Y = sz10, alpha20( X, Y )
% 3.40/3.79 }.
% 3.40/3.79 (14538) {G0,W6,D2,L2,V2,M2} { ! alpha23( X, Y ), alpha26( X, Y ) }.
% 3.40/3.79 (14539) {G0,W6,D2,L2,V2,M2} { ! alpha23( X, Y ), doDivides0( Y, X ) }.
% 3.40/3.79 (14540) {G0,W9,D2,L3,V2,M3} { ! alpha26( X, Y ), ! doDivides0( Y, X ),
% 3.40/3.79 alpha23( X, Y ) }.
% 3.40/3.79 (14541) {G0,W5,D2,L2,V2,M2} { ! alpha26( X, Y ), aNaturalNumber0( Y ) }.
% 3.40/3.79 (14542) {G0,W7,D3,L2,V4,M2} { ! alpha26( X, Y ), aNaturalNumber0( skol9( Z
% 3.40/3.79 , T ) ) }.
% 3.40/3.79 (14543) {G0,W10,D4,L2,V2,M2} { ! alpha26( X, Y ), X = sdtasdt0( Y, skol9(
% 3.40/3.79 X, Y ) ) }.
% 3.40/3.79 (14544) {G0,W12,D3,L4,V3,M4} { ! aNaturalNumber0( Y ), ! aNaturalNumber0(
% 3.40/3.79 Z ), ! X = sdtasdt0( Y, Z ), alpha26( X, Y ) }.
% 3.40/3.79 (14545) {G0,W6,D2,L3,V1,M3} { ! alpha11( X ), ! aNaturalNumber0( X ),
% 3.40/3.79 alpha16( X ) }.
% 3.40/3.79 (14546) {G0,W4,D2,L2,V1,M2} { aNaturalNumber0( X ), alpha11( X ) }.
% 3.40/3.79 (14547) {G0,W4,D2,L2,V1,M2} { ! alpha16( X ), alpha11( X ) }.
% 3.40/3.79 (14548) {G0,W9,D3,L3,V2,M3} { ! alpha16( X ), ! aNaturalNumber0( Y ), ! xk
% 3.40/3.79 = sdtasdt0( X, Y ) }.
% 3.40/3.79 (14549) {G0,W5,D2,L2,V1,M2} { ! alpha16( X ), ! doDivides0( X, xk ) }.
% 3.40/3.79 (14550) {G0,W8,D3,L3,V2,M3} { aNaturalNumber0( skol10( Y ) ), doDivides0(
% 3.40/3.79 X, xk ), alpha16( X ) }.
% 3.40/3.79 (14551) {G0,W11,D4,L3,V1,M3} { xk = sdtasdt0( X, skol10( X ) ), doDivides0
% 3.40/3.79 ( X, xk ), alpha16( X ) }.
% 3.40/3.79 (14552) {G0,W2,D1,L2,V0,M2} { ! alpha8, alpha12 }.
% 3.40/3.79 (14553) {G0,W3,D2,L2,V0,M2} { ! alpha8, isPrime0( xk ) }.
% 3.40/3.79 (14554) {G0,W4,D2,L3,V0,M3} { ! alpha12, ! isPrime0( xk ), alpha8 }.
% 3.40/3.79 (14555) {G0,W6,D2,L3,V1,M3} { ! alpha12, alpha17( X ), X = xk }.
% 3.40/3.79 (14556) {G0,W3,D2,L2,V0,M2} { ! alpha17( skol11 ), alpha12 }.
% 3.40/3.79 (14557) {G0,W4,D2,L2,V0,M2} { ! skol11 = xk, alpha12 }.
% 3.40/3.79 (14558) {G0,W7,D2,L3,V1,M3} { ! alpha17( X ), alpha21( X ), X = sz10 }.
% 3.40/3.79 (14559) {G0,W4,D2,L2,V1,M2} { ! alpha21( X ), alpha17( X ) }.
% 3.40/3.79 (14560) {G0,W5,D2,L2,V1,M2} { ! X = sz10, alpha17( X ) }.
% 3.40/3.79 (14561) {G0,W6,D2,L3,V1,M3} { ! alpha21( X ), ! aNaturalNumber0( X ),
% 3.40/3.79 alpha24( X ) }.
% 3.40/3.79 (14562) {G0,W4,D2,L2,V1,M2} { aNaturalNumber0( X ), alpha21( X ) }.
% 3.40/3.79 (14563) {G0,W4,D2,L2,V1,M2} { ! alpha24( X ), alpha21( X ) }.
% 3.40/3.79 (14564) {G0,W9,D3,L3,V2,M3} { ! alpha24( X ), ! aNaturalNumber0( Y ), ! xk
% 3.40/3.80 = sdtasdt0( X, Y ) }.
% 3.40/3.80 (14565) {G0,W5,D2,L2,V1,M2} { ! alpha24( X ), ! doDivides0( X, xk ) }.
% 3.40/3.80 (14566) {G0,W8,D3,L3,V2,M3} { aNaturalNumber0( skol12( Y ) ), doDivides0(
% 3.40/3.80 X, xk ), alpha24( X ) }.
% 3.40/3.80 (14567) {G0,W11,D4,L3,V1,M3} { xk = sdtasdt0( X, skol12( X ) ), doDivides0
% 3.40/3.80 ( X, xk ), alpha24( X ) }.
% 3.40/3.80
% 3.40/3.80
% 3.40/3.80 Total Proof:
% 3.40/3.80
% 3.40/3.80 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 3.40/3.80 parent0: (14417) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 3.40/3.80 substitution0:
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 3.40/3.80 parent0: (14418) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 3.40/3.80 substitution0:
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 3.40/3.80 X, sz00 ) ==> X }.
% 3.40/3.80 parent0: (14424) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X
% 3.40/3.80 , sz00 ) = X }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 1 ==> 1
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 eqswap: (14596) {G0,W7,D3,L2,V1,M2} { sdtpldt0( sz00, X ) = X, !
% 3.40/3.80 aNaturalNumber0( X ) }.
% 3.40/3.80 parent0[1]: (14425) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X =
% 3.40/3.80 sdtpldt0( sz00, X ) }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 3.40/3.80 sz00, X ) ==> X }.
% 3.40/3.80 parent0: (14596) {G0,W7,D3,L2,V1,M2} { sdtpldt0( sz00, X ) = X, !
% 3.40/3.80 aNaturalNumber0( X ) }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 1
% 3.40/3.80 1 ==> 0
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (12) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtasdt0
% 3.40/3.80 ( X, sz10 ) ==> X }.
% 3.40/3.80 parent0: (14428) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X
% 3.40/3.80 , sz10 ) = X }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 1 ==> 1
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (23) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 3.40/3.80 parent0: (14439) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 Y := Y
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 1 ==> 1
% 3.40/3.80 2 ==> 2
% 3.40/3.80 3 ==> 3
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 3.40/3.80 sdtlseqdt0( X, Y ) }.
% 3.40/3.80 parent0: (14443) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 3.40/3.80 sdtlseqdt0( X, Y ) }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 Y := Y
% 3.40/3.80 Z := Z
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 1 ==> 1
% 3.40/3.80 2 ==> 2
% 3.40/3.80 3 ==> 3
% 3.40/3.80 4 ==> 4
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (28) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 3.40/3.80 aNaturalNumber0( Z ) }.
% 3.40/3.80 parent0: (14444) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 3.40/3.80 aNaturalNumber0( Z ) }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 Y := Y
% 3.40/3.80 Z := Z
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 1 ==> 1
% 3.40/3.80 2 ==> 2
% 3.40/3.80 3 ==> 3
% 3.40/3.80 4 ==> 4
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (29) {G0,W17,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 3.40/3.80 sdtpldt0( X, Z ) = Y }.
% 3.40/3.80 parent0: (14445) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 3.40/3.80 sdtpldt0( X, Z ) = Y }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 Y := Y
% 3.40/3.80 Z := Z
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 1 ==> 1
% 3.40/3.80 2 ==> 2
% 3.40/3.80 3 ==> 3
% 3.40/3.80 4 ==> 4
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (30) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), !
% 3.40/3.80 sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 3.40/3.80 parent0: (14446) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), !
% 3.40/3.80 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), !
% 3.40/3.80 sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 3.40/3.80 substitution0:
% 3.40/3.80 X := X
% 3.40/3.80 Y := Y
% 3.40/3.80 Z := Z
% 3.40/3.80 end
% 3.40/3.80 permutation0:
% 3.40/3.80 0 ==> 0
% 3.40/3.80 1 ==> 1
% 3.40/3.80 2 ==> 2
% 3.40/3.80 3 ==> 3
% 3.40/3.80 4 ==> 4
% 3.40/3.80 5 ==> 5
% 3.40/3.80 end
% 3.40/3.80
% 3.40/3.80 subsumption: (31) {G0,W5,D2,L2,V1,M2} I { ! aNaturalNumber0( X ),
% 3.40/3.80 sdtlseqdt0( X, X ) }.
% 3.40/3.81 parent0: (14447) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0
% 3.40/3.81 ( X, X ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (34) {G0,W10,D2,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 3.40/3.81 aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 3.40/3.81 parent0: (14450) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 3.40/3.81 aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 Y := Y
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 2 ==> 2
% 3.40/3.81 3 ==> 3
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (54) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 3.40/3.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ),
% 3.40/3.81 doDivides0( X, Y ) }.
% 3.40/3.81 parent0: (14471) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 3.40/3.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ),
% 3.40/3.81 doDivides0( X, Y ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 Y := Y
% 3.40/3.81 Z := Z
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 2 ==> 2
% 3.40/3.81 3 ==> 3
% 3.40/3.81 4 ==> 4
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (72) {G0,W9,D2,L3,V2,M3} I { ! alpha4( X, Y ), Y = sz10, Y = X
% 3.40/3.81 }.
% 3.40/3.81 parent0: (14489) {G0,W9,D2,L3,V2,M3} { ! alpha4( X, Y ), Y = sz10, Y = X
% 3.40/3.81 }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 Y := Y
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 2 ==> 2
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 3.40/3.81 parent0: (14490) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha4( X, Y ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 Y := Y
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (78) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xk ) }.
% 3.40/3.81 parent0: (14495) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xk ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (112) {G0,W1,D1,L1,V0,M1} I { alpha8 }.
% 3.40/3.81 parent0: (14529) {G0,W1,D1,L1,V0,M1} { alpha8 }.
% 3.40/3.81 substitution0:
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (114) {G0,W4,D2,L2,V1,M2} I { alpha11( X ), ! isPrime0( X )
% 3.40/3.81 }.
% 3.40/3.81 parent0: (14531) {G0,W4,D2,L2,V1,M2} { alpha11( X ), ! isPrime0( X ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (128) {G0,W6,D2,L3,V1,M3} I { ! alpha11( X ), !
% 3.40/3.81 aNaturalNumber0( X ), alpha16( X ) }.
% 3.40/3.81 parent0: (14545) {G0,W6,D2,L3,V1,M3} { ! alpha11( X ), ! aNaturalNumber0(
% 3.40/3.81 X ), alpha16( X ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 2 ==> 2
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 *** allocated 576640 integers for termspace/termends
% 3.40/3.81 subsumption: (132) {G0,W5,D2,L2,V1,M2} I { ! alpha16( X ), ! doDivides0( X
% 3.40/3.81 , xk ) }.
% 3.40/3.81 parent0: (14549) {G0,W5,D2,L2,V1,M2} { ! alpha16( X ), ! doDivides0( X, xk
% 3.40/3.81 ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 resolution: (19530) {G1,W2,D2,L1,V0,M1} { isPrime0( xk ) }.
% 3.40/3.81 parent0[0]: (14553) {G0,W3,D2,L2,V0,M2} { ! alpha8, isPrime0( xk ) }.
% 3.40/3.81 parent1[0]: (112) {G0,W1,D1,L1,V0,M1} I { alpha8 }.
% 3.40/3.81 substitution0:
% 3.40/3.81 end
% 3.40/3.81 substitution1:
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (136) {G1,W2,D2,L1,V0,M1} I;r(112) { isPrime0( xk ) }.
% 3.40/3.81 parent0: (19530) {G1,W2,D2,L1,V0,M1} { isPrime0( xk ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 factor: (19534) {G0,W6,D2,L2,V1,M2} { ! alpha4( sz10, X ), X = sz10 }.
% 3.40/3.81 parent0[1, 2]: (72) {G0,W9,D2,L3,V2,M3} I { ! alpha4( X, Y ), Y = sz10, Y =
% 3.40/3.81 X }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := sz10
% 3.40/3.81 Y := X
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (278) {G1,W6,D2,L2,V1,M2} F(72) { ! alpha4( sz10, X ), X =
% 3.40/3.81 sz10 }.
% 3.40/3.81 parent0: (19534) {G0,W6,D2,L2,V1,M2} { ! alpha4( sz10, X ), X = sz10 }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 eqswap: (19536) {G0,W14,D3,L5,V3,M5} { ! Z = sdtpldt0( X, Y ), !
% 3.40/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! aNaturalNumber0( Y ),
% 3.40/3.81 sdtlseqdt0( X, Z ) }.
% 3.40/3.81 parent0[3]: (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 3.40/3.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 3.40/3.81 sdtlseqdt0( X, Y ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 Y := Z
% 3.40/3.81 Z := Y
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 resolution: (19538) {G1,W12,D3,L4,V2,M4} { ! X = sdtpldt0( sz00, Y ), !
% 3.40/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( sz00, X ) }.
% 3.40/3.81 parent0[1]: (19536) {G0,W14,D3,L5,V3,M5} { ! Z = sdtpldt0( X, Y ), !
% 3.40/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! aNaturalNumber0( Y ),
% 3.40/3.81 sdtlseqdt0( X, Z ) }.
% 3.40/3.81 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := sz00
% 3.40/3.81 Y := Y
% 3.40/3.81 Z := X
% 3.40/3.81 end
% 3.40/3.81 substitution1:
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 paramod: (19546) {G1,W12,D2,L5,V2,M5} { ! X = Y, ! aNaturalNumber0( Y ), !
% 3.40/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( sz00, X ) }.
% 3.40/3.81 parent0[1]: (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 3.40/3.81 sz00, X ) ==> X }.
% 3.40/3.81 parent1[0; 3]: (19538) {G1,W12,D3,L4,V2,M4} { ! X = sdtpldt0( sz00, Y ), !
% 3.40/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( sz00, X ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := Y
% 3.40/3.81 end
% 3.40/3.81 substitution1:
% 3.40/3.81 X := X
% 3.40/3.81 Y := Y
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 eqswap: (19547) {G1,W12,D2,L5,V2,M5} { ! Y = X, ! aNaturalNumber0( Y ), !
% 3.40/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( sz00, X ) }.
% 3.40/3.81 parent0[0]: (19546) {G1,W12,D2,L5,V2,M5} { ! X = Y, ! aNaturalNumber0( Y )
% 3.40/3.81 , ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( sz00, X )
% 3.40/3.81 }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 Y := Y
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 factor: (19549) {G1,W10,D2,L4,V2,M4} { ! X = Y, ! aNaturalNumber0( X ), !
% 3.40/3.81 aNaturalNumber0( Y ), sdtlseqdt0( sz00, Y ) }.
% 3.40/3.81 parent0[1, 3]: (19547) {G1,W12,D2,L5,V2,M5} { ! Y = X, ! aNaturalNumber0(
% 3.40/3.81 Y ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( sz00, X
% 3.40/3.81 ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := Y
% 3.40/3.81 Y := X
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (1570) {G1,W10,D2,L4,V2,M4} R(27,1);d(9) { ! aNaturalNumber0(
% 3.40/3.81 X ), ! aNaturalNumber0( Y ), sdtlseqdt0( sz00, X ), ! Y = X }.
% 3.40/3.81 parent0: (19549) {G1,W10,D2,L4,V2,M4} { ! X = Y, ! aNaturalNumber0( X ), !
% 3.40/3.81 aNaturalNumber0( Y ), sdtlseqdt0( sz00, Y ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := Y
% 3.40/3.81 Y := X
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 3
% 3.40/3.81 1 ==> 1
% 3.40/3.81 2 ==> 0
% 3.40/3.81 3 ==> 2
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 eqswap: (19552) {G1,W10,D2,L4,V2,M4} { ! Y = X, ! aNaturalNumber0( Y ), !
% 3.40/3.81 aNaturalNumber0( X ), sdtlseqdt0( sz00, Y ) }.
% 3.40/3.81 parent0[3]: (1570) {G1,W10,D2,L4,V2,M4} R(27,1);d(9) { ! aNaturalNumber0( X
% 3.40/3.81 ), ! aNaturalNumber0( Y ), sdtlseqdt0( sz00, X ), ! Y = X }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := Y
% 3.40/3.81 Y := X
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 factor: (19553) {G1,W8,D2,L3,V1,M3} { ! X = X, ! aNaturalNumber0( X ),
% 3.40/3.81 sdtlseqdt0( sz00, X ) }.
% 3.40/3.81 parent0[1, 2]: (19552) {G1,W10,D2,L4,V2,M4} { ! Y = X, ! aNaturalNumber0(
% 3.40/3.81 Y ), ! aNaturalNumber0( X ), sdtlseqdt0( sz00, Y ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 Y := X
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 eqrefl: (19554) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0(
% 3.40/3.81 sz00, X ) }.
% 3.40/3.81 parent0[0]: (19553) {G1,W8,D2,L3,V1,M3} { ! X = X, ! aNaturalNumber0( X )
% 3.40/3.81 , sdtlseqdt0( sz00, X ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (1591) {G2,W5,D2,L2,V1,M2} F(1570);q { ! aNaturalNumber0( X )
% 3.40/3.81 , sdtlseqdt0( sz00, X ) }.
% 3.40/3.81 parent0: (19554) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0
% 3.40/3.81 ( sz00, X ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := X
% 3.40/3.81 end
% 3.40/3.81 permutation0:
% 3.40/3.81 0 ==> 0
% 3.40/3.81 1 ==> 1
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 resolution: (19555) {G1,W3,D2,L1,V0,M1} { sdtlseqdt0( sz00, xk ) }.
% 3.40/3.81 parent0[0]: (1591) {G2,W5,D2,L2,V1,M2} F(1570);q { ! aNaturalNumber0( X ),
% 3.40/3.81 sdtlseqdt0( sz00, X ) }.
% 3.40/3.81 parent1[0]: (78) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xk ) }.
% 3.40/3.81 substitution0:
% 3.40/3.81 X := xk
% 3.40/3.81 end
% 3.40/3.81 substitution1:
% 3.40/3.81 end
% 3.40/3.81
% 3.40/3.81 subsumption: (1668) {G3,W3,D2,L1,V0,M1} R(1591,78) { sdtlseqdt0( sz00, xk )
% 3.40/3.81 }.
% 3.44/3.81 parent0: (19555) {G1,W3,D2,L1,V0,M1} { sdtlseqdt0( sz00, xk ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 end
% 3.44/3.81 permutation0:
% 3.44/3.81 0 ==> 0
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqswap: (19556) {G0,W19,D3,L6,V3,M6} { ! Z = sdtpldt0( X, Y ), !
% 3.44/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Z ), !
% 3.44/3.81 aNaturalNumber0( Y ), Y = sdtmndt0( Z, X ) }.
% 3.44/3.81 parent0[4]: (30) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), !
% 3.44/3.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), !
% 3.44/3.81 sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Z
% 3.44/3.81 Z := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 resolution: (19560) {G1,W18,D3,L6,V2,M6} { ! X = sdtpldt0( sz00, Y ), !
% 3.44/3.81 aNaturalNumber0( sz00 ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ),
% 3.44/3.81 Y = sdtmndt0( X, sz00 ), ! aNaturalNumber0( X ) }.
% 3.44/3.81 parent0[3]: (19556) {G0,W19,D3,L6,V3,M6} { ! Z = sdtpldt0( X, Y ), !
% 3.44/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Z ), !
% 3.44/3.81 aNaturalNumber0( Y ), Y = sdtmndt0( Z, X ) }.
% 3.44/3.81 parent1[1]: (1591) {G2,W5,D2,L2,V1,M2} F(1570);q { ! aNaturalNumber0( X ),
% 3.44/3.81 sdtlseqdt0( sz00, X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := sz00
% 3.44/3.81 Y := Y
% 3.44/3.81 Z := X
% 3.44/3.81 end
% 3.44/3.81 substitution1:
% 3.44/3.81 X := X
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 paramod: (19569) {G1,W18,D3,L7,V2,M7} { ! X = Y, ! aNaturalNumber0( Y ), !
% 3.44/3.81 aNaturalNumber0( sz00 ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 3.44/3.81 , Y = sdtmndt0( X, sz00 ), ! aNaturalNumber0( X ) }.
% 3.44/3.81 parent0[1]: (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 3.44/3.81 sz00, X ) ==> X }.
% 3.44/3.81 parent1[0; 3]: (19560) {G1,W18,D3,L6,V2,M6} { ! X = sdtpldt0( sz00, Y ), !
% 3.44/3.81 aNaturalNumber0( sz00 ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 3.44/3.81 , Y = sdtmndt0( X, sz00 ), ! aNaturalNumber0( X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := Y
% 3.44/3.81 end
% 3.44/3.81 substitution1:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 factor: (19572) {G1,W16,D3,L6,V2,M6} { ! X = Y, ! aNaturalNumber0( Y ), !
% 3.44/3.81 aNaturalNumber0( sz00 ), ! aNaturalNumber0( X ), Y = sdtmndt0( X, sz00 )
% 3.44/3.81 , ! aNaturalNumber0( X ) }.
% 3.44/3.81 parent0[1, 4]: (19569) {G1,W18,D3,L7,V2,M7} { ! X = Y, ! aNaturalNumber0(
% 3.44/3.81 Y ), ! aNaturalNumber0( sz00 ), ! aNaturalNumber0( X ), ! aNaturalNumber0
% 3.44/3.81 ( Y ), Y = sdtmndt0( X, sz00 ), ! aNaturalNumber0( X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 factor: (19576) {G1,W14,D3,L5,V2,M5} { ! X = Y, ! aNaturalNumber0( Y ), !
% 3.44/3.81 aNaturalNumber0( sz00 ), ! aNaturalNumber0( X ), Y = sdtmndt0( X, sz00 )
% 3.44/3.81 }.
% 3.44/3.81 parent0[3, 5]: (19572) {G1,W16,D3,L6,V2,M6} { ! X = Y, ! aNaturalNumber0(
% 3.44/3.81 Y ), ! aNaturalNumber0( sz00 ), ! aNaturalNumber0( X ), Y = sdtmndt0( X,
% 3.44/3.81 sz00 ), ! aNaturalNumber0( X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 resolution: (19629) {G1,W12,D3,L4,V2,M4} { ! X = Y, ! aNaturalNumber0( Y )
% 3.44/3.81 , ! aNaturalNumber0( X ), Y = sdtmndt0( X, sz00 ) }.
% 3.44/3.81 parent0[2]: (19576) {G1,W14,D3,L5,V2,M5} { ! X = Y, ! aNaturalNumber0( Y )
% 3.44/3.81 , ! aNaturalNumber0( sz00 ), ! aNaturalNumber0( X ), Y = sdtmndt0( X,
% 3.44/3.81 sz00 ) }.
% 3.44/3.81 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81 substitution1:
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqswap: (19630) {G1,W12,D3,L4,V2,M4} { ! Y = X, ! aNaturalNumber0( Y ), !
% 3.44/3.81 aNaturalNumber0( X ), Y = sdtmndt0( X, sz00 ) }.
% 3.44/3.81 parent0[0]: (19629) {G1,W12,D3,L4,V2,M4} { ! X = Y, ! aNaturalNumber0( Y )
% 3.44/3.81 , ! aNaturalNumber0( X ), Y = sdtmndt0( X, sz00 ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 subsumption: (2180) {G3,W12,D3,L4,V2,M4} R(30,1591);f;d(9);r(1) { !
% 3.44/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), Y = sdtmndt0( X, sz00 ), !
% 3.44/3.81 Y = X }.
% 3.44/3.81 parent0: (19630) {G1,W12,D3,L4,V2,M4} { ! Y = X, ! aNaturalNumber0( Y ), !
% 3.44/3.81 aNaturalNumber0( X ), Y = sdtmndt0( X, sz00 ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81 permutation0:
% 3.44/3.81 0 ==> 3
% 3.44/3.81 1 ==> 1
% 3.44/3.81 2 ==> 0
% 3.44/3.81 3 ==> 2
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqswap: (19635) {G0,W19,D3,L6,V3,M6} { ! Z = sdtpldt0( X, Y ), !
% 3.44/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Z ), !
% 3.44/3.81 aNaturalNumber0( Y ), Y = sdtmndt0( Z, X ) }.
% 3.44/3.81 parent0[4]: (30) {G0,W19,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), !
% 3.44/3.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), !
% 3.44/3.81 sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Z
% 3.44/3.81 Z := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 resolution: (19641) {G1,W17,D3,L5,V2,M5} { ! X = sdtpldt0( Y, sz00 ), !
% 3.44/3.81 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtlseqdt0( Y, X ), sz00
% 3.44/3.81 = sdtmndt0( X, Y ) }.
% 3.44/3.81 parent0[4]: (19635) {G0,W19,D3,L6,V3,M6} { ! Z = sdtpldt0( X, Y ), !
% 3.44/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Z ), !
% 3.44/3.81 aNaturalNumber0( Y ), Y = sdtmndt0( Z, X ) }.
% 3.44/3.81 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz00 ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := Y
% 3.44/3.81 Y := sz00
% 3.44/3.81 Z := X
% 3.44/3.81 end
% 3.44/3.81 substitution1:
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 paramod: (19649) {G1,W17,D3,L6,V2,M6} { ! X = Y, ! aNaturalNumber0( Y ), !
% 3.44/3.81 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtlseqdt0( Y, X ), sz00
% 3.44/3.81 = sdtmndt0( X, Y ) }.
% 3.44/3.81 parent0[1]: (8) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0( X
% 3.44/3.81 , sz00 ) ==> X }.
% 3.44/3.81 parent1[0; 3]: (19641) {G1,W17,D3,L5,V2,M5} { ! X = sdtpldt0( Y, sz00 ), !
% 3.44/3.81 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtlseqdt0( Y, X ), sz00
% 3.44/3.81 = sdtmndt0( X, Y ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := Y
% 3.44/3.81 end
% 3.44/3.81 substitution1:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqswap: (19651) {G1,W17,D3,L6,V2,M6} { sdtmndt0( X, Y ) = sz00, ! X = Y, !
% 3.44/3.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( X ), !
% 3.44/3.81 sdtlseqdt0( Y, X ) }.
% 3.44/3.81 parent0[5]: (19649) {G1,W17,D3,L6,V2,M6} { ! X = Y, ! aNaturalNumber0( Y )
% 3.44/3.81 , ! aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtlseqdt0( Y, X ),
% 3.44/3.81 sz00 = sdtmndt0( X, Y ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqswap: (19652) {G1,W17,D3,L6,V2,M6} { ! Y = X, sdtmndt0( X, Y ) = sz00, !
% 3.44/3.81 aNaturalNumber0( Y ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( X ), !
% 3.44/3.81 sdtlseqdt0( Y, X ) }.
% 3.44/3.81 parent0[1]: (19651) {G1,W17,D3,L6,V2,M6} { sdtmndt0( X, Y ) = sz00, ! X =
% 3.44/3.81 Y, ! aNaturalNumber0( Y ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( X )
% 3.44/3.81 , ! sdtlseqdt0( Y, X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 factor: (19655) {G1,W15,D3,L5,V2,M5} { ! X = Y, sdtmndt0( Y, X ) = sz00, !
% 3.44/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ) }.
% 3.44/3.81 parent0[2, 3]: (19652) {G1,W17,D3,L6,V2,M6} { ! Y = X, sdtmndt0( X, Y ) =
% 3.44/3.81 sz00, ! aNaturalNumber0( Y ), ! aNaturalNumber0( Y ), ! aNaturalNumber0(
% 3.44/3.81 X ), ! sdtlseqdt0( Y, X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := Y
% 3.44/3.81 Y := X
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 subsumption: (2223) {G1,W15,D3,L5,V2,M5} R(30,1);d(8) { ! aNaturalNumber0(
% 3.44/3.81 X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), sdtmndt0( Y, X ) ==>
% 3.44/3.81 sz00, ! X = Y }.
% 3.44/3.81 parent0: (19655) {G1,W15,D3,L5,V2,M5} { ! X = Y, sdtmndt0( Y, X ) = sz00,
% 3.44/3.81 ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81 permutation0:
% 3.44/3.81 0 ==> 4
% 3.44/3.81 1 ==> 3
% 3.44/3.81 2 ==> 0
% 3.44/3.81 3 ==> 1
% 3.44/3.81 4 ==> 2
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqswap: (19660) {G1,W15,D3,L5,V2,M5} { ! Y = X, ! aNaturalNumber0( X ), !
% 3.44/3.81 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), sdtmndt0( Y, X ) ==> sz00 }.
% 3.44/3.81 parent0[4]: (2223) {G1,W15,D3,L5,V2,M5} R(30,1);d(8) { ! aNaturalNumber0( X
% 3.44/3.81 ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), sdtmndt0( Y, X ) ==>
% 3.44/3.81 sz00, ! X = Y }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := Y
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 factor: (19663) {G1,W13,D3,L4,V1,M4} { ! X = X, ! aNaturalNumber0( X ), !
% 3.44/3.81 sdtlseqdt0( X, X ), sdtmndt0( X, X ) ==> sz00 }.
% 3.44/3.81 parent0[1, 2]: (19660) {G1,W15,D3,L5,V2,M5} { ! Y = X, ! aNaturalNumber0(
% 3.44/3.81 X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), sdtmndt0( Y, X ) ==>
% 3.44/3.81 sz00 }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := X
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqrefl: (19664) {G0,W10,D3,L3,V1,M3} { ! aNaturalNumber0( X ), !
% 3.44/3.81 sdtlseqdt0( X, X ), sdtmndt0( X, X ) ==> sz00 }.
% 3.44/3.81 parent0[0]: (19663) {G1,W13,D3,L4,V1,M4} { ! X = X, ! aNaturalNumber0( X )
% 3.44/3.81 , ! sdtlseqdt0( X, X ), sdtmndt0( X, X ) ==> sz00 }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 resolution: (19665) {G1,W9,D3,L3,V1,M3} { ! aNaturalNumber0( X ), sdtmndt0
% 3.44/3.81 ( X, X ) ==> sz00, ! aNaturalNumber0( X ) }.
% 3.44/3.81 parent0[1]: (19664) {G0,W10,D3,L3,V1,M3} { ! aNaturalNumber0( X ), !
% 3.44/3.81 sdtlseqdt0( X, X ), sdtmndt0( X, X ) ==> sz00 }.
% 3.44/3.81 parent1[1]: (31) {G0,W5,D2,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtlseqdt0
% 3.44/3.81 ( X, X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 end
% 3.44/3.81 substitution1:
% 3.44/3.81 X := X
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 factor: (19668) {G1,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtmndt0( X
% 3.44/3.81 , X ) ==> sz00 }.
% 3.44/3.81 parent0[0, 2]: (19665) {G1,W9,D3,L3,V1,M3} { ! aNaturalNumber0( X ),
% 3.44/3.81 sdtmndt0( X, X ) ==> sz00, ! aNaturalNumber0( X ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 subsumption: (2275) {G2,W7,D3,L2,V1,M2} F(2223);q;r(31) { ! aNaturalNumber0
% 3.44/3.81 ( X ), sdtmndt0( X, X ) ==> sz00 }.
% 3.44/3.81 parent0: (19668) {G1,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtmndt0( X
% 3.44/3.81 , X ) ==> sz00 }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 end
% 3.44/3.81 permutation0:
% 3.44/3.81 0 ==> 0
% 3.44/3.81 1 ==> 1
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqswap: (19670) {G3,W12,D3,L4,V2,M4} { ! Y = X, ! aNaturalNumber0( Y ), !
% 3.44/3.81 aNaturalNumber0( X ), X = sdtmndt0( Y, sz00 ) }.
% 3.44/3.81 parent0[3]: (2180) {G3,W12,D3,L4,V2,M4} R(30,1591);f;d(9);r(1) { !
% 3.44/3.81 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), Y = sdtmndt0( X, sz00 ), !
% 3.44/3.81 Y = X }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := Y
% 3.44/3.81 Y := X
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 factor: (19673) {G3,W10,D3,L3,V1,M3} { ! X = X, ! aNaturalNumber0( X ), X
% 3.44/3.81 = sdtmndt0( X, sz00 ) }.
% 3.44/3.81 parent0[1, 2]: (19670) {G3,W12,D3,L4,V2,M4} { ! Y = X, ! aNaturalNumber0(
% 3.44/3.81 Y ), ! aNaturalNumber0( X ), X = sdtmndt0( Y, sz00 ) }.
% 3.44/3.81 substitution0:
% 3.44/3.81 X := X
% 3.44/3.81 Y := X
% 3.44/3.81 end
% 3.44/3.81
% 3.44/3.81 eqrefl: (19674) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtmndt0
% 4.60/5.01 ( X, sz00 ) }.
% 4.60/5.01 parent0[0]: (19673) {G3,W10,D3,L3,V1,M3} { ! X = X, ! aNaturalNumber0( X )
% 4.60/5.01 , X = sdtmndt0( X, sz00 ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (19675) {G0,W7,D3,L2,V1,M2} { sdtmndt0( X, sz00 ) = X, !
% 4.60/5.01 aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[1]: (19674) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X =
% 4.60/5.01 sdtmndt0( X, sz00 ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 subsumption: (2288) {G4,W7,D3,L2,V1,M2} F(2180);q { ! aNaturalNumber0( X )
% 4.60/5.01 , sdtmndt0( X, sz00 ) ==> X }.
% 4.60/5.01 parent0: (19675) {G0,W7,D3,L2,V1,M2} { sdtmndt0( X, sz00 ) = X, !
% 4.60/5.01 aNaturalNumber0( X ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 permutation0:
% 4.60/5.01 0 ==> 1
% 4.60/5.01 1 ==> 0
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 *** allocated 15000 integers for justifications
% 4.60/5.01 *** allocated 22500 integers for justifications
% 4.60/5.01 eqswap: (19676) {G1,W6,D2,L2,V1,M2} { sz10 = X, ! alpha4( sz10, X ) }.
% 4.60/5.01 parent0[1]: (278) {G1,W6,D2,L2,V1,M2} F(72) { ! alpha4( sz10, X ), X = sz10
% 4.60/5.01 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 paramod: (19677) {G1,W5,D2,L2,V1,M2} { aNaturalNumber0( X ), ! alpha4(
% 4.60/5.01 sz10, X ) }.
% 4.60/5.01 parent0[0]: (19676) {G1,W6,D2,L2,V1,M2} { sz10 = X, ! alpha4( sz10, X )
% 4.60/5.01 }.
% 4.60/5.01 parent1[0; 1]: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 subsumption: (4512) {G2,W5,D2,L2,V1,M2} P(278,2) { aNaturalNumber0( X ), !
% 4.60/5.01 alpha4( sz10, X ) }.
% 4.60/5.01 parent0: (19677) {G1,W5,D2,L2,V1,M2} { aNaturalNumber0( X ), ! alpha4(
% 4.60/5.01 sz10, X ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 permutation0:
% 4.60/5.01 0 ==> 0
% 4.60/5.01 1 ==> 1
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20131) {G0,W6,D2,L2,V2,M2} { ! sz10 = X, alpha4( Y, X ) }.
% 4.60/5.01 parent0[0]: (73) {G0,W6,D2,L2,V2,M2} I { ! Y = sz10, alpha4( X, Y ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := Y
% 4.60/5.01 Y := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 resolution: (20132) {G1,W5,D2,L2,V1,M2} { aNaturalNumber0( X ), ! sz10 = X
% 4.60/5.01 }.
% 4.60/5.01 parent0[1]: (4512) {G2,W5,D2,L2,V1,M2} P(278,2) { aNaturalNumber0( X ), !
% 4.60/5.01 alpha4( sz10, X ) }.
% 4.60/5.01 parent1[1]: (20131) {G0,W6,D2,L2,V2,M2} { ! sz10 = X, alpha4( Y, X ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 X := X
% 4.60/5.01 Y := sz10
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20133) {G1,W5,D2,L2,V1,M2} { ! X = sz10, aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[1]: (20132) {G1,W5,D2,L2,V1,M2} { aNaturalNumber0( X ), ! sz10 = X
% 4.60/5.01 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 subsumption: (4599) {G3,W5,D2,L2,V1,M2} R(4512,73) { aNaturalNumber0( X ),
% 4.60/5.01 ! X = sz10 }.
% 4.60/5.01 parent0: (20133) {G1,W5,D2,L2,V1,M2} { ! X = sz10, aNaturalNumber0( X )
% 4.60/5.01 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 permutation0:
% 4.60/5.01 0 ==> 1
% 4.60/5.01 1 ==> 0
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20134) {G3,W5,D2,L2,V1,M2} { ! sz10 = X, aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[1]: (4599) {G3,W5,D2,L2,V1,M2} R(4512,73) { aNaturalNumber0( X ), !
% 4.60/5.01 X = sz10 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20135) {G0,W10,D2,L4,V2,M4} { ! Y = X, ! aNaturalNumber0( Y ), !
% 4.60/5.01 aNaturalNumber0( X ), sdtlseqdt0( Y, X ) }.
% 4.60/5.01 parent0[3]: (34) {G0,W10,D2,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 4.60/5.01 aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := Y
% 4.60/5.01 Y := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 resolution: (20137) {G1,W11,D2,L4,V2,M4} { ! X = Y, ! aNaturalNumber0( X )
% 4.60/5.01 , sdtlseqdt0( X, Y ), ! sz10 = Y }.
% 4.60/5.01 parent0[2]: (20135) {G0,W10,D2,L4,V2,M4} { ! Y = X, ! aNaturalNumber0( Y )
% 4.60/5.01 , ! aNaturalNumber0( X ), sdtlseqdt0( Y, X ) }.
% 4.60/5.01 parent1[1]: (20134) {G3,W5,D2,L2,V1,M2} { ! sz10 = X, aNaturalNumber0( X )
% 4.60/5.01 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := Y
% 4.60/5.01 Y := X
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 X := Y
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20139) {G1,W11,D2,L4,V2,M4} { ! X = sz10, ! Y = X, !
% 4.60/5.01 aNaturalNumber0( Y ), sdtlseqdt0( Y, X ) }.
% 4.60/5.01 parent0[3]: (20137) {G1,W11,D2,L4,V2,M4} { ! X = Y, ! aNaturalNumber0( X )
% 4.60/5.01 , sdtlseqdt0( X, Y ), ! sz10 = Y }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := Y
% 4.60/5.01 Y := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20140) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! Y = sz10, !
% 4.60/5.01 aNaturalNumber0( X ), sdtlseqdt0( X, Y ) }.
% 4.60/5.01 parent0[1]: (20139) {G1,W11,D2,L4,V2,M4} { ! X = sz10, ! Y = X, !
% 4.60/5.01 aNaturalNumber0( Y ), sdtlseqdt0( Y, X ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := Y
% 4.60/5.01 Y := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 subsumption: (4716) {G4,W11,D2,L4,V2,M4} R(4599,34) { ! X = sz10, !
% 4.60/5.01 aNaturalNumber0( Y ), sdtlseqdt0( Y, X ), ! X = Y }.
% 4.60/5.01 parent0: (20140) {G1,W11,D2,L4,V2,M4} { ! Y = X, ! Y = sz10, !
% 4.60/5.01 aNaturalNumber0( X ), sdtlseqdt0( X, Y ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := Y
% 4.60/5.01 Y := X
% 4.60/5.01 end
% 4.60/5.01 permutation0:
% 4.60/5.01 0 ==> 3
% 4.60/5.01 1 ==> 0
% 4.60/5.01 2 ==> 1
% 4.60/5.01 3 ==> 2
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 factor: (20153) {G4,W8,D2,L3,V1,M3} { ! X = sz10, ! aNaturalNumber0( sz10
% 4.60/5.01 ), sdtlseqdt0( sz10, X ) }.
% 4.60/5.01 parent0[0, 3]: (4716) {G4,W11,D2,L4,V2,M4} R(4599,34) { ! X = sz10, !
% 4.60/5.01 aNaturalNumber0( Y ), sdtlseqdt0( Y, X ), ! X = Y }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := sz10
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 resolution: (20154) {G1,W6,D2,L2,V1,M2} { ! X = sz10, sdtlseqdt0( sz10, X
% 4.60/5.01 ) }.
% 4.60/5.01 parent0[1]: (20153) {G4,W8,D2,L3,V1,M3} { ! X = sz10, ! aNaturalNumber0(
% 4.60/5.01 sz10 ), sdtlseqdt0( sz10, X ) }.
% 4.60/5.01 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 subsumption: (4750) {G5,W6,D2,L2,V1,M2} F(4716);r(2) { ! X = sz10,
% 4.60/5.01 sdtlseqdt0( sz10, X ) }.
% 4.60/5.01 parent0: (20154) {G1,W6,D2,L2,V1,M2} { ! X = sz10, sdtlseqdt0( sz10, X )
% 4.60/5.01 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 permutation0:
% 4.60/5.01 0 ==> 0
% 4.60/5.01 1 ==> 1
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20156) {G5,W6,D2,L2,V1,M2} { ! sz10 = X, sdtlseqdt0( sz10, X )
% 4.60/5.01 }.
% 4.60/5.01 parent0[0]: (4750) {G5,W6,D2,L2,V1,M2} F(4716);r(2) { ! X = sz10,
% 4.60/5.01 sdtlseqdt0( sz10, X ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20157) {G0,W14,D3,L5,V3,M5} { ! sdtmndt0( Y, Z ) = X, !
% 4.60/5.01 aNaturalNumber0( Z ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( Z, Y ),
% 4.60/5.01 aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[3]: (28) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 4.60/5.01 aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ),
% 4.60/5.01 aNaturalNumber0( Z ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := Z
% 4.60/5.01 Y := Y
% 4.60/5.01 Z := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 resolution: (20158) {G1,W14,D3,L5,V2,M5} { ! sdtmndt0( X, sz10 ) = Y, !
% 4.60/5.01 aNaturalNumber0( sz10 ), ! aNaturalNumber0( X ), aNaturalNumber0( Y ), !
% 4.60/5.01 sz10 = X }.
% 4.60/5.01 parent0[3]: (20157) {G0,W14,D3,L5,V3,M5} { ! sdtmndt0( Y, Z ) = X, !
% 4.60/5.01 aNaturalNumber0( Z ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( Z, Y ),
% 4.60/5.01 aNaturalNumber0( X ) }.
% 4.60/5.01 parent1[1]: (20156) {G5,W6,D2,L2,V1,M2} { ! sz10 = X, sdtlseqdt0( sz10, X
% 4.60/5.01 ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := Y
% 4.60/5.01 Y := X
% 4.60/5.01 Z := sz10
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 resolution: (20162) {G1,W12,D3,L4,V2,M4} { ! sdtmndt0( X, sz10 ) = Y, !
% 4.60/5.01 aNaturalNumber0( X ), aNaturalNumber0( Y ), ! sz10 = X }.
% 4.60/5.01 parent0[1]: (20158) {G1,W14,D3,L5,V2,M5} { ! sdtmndt0( X, sz10 ) = Y, !
% 4.60/5.01 aNaturalNumber0( sz10 ), ! aNaturalNumber0( X ), aNaturalNumber0( Y ), !
% 4.60/5.01 sz10 = X }.
% 4.60/5.01 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20164) {G1,W12,D3,L4,V2,M4} { ! X = sz10, ! sdtmndt0( X, sz10 ) =
% 4.60/5.01 Y, ! aNaturalNumber0( X ), aNaturalNumber0( Y ) }.
% 4.60/5.01 parent0[3]: (20162) {G1,W12,D3,L4,V2,M4} { ! sdtmndt0( X, sz10 ) = Y, !
% 4.60/5.01 aNaturalNumber0( X ), aNaturalNumber0( Y ), ! sz10 = X }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20165) {G1,W12,D3,L4,V2,M4} { ! Y = sdtmndt0( X, sz10 ), ! X =
% 4.60/5.01 sz10, ! aNaturalNumber0( X ), aNaturalNumber0( Y ) }.
% 4.60/5.01 parent0[1]: (20164) {G1,W12,D3,L4,V2,M4} { ! X = sz10, ! sdtmndt0( X, sz10
% 4.60/5.01 ) = Y, ! aNaturalNumber0( X ), aNaturalNumber0( Y ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 subsumption: (4965) {G6,W12,D3,L4,V2,M4} R(4750,28);r(2) { ! X = sz10, !
% 4.60/5.01 aNaturalNumber0( X ), ! Y = sdtmndt0( X, sz10 ), aNaturalNumber0( Y ) }.
% 4.60/5.01 parent0: (20165) {G1,W12,D3,L4,V2,M4} { ! Y = sdtmndt0( X, sz10 ), ! X =
% 4.60/5.01 sz10, ! aNaturalNumber0( X ), aNaturalNumber0( Y ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01 permutation0:
% 4.60/5.01 0 ==> 2
% 4.60/5.01 1 ==> 0
% 4.60/5.01 2 ==> 1
% 4.60/5.01 3 ==> 3
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20166) {G6,W12,D3,L4,V2,M4} { ! sz10 = X, ! aNaturalNumber0( X )
% 4.60/5.01 , ! Y = sdtmndt0( X, sz10 ), aNaturalNumber0( Y ) }.
% 4.60/5.01 parent0[0]: (4965) {G6,W12,D3,L4,V2,M4} R(4750,28);r(2) { ! X = sz10, !
% 4.60/5.01 aNaturalNumber0( X ), ! Y = sdtmndt0( X, sz10 ), aNaturalNumber0( Y ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqrefl: (20170) {G0,W9,D3,L3,V1,M3} { ! aNaturalNumber0( sz10 ), ! X =
% 4.60/5.01 sdtmndt0( sz10, sz10 ), aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[0]: (20166) {G6,W12,D3,L4,V2,M4} { ! sz10 = X, ! aNaturalNumber0(
% 4.60/5.01 X ), ! Y = sdtmndt0( X, sz10 ), aNaturalNumber0( Y ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := sz10
% 4.60/5.01 Y := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 paramod: (20172) {G1,W9,D2,L4,V1,M4} { ! X = sz00, ! aNaturalNumber0( sz10
% 4.60/5.01 ), ! aNaturalNumber0( sz10 ), aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[1]: (2275) {G2,W7,D3,L2,V1,M2} F(2223);q;r(31) { ! aNaturalNumber0
% 4.60/5.01 ( X ), sdtmndt0( X, X ) ==> sz00 }.
% 4.60/5.01 parent1[1; 3]: (20170) {G0,W9,D3,L3,V1,M3} { ! aNaturalNumber0( sz10 ), !
% 4.60/5.01 X = sdtmndt0( sz10, sz10 ), aNaturalNumber0( X ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := sz10
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 factor: (20173) {G1,W7,D2,L3,V1,M3} { ! X = sz00, ! aNaturalNumber0( sz10
% 4.60/5.01 ), aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[1, 2]: (20172) {G1,W9,D2,L4,V1,M4} { ! X = sz00, ! aNaturalNumber0
% 4.60/5.01 ( sz10 ), ! aNaturalNumber0( sz10 ), aNaturalNumber0( X ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 resolution: (20174) {G1,W5,D2,L2,V1,M2} { ! X = sz00, aNaturalNumber0( X )
% 4.60/5.01 }.
% 4.60/5.01 parent0[1]: (20173) {G1,W7,D2,L3,V1,M3} { ! X = sz00, ! aNaturalNumber0(
% 4.60/5.01 sz10 ), aNaturalNumber0( X ) }.
% 4.60/5.01 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 subsumption: (4975) {G7,W5,D2,L2,V1,M2} Q(4965);d(2275);r(2) {
% 4.60/5.01 aNaturalNumber0( X ), ! X = sz00 }.
% 4.60/5.01 parent0: (20174) {G1,W5,D2,L2,V1,M2} { ! X = sz00, aNaturalNumber0( X )
% 4.60/5.01 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01 permutation0:
% 4.60/5.01 0 ==> 1
% 4.60/5.01 1 ==> 0
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20176) {G7,W5,D2,L2,V1,M2} { ! sz00 = X, aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[1]: (4975) {G7,W5,D2,L2,V1,M2} Q(4965);d(2275);r(2) {
% 4.60/5.01 aNaturalNumber0( X ), ! X = sz00 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20177) {G0,W12,D3,L4,V2,M4} { ! sz00 ==> sdtpldt0( X, Y ), !
% 4.60/5.01 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), Y = sz00 }.
% 4.60/5.01 parent0[2]: (23) {G0,W12,D3,L4,V2,M4} I { ! aNaturalNumber0( X ), !
% 4.60/5.01 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 resolution: (20184) {G1,W13,D3,L4,V2,M4} { ! sz00 ==> sdtpldt0( X, Y ), !
% 4.60/5.01 aNaturalNumber0( Y ), Y = sz00, ! sz00 = X }.
% 4.60/5.01 parent0[1]: (20177) {G0,W12,D3,L4,V2,M4} { ! sz00 ==> sdtpldt0( X, Y ), !
% 4.60/5.01 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), Y = sz00 }.
% 4.60/5.01 parent1[1]: (20176) {G7,W5,D2,L2,V1,M2} { ! sz00 = X, aNaturalNumber0( X )
% 4.60/5.01 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01 substitution1:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20195) {G1,W13,D3,L4,V2,M4} { ! X = sz00, ! sz00 ==> sdtpldt0( X
% 4.60/5.01 , Y ), ! aNaturalNumber0( Y ), Y = sz00 }.
% 4.60/5.01 parent0[3]: (20184) {G1,W13,D3,L4,V2,M4} { ! sz00 ==> sdtpldt0( X, Y ), !
% 4.60/5.01 aNaturalNumber0( Y ), Y = sz00, ! sz00 = X }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20196) {G1,W13,D3,L4,V2,M4} { ! sdtpldt0( X, Y ) ==> sz00, ! X =
% 4.60/5.01 sz00, ! aNaturalNumber0( Y ), Y = sz00 }.
% 4.60/5.01 parent0[1]: (20195) {G1,W13,D3,L4,V2,M4} { ! X = sz00, ! sz00 ==> sdtpldt0
% 4.60/5.01 ( X, Y ), ! aNaturalNumber0( Y ), Y = sz00 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 subsumption: (4988) {G8,W13,D3,L4,V2,M4} R(4975,23) { ! X = sz00, !
% 4.60/5.01 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 4.60/5.01 parent0: (20196) {G1,W13,D3,L4,V2,M4} { ! sdtpldt0( X, Y ) ==> sz00, ! X =
% 4.60/5.01 sz00, ! aNaturalNumber0( Y ), Y = sz00 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01 permutation0:
% 4.60/5.01 0 ==> 2
% 4.60/5.01 1 ==> 0
% 4.60/5.01 2 ==> 1
% 4.60/5.01 3 ==> 3
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20200) {G8,W13,D3,L4,V2,M4} { ! sz00 = X, ! aNaturalNumber0( Y )
% 4.60/5.01 , ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 4.60/5.01 parent0[0]: (4988) {G8,W13,D3,L4,V2,M4} R(4975,23) { ! X = sz00, !
% 4.60/5.01 aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 Y := Y
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqswap: (20208) {G7,W5,D2,L2,V1,M2} { ! sz00 = X, aNaturalNumber0( X ) }.
% 4.60/5.01 parent0[1]: (4975) {G7,W5,D2,L2,V1,M2} Q(4965);d(2275);r(2) {
% 4.60/5.01 aNaturalNumber0( X ), ! X = sz00 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 eqrefl: (20209) {G0,W10,D3,L3,V1,M3} { ! aNaturalNumber0( X ), ! sdtpldt0
% 4.60/5.01 ( sz00, X ) ==> sz00, X = sz00 }.
% 4.60/5.01 parent0[0]: (20200) {G8,W13,D3,L4,V2,M4} { ! sz00 = X, ! aNaturalNumber0(
% 4.60/5.01 Y ), ! sdtpldt0( X, Y ) ==> sz00, Y = sz00 }.
% 4.60/5.01 substitution0:
% 4.60/5.01 X := sz00
% 4.60/5.01 Y := X
% 4.60/5.01 end
% 4.60/5.01
% 4.60/5.01 paramod: (20210) {G1,W10,D2,L4,V1,M4} { ! X ==> sz00, ! aNaturalNumber0( X
% 4.60/5.01 ), ! aNaturalNumber0( X ), X = sz00 }.
% 4.60/5.01 parent0[1]: (9) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtpldt0(
% 4.60/5.01 sz00, X ) ==> X }.
% 4.60/5.01 parent1[1; 2]: (20209) {G0,W10,D3,L3,V1,M3} { ! aNaturalNumber0( X ), !
% 300.03/300.42 Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------