%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM496+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n013.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:54 EDT 2022
% Result : Theorem 236.12s 236.53s
% Output : Refutation 236.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUM496+3 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Tue Jul 5 07:13:29 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.66/1.09 *** allocated 10000 integers for termspace/termends
% 0.66/1.09 *** allocated 10000 integers for clauses
% 0.66/1.09 *** allocated 10000 integers for justifications
% 0.66/1.09 Bliksem 1.12
% 0.66/1.09
% 0.66/1.09
% 0.66/1.09 Automatic Strategy Selection
% 0.66/1.09
% 0.66/1.09
% 0.66/1.09 Clauses:
% 0.66/1.09
% 0.66/1.09 { && }.
% 0.66/1.09 { aNaturalNumber0( sz00 ) }.
% 0.66/1.09 { aNaturalNumber0( sz10 ) }.
% 0.66/1.09 { ! sz10 = sz00 }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0
% 0.66/1.09 ( X, Y ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0
% 0.66/1.09 ( X, Y ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtpldt0( X, Y ) =
% 0.66/1.09 sdtpldt0( Y, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.66/1.09 sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) = X }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sdtpldt0( sz00, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtasdt0( X, Y ) =
% 0.66/1.09 sdtasdt0( Y, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.66/1.09 sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 ) = X }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sdtasdt0( sz10, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 0.66/1.09 { ! aNaturalNumber0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.66/1.09 sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X
% 0.66/1.09 , Z ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.66/1.09 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z
% 0.66/1.09 , X ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.66/1.09 sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.66/1.09 sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.66/1.09 aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ), Y = Z }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.66/1.09 aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ), Y = Z }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.66/1.09 , X = sz00 }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.66/1.09 , Y = sz00 }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sz00
% 0.66/1.09 , X = sz00, Y = sz00 }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.66/1.09 aNaturalNumber0( skol1( Z, T ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.66/1.09 sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.66/1.09 sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.66/1.09 = sdtmndt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.66/1.09 = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.66/1.09 aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.66/1.09 sdtlseqdt0( Y, X ), X = Y }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.66/1.09 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y =
% 0.66/1.09 X }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ),
% 0.66/1.09 sdtlseqdt0( Y, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.66/1.09 ), ! aNaturalNumber0( Z ), alpha5( X, Y, Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.66/1.09 ), ! aNaturalNumber0( Z ), sdtlseqdt0( sdtpldt0( X, Z ), sdtpldt0( Y, Z
% 0.66/1.09 ) ) }.
% 0.66/1.09 { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) = sdtpldt0( Z, Y ) }.
% 0.66/1.09 { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ) }.
% 0.66/1.09 { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) = sdtpldt0( Y, Z ) }.
% 0.66/1.09 { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), ! sdtlseqdt0( sdtpldt0( Z, X ),
% 0.66/1.09 sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) = sdtpldt0( Y, Z ), alpha5( X, Y, Z
% 0.66/1.09 ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 0.66/1.09 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), alpha6( X, Y, Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 0.66/1.09 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), sdtlseqdt0( sdtasdt0( Y, X ),
% 0.66/1.09 sdtasdt0( Z, X ) ) }.
% 0.66/1.09 { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ) }.
% 0.66/1.09 { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 0.66/1.09 { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ) }.
% 0.66/1.09 { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), ! sdtlseqdt0( sdtasdt0( X, Y ),
% 0.66/1.09 sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) = sdtasdt0( Z, X ), alpha6( X, Y, Z
% 0.66/1.09 ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! sz10 = X }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sz00, X = sz10, sdtlseqdt0( sz10, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, sdtlseqdt0( Y,
% 0.66/1.09 sdtasdt0( Y, X ) ) }.
% 0.66/1.09 { && }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.66/1.09 ), iLess0( X, Y ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ),
% 0.66/1.09 aNaturalNumber0( skol2( Z, T ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 0.66/1.09 sdtasdt0( X, skol2( X, Y ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.66/1.09 Y = sdtasdt0( X, Z ), doDivides0( X, Y ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.66/1.09 , Y ), ! Z = sdtsldt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.66/1.09 , Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0( X, Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.66/1.09 , Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), Z = sdtsldt0( Y, X
% 0.66/1.09 ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.66/1.09 doDivides0( X, Y ), ! doDivides0( Y, Z ), doDivides0( X, Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.66/1.09 doDivides0( X, Y ), ! doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z
% 0.66/1.09 ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.66/1.09 doDivides0( X, Y ), ! doDivides0( X, sdtpldt0( Y, Z ) ), doDivides0( X,
% 0.66/1.09 Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 0.66/1.09 sz00, sdtlseqdt0( X, Y ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 0.66/1.09 , Y ), ! aNaturalNumber0( Z ), sdtasdt0( Z, sdtsldt0( Y, X ) ) = sdtsldt0
% 0.66/1.09 ( sdtasdt0( Z, Y ), X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! isPrime0( X ), ! X = sz00 }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! isPrime0( X ), alpha1( X ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sz00, ! alpha1( X ), isPrime0( X ) }.
% 0.66/1.09 { ! alpha1( X ), ! X = sz10 }.
% 0.66/1.09 { ! alpha1( X ), alpha2( X ) }.
% 0.66/1.09 { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 0.66/1.09 { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X, Y ) }.
% 0.66/1.09 { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 0.66/1.09 { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 0.66/1.09 { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 0.66/1.09 { ! Y = sz10, alpha4( X, Y ) }.
% 0.66/1.09 { ! Y = X, alpha4( X, Y ) }.
% 0.66/1.09 { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 0.66/1.09 { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 0.66/1.09 { ! aNaturalNumber0( Y ), ! doDivides0( Y, X ), alpha3( X, Y ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sz00, X = sz10, aNaturalNumber0( skol4( Y ) )
% 0.66/1.09 }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sz00, X = sz10, isPrime0( skol4( Y ) ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), X = sz00, X = sz10, doDivides0( skol4( X ), X ) }
% 0.66/1.09 .
% 0.66/1.09 { aNaturalNumber0( xn ) }.
% 0.66/1.09 { aNaturalNumber0( xm ) }.
% 0.66/1.09 { aNaturalNumber0( xp ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.66/1.09 alpha7( Z ), ! aNaturalNumber0( T ), ! sdtasdt0( X, Y ) = sdtasdt0( Z, T
% 0.66/1.09 ), ! iLess0( sdtpldt0( sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0( xn, xm
% 0.66/1.09 ), xp ) ), alpha9( X, Z ), alpha11( Y, Z ) }.
% 0.66/1.09 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.66/1.09 alpha7( Z ), ! doDivides0( Z, sdtasdt0( X, Y ) ), ! iLess0( sdtpldt0(
% 2.94/3.40 sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0( xn, xm ), xp ) ), alpha9( X, Z
% 2.94/3.40 ), alpha11( Y, Z ) }.
% 2.94/3.40 { ! alpha11( X, Y ), aNaturalNumber0( skol5( Z, T ) ) }.
% 2.94/3.40 { ! alpha11( X, Y ), X = sdtasdt0( Y, skol5( X, Y ) ) }.
% 2.94/3.40 { ! alpha11( X, Y ), doDivides0( Y, X ) }.
% 2.94/3.40 { ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ), ! doDivides0( Y, X ),
% 2.94/3.40 alpha11( X, Y ) }.
% 2.94/3.40 { ! alpha9( X, Y ), aNaturalNumber0( skol6( Z, T ) ) }.
% 2.94/3.40 { ! alpha9( X, Y ), X = sdtasdt0( Y, skol6( X, Y ) ) }.
% 2.94/3.40 { ! alpha9( X, Y ), doDivides0( Y, X ) }.
% 2.94/3.40 { ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ), ! doDivides0( Y, X ),
% 2.94/3.40 alpha9( X, Y ) }.
% 2.94/3.40 { ! alpha7( X ), alpha10( X ) }.
% 2.94/3.40 { ! alpha7( X ), ! isPrime0( X ) }.
% 2.94/3.40 { ! alpha10( X ), isPrime0( X ), alpha7( X ) }.
% 2.94/3.40 { ! alpha10( X ), alpha12( X ), alpha13( X ) }.
% 2.94/3.40 { ! alpha12( X ), alpha10( X ) }.
% 2.94/3.40 { ! alpha13( X ), alpha10( X ) }.
% 2.94/3.40 { ! alpha13( X ), alpha14( X, skol7( X ) ) }.
% 2.94/3.40 { ! alpha13( X ), ! skol7( X ) = X }.
% 2.94/3.40 { ! alpha14( X, Y ), Y = X, alpha13( X ) }.
% 2.94/3.40 { ! alpha14( X, Y ), alpha15( X, Y ) }.
% 2.94/3.40 { ! alpha14( X, Y ), ! Y = sz10 }.
% 2.94/3.40 { ! alpha15( X, Y ), Y = sz10, alpha14( X, Y ) }.
% 2.94/3.40 { ! alpha15( X, Y ), alpha16( X, Y ) }.
% 2.94/3.40 { ! alpha15( X, Y ), doDivides0( Y, X ) }.
% 2.94/3.40 { ! alpha16( X, Y ), ! doDivides0( Y, X ), alpha15( X, Y ) }.
% 2.94/3.40 { ! alpha16( X, Y ), aNaturalNumber0( Y ) }.
% 2.94/3.40 { ! alpha16( X, Y ), aNaturalNumber0( skol8( Z, T ) ) }.
% 2.94/3.40 { ! alpha16( X, Y ), X = sdtasdt0( Y, skol8( X, Y ) ) }.
% 2.94/3.40 { ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y, Z ),
% 2.94/3.40 alpha16( X, Y ) }.
% 2.94/3.40 { ! alpha12( X ), X = sz00, X = sz10 }.
% 2.94/3.40 { ! X = sz00, alpha12( X ) }.
% 2.94/3.40 { ! X = sz10, alpha12( X ) }.
% 2.94/3.40 { ! xp = sz00 }.
% 2.94/3.40 { ! xp = sz10 }.
% 2.94/3.40 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! xp = sdtasdt0( X, Y ),
% 2.94/3.40 X = sz10, X = xp }.
% 2.94/3.40 { ! aNaturalNumber0( X ), ! doDivides0( X, xp ), X = sz10, X = xp }.
% 2.94/3.40 { isPrime0( xp ) }.
% 2.94/3.40 { aNaturalNumber0( skol9 ) }.
% 2.94/3.40 { sdtasdt0( xn, xm ) = sdtasdt0( xp, skol9 ) }.
% 2.94/3.40 { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 2.94/3.40 { aNaturalNumber0( skol10 ) }.
% 2.94/3.40 { sdtpldt0( xp, skol10 ) = xn }.
% 2.94/3.40 { sdtlseqdt0( xp, xn ) }.
% 2.94/3.40 { aNaturalNumber0( xr ) }.
% 2.94/3.40 { sdtpldt0( xp, xr ) = xn }.
% 2.94/3.40 { xr = sdtmndt0( xn, xp ) }.
% 2.94/3.40 { ! xr = xn }.
% 2.94/3.40 { aNaturalNumber0( skol11 ) }.
% 2.94/3.40 { sdtpldt0( xr, skol11 ) = xn }.
% 2.94/3.40 { sdtlseqdt0( xr, xn ) }.
% 2.94/3.40 { aNaturalNumber0( skol12 ) }.
% 2.94/3.40 { sdtasdt0( xr, xm ) = sdtasdt0( xp, skol12 ) }.
% 2.94/3.40 { doDivides0( xp, sdtasdt0( xr, xm ) ) }.
% 2.94/3.40 { alpha8, aNaturalNumber0( skol13 ) }.
% 2.94/3.40 { alpha8, xm = sdtasdt0( xp, skol13 ) }.
% 2.94/3.40 { alpha8, doDivides0( xp, xm ) }.
% 2.94/3.40 { ! alpha8, aNaturalNumber0( skol14 ) }.
% 2.94/3.40 { ! alpha8, xr = sdtasdt0( xp, skol14 ) }.
% 2.94/3.40 { ! alpha8, doDivides0( xp, xr ) }.
% 2.94/3.40 { ! aNaturalNumber0( X ), ! xr = sdtasdt0( xp, X ), ! doDivides0( xp, xr )
% 2.94/3.40 , alpha8 }.
% 2.94/3.40 { ! aNaturalNumber0( X ), ! xn = sdtasdt0( xp, X ) }.
% 2.94/3.40 { ! doDivides0( xp, xn ) }.
% 2.94/3.40 { ! aNaturalNumber0( X ), ! xm = sdtasdt0( xp, X ) }.
% 2.94/3.40 { ! doDivides0( xp, xm ) }.
% 2.94/3.40
% 2.94/3.40 percentage equality = 0.271910, percentage horn = 0.743243
% 2.94/3.40 This is a problem with some equality
% 2.94/3.40
% 2.94/3.40
% 2.94/3.40
% 2.94/3.40 Options Used:
% 2.94/3.40
% 2.94/3.40 useres = 1
% 2.94/3.40 useparamod = 1
% 2.94/3.40 useeqrefl = 1
% 2.94/3.40 useeqfact = 1
% 2.94/3.40 usefactor = 1
% 2.94/3.40 usesimpsplitting = 0
% 2.94/3.40 usesimpdemod = 5
% 2.94/3.40 usesimpres = 3
% 2.94/3.40
% 2.94/3.40 resimpinuse = 1000
% 2.94/3.40 resimpclauses = 20000
% 2.94/3.40 substype = eqrewr
% 2.94/3.40 backwardsubs = 1
% 2.94/3.40 selectoldest = 5
% 2.94/3.40
% 2.94/3.40 litorderings [0] = split
% 2.94/3.40 litorderings [1] = extend the termordering, first sorting on arguments
% 2.94/3.40
% 2.94/3.40 termordering = kbo
% 2.94/3.40
% 2.94/3.40 litapriori = 0
% 2.94/3.40 termapriori = 1
% 2.94/3.40 litaposteriori = 0
% 2.94/3.40 termaposteriori = 0
% 2.94/3.40 demodaposteriori = 0
% 2.94/3.40 ordereqreflfact = 0
% 2.94/3.40
% 2.94/3.40 litselect = negord
% 2.94/3.40
% 2.94/3.40 maxweight = 15
% 2.94/3.40 maxdepth = 30000
% 2.94/3.40 maxlength = 115
% 2.94/3.40 maxnrvars = 195
% 2.94/3.40 excuselevel = 1
% 2.94/3.40 increasemaxweight = 1
% 2.94/3.40
% 2.94/3.40 maxselected = 10000000
% 2.94/3.40 maxnrclauses = 10000000
% 2.94/3.40
% 2.94/3.40 showgenerated = 0
% 2.94/3.40 showkept = 0
% 2.94/3.40 showselected = 0
% 2.94/3.40 showdeleted = 0
% 2.94/3.40 showresimp = 1
% 2.94/3.40 showstatus = 2000
% 2.94/3.40
% 2.94/3.40 prologoutput = 0
% 2.94/3.40 nrgoals = 5000000
% 2.94/3.40 totalproof = 1
% 2.94/3.40
% 2.94/3.40 Symbols occurring in the translation:
% 2.94/3.40
% 2.94/3.40 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.94/3.40 . [1, 2] (w:1, o:40, a:1, s:1, b:0),
% 2.94/3.40 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 44.01/44.41 ! [4, 1] (w:0, o:24, a:1, s:1, b:0),
% 44.01/44.41 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 44.01/44.41 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 44.01/44.41 aNaturalNumber0 [36, 1] (w:1, o:29, a:1, s:1, b:0),
% 44.01/44.41 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 44.01/44.41 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 44.01/44.41 sdtpldt0 [40, 2] (w:1, o:64, a:1, s:1, b:0),
% 44.01/44.41 sdtasdt0 [41, 2] (w:1, o:65, a:1, s:1, b:0),
% 44.01/44.41 sdtlseqdt0 [43, 2] (w:1, o:66, a:1, s:1, b:0),
% 44.01/44.41 sdtmndt0 [44, 2] (w:1, o:67, a:1, s:1, b:0),
% 44.01/44.41 iLess0 [45, 2] (w:1, o:68, a:1, s:1, b:0),
% 44.01/44.41 doDivides0 [46, 2] (w:1, o:69, a:1, s:1, b:0),
% 44.01/44.41 sdtsldt0 [47, 2] (w:1, o:70, a:1, s:1, b:0),
% 44.01/44.41 isPrime0 [48, 1] (w:1, o:30, a:1, s:1, b:0),
% 44.01/44.41 xn [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 44.01/44.41 xm [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 44.01/44.41 xp [51, 0] (w:1, o:13, a:1, s:1, b:0),
% 44.01/44.41 xr [54, 0] (w:1, o:16, a:1, s:1, b:0),
% 44.01/44.41 alpha1 [55, 1] (w:1, o:31, a:1, s:1, b:1),
% 44.01/44.41 alpha2 [56, 1] (w:1, o:35, a:1, s:1, b:1),
% 44.01/44.41 alpha3 [57, 2] (w:1, o:71, a:1, s:1, b:1),
% 44.01/44.41 alpha4 [58, 2] (w:1, o:72, a:1, s:1, b:1),
% 44.01/44.41 alpha5 [59, 3] (w:1, o:83, a:1, s:1, b:1),
% 44.01/44.41 alpha6 [60, 3] (w:1, o:84, a:1, s:1, b:1),
% 44.01/44.41 alpha7 [61, 1] (w:1, o:36, a:1, s:1, b:1),
% 44.01/44.41 alpha8 [62, 0] (w:1, o:17, a:1, s:1, b:1),
% 44.01/44.41 alpha9 [63, 2] (w:1, o:73, a:1, s:1, b:1),
% 44.01/44.41 alpha10 [64, 1] (w:1, o:32, a:1, s:1, b:1),
% 44.01/44.41 alpha11 [65, 2] (w:1, o:74, a:1, s:1, b:1),
% 44.01/44.41 alpha12 [66, 1] (w:1, o:33, a:1, s:1, b:1),
% 44.01/44.41 alpha13 [67, 1] (w:1, o:34, a:1, s:1, b:1),
% 44.01/44.41 alpha14 [68, 2] (w:1, o:75, a:1, s:1, b:1),
% 44.01/44.41 alpha15 [69, 2] (w:1, o:76, a:1, s:1, b:1),
% 44.01/44.41 alpha16 [70, 2] (w:1, o:77, a:1, s:1, b:1),
% 44.01/44.41 skol1 [71, 2] (w:1, o:78, a:1, s:1, b:1),
% 44.01/44.41 skol2 [72, 2] (w:1, o:79, a:1, s:1, b:1),
% 44.01/44.41 skol3 [73, 1] (w:1, o:37, a:1, s:1, b:1),
% 44.01/44.41 skol4 [74, 1] (w:1, o:38, a:1, s:1, b:1),
% 44.01/44.41 skol5 [75, 2] (w:1, o:80, a:1, s:1, b:1),
% 44.01/44.41 skol6 [76, 2] (w:1, o:81, a:1, s:1, b:1),
% 44.01/44.41 skol7 [77, 1] (w:1, o:39, a:1, s:1, b:1),
% 44.01/44.41 skol8 [78, 2] (w:1, o:82, a:1, s:1, b:1),
% 44.01/44.41 skol9 [79, 0] (w:1, o:18, a:1, s:1, b:1),
% 44.01/44.41 skol10 [80, 0] (w:1, o:19, a:1, s:1, b:1),
% 44.01/44.41 skol11 [81, 0] (w:1, o:20, a:1, s:1, b:1),
% 44.01/44.41 skol12 [82, 0] (w:1, o:21, a:1, s:1, b:1),
% 44.01/44.41 skol13 [83, 0] (w:1, o:22, a:1, s:1, b:1),
% 44.01/44.41 skol14 [84, 0] (w:1, o:23, a:1, s:1, b:1).
% 44.01/44.41
% 44.01/44.41
% 44.01/44.41 Starting Search:
% 44.01/44.41
% 44.01/44.41 *** allocated 15000 integers for clauses
% 44.01/44.41 *** allocated 22500 integers for clauses
% 44.01/44.41 *** allocated 33750 integers for clauses
% 44.01/44.41 *** allocated 15000 integers for termspace/termends
% 44.01/44.41 *** allocated 50625 integers for clauses
% 44.01/44.41 *** allocated 75937 integers for clauses
% 44.01/44.41 *** allocated 22500 integers for termspace/termends
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 *** allocated 113905 integers for clauses
% 44.01/44.41 *** allocated 33750 integers for termspace/termends
% 44.01/44.41 *** allocated 50625 integers for termspace/termends
% 44.01/44.41 *** allocated 170857 integers for clauses
% 44.01/44.41
% 44.01/44.41 Intermediate Status:
% 44.01/44.41 Generated: 11604
% 44.01/44.41 Kept: 2012
% 44.01/44.41 Inuse: 128
% 44.01/44.41 Deleted: 7
% 44.01/44.41 Deletedinuse: 4
% 44.01/44.41
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 *** allocated 75937 integers for termspace/termends
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 *** allocated 256285 integers for clauses
% 44.01/44.41 *** allocated 113905 integers for termspace/termends
% 44.01/44.41
% 44.01/44.41 Intermediate Status:
% 44.01/44.41 Generated: 24208
% 44.01/44.41 Kept: 4207
% 44.01/44.41 Inuse: 177
% 44.01/44.41 Deleted: 8
% 44.01/44.41 Deletedinuse: 4
% 44.01/44.41
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 *** allocated 384427 integers for clauses
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 *** allocated 170857 integers for termspace/termends
% 44.01/44.41
% 44.01/44.41 Intermediate Status:
% 44.01/44.41 Generated: 42711
% 44.01/44.41 Kept: 6277
% 44.01/44.41 Inuse: 217
% 44.01/44.41 Deleted: 8
% 44.01/44.41 Deletedinuse: 4
% 44.01/44.41
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 *** allocated 576640 integers for clauses
% 44.01/44.41 *** allocated 256285 integers for termspace/termends
% 44.01/44.41
% 44.01/44.41 Intermediate Status:
% 44.01/44.41 Generated: 54881
% 44.01/44.41 Kept: 8324
% 44.01/44.41 Inuse: 256
% 44.01/44.41 Deleted: 10
% 44.01/44.41 Deletedinuse: 5
% 44.01/44.41
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41
% 44.01/44.41 Intermediate Status:
% 44.01/44.41 Generated: 73882
% 44.01/44.41 Kept: 10434
% 44.01/44.41 Inuse: 291
% 44.01/44.41 Deleted: 11
% 44.01/44.41 Deletedinuse: 6
% 44.01/44.41
% 44.01/44.41 Resimplifying inuse:
% 44.01/44.41 Done
% 44.01/44.41
% 44.01/44.41 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 *** allocated 384427 integers for termspace/termends
% 157.52/157.97 *** allocated 864960 integers for clauses
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 88271
% 157.52/157.97 Kept: 12802
% 157.52/157.97 Inuse: 340
% 157.52/157.97 Deleted: 14
% 157.52/157.97 Deletedinuse: 8
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 109675
% 157.52/157.97 Kept: 14850
% 157.52/157.97 Inuse: 370
% 157.52/157.97 Deleted: 14
% 157.52/157.97 Deletedinuse: 8
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 116389
% 157.52/157.97 Kept: 16854
% 157.52/157.97 Inuse: 430
% 157.52/157.97 Deleted: 17
% 157.52/157.97 Deletedinuse: 11
% 157.52/157.97
% 157.52/157.97 *** allocated 576640 integers for termspace/termends
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 130445
% 157.52/157.97 Kept: 18902
% 157.52/157.97 Inuse: 492
% 157.52/157.97 Deleted: 21
% 157.52/157.97 Deletedinuse: 12
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 *** allocated 1297440 integers for clauses
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying clauses:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 140404
% 157.52/157.97 Kept: 21353
% 157.52/157.97 Inuse: 552
% 157.52/157.97 Deleted: 5169
% 157.52/157.97 Deletedinuse: 13
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 160078
% 157.52/157.97 Kept: 23402
% 157.52/157.97 Inuse: 627
% 157.52/157.97 Deleted: 5206
% 157.52/157.97 Deletedinuse: 50
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 177688
% 157.52/157.97 Kept: 25447
% 157.52/157.97 Inuse: 714
% 157.52/157.97 Deleted: 5211
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 203423
% 157.52/157.97 Kept: 27456
% 157.52/157.97 Inuse: 759
% 157.52/157.97 Deleted: 5212
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 *** allocated 1946160 integers for clauses
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 229310
% 157.52/157.97 Kept: 29470
% 157.52/157.97 Inuse: 839
% 157.52/157.97 Deleted: 5213
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 242073
% 157.52/157.97 Kept: 31578
% 157.52/157.97 Inuse: 878
% 157.52/157.97 Deleted: 5213
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 *** allocated 864960 integers for termspace/termends
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 253460
% 157.52/157.97 Kept: 33620
% 157.52/157.97 Inuse: 901
% 157.52/157.97 Deleted: 5213
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 264287
% 157.52/157.97 Kept: 35637
% 157.52/157.97 Inuse: 919
% 157.52/157.97 Deleted: 5213
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 275110
% 157.52/157.97 Kept: 37683
% 157.52/157.97 Inuse: 937
% 157.52/157.97 Deleted: 5213
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 284904
% 157.52/157.97 Kept: 39738
% 157.52/157.97 Inuse: 953
% 157.52/157.97 Deleted: 5213
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 *** allocated 2919240 integers for clauses
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying clauses:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 296084
% 157.52/157.97 Kept: 42999
% 157.52/157.97 Inuse: 967
% 157.52/157.97 Deleted: 9262
% 157.52/157.97 Deletedinuse: 54
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 303353
% 157.52/157.97 Kept: 46150
% 157.52/157.97 Inuse: 988
% 157.52/157.97 Deleted: 9266
% 157.52/157.97 Deletedinuse: 58
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 307500
% 157.52/157.97 Kept: 48477
% 157.52/157.97 Inuse: 998
% 157.52/157.97 Deleted: 9266
% 157.52/157.97 Deletedinuse: 58
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 312658
% 157.52/157.97 Kept: 50660
% 157.52/157.97 Inuse: 1013
% 157.52/157.97 Deleted: 9266
% 157.52/157.97 Deletedinuse: 58
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 319352
% 157.52/157.97 Kept: 52874
% 157.52/157.97 Inuse: 1038
% 157.52/157.97 Deleted: 9266
% 157.52/157.97 Deletedinuse: 58
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 326747
% 157.52/157.97 Kept: 54877
% 157.52/157.97 Inuse: 1049
% 157.52/157.97 Deleted: 9266
% 157.52/157.97 Deletedinuse: 58
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 334189
% 157.52/157.97 Kept: 56920
% 157.52/157.97 Inuse: 1060
% 157.52/157.97 Deleted: 9266
% 157.52/157.97 Deletedinuse: 58
% 157.52/157.97
% 157.52/157.97 *** allocated 1297440 integers for termspace/termends
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 Resimplifying inuse:
% 157.52/157.97 Done
% 157.52/157.97
% 157.52/157.97 *** allocated 4378860 integers for clauses
% 157.52/157.97
% 157.52/157.97 Intermediate Status:
% 157.52/157.97 Generated: 341673
% 236.12/236.53 Kept: 59000
% 236.12/236.53 Inuse: 1071
% 236.12/236.53 Deleted: 9266
% 236.12/236.53 Deletedinuse: 58
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 350433
% 236.12/236.53 Kept: 61223
% 236.12/236.53 Inuse: 1083
% 236.12/236.53 Deleted: 9266
% 236.12/236.53 Deletedinuse: 58
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying clauses:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 359030
% 236.12/236.53 Kept: 63459
% 236.12/236.53 Inuse: 1094
% 236.12/236.53 Deleted: 10074
% 236.12/236.53 Deletedinuse: 58
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 367616
% 236.12/236.53 Kept: 65557
% 236.12/236.53 Inuse: 1118
% 236.12/236.53 Deleted: 10074
% 236.12/236.53 Deletedinuse: 58
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 375403
% 236.12/236.53 Kept: 67581
% 236.12/236.53 Inuse: 1139
% 236.12/236.53 Deleted: 10074
% 236.12/236.53 Deletedinuse: 58
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 381779
% 236.12/236.53 Kept: 69750
% 236.12/236.53 Inuse: 1151
% 236.12/236.53 Deleted: 10074
% 236.12/236.53 Deletedinuse: 58
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 388021
% 236.12/236.53 Kept: 71777
% 236.12/236.53 Inuse: 1162
% 236.12/236.53 Deleted: 10074
% 236.12/236.53 Deletedinuse: 58
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 393279
% 236.12/236.53 Kept: 73866
% 236.12/236.53 Inuse: 1172
% 236.12/236.53 Deleted: 10087
% 236.12/236.53 Deletedinuse: 71
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 399653
% 236.12/236.53 Kept: 76071
% 236.12/236.53 Inuse: 1183
% 236.12/236.53 Deleted: 10101
% 236.12/236.53 Deletedinuse: 85
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 407033
% 236.12/236.53 Kept: 78134
% 236.12/236.53 Inuse: 1207
% 236.12/236.53 Deleted: 10106
% 236.12/236.53 Deletedinuse: 90
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 415776
% 236.12/236.53 Kept: 80296
% 236.12/236.53 Inuse: 1225
% 236.12/236.53 Deleted: 10106
% 236.12/236.53 Deletedinuse: 90
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 443800
% 236.12/236.53 Kept: 82319
% 236.12/236.53 Inuse: 1308
% 236.12/236.53 Deleted: 10106
% 236.12/236.53 Deletedinuse: 90
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying clauses:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 460261
% 236.12/236.53 Kept: 84406
% 236.12/236.53 Inuse: 1338
% 236.12/236.53 Deleted: 18605
% 236.12/236.53 Deletedinuse: 90
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 489002
% 236.12/236.53 Kept: 86471
% 236.12/236.53 Inuse: 1463
% 236.12/236.53 Deleted: 18610
% 236.12/236.53 Deletedinuse: 95
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 *** allocated 6568290 integers for clauses
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 505756
% 236.12/236.53 Kept: 88597
% 236.12/236.53 Inuse: 1533
% 236.12/236.53 Deleted: 18610
% 236.12/236.53 Deletedinuse: 95
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 515944
% 236.12/236.53 Kept: 90923
% 236.12/236.53 Inuse: 1568
% 236.12/236.53 Deleted: 18610
% 236.12/236.53 Deletedinuse: 95
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 *** allocated 1946160 integers for termspace/termends
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 528473
% 236.12/236.53 Kept: 92961
% 236.12/236.53 Inuse: 1612
% 236.12/236.53 Deleted: 18611
% 236.12/236.53 Deletedinuse: 95
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 551807
% 236.12/236.53 Kept: 95134
% 236.12/236.53 Inuse: 1703
% 236.12/236.53 Deleted: 18667
% 236.12/236.53 Deletedinuse: 147
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 557074
% 236.12/236.53 Kept: 97414
% 236.12/236.53 Inuse: 1712
% 236.12/236.53 Deleted: 18693
% 236.12/236.53 Deletedinuse: 171
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 573454
% 236.12/236.53 Kept: 99583
% 236.12/236.53 Inuse: 1766
% 236.12/236.53 Deleted: 18693
% 236.12/236.53 Deletedinuse: 171
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 610048
% 236.12/236.53 Kept: 101630
% 236.12/236.53 Inuse: 1881
% 236.12/236.53 Deleted: 18713
% 236.12/236.53 Deletedinuse: 171
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 637799
% 236.12/236.53 Kept: 103754
% 236.12/236.53 Inuse: 1980
% 236.12/236.53 Deleted: 18739
% 236.12/236.53 Deletedinuse: 171
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying clauses:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 653323
% 236.12/236.53 Kept: 106188
% 236.12/236.53 Inuse: 2020
% 236.12/236.53 Deleted: 33746
% 236.12/236.53 Deletedinuse: 171
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 665504
% 236.12/236.53 Kept: 108257
% 236.12/236.53 Inuse: 2051
% 236.12/236.53 Deleted: 33797
% 236.12/236.53 Deletedinuse: 222
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 678267
% 236.12/236.53 Kept: 110320
% 236.12/236.53 Inuse: 2099
% 236.12/236.53 Deleted: 33797
% 236.12/236.53 Deletedinuse: 222
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 688875
% 236.12/236.53 Kept: 112398
% 236.12/236.53 Inuse: 2144
% 236.12/236.53 Deleted: 33800
% 236.12/236.53 Deletedinuse: 224
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 711985
% 236.12/236.53 Kept: 114415
% 236.12/236.53 Inuse: 2213
% 236.12/236.53 Deleted: 33804
% 236.12/236.53 Deletedinuse: 228
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 782471
% 236.12/236.53 Kept: 116430
% 236.12/236.53 Inuse: 2375
% 236.12/236.53 Deleted: 33809
% 236.12/236.53 Deletedinuse: 228
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 852630
% 236.12/236.53 Kept: 118466
% 236.12/236.53 Inuse: 2609
% 236.12/236.53 Deleted: 33809
% 236.12/236.53 Deletedinuse: 228
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 864718
% 236.12/236.53 Kept: 120482
% 236.12/236.53 Inuse: 2634
% 236.12/236.53 Deleted: 33809
% 236.12/236.53 Deletedinuse: 228
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 898933
% 236.12/236.53 Kept: 122492
% 236.12/236.53 Inuse: 2660
% 236.12/236.53 Deleted: 33809
% 236.12/236.53 Deletedinuse: 228
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 949796
% 236.12/236.53 Kept: 124615
% 236.12/236.53 Inuse: 2699
% 236.12/236.53 Deleted: 33853
% 236.12/236.53 Deletedinuse: 272
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 *** allocated 9852435 integers for clauses
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53 Resimplifying clauses:
% 236.12/236.53 Done
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Intermediate Status:
% 236.12/236.53 Generated: 987674
% 236.12/236.53 Kept: 128907
% 236.12/236.53 Inuse: 2716
% 236.12/236.53 Deleted: 48627
% 236.12/236.53 Deletedinuse: 511
% 236.12/236.53
% 236.12/236.53 Resimplifying inuse:
% 236.12/236.53
% 236.12/236.53 Bliksems!, er is een bewijs:
% 236.12/236.53 % SZS status Theorem
% 236.12/236.53 % SZS output start Refutation
% 236.12/236.53
% 236.12/236.53 (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 236.12/236.53 (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 236.12/236.53 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 236.12/236.53 (12) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 236.12/236.53 ==> X }.
% 236.12/236.53 (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 236.12/236.53 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 236.12/236.53 }.
% 236.12/236.53 (54) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 236.12/236.53 ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 236.12/236.53 }.
% 236.12/236.53 (59) {G0,W17,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 236.12/236.53 ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X, Z ),
% 236.12/236.53 doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 236.12/236.53 (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 236.12/236.53 (127) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 236.12/236.53 (128) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xp, xr ) ==> xn }.
% 236.12/236.53 (131) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol11 ) }.
% 236.12/236.53 (132) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xr, skol11 ) ==> xn }.
% 236.12/236.53 (139) {G0,W4,D2,L2,V0,M2} I { alpha8, doDivides0( xp, xm ) }.
% 236.12/236.53 (142) {G0,W4,D2,L2,V0,M2} I { ! alpha8, doDivides0( xp, xr ) }.
% 236.12/236.53 (145) {G0,W3,D2,L1,V0,M1} I { ! doDivides0( xp, xn ) }.
% 236.12/236.53 (147) {G0,W3,D2,L1,V0,M1} I { ! doDivides0( xp, xm ) }.
% 236.12/236.53 (514) {G1,W1,D1,L1,V0,M1} S(139);r(147) { alpha8 }.
% 236.12/236.53 (515) {G2,W3,D2,L1,V0,M1} R(514,142) { doDivides0( xp, xr ) }.
% 236.12/236.53 (873) {G1,W14,D3,L4,V2,M4} R(18,83) { ! aNaturalNumber0( X ), !
% 236.12/236.53 aNaturalNumber0( Y ), ! sdtpldt0( X, xp ) = sdtpldt0( X, Y ), xp = Y }.
% 236.12/236.53 (5489) {G1,W7,D3,L2,V0,M2} P(128,6);r(83) { ! aNaturalNumber0( xr ),
% 236.12/236.53 sdtpldt0( xr, xp ) ==> xn }.
% 236.12/236.53 (8410) {G1,W10,D2,L4,V2,M4} R(54,2);d(12) { ! aNaturalNumber0( X ), !
% 236.12/236.53 aNaturalNumber0( Y ), doDivides0( X, Y ), ! Y = X }.
% 236.12/236.53 (8526) {G2,W5,D2,L2,V1,M2} F(8410);q { ! aNaturalNumber0( X ), doDivides0(
% 236.12/236.53 X, X ) }.
% 236.12/236.53 (10128) {G1,W13,D2,L5,V1,M5} P(132,59);r(127) { ! aNaturalNumber0( X ), !
% 236.12/236.53 aNaturalNumber0( skol11 ), ! doDivides0( X, xr ), ! doDivides0( X, skol11
% 236.12/236.53 ), doDivides0( X, xn ) }.
% 236.12/236.53 (10150) {G2,W9,D2,L3,V0,M3} F(10128);r(131) { ! doDivides0( skol11, xr ), !
% 236.12/236.53 doDivides0( skol11, skol11 ), doDivides0( skol11, xn ) }.
% 236.12/236.53 (10303) {G3,W3,D2,L1,V0,M1} R(8526,131) { doDivides0( skol11, skol11 ) }.
% 236.12/236.53 (20579) {G4,W6,D2,L2,V0,M2} S(10150);r(10303) { ! doDivides0( skol11, xr )
% 236.12/236.53 , doDivides0( skol11, xn ) }.
% 236.12/236.53 (20923) {G2,W5,D3,L1,V0,M1} S(5489);r(127) { sdtpldt0( xr, xp ) ==> xn }.
% 236.12/236.53 (125527) {G3,W5,D2,L2,V0,M2} P(132,873);d(20923);q;r(127) { !
% 236.12/236.53 aNaturalNumber0( skol11 ), skol11 ==> xp }.
% 236.12/236.53 (125538) {G4,W3,D2,L1,V0,M1} S(125527);r(131) { skol11 ==> xp }.
% 236.12/236.53 (128841) {G5,W3,D2,L1,V0,M1} S(20579);d(125538);d(125538);r(515) {
% 236.12/236.53 doDivides0( xp, xn ) }.
% 236.12/236.53 (128907) {G6,W0,D0,L0,V0,M0} S(145);r(128841) { }.
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 % SZS output end Refutation
% 236.12/236.53 found a proof!
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Unprocessed initial clauses:
% 236.12/236.53
% 236.12/236.53 (128909) {G0,W1,D1,L1,V0,M1} { && }.
% 236.12/236.53 (128910) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 236.12/236.53 (128911) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 236.12/236.53 (128912) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 236.12/236.53 (128913) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 236.12/236.53 Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 236.12/236.53 (128914) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 236.12/236.53 Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 236.12/236.53 (128915) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 236.12/236.53 (128916) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0
% 236.12/236.53 ( X, sdtpldt0( Y, Z ) ) }.
% 236.12/236.53 (128917) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 )
% 236.12/236.53 = X }.
% 236.12/236.53 (128918) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtpldt0( sz00
% 236.12/236.53 , X ) }.
% 236.12/236.53 (128919) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 236.12/236.53 (128920) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0
% 236.12/236.53 ( X, sdtasdt0( Y, Z ) ) }.
% 236.12/236.53 (128921) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 236.12/236.53 = X }.
% 236.12/236.53 (128922) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtasdt0( sz10
% 236.12/236.53 , X ) }.
% 236.12/236.53 (128923) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 )
% 236.12/236.53 = sz00 }.
% 236.12/236.53 (128924) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sz00 = sdtasdt0(
% 236.12/236.53 sz00, X ) }.
% 236.12/236.53 (128925) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0
% 236.12/236.53 ( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 236.12/236.53 (128926) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0
% 236.12/236.53 ( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 236.12/236.53 (128927) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y =
% 236.12/236.53 Z }.
% 236.12/236.53 (128928) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y =
% 236.12/236.53 Z }.
% 236.12/236.53 (128929) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 236.12/236.53 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 236.12/236.53 sdtasdt0( X, Z ), Y = Z }.
% 236.12/236.53 (128930) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 236.12/236.53 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) =
% 236.12/236.53 sdtasdt0( Z, X ), Y = Z }.
% 236.12/236.53 (128931) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 236.12/236.53 (128932) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 236.12/236.53 (128933) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 236.12/236.53 (128934) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtlseqdt0( X, Y ), aNaturalNumber0( skol1( Z, T ) ) }.
% 236.12/236.53 (128935) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtlseqdt0( X, Y ), sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 236.12/236.53 (128936) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 236.12/236.53 }.
% 236.12/236.53 (128937) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 236.12/236.53 }.
% 236.12/236.53 (128938) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 236.12/236.53 }.
% 236.12/236.53 (128939) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) =
% 236.12/236.53 Y, Z = sdtmndt0( Y, X ) }.
% 236.12/236.53 (128940) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0( X, X )
% 236.12/236.53 }.
% 236.12/236.53 (128941) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 236.12/236.53 (128942) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z )
% 236.12/236.53 , sdtlseqdt0( X, Z ) }.
% 236.12/236.53 (128943) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 236.12/236.53 (128944) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), sdtlseqdt0( X, Y ), sdtlseqdt0( Y, X ) }.
% 236.12/236.53 (128945) {G0,W16,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), alpha5( X, Y
% 236.12/236.53 , Z ) }.
% 236.12/236.53 (128946) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), sdtlseqdt0(
% 236.12/236.53 sdtpldt0( X, Z ), sdtpldt0( Y, Z ) ) }.
% 236.12/236.53 (128947) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( Z, X ) =
% 236.12/236.53 sdtpldt0( Z, Y ) }.
% 236.12/236.53 (128948) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtlseqdt0( sdtpldt0
% 236.12/236.53 ( Z, X ), sdtpldt0( Z, Y ) ) }.
% 236.12/236.53 (128949) {G0,W11,D3,L2,V3,M2} { ! alpha5( X, Y, Z ), ! sdtpldt0( X, Z ) =
% 236.12/236.53 sdtpldt0( Y, Z ) }.
% 236.12/236.53 (128950) {G0,W25,D3,L4,V3,M4} { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), !
% 236.12/236.53 sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) =
% 236.12/236.53 sdtpldt0( Y, Z ), alpha5( X, Y, Z ) }.
% 236.12/236.53 (128951) {G0,W19,D2,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 236.12/236.53 alpha6( X, Y, Z ) }.
% 236.12/236.53 (128952) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 236.12/236.53 sdtlseqdt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 236.12/236.53 (128953) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( X, Y ) =
% 236.12/236.53 sdtasdt0( X, Z ) }.
% 236.12/236.53 (128954) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), sdtlseqdt0( sdtasdt0
% 236.12/236.53 ( X, Y ), sdtasdt0( X, Z ) ) }.
% 236.12/236.53 (128955) {G0,W11,D3,L2,V3,M2} { ! alpha6( X, Y, Z ), ! sdtasdt0( Y, X ) =
% 236.12/236.53 sdtasdt0( Z, X ) }.
% 236.12/236.53 (128956) {G0,W25,D3,L4,V3,M4} { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), !
% 236.12/236.53 sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) =
% 236.12/236.53 sdtasdt0( Z, X ), alpha6( X, Y, Z ) }.
% 236.12/236.53 (128957) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 236.12/236.53 , ! sz10 = X }.
% 236.12/236.53 (128958) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 236.12/236.53 , sdtlseqdt0( sz10, X ) }.
% 236.12/236.53 (128959) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), X = sz00, sdtlseqdt0( Y, sdtasdt0( Y, X ) ) }.
% 236.12/236.53 (128960) {G0,W1,D1,L1,V0,M1} { && }.
% 236.12/236.53 (128961) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), X = Y, ! sdtlseqdt0( X, Y ), iLess0( X, Y ) }.
% 236.12/236.53 (128962) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! doDivides0( X, Y ), aNaturalNumber0( skol2( Z, T ) ) }.
% 236.12/236.53 (128963) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! doDivides0( X, Y ), Y = sdtasdt0( X, skol2( X, Y ) ) }.
% 236.12/236.53 (128964) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 236.12/236.53 }.
% 236.12/236.53 (128965) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 236.12/236.53 aNaturalNumber0( Z ) }.
% 236.12/236.53 (128966) {G0,W20,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ), Y =
% 236.12/236.53 sdtasdt0( X, Z ) }.
% 236.12/236.53 (128967) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), ! Y =
% 236.12/236.53 sdtasdt0( X, Z ), Z = sdtsldt0( Y, X ) }.
% 236.12/236.53 (128968) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( Y, Z )
% 236.12/236.53 , doDivides0( X, Z ) }.
% 236.12/236.53 (128969) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X, Z )
% 236.12/236.53 , doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 236.12/236.53 (128970) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X,
% 236.12/236.53 sdtpldt0( Y, Z ) ), doDivides0( X, Z ) }.
% 236.12/236.53 (128971) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! doDivides0( X, Y ), Y = sz00, sdtlseqdt0( X, Y ) }.
% 236.12/236.53 (128972) {G0,W23,D4,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), sdtasdt0(
% 236.12/236.53 Z, sdtsldt0( Y, X ) ) = sdtsldt0( sdtasdt0( Z, Y ), X ) }.
% 236.12/236.53 (128973) {G0,W7,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ), !
% 236.12/236.53 X = sz00 }.
% 236.12/236.53 (128974) {G0,W6,D2,L3,V1,M3} { ! aNaturalNumber0( X ), ! isPrime0( X ),
% 236.12/236.53 alpha1( X ) }.
% 236.12/236.53 (128975) {G0,W9,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, ! alpha1
% 236.12/236.53 ( X ), isPrime0( X ) }.
% 236.12/236.53 (128976) {G0,W5,D2,L2,V1,M2} { ! alpha1( X ), ! X = sz10 }.
% 236.12/236.53 (128977) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), alpha2( X ) }.
% 236.12/236.53 (128978) {G0,W7,D2,L3,V1,M3} { X = sz10, ! alpha2( X ), alpha1( X ) }.
% 236.12/236.53 (128979) {G0,W8,D2,L3,V2,M3} { ! alpha2( X ), ! alpha3( X, Y ), alpha4( X
% 236.12/236.53 , Y ) }.
% 236.12/236.53 (128980) {G0,W6,D3,L2,V1,M2} { alpha3( X, skol3( X ) ), alpha2( X ) }.
% 236.12/236.53 (128981) {G0,W6,D3,L2,V1,M2} { ! alpha4( X, skol3( X ) ), alpha2( X ) }.
% 236.12/236.53 (128982) {G0,W9,D2,L3,V2,M3} { ! alpha4( X, Y ), Y = sz10, Y = X }.
% 236.12/236.53 (128983) {G0,W6,D2,L2,V2,M2} { ! Y = sz10, alpha4( X, Y ) }.
% 236.12/236.53 (128984) {G0,W6,D2,L2,V2,M2} { ! Y = X, alpha4( X, Y ) }.
% 236.12/236.53 (128985) {G0,W5,D2,L2,V2,M2} { ! alpha3( X, Y ), aNaturalNumber0( Y ) }.
% 236.12/236.53 (128986) {G0,W6,D2,L2,V2,M2} { ! alpha3( X, Y ), doDivides0( Y, X ) }.
% 236.12/236.53 (128987) {G0,W8,D2,L3,V2,M3} { ! aNaturalNumber0( Y ), ! doDivides0( Y, X
% 236.12/236.53 ), alpha3( X, Y ) }.
% 236.12/236.53 (128988) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 236.12/236.53 , aNaturalNumber0( skol4( Y ) ) }.
% 236.12/236.53 (128989) {G0,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 236.12/236.53 , isPrime0( skol4( Y ) ) }.
% 236.12/236.53 (128990) {G0,W12,D3,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 236.12/236.53 , doDivides0( skol4( X ), X ) }.
% 236.12/236.53 (128991) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 236.12/236.53 (128992) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 236.12/236.53 (128993) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 236.12/236.53 (128994) {G0,W34,D4,L9,V4,M9} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), alpha7( Z ), ! aNaturalNumber0( T ), !
% 236.12/236.53 sdtasdt0( X, Y ) = sdtasdt0( Z, T ), ! iLess0( sdtpldt0( sdtpldt0( X, Y )
% 236.12/236.53 , Z ), sdtpldt0( sdtpldt0( xn, xm ), xp ) ), alpha9( X, Z ), alpha11( Y,
% 236.12/236.53 Z ) }.
% 236.12/236.53 (128995) {G0,W30,D4,L8,V3,M8} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! aNaturalNumber0( Z ), alpha7( Z ), ! doDivides0( Z, sdtasdt0( X
% 236.12/236.53 , Y ) ), ! iLess0( sdtpldt0( sdtpldt0( X, Y ), Z ), sdtpldt0( sdtpldt0(
% 236.12/236.53 xn, xm ), xp ) ), alpha9( X, Z ), alpha11( Y, Z ) }.
% 236.12/236.53 (128996) {G0,W7,D3,L2,V4,M2} { ! alpha11( X, Y ), aNaturalNumber0( skol5(
% 236.12/236.53 Z, T ) ) }.
% 236.12/236.53 (128997) {G0,W10,D4,L2,V2,M2} { ! alpha11( X, Y ), X = sdtasdt0( Y, skol5
% 236.12/236.53 ( X, Y ) ) }.
% 236.12/236.53 (128998) {G0,W6,D2,L2,V2,M2} { ! alpha11( X, Y ), doDivides0( Y, X ) }.
% 236.12/236.53 (128999) {G0,W13,D3,L4,V3,M4} { ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y
% 236.12/236.53 , Z ), ! doDivides0( Y, X ), alpha11( X, Y ) }.
% 236.12/236.53 (129000) {G0,W7,D3,L2,V4,M2} { ! alpha9( X, Y ), aNaturalNumber0( skol6( Z
% 236.12/236.53 , T ) ) }.
% 236.12/236.53 (129001) {G0,W10,D4,L2,V2,M2} { ! alpha9( X, Y ), X = sdtasdt0( Y, skol6(
% 236.12/236.53 X, Y ) ) }.
% 236.12/236.53 (129002) {G0,W6,D2,L2,V2,M2} { ! alpha9( X, Y ), doDivides0( Y, X ) }.
% 236.12/236.53 (129003) {G0,W13,D3,L4,V3,M4} { ! aNaturalNumber0( Z ), ! X = sdtasdt0( Y
% 236.12/236.53 , Z ), ! doDivides0( Y, X ), alpha9( X, Y ) }.
% 236.12/236.53 (129004) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), alpha10( X ) }.
% 236.12/236.53 (129005) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), ! isPrime0( X ) }.
% 236.12/236.53 (129006) {G0,W6,D2,L3,V1,M3} { ! alpha10( X ), isPrime0( X ), alpha7( X )
% 236.12/236.53 }.
% 236.12/236.53 (129007) {G0,W6,D2,L3,V1,M3} { ! alpha10( X ), alpha12( X ), alpha13( X )
% 236.12/236.53 }.
% 236.12/236.53 (129008) {G0,W4,D2,L2,V1,M2} { ! alpha12( X ), alpha10( X ) }.
% 236.12/236.53 (129009) {G0,W4,D2,L2,V1,M2} { ! alpha13( X ), alpha10( X ) }.
% 236.12/236.53 (129010) {G0,W6,D3,L2,V1,M2} { ! alpha13( X ), alpha14( X, skol7( X ) )
% 236.12/236.53 }.
% 236.12/236.53 (129011) {G0,W6,D3,L2,V1,M2} { ! alpha13( X ), ! skol7( X ) = X }.
% 236.12/236.53 (129012) {G0,W8,D2,L3,V2,M3} { ! alpha14( X, Y ), Y = X, alpha13( X ) }.
% 236.12/236.53 (129013) {G0,W6,D2,L2,V2,M2} { ! alpha14( X, Y ), alpha15( X, Y ) }.
% 236.12/236.53 (129014) {G0,W6,D2,L2,V2,M2} { ! alpha14( X, Y ), ! Y = sz10 }.
% 236.12/236.53 (129015) {G0,W9,D2,L3,V2,M3} { ! alpha15( X, Y ), Y = sz10, alpha14( X, Y
% 236.12/236.53 ) }.
% 236.12/236.53 (129016) {G0,W6,D2,L2,V2,M2} { ! alpha15( X, Y ), alpha16( X, Y ) }.
% 236.12/236.53 (129017) {G0,W6,D2,L2,V2,M2} { ! alpha15( X, Y ), doDivides0( Y, X ) }.
% 236.12/236.53 (129018) {G0,W9,D2,L3,V2,M3} { ! alpha16( X, Y ), ! doDivides0( Y, X ),
% 236.12/236.53 alpha15( X, Y ) }.
% 236.12/236.53 (129019) {G0,W5,D2,L2,V2,M2} { ! alpha16( X, Y ), aNaturalNumber0( Y ) }.
% 236.12/236.53 (129020) {G0,W7,D3,L2,V4,M2} { ! alpha16( X, Y ), aNaturalNumber0( skol8(
% 236.12/236.53 Z, T ) ) }.
% 236.12/236.53 (129021) {G0,W10,D4,L2,V2,M2} { ! alpha16( X, Y ), X = sdtasdt0( Y, skol8
% 236.12/236.53 ( X, Y ) ) }.
% 236.12/236.53 (129022) {G0,W12,D3,L4,V3,M4} { ! aNaturalNumber0( Y ), ! aNaturalNumber0
% 236.12/236.53 ( Z ), ! X = sdtasdt0( Y, Z ), alpha16( X, Y ) }.
% 236.12/236.53 (129023) {G0,W8,D2,L3,V1,M3} { ! alpha12( X ), X = sz00, X = sz10 }.
% 236.12/236.53 (129024) {G0,W5,D2,L2,V1,M2} { ! X = sz00, alpha12( X ) }.
% 236.12/236.53 (129025) {G0,W5,D2,L2,V1,M2} { ! X = sz10, alpha12( X ) }.
% 236.12/236.53 (129026) {G0,W3,D2,L1,V0,M1} { ! xp = sz00 }.
% 236.12/236.53 (129027) {G0,W3,D2,L1,V0,M1} { ! xp = sz10 }.
% 236.12/236.53 (129028) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 236.12/236.53 ( Y ), ! xp = sdtasdt0( X, Y ), X = sz10, X = xp }.
% 236.12/236.53 (129029) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), ! doDivides0( X,
% 236.12/236.53 xp ), X = sz10, X = xp }.
% 236.12/236.53 (129030) {G0,W2,D2,L1,V0,M1} { isPrime0( xp ) }.
% 236.12/236.53 (129031) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol9 ) }.
% 236.12/236.53 (129032) {G0,W7,D3,L1,V0,M1} { sdtasdt0( xn, xm ) = sdtasdt0( xp, skol9 )
% 236.12/236.53 }.
% 236.12/236.53 (129033) {G0,W5,D3,L1,V0,M1} { doDivides0( xp, sdtasdt0( xn, xm ) ) }.
% 236.12/236.53 (129034) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol10 ) }.
% 236.12/236.53 (129035) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xp, skol10 ) = xn }.
% 236.12/236.53 (129036) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xp, xn ) }.
% 236.12/236.53 (129037) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xr ) }.
% 236.12/236.53 (129038) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xp, xr ) = xn }.
% 236.12/236.53 (129039) {G0,W5,D3,L1,V0,M1} { xr = sdtmndt0( xn, xp ) }.
% 236.12/236.53 (129040) {G0,W3,D2,L1,V0,M1} { ! xr = xn }.
% 236.12/236.53 (129041) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol11 ) }.
% 236.12/236.53 (129042) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xr, skol11 ) = xn }.
% 236.12/236.53 (129043) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xr, xn ) }.
% 236.12/236.53 (129044) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol12 ) }.
% 236.12/236.53 (129045) {G0,W7,D3,L1,V0,M1} { sdtasdt0( xr, xm ) = sdtasdt0( xp, skol12 )
% 236.12/236.53 }.
% 236.12/236.53 (129046) {G0,W5,D3,L1,V0,M1} { doDivides0( xp, sdtasdt0( xr, xm ) ) }.
% 236.12/236.53 (129047) {G0,W3,D2,L2,V0,M2} { alpha8, aNaturalNumber0( skol13 ) }.
% 236.12/236.53 (129048) {G0,W6,D3,L2,V0,M2} { alpha8, xm = sdtasdt0( xp, skol13 ) }.
% 236.12/236.53 (129049) {G0,W4,D2,L2,V0,M2} { alpha8, doDivides0( xp, xm ) }.
% 236.12/236.53 (129050) {G0,W3,D2,L2,V0,M2} { ! alpha8, aNaturalNumber0( skol14 ) }.
% 236.12/236.53 (129051) {G0,W6,D3,L2,V0,M2} { ! alpha8, xr = sdtasdt0( xp, skol14 ) }.
% 236.12/236.53 (129052) {G0,W4,D2,L2,V0,M2} { ! alpha8, doDivides0( xp, xr ) }.
% 236.12/236.53 (129053) {G0,W11,D3,L4,V1,M4} { ! aNaturalNumber0( X ), ! xr = sdtasdt0(
% 236.12/236.53 xp, X ), ! doDivides0( xp, xr ), alpha8 }.
% 236.12/236.53 (129054) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), ! xn = sdtasdt0( xp
% 236.12/236.53 , X ) }.
% 236.12/236.53 (129055) {G0,W3,D2,L1,V0,M1} { ! doDivides0( xp, xn ) }.
% 236.12/236.53 (129056) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), ! xm = sdtasdt0( xp
% 236.12/236.53 , X ) }.
% 236.12/236.53 (129057) {G0,W3,D2,L1,V0,M1} { ! doDivides0( xp, xm ) }.
% 236.12/236.53
% 236.12/236.53
% 236.12/236.53 Total Proof:
% 236.12/236.53
% 236.12/236.53 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 236.12/236.53 parent0: (128911) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 236.12/236.53 substitution0:
% 236.12/236.53 end
% 236.12/236.53 permutation0:
% 236.12/236.53 0 ==> 0
% 236.12/236.53 end
% 236.12/236.53
% 236.12/236.53 subsumption: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 236.12/236.53 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 236.12/236.55 parent0: (128915) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 236.12/236.55 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 X := X
% 236.12/236.55 Y := Y
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 1 ==> 1
% 236.12/236.55 2 ==> 2
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (12) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtasdt0
% 236.12/236.55 ( X, sz10 ) ==> X }.
% 236.12/236.55 parent0: (128921) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0(
% 236.12/236.55 X, sz10 ) = X }.
% 236.12/236.55 substitution0:
% 236.12/236.55 X := X
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 1 ==> 1
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 236.12/236.55 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 236.12/236.55 sdtpldt0( X, Z ), Y = Z }.
% 236.12/236.55 parent0: (128927) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 236.12/236.55 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 236.12/236.55 sdtpldt0( X, Z ), Y = Z }.
% 236.12/236.55 substitution0:
% 236.12/236.55 X := X
% 236.12/236.55 Y := Y
% 236.12/236.55 Z := Z
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 1 ==> 1
% 236.12/236.55 2 ==> 2
% 236.12/236.55 3 ==> 3
% 236.12/236.55 4 ==> 4
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (54) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 236.12/236.55 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ),
% 236.12/236.55 doDivides0( X, Y ) }.
% 236.12/236.55 parent0: (128964) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 236.12/236.55 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ),
% 236.12/236.55 doDivides0( X, Y ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 X := X
% 236.12/236.55 Y := Y
% 236.12/236.55 Z := Z
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 1 ==> 1
% 236.12/236.55 2 ==> 2
% 236.12/236.55 3 ==> 3
% 236.12/236.55 4 ==> 4
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (59) {G0,W17,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), !
% 236.12/236.55 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), !
% 236.12/236.55 doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 236.12/236.55 parent0: (128969) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), !
% 236.12/236.55 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), !
% 236.12/236.55 doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 X := X
% 236.12/236.55 Y := Y
% 236.12/236.55 Z := Z
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 1 ==> 1
% 236.12/236.55 2 ==> 2
% 236.12/236.55 3 ==> 3
% 236.12/236.55 4 ==> 4
% 236.12/236.55 5 ==> 5
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 236.12/236.55 parent0: (128993) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (127) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 236.12/236.55 parent0: (129037) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xr ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (128) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xp, xr ) ==> xn }.
% 236.12/236.55 parent0: (129038) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xp, xr ) = xn }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (131) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol11 ) }.
% 236.12/236.55 parent0: (129041) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol11 ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (132) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xr, skol11 ) ==> xn
% 236.12/236.55 }.
% 236.12/236.55 parent0: (129042) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xr, skol11 ) = xn }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (139) {G0,W4,D2,L2,V0,M2} I { alpha8, doDivides0( xp, xm ) }.
% 236.12/236.55 parent0: (129049) {G0,W4,D2,L2,V0,M2} { alpha8, doDivides0( xp, xm ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 1 ==> 1
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (142) {G0,W4,D2,L2,V0,M2} I { ! alpha8, doDivides0( xp, xr )
% 236.12/236.55 }.
% 236.12/236.55 parent0: (129052) {G0,W4,D2,L2,V0,M2} { ! alpha8, doDivides0( xp, xr ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 1 ==> 1
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (145) {G0,W3,D2,L1,V0,M1} I { ! doDivides0( xp, xn ) }.
% 236.12/236.55 parent0: (129055) {G0,W3,D2,L1,V0,M1} { ! doDivides0( xp, xn ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (147) {G0,W3,D2,L1,V0,M1} I { ! doDivides0( xp, xm ) }.
% 236.12/236.55 parent0: (129057) {G0,W3,D2,L1,V0,M1} { ! doDivides0( xp, xm ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.12/236.55 0 ==> 0
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 resolution: (134196) {G1,W1,D1,L1,V0,M1} { alpha8 }.
% 236.12/236.55 parent0[0]: (147) {G0,W3,D2,L1,V0,M1} I { ! doDivides0( xp, xm ) }.
% 236.12/236.55 parent1[1]: (139) {G0,W4,D2,L2,V0,M2} I { alpha8, doDivides0( xp, xm ) }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 substitution1:
% 236.12/236.55 end
% 236.12/236.55
% 236.12/236.55 subsumption: (514) {G1,W1,D1,L1,V0,M1} S(139);r(147) { alpha8 }.
% 236.12/236.55 parent0: (134196) {G1,W1,D1,L1,V0,M1} { alpha8 }.
% 236.12/236.55 substitution0:
% 236.12/236.55 end
% 236.12/236.55 permutation0:
% 236.16/236.56 0 ==> 0
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 resolution: (134197) {G1,W3,D2,L1,V0,M1} { doDivides0( xp, xr ) }.
% 236.16/236.56 parent0[0]: (142) {G0,W4,D2,L2,V0,M2} I { ! alpha8, doDivides0( xp, xr )
% 236.16/236.56 }.
% 236.16/236.56 parent1[0]: (514) {G1,W1,D1,L1,V0,M1} S(139);r(147) { alpha8 }.
% 236.16/236.56 substitution0:
% 236.16/236.56 end
% 236.16/236.56 substitution1:
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 subsumption: (515) {G2,W3,D2,L1,V0,M1} R(514,142) { doDivides0( xp, xr )
% 236.16/236.56 }.
% 236.16/236.56 parent0: (134197) {G1,W3,D2,L1,V0,M1} { doDivides0( xp, xr ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 end
% 236.16/236.56 permutation0:
% 236.16/236.56 0 ==> 0
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 eqswap: (134198) {G0,W16,D3,L5,V3,M5} { ! sdtpldt0( X, Z ) = sdtpldt0( X,
% 236.16/236.56 Y ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z
% 236.16/236.56 ), Y = Z }.
% 236.16/236.56 parent0[3]: (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 236.16/236.56 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 236.16/236.56 sdtpldt0( X, Z ), Y = Z }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := X
% 236.16/236.56 Y := Y
% 236.16/236.56 Z := Z
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 resolution: (134201) {G1,W14,D3,L4,V2,M4} { ! sdtpldt0( X, xp ) = sdtpldt0
% 236.16/236.56 ( X, Y ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), Y = xp }.
% 236.16/236.56 parent0[3]: (134198) {G0,W16,D3,L5,V3,M5} { ! sdtpldt0( X, Z ) = sdtpldt0
% 236.16/236.56 ( X, Y ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), !
% 236.16/236.56 aNaturalNumber0( Z ), Y = Z }.
% 236.16/236.56 parent1[0]: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := X
% 236.16/236.56 Y := Y
% 236.16/236.56 Z := xp
% 236.16/236.56 end
% 236.16/236.56 substitution1:
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 eqswap: (134203) {G1,W14,D3,L4,V2,M4} { xp = X, ! sdtpldt0( Y, xp ) =
% 236.16/236.56 sdtpldt0( Y, X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( X ) }.
% 236.16/236.56 parent0[3]: (134201) {G1,W14,D3,L4,V2,M4} { ! sdtpldt0( X, xp ) = sdtpldt0
% 236.16/236.56 ( X, Y ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), Y = xp }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := Y
% 236.16/236.56 Y := X
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 subsumption: (873) {G1,W14,D3,L4,V2,M4} R(18,83) { ! aNaturalNumber0( X ),
% 236.16/236.56 ! aNaturalNumber0( Y ), ! sdtpldt0( X, xp ) = sdtpldt0( X, Y ), xp = Y
% 236.16/236.56 }.
% 236.16/236.56 parent0: (134203) {G1,W14,D3,L4,V2,M4} { xp = X, ! sdtpldt0( Y, xp ) =
% 236.16/236.56 sdtpldt0( Y, X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( X ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := Y
% 236.16/236.56 Y := X
% 236.16/236.56 end
% 236.16/236.56 permutation0:
% 236.16/236.56 0 ==> 3
% 236.16/236.56 1 ==> 2
% 236.16/236.56 2 ==> 0
% 236.16/236.56 3 ==> 1
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 eqswap: (134210) {G0,W5,D3,L1,V0,M1} { xn ==> sdtpldt0( xp, xr ) }.
% 236.16/236.56 parent0[0]: (128) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xp, xr ) ==> xn }.
% 236.16/236.56 substitution0:
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 paramod: (134211) {G1,W9,D3,L3,V0,M3} { xn ==> sdtpldt0( xr, xp ), !
% 236.16/236.56 aNaturalNumber0( xp ), ! aNaturalNumber0( xr ) }.
% 236.16/236.56 parent0[2]: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 236.16/236.56 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 236.16/236.56 parent1[0; 2]: (134210) {G0,W5,D3,L1,V0,M1} { xn ==> sdtpldt0( xp, xr )
% 236.16/236.56 }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := xp
% 236.16/236.56 Y := xr
% 236.16/236.56 end
% 236.16/236.56 substitution1:
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 resolution: (134251) {G1,W7,D3,L2,V0,M2} { xn ==> sdtpldt0( xr, xp ), !
% 236.16/236.56 aNaturalNumber0( xr ) }.
% 236.16/236.56 parent0[1]: (134211) {G1,W9,D3,L3,V0,M3} { xn ==> sdtpldt0( xr, xp ), !
% 236.16/236.56 aNaturalNumber0( xp ), ! aNaturalNumber0( xr ) }.
% 236.16/236.56 parent1[0]: (83) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 end
% 236.16/236.56 substitution1:
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 eqswap: (134252) {G1,W7,D3,L2,V0,M2} { sdtpldt0( xr, xp ) ==> xn, !
% 236.16/236.56 aNaturalNumber0( xr ) }.
% 236.16/236.56 parent0[0]: (134251) {G1,W7,D3,L2,V0,M2} { xn ==> sdtpldt0( xr, xp ), !
% 236.16/236.56 aNaturalNumber0( xr ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 subsumption: (5489) {G1,W7,D3,L2,V0,M2} P(128,6);r(83) { ! aNaturalNumber0
% 236.16/236.56 ( xr ), sdtpldt0( xr, xp ) ==> xn }.
% 236.16/236.56 parent0: (134252) {G1,W7,D3,L2,V0,M2} { sdtpldt0( xr, xp ) ==> xn, !
% 236.16/236.56 aNaturalNumber0( xr ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 end
% 236.16/236.56 permutation0:
% 236.16/236.56 0 ==> 1
% 236.16/236.56 1 ==> 0
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 eqswap: (134253) {G0,W14,D3,L5,V3,M5} { ! sdtasdt0( Y, Z ) = X, !
% 236.16/236.56 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Z ),
% 236.16/236.56 doDivides0( Y, X ) }.
% 236.16/236.56 parent0[3]: (54) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 236.16/236.56 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ),
% 236.16/236.56 doDivides0( X, Y ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := Y
% 236.16/236.56 Y := X
% 236.16/236.56 Z := Z
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 resolution: (134257) {G1,W12,D3,L4,V2,M4} { ! sdtasdt0( X, sz10 ) = Y, !
% 236.16/236.56 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), doDivides0( X, Y ) }.
% 236.16/236.56 parent0[3]: (134253) {G0,W14,D3,L5,V3,M5} { ! sdtasdt0( Y, Z ) = X, !
% 236.16/236.56 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Z ),
% 236.16/236.56 doDivides0( Y, X ) }.
% 236.16/236.56 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( sz10 ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := Y
% 236.16/236.56 Y := X
% 236.16/236.56 Z := sz10
% 236.16/236.56 end
% 236.16/236.56 substitution1:
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 paramod: (134263) {G1,W12,D2,L5,V2,M5} { ! X = Y, ! aNaturalNumber0( X ),
% 236.16/236.56 ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), doDivides0( X, Y ) }.
% 236.16/236.56 parent0[1]: (12) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), sdtasdt0(
% 236.16/236.56 X, sz10 ) ==> X }.
% 236.16/236.56 parent1[0; 2]: (134257) {G1,W12,D3,L4,V2,M4} { ! sdtasdt0( X, sz10 ) = Y,
% 236.16/236.56 ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), doDivides0( X, Y ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := X
% 236.16/236.56 end
% 236.16/236.56 substitution1:
% 236.16/236.56 X := X
% 236.16/236.56 Y := Y
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 eqswap: (134264) {G1,W12,D2,L5,V2,M5} { ! Y = X, ! aNaturalNumber0( X ), !
% 236.16/236.56 aNaturalNumber0( X ), ! aNaturalNumber0( Y ), doDivides0( X, Y ) }.
% 236.16/236.56 parent0[0]: (134263) {G1,W12,D2,L5,V2,M5} { ! X = Y, ! aNaturalNumber0( X
% 236.16/236.56 ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), doDivides0( X, Y )
% 236.16/236.56 }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := X
% 236.16/236.56 Y := Y
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 factor: (134265) {G1,W10,D2,L4,V2,M4} { ! X = Y, ! aNaturalNumber0( Y ), !
% 236.16/236.56 aNaturalNumber0( X ), doDivides0( Y, X ) }.
% 236.16/236.56 parent0[1, 2]: (134264) {G1,W12,D2,L5,V2,M5} { ! Y = X, ! aNaturalNumber0
% 236.16/236.56 ( X ), ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), doDivides0( X, Y )
% 236.16/236.56 }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := Y
% 236.16/236.56 Y := X
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 subsumption: (8410) {G1,W10,D2,L4,V2,M4} R(54,2);d(12) { ! aNaturalNumber0
% 236.16/236.56 ( X ), ! aNaturalNumber0( Y ), doDivides0( X, Y ), ! Y = X }.
% 236.16/236.56 parent0: (134265) {G1,W10,D2,L4,V2,M4} { ! X = Y, ! aNaturalNumber0( Y ),
% 236.16/236.56 ! aNaturalNumber0( X ), doDivides0( Y, X ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := Y
% 236.16/236.56 Y := X
% 236.16/236.56 end
% 236.16/236.56 permutation0:
% 236.16/236.56 0 ==> 3
% 236.16/236.56 1 ==> 0
% 236.16/236.56 2 ==> 1
% 236.16/236.56 3 ==> 2
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 eqswap: (134268) {G1,W10,D2,L4,V2,M4} { ! Y = X, ! aNaturalNumber0( Y ), !
% 236.16/236.56 aNaturalNumber0( X ), doDivides0( Y, X ) }.
% 236.16/236.56 parent0[3]: (8410) {G1,W10,D2,L4,V2,M4} R(54,2);d(12) { ! aNaturalNumber0(
% 236.16/236.56 X ), ! aNaturalNumber0( Y ), doDivides0( X, Y ), ! Y = X }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := Y
% 236.16/236.56 Y := X
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 factor: (134269) {G1,W8,D2,L3,V1,M3} { ! X = X, ! aNaturalNumber0( X ),
% 236.16/236.56 doDivides0( X, X ) }.
% 236.16/236.56 parent0[1, 2]: (134268) {G1,W10,D2,L4,V2,M4} { ! Y = X, ! aNaturalNumber0
% 236.16/236.56 ( Y ), ! aNaturalNumber0( X ), doDivides0( Y, X ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := X
% 236.16/236.56 Y := X
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 eqrefl: (134270) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), doDivides0
% 236.16/236.56 ( X, X ) }.
% 236.16/236.56 parent0[0]: (134269) {G1,W8,D2,L3,V1,M3} { ! X = X, ! aNaturalNumber0( X )
% 236.16/236.56 , doDivides0( X, X ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := X
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 subsumption: (8526) {G2,W5,D2,L2,V1,M2} F(8410);q { ! aNaturalNumber0( X )
% 236.16/236.56 , doDivides0( X, X ) }.
% 236.16/236.56 parent0: (134270) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), doDivides0
% 236.16/236.56 ( X, X ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := X
% 236.16/236.56 end
% 236.16/236.56 permutation0:
% 236.16/236.56 0 ==> 0
% 236.16/236.56 1 ==> 1
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 paramod: (134272) {G1,W15,D2,L6,V1,M6} { doDivides0( X, xn ), !
% 236.16/236.56 aNaturalNumber0( X ), ! aNaturalNumber0( xr ), ! aNaturalNumber0( skol11
% 236.16/236.56 ), ! doDivides0( X, xr ), ! doDivides0( X, skol11 ) }.
% 236.16/236.56 parent0[0]: (132) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xr, skol11 ) ==> xn }.
% 236.16/236.56 parent1[5; 2]: (59) {G0,W17,D3,L6,V3,M6} I { ! aNaturalNumber0( X ), !
% 236.16/236.56 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), !
% 236.16/236.56 doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 end
% 236.16/236.56 substitution1:
% 236.16/236.56 X := X
% 236.16/236.56 Y := xr
% 236.16/236.56 Z := skol11
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 resolution: (134277) {G1,W13,D2,L5,V1,M5} { doDivides0( X, xn ), !
% 236.16/236.56 aNaturalNumber0( X ), ! aNaturalNumber0( skol11 ), ! doDivides0( X, xr )
% 236.16/236.56 , ! doDivides0( X, skol11 ) }.
% 236.16/236.56 parent0[2]: (134272) {G1,W15,D2,L6,V1,M6} { doDivides0( X, xn ), !
% 236.16/236.56 aNaturalNumber0( X ), ! aNaturalNumber0( xr ), ! aNaturalNumber0( skol11
% 236.16/236.56 ), ! doDivides0( X, xr ), ! doDivides0( X, skol11 ) }.
% 236.16/236.56 parent1[0]: (127) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 236.16/236.56 substitution0:
% 236.16/236.56 X := X
% 236.16/236.56 end
% 236.16/236.56 substitution1:
% 236.16/236.56 end
% 236.16/236.56
% 236.16/236.56 subsumption: (10128) {G1,W13,D2,L5,V1,M5} P(132,59);r(127) { !
% 236.16/236.56 aNaturalNumber0( X ), ! aNaturalNumber0( skol11 ), ! doDivides0( X, xr )
% 236.16/236.56 , ! doDivides0( X, skol11 ), doDivides0( X, xn ) }.
% 236.16/236.56 parent0: (134277) {G1,W13,D2,L5,V1,M5} { doDivides0( X, xn ), !
% 236.16/236.56 aNaturalNumber0( X ), ! aNaturalNumber0( skol11 ), ! doDivides0( X, xr )
% 236.16/236.56 , ! doDivides0( X, skolCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------