%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : COM021+4 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.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 : Fri Jul 15 00:51:11 EDT 2022
% Result : Theorem 0.70s 1.12s
% Output : Refutation 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : COM021+4 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n017.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % DateTime : Thu Jun 16 16:19:11 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.70/1.11 *** allocated 10000 integers for termspace/termends
% 0.70/1.11 *** allocated 10000 integers for clauses
% 0.70/1.11 *** allocated 10000 integers for justifications
% 0.70/1.11 Bliksem 1.12
% 0.70/1.11
% 0.70/1.11
% 0.70/1.11 Automatic Strategy Selection
% 0.70/1.11
% 0.70/1.11
% 0.70/1.11 Clauses:
% 0.70/1.11
% 0.70/1.11 { && }.
% 0.70/1.11 { && }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aReductOfIn0( Z, X, Y ),
% 0.70/1.11 aElement0( Z ) }.
% 0.70/1.11 { && }.
% 0.70/1.11 { && }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.70/1.11 sdtmndtplgtdt0( X, Y, Z ), aReductOfIn0( Z, X, Y ), alpha1( X, Y, Z ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.70/1.11 aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha1( X
% 0.70/1.11 , Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.70/1.11 { ! alpha1( X, Y, Z ), aElement0( skol1( T, U, W ) ) }.
% 0.70/1.11 { ! alpha1( X, Y, Z ), alpha6( X, Y, Z, skol1( X, Y, Z ) ) }.
% 0.70/1.11 { ! aElement0( T ), ! alpha6( X, Y, Z, T ), alpha1( X, Y, Z ) }.
% 0.70/1.11 { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X, Y ) }.
% 0.70/1.11 { ! alpha6( X, Y, Z, T ), sdtmndtplgtdt0( T, Y, Z ) }.
% 0.70/1.11 { ! aReductOfIn0( T, X, Y ), ! sdtmndtplgtdt0( T, Y, Z ), alpha6( X, Y, Z,
% 0.70/1.11 T ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0
% 0.70/1.11 ( T ), ! sdtmndtplgtdt0( X, Y, Z ), ! sdtmndtplgtdt0( Z, Y, T ),
% 0.70/1.11 sdtmndtplgtdt0( X, Y, T ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.70/1.11 sdtmndtasgtdt0( X, Y, Z ), X = Z, sdtmndtplgtdt0( X, Y, Z ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! X = Z,
% 0.70/1.11 sdtmndtasgtdt0( X, Y, Z ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), !
% 0.70/1.11 sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! aElement0
% 0.70/1.11 ( T ), ! sdtmndtasgtdt0( X, Y, Z ), ! sdtmndtasgtdt0( Z, Y, T ),
% 0.70/1.11 sdtmndtasgtdt0( X, Y, T ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), ! isConfluent0( X ), ! alpha2( X, Y, Z ),
% 0.70/1.11 alpha7( X, Y, Z ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), alpha2( X, skol2( X ), skol30( X ) ),
% 0.70/1.11 isConfluent0( X ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), ! alpha7( X, skol2( X ), skol30( X ) ),
% 0.70/1.11 isConfluent0( X ) }.
% 0.70/1.11 { ! alpha7( X, Y, Z ), aElement0( skol3( T, U, W ) ) }.
% 0.70/1.11 { ! alpha7( X, Y, Z ), alpha12( X, Y, Z, skol3( X, Y, Z ) ) }.
% 0.70/1.11 { ! aElement0( T ), ! alpha12( X, Y, Z, T ), alpha7( X, Y, Z ) }.
% 0.70/1.11 { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Y, X, T ) }.
% 0.70/1.11 { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Z, X, T ) }.
% 0.70/1.11 { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0( Z, X, T ), alpha12( X, Y,
% 0.70/1.11 Z, T ) }.
% 0.70/1.11 { ! alpha2( X, Y, Z ), aElement0( skol4( T, U, W ) ) }.
% 0.70/1.11 { ! alpha2( X, Y, Z ), alpha8( X, Y, Z, skol4( X, Y, Z ) ) }.
% 0.70/1.11 { ! aElement0( T ), ! alpha8( X, Y, Z, T ), alpha2( X, Y, Z ) }.
% 0.70/1.11 { ! alpha8( X, Y, Z, T ), aElement0( Y ) }.
% 0.70/1.11 { ! alpha8( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.70/1.11 { ! aElement0( Y ), ! alpha13( X, Y, Z, T ), alpha8( X, Y, Z, T ) }.
% 0.70/1.11 { ! alpha13( X, Y, Z, T ), aElement0( Z ) }.
% 0.70/1.11 { ! alpha13( X, Y, Z, T ), alpha16( X, Y, Z, T ) }.
% 0.70/1.11 { ! aElement0( Z ), ! alpha16( X, Y, Z, T ), alpha13( X, Y, Z, T ) }.
% 0.70/1.11 { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X, Y ) }.
% 0.70/1.11 { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X, Z ) }.
% 0.70/1.11 { ! sdtmndtasgtdt0( T, X, Y ), ! sdtmndtasgtdt0( T, X, Z ), alpha16( X, Y,
% 0.70/1.11 Z, T ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), ! isLocallyConfluent0( X ), ! alpha3( X, Y, Z )
% 0.70/1.11 , alpha9( X, Y, Z ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), alpha3( X, skol5( X ), skol31( X ) ),
% 0.70/1.11 isLocallyConfluent0( X ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), ! alpha9( X, skol5( X ), skol31( X ) ),
% 0.70/1.11 isLocallyConfluent0( X ) }.
% 0.70/1.11 { ! alpha9( X, Y, Z ), aElement0( skol6( T, U, W ) ) }.
% 0.70/1.11 { ! alpha9( X, Y, Z ), alpha14( X, Y, Z, skol6( X, Y, Z ) ) }.
% 0.70/1.11 { ! aElement0( T ), ! alpha14( X, Y, Z, T ), alpha9( X, Y, Z ) }.
% 0.70/1.11 { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y, X, T ) }.
% 0.70/1.11 { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z, X, T ) }.
% 0.70/1.11 { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0( Z, X, T ), alpha14( X, Y,
% 0.70/1.11 Z, T ) }.
% 0.70/1.11 { ! alpha3( X, Y, Z ), aElement0( skol7( T, U, W ) ) }.
% 0.70/1.11 { ! alpha3( X, Y, Z ), alpha10( X, Y, Z, skol7( X, Y, Z ) ) }.
% 0.70/1.11 { ! aElement0( T ), ! alpha10( X, Y, Z, T ), alpha3( X, Y, Z ) }.
% 0.70/1.11 { ! alpha10( X, Y, Z, T ), aElement0( Y ) }.
% 0.70/1.11 { ! alpha10( X, Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 0.70/1.11 { ! aElement0( Y ), ! alpha15( X, Y, Z, T ), alpha10( X, Y, Z, T ) }.
% 0.70/1.11 { ! alpha15( X, Y, Z, T ), aElement0( Z ) }.
% 0.70/1.11 { ! alpha15( X, Y, Z, T ), alpha17( X, Y, Z, T ) }.
% 0.70/1.11 { ! aElement0( Z ), ! alpha17( X, Y, Z, T ), alpha15( X, Y, Z, T ) }.
% 0.70/1.11 { ! alpha17( X, Y, Z, T ), aReductOfIn0( Y, T, X ) }.
% 0.70/1.11 { ! alpha17( X, Y, Z, T ), aReductOfIn0( Z, T, X ) }.
% 0.70/1.11 { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0( Z, T, X ), alpha17( X, Y, Z, T
% 0.70/1.11 ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), ! isTerminating0( X ), ! alpha4( Y, Z ),
% 0.70/1.11 alpha11( X, Y, Z ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), alpha4( skol8( X ), skol32( X ) ),
% 0.70/1.11 isTerminating0( X ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), ! alpha11( X, skol8( X ), skol32( X ) ),
% 0.70/1.11 isTerminating0( X ) }.
% 0.70/1.11 { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y, X, Z ), iLess0( Z, Y ) }.
% 0.70/1.11 { sdtmndtplgtdt0( Y, X, Z ), alpha11( X, Y, Z ) }.
% 0.70/1.11 { ! iLess0( Z, Y ), alpha11( X, Y, Z ) }.
% 0.70/1.11 { ! alpha4( X, Y ), aElement0( X ) }.
% 0.70/1.11 { ! alpha4( X, Y ), aElement0( Y ) }.
% 0.70/1.11 { ! aElement0( X ), ! aElement0( Y ), alpha4( X, Y ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y )
% 0.70/1.11 , aElement0( Z ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aNormalFormOfIn0( Z, X, Y )
% 0.70/1.11 , alpha5( X, Y, Z ) }.
% 0.70/1.11 { ! aElement0( X ), ! aRewritingSystem0( Y ), ! aElement0( Z ), ! alpha5( X
% 0.70/1.11 , Y, Z ), aNormalFormOfIn0( Z, X, Y ) }.
% 0.70/1.11 { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z ) }.
% 0.70/1.11 { ! alpha5( X, Y, Z ), ! aReductOfIn0( T, Z, Y ) }.
% 0.70/1.11 { ! sdtmndtasgtdt0( X, Y, Z ), aReductOfIn0( skol9( Y, Z ), Z, Y ), alpha5
% 0.70/1.11 ( X, Y, Z ) }.
% 0.70/1.11 { ! aRewritingSystem0( X ), ! isTerminating0( X ), ! aElement0( Y ),
% 0.70/1.11 aNormalFormOfIn0( skol10( X, Y ), Y, X ) }.
% 0.70/1.11 { aRewritingSystem0( xR ) }.
% 0.70/1.11 { ! aElement0( Z ), ! aElement0( X ), ! aElement0( Y ), ! aReductOfIn0( X,
% 0.70/1.11 Z, xR ), ! aReductOfIn0( Y, Z, xR ), Y = skol11( T, Y ), alpha35( Y,
% 0.70/1.11 skol11( T, Y ) ) }.
% 0.70/1.11 { ! aElement0( Z ), ! aElement0( X ), ! aElement0( Y ), ! aReductOfIn0( X,
% 0.70/1.11 Z, xR ), ! aReductOfIn0( Y, Z, xR ), sdtmndtasgtdt0( Y, xR, skol11( T, Y
% 0.70/1.11 ) ) }.
% 0.70/1.11 { ! aElement0( Z ), ! aElement0( X ), ! aElement0( Y ), ! aReductOfIn0( X,
% 0.70/1.11 Z, xR ), ! aReductOfIn0( Y, Z, xR ), alpha26( X, skol11( X, Y ) ) }.
% 0.70/1.11 { isLocallyConfluent0( xR ) }.
% 0.70/1.11 { alpha18 }.
% 0.70/1.11 { isTerminating0( xR ) }.
% 0.70/1.11 { ! alpha35( X, Y ), alpha43( X, Y ) }.
% 0.70/1.11 { ! alpha35( X, Y ), sdtmndtplgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha43( X, Y ), ! sdtmndtplgtdt0( X, xR, Y ), alpha35( X, Y ) }.
% 0.70/1.11 { ! alpha43( X, Y ), aReductOfIn0( Y, X, xR ), alpha52( X, Y ) }.
% 0.70/1.11 { ! aReductOfIn0( Y, X, xR ), alpha43( X, Y ) }.
% 0.70/1.11 { ! alpha52( X, Y ), alpha43( X, Y ) }.
% 0.70/1.11 { ! alpha52( X, Y ), aElement0( skol12( Z, T ) ) }.
% 0.70/1.11 { ! alpha52( X, Y ), sdtmndtplgtdt0( skol12( Z, Y ), xR, Y ) }.
% 0.70/1.11 { ! alpha52( X, Y ), aReductOfIn0( skol12( X, Y ), X, xR ) }.
% 0.70/1.11 { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y
% 0.70/1.11 ), alpha52( X, Y ) }.
% 0.70/1.11 { ! alpha26( X, Y ), alpha36( X, Y ) }.
% 0.70/1.11 { ! alpha26( X, Y ), sdtmndtasgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha36( X, Y ), ! sdtmndtasgtdt0( X, xR, Y ), alpha26( X, Y ) }.
% 0.70/1.11 { ! alpha36( X, Y ), aElement0( Y ) }.
% 0.70/1.11 { ! alpha36( X, Y ), alpha44( X, Y ) }.
% 0.70/1.11 { ! aElement0( Y ), ! alpha44( X, Y ), alpha36( X, Y ) }.
% 0.70/1.11 { ! alpha44( X, Y ), X = Y, alpha53( X, Y ) }.
% 0.70/1.11 { ! X = Y, alpha44( X, Y ) }.
% 0.70/1.11 { ! alpha53( X, Y ), alpha44( X, Y ) }.
% 0.70/1.11 { ! alpha53( X, Y ), alpha59( X, Y ) }.
% 0.70/1.11 { ! alpha53( X, Y ), sdtmndtplgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha59( X, Y ), ! sdtmndtplgtdt0( X, xR, Y ), alpha53( X, Y ) }.
% 0.70/1.11 { ! alpha59( X, Y ), aReductOfIn0( Y, X, xR ), alpha64( X, Y ) }.
% 0.70/1.11 { ! aReductOfIn0( Y, X, xR ), alpha59( X, Y ) }.
% 0.70/1.11 { ! alpha64( X, Y ), alpha59( X, Y ) }.
% 0.70/1.11 { ! alpha64( X, Y ), aElement0( skol13( Z, T ) ) }.
% 0.70/1.11 { ! alpha64( X, Y ), sdtmndtplgtdt0( skol13( Z, Y ), xR, Y ) }.
% 0.70/1.11 { ! alpha64( X, Y ), aReductOfIn0( skol13( X, Y ), X, xR ) }.
% 0.70/1.11 { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y
% 0.70/1.11 ), alpha64( X, Y ) }.
% 0.70/1.11 { ! alpha18, alpha27( X, Y ), iLess0( Y, X ) }.
% 0.70/1.11 { ! alpha27( skol14, skol33 ), alpha18 }.
% 0.70/1.11 { ! iLess0( skol33, skol14 ), alpha18 }.
% 0.70/1.11 { ! alpha27( X, Y ), alpha37( X, Y ), alpha45( X, Y ) }.
% 0.70/1.11 { ! alpha37( X, Y ), alpha27( X, Y ) }.
% 0.70/1.11 { ! alpha45( X, Y ), alpha27( X, Y ) }.
% 0.70/1.11 { ! alpha45( X, Y ), alpha54( X, Y ) }.
% 0.70/1.11 { ! alpha45( X, Y ), ! sdtmndtplgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha54( X, Y ), sdtmndtplgtdt0( X, xR, Y ), alpha45( X, Y ) }.
% 0.70/1.11 { ! alpha54( X, Y ), ! aReductOfIn0( Y, X, xR ) }.
% 0.70/1.11 { ! alpha54( X, Y ), alpha60( X, Y ) }.
% 0.70/1.11 { aReductOfIn0( Y, X, xR ), ! alpha60( X, Y ), alpha54( X, Y ) }.
% 0.70/1.11 { ! alpha60( X, Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, xR ), !
% 0.70/1.11 sdtmndtplgtdt0( Z, xR, Y ) }.
% 0.70/1.11 { aElement0( skol15( Z, T ) ), alpha60( X, Y ) }.
% 0.70/1.11 { sdtmndtplgtdt0( skol15( Z, Y ), xR, Y ), alpha60( X, Y ) }.
% 0.70/1.11 { aReductOfIn0( skol15( X, Y ), X, xR ), alpha60( X, Y ) }.
% 0.70/1.11 { ! alpha37( X, Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 0.70/1.11 { aElement0( X ), alpha37( X, Y ) }.
% 0.70/1.11 { aElement0( Y ), alpha37( X, Y ) }.
% 0.70/1.11 { aElement0( xa ) }.
% 0.70/1.11 { aElement0( xb ) }.
% 0.70/1.11 { aElement0( xc ) }.
% 0.70/1.11 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), alpha19( X, Y ),
% 0.70/1.11 alpha28( X, Z ), ! iLess0( X, xa ), Z = skol16( T, Z ), alpha46( Z,
% 0.70/1.11 skol16( T, Z ) ) }.
% 0.70/1.11 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), alpha19( X, Y ),
% 0.70/1.11 alpha28( X, Z ), ! iLess0( X, xa ), sdtmndtasgtdt0( Z, xR, skol16( T, Z )
% 0.70/1.11 ) }.
% 0.70/1.11 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), alpha19( X, Y ),
% 0.70/1.11 alpha28( X, Z ), ! iLess0( X, xa ), alpha38( Y, skol16( Y, Z ) ) }.
% 0.70/1.11 { ! alpha46( X, Y ), alpha55( X, Y ) }.
% 0.70/1.11 { ! alpha46( X, Y ), sdtmndtplgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha55( X, Y ), ! sdtmndtplgtdt0( X, xR, Y ), alpha46( X, Y ) }.
% 0.70/1.11 { ! alpha55( X, Y ), aReductOfIn0( Y, X, xR ), alpha61( X, Y ) }.
% 0.70/1.11 { ! aReductOfIn0( Y, X, xR ), alpha55( X, Y ) }.
% 0.70/1.11 { ! alpha61( X, Y ), alpha55( X, Y ) }.
% 0.70/1.11 { ! alpha61( X, Y ), aElement0( skol17( Z, T ) ) }.
% 0.70/1.11 { ! alpha61( X, Y ), sdtmndtplgtdt0( skol17( Z, Y ), xR, Y ) }.
% 0.70/1.11 { ! alpha61( X, Y ), aReductOfIn0( skol17( X, Y ), X, xR ) }.
% 0.70/1.11 { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y
% 0.70/1.11 ), alpha61( X, Y ) }.
% 0.70/1.11 { ! alpha38( X, Y ), alpha47( X, Y ) }.
% 0.70/1.11 { ! alpha38( X, Y ), sdtmndtasgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha47( X, Y ), ! sdtmndtasgtdt0( X, xR, Y ), alpha38( X, Y ) }.
% 0.70/1.11 { ! alpha47( X, Y ), aElement0( Y ) }.
% 0.70/1.11 { ! alpha47( X, Y ), alpha56( X, Y ) }.
% 0.70/1.11 { ! aElement0( Y ), ! alpha56( X, Y ), alpha47( X, Y ) }.
% 0.70/1.11 { ! alpha56( X, Y ), X = Y, alpha62( X, Y ) }.
% 0.70/1.11 { ! X = Y, alpha56( X, Y ) }.
% 0.70/1.11 { ! alpha62( X, Y ), alpha56( X, Y ) }.
% 0.70/1.11 { ! alpha62( X, Y ), alpha65( X, Y ) }.
% 0.70/1.11 { ! alpha62( X, Y ), sdtmndtplgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha65( X, Y ), ! sdtmndtplgtdt0( X, xR, Y ), alpha62( X, Y ) }.
% 0.70/1.11 { ! alpha65( X, Y ), aReductOfIn0( Y, X, xR ), alpha66( X, Y ) }.
% 0.70/1.11 { ! aReductOfIn0( Y, X, xR ), alpha65( X, Y ) }.
% 0.70/1.11 { ! alpha66( X, Y ), alpha65( X, Y ) }.
% 0.70/1.11 { ! alpha66( X, Y ), aElement0( skol18( Z, T ) ) }.
% 0.70/1.11 { ! alpha66( X, Y ), sdtmndtplgtdt0( skol18( Z, Y ), xR, Y ) }.
% 0.70/1.11 { ! alpha66( X, Y ), aReductOfIn0( skol18( X, Y ), X, xR ) }.
% 0.70/1.11 { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y
% 0.70/1.11 ), alpha66( X, Y ) }.
% 0.70/1.11 { ! alpha28( X, Y ), alpha39( X, Y ) }.
% 0.70/1.11 { ! alpha28( X, Y ), ! sdtmndtasgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha39( X, Y ), sdtmndtasgtdt0( X, xR, Y ), alpha28( X, Y ) }.
% 0.70/1.11 { ! alpha39( X, Y ), alpha48( X, Y ) }.
% 0.70/1.11 { ! alpha39( X, Y ), ! sdtmndtplgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha48( X, Y ), sdtmndtplgtdt0( X, xR, Y ), alpha39( X, Y ) }.
% 0.70/1.11 { ! alpha48( X, Y ), alpha57( X, Y ) }.
% 0.70/1.11 { ! alpha48( X, Y ), alpha63( X, Y ) }.
% 0.70/1.11 { ! alpha57( X, Y ), ! alpha63( X, Y ), alpha48( X, Y ) }.
% 0.70/1.11 { ! alpha63( X, Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, xR ), !
% 0.70/1.11 sdtmndtplgtdt0( Z, xR, Y ) }.
% 0.70/1.11 { aElement0( skol19( Z, T ) ), alpha63( X, Y ) }.
% 0.70/1.11 { sdtmndtplgtdt0( skol19( Z, Y ), xR, Y ), alpha63( X, Y ) }.
% 0.70/1.11 { aReductOfIn0( skol19( X, Y ), X, xR ), alpha63( X, Y ) }.
% 0.70/1.11 { ! alpha57( X, Y ), ! X = Y }.
% 0.70/1.11 { ! alpha57( X, Y ), ! aReductOfIn0( Y, X, xR ) }.
% 0.70/1.11 { X = Y, aReductOfIn0( Y, X, xR ), alpha57( X, Y ) }.
% 0.70/1.11 { ! alpha19( X, Y ), alpha29( X, Y ) }.
% 0.70/1.11 { ! alpha19( X, Y ), ! sdtmndtasgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha29( X, Y ), sdtmndtasgtdt0( X, xR, Y ), alpha19( X, Y ) }.
% 0.70/1.11 { ! alpha29( X, Y ), alpha40( X, Y ) }.
% 0.70/1.11 { ! alpha29( X, Y ), ! sdtmndtplgtdt0( X, xR, Y ) }.
% 0.70/1.11 { ! alpha40( X, Y ), sdtmndtplgtdt0( X, xR, Y ), alpha29( X, Y ) }.
% 0.70/1.11 { ! alpha40( X, Y ), alpha49( X, Y ) }.
% 0.70/1.11 { ! alpha40( X, Y ), alpha58( X, Y ) }.
% 0.70/1.11 { ! alpha49( X, Y ), ! alpha58( X, Y ), alpha40( X, Y ) }.
% 0.70/1.11 { ! alpha58( X, Y ), ! aElement0( Z ), ! aReductOfIn0( Z, X, xR ), !
% 0.70/1.11 sdtmndtplgtdt0( Z, xR, Y ) }.
% 0.70/1.11 { aElement0( skol20( Z, T ) ), alpha58( X, Y ) }.
% 0.70/1.11 { sdtmndtplgtdt0( skol20( Z, Y ), xR, Y ), alpha58( X, Y ) }.
% 0.70/1.11 { aReductOfIn0( skol20( X, Y ), X, xR ), alpha58( X, Y ) }.
% 0.70/1.11 { ! alpha49( X, Y ), ! X = Y }.
% 0.70/1.11 { ! alpha49( X, Y ), ! aReductOfIn0( Y, X, xR ) }.
% 0.70/1.11 { X = Y, aReductOfIn0( Y, X, xR ), alpha49( X, Y ) }.
% 0.70/1.11 { alpha20 }.
% 0.70/1.11 { sdtmndtplgtdt0( xa, xR, xb ) }.
% 0.70/1.11 { aReductOfIn0( xc, xa, xR ), aElement0( skol21 ) }.
% 0.70/1.11 { aReductOfIn0( xc, xa, xR ), aReductOfIn0( skol21, xa, xR ) }.
% 0.70/1.11 { aReductOfIn0( xc, xa, xR ), sdtmndtplgtdt0( skol21, xR, xc ) }.
% 0.70/1.11 { sdtmndtplgtdt0( xa, xR, xc ) }.
% 0.70/1.11 { ! alpha20, aReductOfIn0( xb, xa, xR ), alpha30 }.
% 0.70/1.11 { ! aReductOfIn0( xb, xa, xR ), alpha20 }.
% 0.70/1.11 { ! alpha30, alpha20 }.
% 0.70/1.11 { ! alpha30, aElement0( skol22 ) }.
% 0.70/1.11 { ! alpha30, aReductOfIn0( skol22, xa, xR ) }.
% 0.70/1.11 { ! alpha30, sdtmndtplgtdt0( skol22, xR, xb ) }.
% 0.70/1.11 { ! aElement0( X ), ! aReductOfIn0( X, xa, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.11 xb ), alpha30 }.
% 0.70/1.11 { aElement0( xu ) }.
% 0.70/1.11 { aReductOfIn0( xu, xa, xR ) }.
% 0.70/1.11 { xu = xb, aReductOfIn0( xb, xu, xR ), alpha21 }.
% 0.70/1.11 { xu = xb, sdtmndtplgtdt0( xu, xR, xb ) }.
% 0.70/1.11 { sdtmndtasgtdt0( xu, xR, xb ) }.
% 0.70/1.11 { ! alpha21, aElement0( skol23 ) }.
% 0.70/1.11 { ! alpha21, aReductOfIn0( skol23, xu, xR ) }.
% 0.70/1.11 { ! alpha21, sdtmndtplgtdt0( skol23, xR, xb ) }.
% 0.70/1.11 { ! aElement0( X ), ! aReductOfIn0( X, xu, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.11 xb ), alpha21 }.
% 0.70/1.11 { aElement0( xv ) }.
% 0.70/1.11 { aReductOfIn0( xv, xa, xR ) }.
% 0.70/1.11 { xv = xc, aReductOfIn0( xc, xv, xR ), alpha22 }.
% 0.70/1.11 { xv = xc, sdtmndtplgtdt0( xv, xR, xc ) }.
% 0.70/1.11 { sdtmndtasgtdt0( xv, xR, xc ) }.
% 0.70/1.11 { ! alpha22, aElement0( skol24 ) }.
% 0.70/1.11 { ! alpha22, aReductOfIn0( skol24, xv, xR ) }.
% 0.70/1.11 { ! alpha22, sdtmndtplgtdt0( skol24, xR, xc ) }.
% 0.70/1.11 { ! aElement0( X ), ! aReductOfIn0( X, xv, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.11 xc ), alpha22 }.
% 0.70/1.11 { aElement0( xw ) }.
% 0.70/1.11 { alpha23 }.
% 0.70/1.11 { sdtmndtasgtdt0( xu, xR, xw ) }.
% 0.70/1.11 { xv = xw, aReductOfIn0( xw, xv, xR ), alpha31 }.
% 0.70/1.11 { xv = xw, sdtmndtplgtdt0( xv, xR, xw ) }.
% 0.70/1.11 { sdtmndtasgtdt0( xv, xR, xw ) }.
% 0.70/1.11 { ! alpha31, aElement0( skol25 ) }.
% 0.70/1.11 { ! alpha31, aReductOfIn0( skol25, xv, xR ) }.
% 0.70/1.11 { ! alpha31, sdtmndtplgtdt0( skol25, xR, xw ) }.
% 0.70/1.11 { ! aElement0( X ), ! aReductOfIn0( X, xv, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.11 xw ), alpha31 }.
% 0.70/1.11 { ! alpha23, xu = xw, alpha32 }.
% 0.70/1.11 { ! xu = xw, alpha23 }.
% 0.70/1.11 { ! alpha32, alpha23 }.
% 0.70/1.11 { ! alpha32, alpha41 }.
% 0.70/1.11 { ! alpha32, sdtmndtplgtdt0( xu, xR, xw ) }.
% 0.70/1.11 { ! alpha41, ! sdtmndtplgtdt0( xu, xR, xw ), alpha32 }.
% 0.70/1.11 { ! alpha41, aReductOfIn0( xw, xu, xR ), alpha50 }.
% 0.70/1.11 { ! aReductOfIn0( xw, xu, xR ), alpha41 }.
% 0.70/1.11 { ! alpha50, alpha41 }.
% 0.70/1.11 { ! alpha50, aElement0( skol26 ) }.
% 0.70/1.11 { ! alpha50, aReductOfIn0( skol26, xu, xR ) }.
% 0.70/1.11 { ! alpha50, sdtmndtplgtdt0( skol26, xR, xw ) }.
% 0.70/1.11 { ! aElement0( X ), ! aReductOfIn0( X, xu, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.11 xw ), alpha50 }.
% 0.70/1.11 { aElement0( xd ) }.
% 0.70/1.11 { xw = xd, aReductOfIn0( xd, xw, xR ), alpha24 }.
% 0.70/1.11 { xw = xd, sdtmndtplgtdt0( xw, xR, xd ) }.
% 0.70/1.11 { sdtmndtasgtdt0( xw, xR, xd ) }.
% 0.70/1.11 { ! aReductOfIn0( X, xd, xR ) }.
% 0.70/1.11 { aNormalFormOfIn0( xd, xw, xR ) }.
% 0.70/1.11 { ! alpha24, aElement0( skol27 ) }.
% 0.70/1.11 { ! alpha24, aReductOfIn0( skol27, xw, xR ) }.
% 0.70/1.11 { ! alpha24, sdtmndtplgtdt0( skol27, xR, xd ) }.
% 0.70/1.11 { ! aElement0( X ), ! aReductOfIn0( X, xw, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.11 xd ), alpha24 }.
% 0.70/1.11 { aElement0( xx ) }.
% 0.70/1.11 { alpha25 }.
% 0.70/1.11 { sdtmndtasgtdt0( xb, xR, xx ) }.
% 0.70/1.11 { xd = xx, aReductOfIn0( xx, xd, xR ), alpha33 }.
% 0.70/1.11 { xd = xx, sdtmndtplgtdt0( xd, xR, xx ) }.
% 0.70/1.11 { sdtmndtasgtdt0( xd, xR, xx ) }.
% 0.70/1.11 { ! alpha33, aElement0( skol28 ) }.
% 0.70/1.11 { ! alpha33, aReductOfIn0( skol28, xd, xR ) }.
% 0.70/1.11 { ! alpha33, sdtmndtplgtdt0( skol28, xR, xx ) }.
% 0.70/1.11 { ! aElement0( X ), ! aReductOfIn0( X, xd, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.11 xx ), alpha33 }.
% 0.70/1.11 { ! alpha25, xb = xx, alpha34 }.
% 0.70/1.11 { ! xb = xx, alpha25 }.
% 0.70/1.11 { ! alpha34, alpha25 }.
% 0.70/1.11 { ! alpha34, alpha42 }.
% 0.70/1.11 { ! alpha34, sdtmndtplgtdt0( xb, xR, xx ) }.
% 0.70/1.11 { ! alpha42, ! sdtmndtplgtdt0( xb, xR, xx ), alpha34 }.
% 0.70/1.11 { ! alpha42, aReductOfIn0( xx, xb, xR ), alpha51 }.
% 0.70/1.11 { ! aReductOfIn0( xx, xb, xR ), alpha42 }.
% 0.70/1.11 { ! alpha51, alpha42 }.
% 0.70/1.12 { ! alpha51, aElement0( skol29 ) }.
% 0.70/1.12 { ! alpha51, aReductOfIn0( skol29, xb, xR ) }.
% 0.70/1.12 { ! alpha51, sdtmndtplgtdt0( skol29, xR, xx ) }.
% 0.70/1.12 { ! aElement0( X ), ! aReductOfIn0( X, xb, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.12 xx ), alpha51 }.
% 0.70/1.12 { ! xb = xd }.
% 0.70/1.12 { ! aReductOfIn0( xd, xb, xR ) }.
% 0.70/1.12 { ! aElement0( X ), ! aReductOfIn0( X, xb, xR ), ! sdtmndtplgtdt0( X, xR,
% 0.70/1.12 xd ) }.
% 0.70/1.12 { ! sdtmndtplgtdt0( xb, xR, xd ) }.
% 0.70/1.12 { ! sdtmndtasgtdt0( xb, xR, xd ) }.
% 0.70/1.12
% 0.70/1.12 *** allocated 15000 integers for clauses
% 0.70/1.12 percentage equality = 0.036127, percentage horn = 0.799283
% 0.70/1.12 This is a problem with some equality
% 0.70/1.12
% 0.70/1.12
% 0.70/1.12
% 0.70/1.12 Options Used:
% 0.70/1.12
% 0.70/1.12 useres = 1
% 0.70/1.12 useparamod = 1
% 0.70/1.12 useeqrefl = 1
% 0.70/1.12 useeqfact = 1
% 0.70/1.12 usefactor = 1
% 0.70/1.12 usesimpsplitting = 0
% 0.70/1.12 usesimpdemod = 5
% 0.70/1.12 usesimpres = 3
% 0.70/1.12
% 0.70/1.12 resimpinuse = 1000
% 0.70/1.12 resimpclauses = 20000
% 0.70/1.12 substype = eqrewr
% 0.70/1.12 backwardsubs = 1
% 0.70/1.12 selectoldest = 5
% 0.70/1.12
% 0.70/1.12 litorderings [0] = split
% 0.70/1.12 litorderings [1] = extend the termordering, first sorting on arguments
% 0.70/1.12
% 0.70/1.12 termordering = kbo
% 0.70/1.12
% 0.70/1.12 litapriori = 0
% 0.70/1.12 termapriori = 1
% 0.70/1.12 litaposteriori = 0
% 0.70/1.12 termaposteriori = 0
% 0.70/1.12 demodaposteriori = 0
% 0.70/1.12 ordereqreflfact = 0
% 0.70/1.12
% 0.70/1.12 litselect = negord
% 0.70/1.12
% 0.70/1.12 maxweight = 15
% 0.70/1.12 maxdepth = 30000
% 0.70/1.12 maxlength = 115
% 0.70/1.12 maxnrvars = 195
% 0.70/1.12 excuselevel = 1
% 0.70/1.12 increasemaxweight = 1
% 0.70/1.12
% 0.70/1.12 maxselected = 10000000
% 0.70/1.12 maxnrclauses = 10000000
% 0.70/1.12
% 0.70/1.12 showgenerated = 0
% 0.70/1.12 showkept = 0
% 0.70/1.12 showselected = 0
% 0.70/1.12 showdeleted = 0
% 0.70/1.12 showresimp = 1
% 0.70/1.12 showstatus = 2000
% 0.70/1.12
% 0.70/1.12 prologoutput = 0
% 0.70/1.12 nrgoals = 5000000
% 0.70/1.12 totalproof = 1
% 0.70/1.12
% 0.70/1.12 Symbols occurring in the translation:
% 0.70/1.12
% 0.70/1.12 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.70/1.12 . [1, 2] (w:1, o:63, a:1, s:1, b:0),
% 0.70/1.12 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 0.70/1.12 ! [4, 1] (w:0, o:47, a:1, s:1, b:0),
% 0.70/1.12 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.12 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.12 aElement0 [36, 1] (w:1, o:52, a:1, s:1, b:0),
% 0.70/1.12 aRewritingSystem0 [37, 1] (w:1, o:53, a:1, s:1, b:0),
% 0.70/1.12 aReductOfIn0 [40, 3] (w:1, o:133, a:1, s:1, b:0),
% 0.70/1.12 iLess0 [41, 2] (w:1, o:87, a:1, s:1, b:0),
% 0.70/1.12 sdtmndtplgtdt0 [42, 3] (w:1, o:134, a:1, s:1, b:0),
% 0.70/1.12 sdtmndtasgtdt0 [44, 3] (w:1, o:135, a:1, s:1, b:0),
% 0.70/1.12 isConfluent0 [45, 1] (w:1, o:54, a:1, s:1, b:0),
% 0.70/1.12 isLocallyConfluent0 [47, 1] (w:1, o:55, a:1, s:1, b:0),
% 0.70/1.12 isTerminating0 [48, 1] (w:1, o:56, a:1, s:1, b:0),
% 0.70/1.12 aNormalFormOfIn0 [49, 3] (w:1, o:136, a:1, s:1, b:0),
% 0.70/1.12 xR [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.70/1.12 xa [51, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.70/1.12 xb [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.70/1.12 xc [53, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.70/1.12 xu [54, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.70/1.12 xv [55, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.70/1.12 xw [56, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.70/1.12 xd [57, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.70/1.12 xx [58, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.70/1.12 alpha1 [59, 3] (w:1, o:137, a:1, s:1, b:1),
% 0.70/1.12 alpha2 [60, 3] (w:1, o:139, a:1, s:1, b:1),
% 0.70/1.12 alpha3 [61, 3] (w:1, o:140, a:1, s:1, b:1),
% 0.70/1.12 alpha4 [62, 2] (w:1, o:93, a:1, s:1, b:1),
% 0.70/1.12 alpha5 [63, 3] (w:1, o:141, a:1, s:1, b:1),
% 0.70/1.12 alpha6 [64, 4] (w:1, o:149, a:1, s:1, b:1),
% 0.70/1.12 alpha7 [65, 3] (w:1, o:142, a:1, s:1, b:1),
% 0.70/1.12 alpha8 [66, 4] (w:1, o:150, a:1, s:1, b:1),
% 0.70/1.12 alpha9 [67, 3] (w:1, o:143, a:1, s:1, b:1),
% 0.70/1.12 alpha10 [68, 4] (w:1, o:151, a:1, s:1, b:1),
% 0.70/1.12 alpha11 [69, 3] (w:1, o:138, a:1, s:1, b:1),
% 0.70/1.12 alpha12 [70, 4] (w:1, o:152, a:1, s:1, b:1),
% 0.70/1.12 alpha13 [71, 4] (w:1, o:153, a:1, s:1, b:1),
% 0.70/1.12 alpha14 [72, 4] (w:1, o:154, a:1, s:1, b:1),
% 0.70/1.12 alpha15 [73, 4] (w:1, o:155, a:1, s:1, b:1),
% 0.70/1.12 alpha16 [74, 4] (w:1, o:156, a:1, s:1, b:1),
% 0.70/1.12 alpha17 [75, 4] (w:1, o:157, a:1, s:1, b:1),
% 0.70/1.12 alpha18 [76, 0] (w:1, o:20, a:1, s:1, b:1),
% 0.70/1.12 alpha19 [77, 2] (w:1, o:94, a:1, s:1, b:1),
% 0.70/1.12 alpha20 [78, 0] (w:1, o:21, a:1, s:1, b:1),
% 0.70/1.12 alpha21 [79, 0] (w:1, o:22, a:1, s:1, b:1),
% 0.70/1.12 alpha22 [80, 0] (w:1, o:23, a:1, s:1, b:1),
% 0.70/1.12 alpha23 [81, 0] (w:1, o:24, a:1, s:1, b:1),
% 0.70/1.12 alpha24 [82, 0] (w:1, o:25, a:1, s:1, b:1),
% 0.70/1.12 alpha25 [83, 0] (w:1, o:26, a:1, s:1, b:1),
% 0.70/1.12 alpha26 [84, 2] (w:1, o:95, a:1, s:1, b:1),
% 0.70/1.12 alpha27 [85, 2] (w:1, o:96, a:1, s:1, b:1),
% 0.70/1.12 alpha28 [86, 2] (w:1, o:97, a:1, s:1, b:1),
% 0.70/1.12 alpha29 [87, 2] (w:1, o:98, a:1, s:1, b:1),
% 0.70/1.12 alpha30 [88, 0] (w:1, o:27, a:1, s:1, b:1),
% 0.70/1.12 alpha31 [89, 0] (w:1, o:28, a:1, s:1, b:1),
% 0.70/1.12 alpha32 [90, 0] (w:1, o:29, a:1, s:1, b:1),
% 0.70/1.12 alpha33 [91, 0] (w:1, o:30, a:1, s:1, b:1),
% 0.70/1.12 alpha34 [92, 0] (w:1, o:31, a:1, s:1, b:1),
% 0.70/1.12 alpha35 [93, 2] (w:1, o:88, a:1, s:1, b:1),
% 0.70/1.12 alpha36 [94, 2] (w:1, o:89, a:1, s:1, b:1),
% 0.70/1.12 alpha37 [95, 2] (w:1, o:90, a:1, s:1, b:1),
% 0.70/1.12 alpha38 [96, 2] (w:1, o:91, a:1, s:1, b:1),
% 0.70/1.12 alpha39 [97, 2] (w:1, o:92, a:1, s:1, b:1),
% 0.70/1.12 alpha40 [98, 2] (w:1, o:99, a:1, s:1, b:1),
% 0.70/1.12 alpha41 [99, 0] (w:1, o:32, a:1, s:1, b:1),
% 0.70/1.12 alpha42 [100, 0] (w:1, o:33, a:1, s:1, b:1),
% 0.70/1.12 alpha43 [101, 2] (w:1, o:100, a:1, s:1, b:1),
% 0.70/1.12 alpha44 [102, 2] (w:1, o:101, a:1, s:1, b:1),
% 0.70/1.12 alpha45 [103, 2] (w:1, o:102, a:1, s:1, b:1),
% 0.70/1.12 alpha46 [104, 2] (w:1, o:103, a:1, s:1, b:1),
% 0.70/1.12 alpha47 [105, 2] (w:1, o:104, a:1, s:1, b:1),
% 0.70/1.12 alpha48 [106, 2] (w:1, o:105, a:1, s:1, b:1),
% 0.70/1.12 alpha49 [107, 2] (w:1, o:106, a:1, s:1, b:1),
% 0.70/1.12 alpha50 [108, 0] (w:1, o:34, a:1, s:1, b:1),
% 0.70/1.12 alpha51 [109, 0] (w:1, o:35, a:1, s:1, b:1),
% 0.70/1.12 alpha52 [110, 2] (w:1, o:107, a:1, s:1, b:1),
% 0.70/1.12 alpha53 [111, 2] (w:1, o:108, a:1, s:1, b:1),
% 0.70/1.12 alpha54 [112, 2] (w:1, o:109, a:1, s:1, b:1),
% 0.70/1.12 alpha55 [113, 2] (w:1, o:110, a:1, s:1, b:1),
% 0.70/1.12 alpha56 [114, 2] (w:1, o:111, a:1, s:1, b:1),
% 0.70/1.12 alpha57 [115, 2] (w:1, o:112, a:1, s:1, b:1),
% 0.70/1.12 alpha58 [116, 2] (w:1, o:113, a:1, s:1, b:1),
% 0.70/1.12 alpha59 [117, 2] (w:1, o:114, a:1, s:1, b:1),
% 0.70/1.12 alpha60 [118, 2] (w:1, o:115, a:1, s:1, b:1),
% 0.70/1.12 alpha61 [119, 2] (w:1, o:116, a:1, s:1, b:1),
% 0.70/1.12 alpha62 [120, 2] (w:1, o:117, a:1, s:1, b:1),
% 0.70/1.12 alpha63 [121, 2] (w:1, o:118, a:1, s:1, b:1),
% 0.70/1.12 alpha64 [122, 2] (w:1, o:119, a:1, s:1, b:1),
% 0.70/1.12 alpha65 [123, 2] (w:1, o:120, a:1, s:1, b:1),
% 0.70/1.12 alpha66 [124, 2] (w:1, o:121, a:1, s:1, b:1),
% 0.70/1.12 skol1 [125, 3] (w:1, o:144, a:1, s:1, b:1),
% 0.70/1.12 skol2 [126, 1] (w:1, o:57, a:1, s:1, b:1),
% 0.70/1.12 skol3 [127, 3] (w:1, o:145, a:1, s:1, b:1),
% 0.70/1.12 skol4 [128, 3] (w:1, o:146, a:1, s:1, b:1),
% 0.70/1.12 skol5 [129, 1] (w:1, o:58, a:1, s:1, b:1),
% 0.70/1.12 skol6 [130, 3] (w:1, o:147, a:1, s:1, b:1),
% 0.70/1.12 skol7 [131, 3] (w:1, o:148, a:1, s:1, b:1),
% 0.70/1.12 skol8 [132, 1] (w:1, o:59, a:1, s:1, b:1),
% 0.70/1.12 skol9 [133, 2] (w:1, o:122, a:1, s:1, b:1),
% 0.70/1.12 skol10 [134, 2] (w:1, o:123, a:1, s:1, b:1),
% 0.70/1.12 skol11 [135, 2] (w:1, o:124, a:1, s:1, b:1),
% 0.70/1.12 skol12 [136, 2] (w:1, o:125, a:1, s:1, b:1),
% 0.70/1.12 skol13 [137, 2] (w:1, o:126, a:1, s:1, b:1),
% 0.70/1.12 skol14 [138, 0] (w:1, o:36, a:1, s:1, b:1),
% 0.70/1.12 skol15 [139, 2] (w:1, o:127, a:1, s:1, b:1),
% 0.70/1.12 skol16 [140, 2] (w:1, o:128, a:1, s:1, b:1),
% 0.70/1.12 skol17 [141, 2] (w:1, o:129, a:1, s:1, b:1),
% 0.70/1.12 skol18 [142, 2] (w:1, o:130, a:1, s:1, b:1),
% 0.70/1.12 skol19 [143, 2] (w:1, o:131, a:1, s:1, b:1),
% 0.70/1.12 skol20 [144, 2] (w:1, o:132, a:1, s:1, b:1),
% 0.70/1.12 skol21 [145, 0] (w:1, o:37, a:1, s:1, b:1),
% 0.70/1.12 skol22 [146, 0] (w:1, o:38, a:1, s:1, b:1),
% 0.70/1.12 skol23 [147, 0] (w:1, o:39, a:1, s:1, b:1),
% 0.70/1.12 skol24 [148, 0] (w:1, o:40, a:1, s:1, b:1),
% 0.70/1.12 skol25 [149, 0] (w:1, o:41, a:1, s:1, b:1),
% 0.70/1.12 skol26 [150, 0] (w:1, o:42, a:1, s:1, b:1),
% 0.70/1.12 skol27 [151, 0] (w:1, o:43, a:1, s:1, b:1),
% 0.70/1.12 skol28 [152, 0] (w:1, o:44, a:1, s:1, b:1),
% 0.70/1.12 skol29 [153, 0] (w:1, o:45, a:1, s:1, b:1),
% 0.70/1.12 skol30 [154, 1] (w:1, o:60, a:1, s:1, b:1),
% 0.70/1.12 skol31 [155, 1] (w:1, o:61, a:1, s:1, b:1),
% 0.70/1.12 skol32 [156, 1] (w:1, o:62, a:1, s:1, b:1),
% 0.70/1.12 skol33 [157, 0] (w:1, o:46, a:1, s:1, b:1).
% 0.70/1.12
% 0.70/1.12
% 0.70/1.12 Starting Search:
% 0.70/1.12
% 0.70/1.12 *** allocated 22500 integers for clauses
% 0.70/1.12 *** allocated 33750 integers for clauses
% 0.70/1.12 *** allocated 15000 integers for termspace/termends
% 0.70/1.12
% 0.70/1.12 Bliksems!, er is een bewijs:
% 0.70/1.12 % SZS status Theorem
% 0.70/1.12 % SZS output start Refutation
% 0.70/1.12
% 0.70/1.12 (248) {G0,W4,D2,L1,V1,M1} I { ! aReductOfIn0( X, xd, xR ) }.
% 0.70/1.12 (256) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xb, xR, xx ) }.
% 0.70/1.12 (257) {G1,W4,D2,L2,V0,M2} I;r(248) { xx ==> xd, alpha33 }.
% 0.70/1.12 (261) {G1,W1,D1,L1,V0,M1} I;r(248) { ! alpha33 }.
% 0.70/1.12 (277) {G0,W4,D2,L1,V0,M1} I { ! sdtmndtasgtdt0( xb, xR, xd ) }.
% 0.70/1.12 (556) {G2,W3,D2,L1,V0,M1} S(257);r(261) { xx ==> xd }.
% 0.70/1.12 (559) {G3,W0,D0,L0,V0,M0} P(556,256);r(277) { }.
% 0.70/1.12
% 0.70/1.12
% 0.70/1.12 % SZS output end Refutation
% 0.70/1.12 found a proof!
% 0.70/1.12
% 0.70/1.12 *** allocated 50625 integers for clauses
% 0.70/1.12
% 0.70/1.12 Unprocessed initial clauses:
% 0.70/1.12
% 0.70/1.12 (561) {G0,W1,D1,L1,V0,M1} { && }.
% 0.70/1.12 (562) {G0,W1,D1,L1,V0,M1} { && }.
% 0.70/1.12 (563) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aReductOfIn0( Z, X, Y ), aElement0( Z ) }.
% 0.70/1.12 (564) {G0,W1,D1,L1,V0,M1} { && }.
% 0.70/1.12 (565) {G0,W1,D1,L1,V0,M1} { && }.
% 0.70/1.12 (566) {G0,W18,D2,L6,V3,M6} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), aReductOfIn0( Z, X, Y ),
% 0.70/1.12 alpha1( X, Y, Z ) }.
% 0.70/1.12 (567) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! aReductOfIn0( Z, X, Y ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.70/1.12 (568) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! alpha1( X, Y, Z ), sdtmndtplgtdt0( X, Y, Z ) }.
% 0.70/1.12 (569) {G0,W9,D3,L2,V6,M2} { ! alpha1( X, Y, Z ), aElement0( skol1( T, U, W
% 0.70/1.12 ) ) }.
% 0.70/1.12 (570) {G0,W12,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), alpha6( X, Y, Z, skol1(
% 0.70/1.12 X, Y, Z ) ) }.
% 0.70/1.12 (571) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha6( X, Y, Z, T ),
% 0.70/1.12 alpha1( X, Y, Z ) }.
% 0.70/1.12 (572) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), aReductOfIn0( T, X, Y
% 0.70/1.12 ) }.
% 0.70/1.12 (573) {G0,W9,D2,L2,V4,M2} { ! alpha6( X, Y, Z, T ), sdtmndtplgtdt0( T, Y,
% 0.70/1.12 Z ) }.
% 0.70/1.12 (574) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( T, X, Y ), ! sdtmndtplgtdt0(
% 0.70/1.12 T, Y, Z ), alpha6( X, Y, Z, T ) }.
% 0.70/1.12 (575) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! aElement0( T ), ! sdtmndtplgtdt0( X, Y, Z ), !
% 0.70/1.12 sdtmndtplgtdt0( Z, Y, T ), sdtmndtplgtdt0( X, Y, T ) }.
% 0.70/1.12 (576) {G0,W17,D2,L6,V3,M6} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! sdtmndtasgtdt0( X, Y, Z ), X = Z, sdtmndtplgtdt0( X, Y
% 0.70/1.12 , Z ) }.
% 0.70/1.12 (577) {G0,W13,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! X = Z, sdtmndtasgtdt0( X, Y, Z ) }.
% 0.70/1.12 (578) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! sdtmndtplgtdt0( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z )
% 0.70/1.12 }.
% 0.70/1.12 (579) {G0,W20,D2,L7,V4,M7} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! aElement0( T ), ! sdtmndtasgtdt0( X, Y, Z ), !
% 0.70/1.12 sdtmndtasgtdt0( Z, Y, T ), sdtmndtasgtdt0( X, Y, T ) }.
% 0.70/1.12 (580) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), ! isConfluent0( X )
% 0.70/1.12 , ! alpha2( X, Y, Z ), alpha7( X, Y, Z ) }.
% 0.70/1.12 (581) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha2( X, skol2( X
% 0.70/1.12 ), skol30( X ) ), isConfluent0( X ) }.
% 0.70/1.12 (582) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha7( X, skol2
% 0.70/1.12 ( X ), skol30( X ) ), isConfluent0( X ) }.
% 0.70/1.12 (583) {G0,W9,D3,L2,V6,M2} { ! alpha7( X, Y, Z ), aElement0( skol3( T, U, W
% 0.70/1.12 ) ) }.
% 0.70/1.12 (584) {G0,W12,D3,L2,V3,M2} { ! alpha7( X, Y, Z ), alpha12( X, Y, Z, skol3
% 0.70/1.12 ( X, Y, Z ) ) }.
% 0.70/1.12 (585) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha12( X, Y, Z, T ),
% 0.70/1.12 alpha7( X, Y, Z ) }.
% 0.70/1.12 (586) {G0,W9,D2,L2,V4,M2} { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Y, X
% 0.70/1.12 , T ) }.
% 0.70/1.12 (587) {G0,W9,D2,L2,V4,M2} { ! alpha12( X, Y, Z, T ), sdtmndtasgtdt0( Z, X
% 0.70/1.12 , T ) }.
% 0.70/1.12 (588) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0
% 0.70/1.12 ( Z, X, T ), alpha12( X, Y, Z, T ) }.
% 0.70/1.12 (589) {G0,W9,D3,L2,V6,M2} { ! alpha2( X, Y, Z ), aElement0( skol4( T, U, W
% 0.70/1.12 ) ) }.
% 0.70/1.12 (590) {G0,W12,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), alpha8( X, Y, Z, skol4(
% 0.70/1.12 X, Y, Z ) ) }.
% 0.70/1.12 (591) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha8( X, Y, Z, T ),
% 0.70/1.12 alpha2( X, Y, Z ) }.
% 0.70/1.12 (592) {G0,W7,D2,L2,V4,M2} { ! alpha8( X, Y, Z, T ), aElement0( Y ) }.
% 0.70/1.12 (593) {G0,W10,D2,L2,V4,M2} { ! alpha8( X, Y, Z, T ), alpha13( X, Y, Z, T )
% 0.70/1.12 }.
% 0.70/1.12 (594) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha13( X, Y, Z, T ),
% 0.70/1.12 alpha8( X, Y, Z, T ) }.
% 0.70/1.12 (595) {G0,W7,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), aElement0( Z ) }.
% 0.70/1.12 (596) {G0,W10,D2,L2,V4,M2} { ! alpha13( X, Y, Z, T ), alpha16( X, Y, Z, T
% 0.70/1.12 ) }.
% 0.70/1.12 (597) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha16( X, Y, Z, T ),
% 0.70/1.12 alpha13( X, Y, Z, T ) }.
% 0.70/1.12 (598) {G0,W9,D2,L2,V4,M2} { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X
% 0.70/1.12 , Y ) }.
% 0.70/1.12 (599) {G0,W9,D2,L2,V4,M2} { ! alpha16( X, Y, Z, T ), sdtmndtasgtdt0( T, X
% 0.70/1.12 , Z ) }.
% 0.70/1.12 (600) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( T, X, Y ), ! sdtmndtasgtdt0
% 0.70/1.12 ( T, X, Z ), alpha16( X, Y, Z, T ) }.
% 0.70/1.12 (601) {G0,W12,D2,L4,V3,M4} { ! aRewritingSystem0( X ), !
% 0.70/1.12 isLocallyConfluent0( X ), ! alpha3( X, Y, Z ), alpha9( X, Y, Z ) }.
% 0.70/1.12 (602) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha3( X, skol5( X
% 0.70/1.12 ), skol31( X ) ), isLocallyConfluent0( X ) }.
% 0.70/1.12 (603) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha9( X, skol5
% 0.70/1.12 ( X ), skol31( X ) ), isLocallyConfluent0( X ) }.
% 0.70/1.12 (604) {G0,W9,D3,L2,V6,M2} { ! alpha9( X, Y, Z ), aElement0( skol6( T, U, W
% 0.70/1.12 ) ) }.
% 0.70/1.12 (605) {G0,W12,D3,L2,V3,M2} { ! alpha9( X, Y, Z ), alpha14( X, Y, Z, skol6
% 0.70/1.12 ( X, Y, Z ) ) }.
% 0.70/1.12 (606) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha14( X, Y, Z, T ),
% 0.70/1.12 alpha9( X, Y, Z ) }.
% 0.70/1.12 (607) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Y, X
% 0.70/1.12 , T ) }.
% 0.70/1.12 (608) {G0,W9,D2,L2,V4,M2} { ! alpha14( X, Y, Z, T ), sdtmndtasgtdt0( Z, X
% 0.70/1.12 , T ) }.
% 0.70/1.12 (609) {G0,W13,D2,L3,V4,M3} { ! sdtmndtasgtdt0( Y, X, T ), ! sdtmndtasgtdt0
% 0.70/1.12 ( Z, X, T ), alpha14( X, Y, Z, T ) }.
% 0.70/1.12 (610) {G0,W9,D3,L2,V6,M2} { ! alpha3( X, Y, Z ), aElement0( skol7( T, U, W
% 0.70/1.12 ) ) }.
% 0.70/1.12 (611) {G0,W12,D3,L2,V3,M2} { ! alpha3( X, Y, Z ), alpha10( X, Y, Z, skol7
% 0.70/1.12 ( X, Y, Z ) ) }.
% 0.70/1.12 (612) {G0,W11,D2,L3,V4,M3} { ! aElement0( T ), ! alpha10( X, Y, Z, T ),
% 0.70/1.12 alpha3( X, Y, Z ) }.
% 0.70/1.12 (613) {G0,W7,D2,L2,V4,M2} { ! alpha10( X, Y, Z, T ), aElement0( Y ) }.
% 0.70/1.12 (614) {G0,W10,D2,L2,V4,M2} { ! alpha10( X, Y, Z, T ), alpha15( X, Y, Z, T
% 0.70/1.12 ) }.
% 0.70/1.12 (615) {G0,W12,D2,L3,V4,M3} { ! aElement0( Y ), ! alpha15( X, Y, Z, T ),
% 0.70/1.12 alpha10( X, Y, Z, T ) }.
% 0.70/1.12 (616) {G0,W7,D2,L2,V4,M2} { ! alpha15( X, Y, Z, T ), aElement0( Z ) }.
% 0.70/1.12 (617) {G0,W10,D2,L2,V4,M2} { ! alpha15( X, Y, Z, T ), alpha17( X, Y, Z, T
% 0.70/1.12 ) }.
% 0.70/1.12 (618) {G0,W12,D2,L3,V4,M3} { ! aElement0( Z ), ! alpha17( X, Y, Z, T ),
% 0.70/1.12 alpha15( X, Y, Z, T ) }.
% 0.70/1.12 (619) {G0,W9,D2,L2,V4,M2} { ! alpha17( X, Y, Z, T ), aReductOfIn0( Y, T, X
% 0.70/1.12 ) }.
% 0.70/1.12 (620) {G0,W9,D2,L2,V4,M2} { ! alpha17( X, Y, Z, T ), aReductOfIn0( Z, T, X
% 0.70/1.12 ) }.
% 0.70/1.12 (621) {G0,W13,D2,L3,V4,M3} { ! aReductOfIn0( Y, T, X ), ! aReductOfIn0( Z
% 0.70/1.12 , T, X ), alpha17( X, Y, Z, T ) }.
% 0.70/1.12 (622) {G0,W11,D2,L4,V3,M4} { ! aRewritingSystem0( X ), ! isTerminating0( X
% 0.70/1.12 ), ! alpha4( Y, Z ), alpha11( X, Y, Z ) }.
% 0.70/1.12 (623) {G0,W9,D3,L3,V1,M3} { ! aRewritingSystem0( X ), alpha4( skol8( X ),
% 0.70/1.12 skol32( X ) ), isTerminating0( X ) }.
% 0.70/1.12 (624) {G0,W10,D3,L3,V1,M3} { ! aRewritingSystem0( X ), ! alpha11( X, skol8
% 0.70/1.12 ( X ), skol32( X ) ), isTerminating0( X ) }.
% 0.70/1.12 (625) {G0,W11,D2,L3,V3,M3} { ! alpha11( X, Y, Z ), ! sdtmndtplgtdt0( Y, X
% 0.70/1.12 , Z ), iLess0( Z, Y ) }.
% 0.70/1.12 (626) {G0,W8,D2,L2,V3,M2} { sdtmndtplgtdt0( Y, X, Z ), alpha11( X, Y, Z )
% 0.70/1.12 }.
% 0.70/1.12 (627) {G0,W7,D2,L2,V3,M2} { ! iLess0( Z, Y ), alpha11( X, Y, Z ) }.
% 0.70/1.12 (628) {G0,W5,D2,L2,V2,M2} { ! alpha4( X, Y ), aElement0( X ) }.
% 0.70/1.12 (629) {G0,W5,D2,L2,V2,M2} { ! alpha4( X, Y ), aElement0( Y ) }.
% 0.70/1.12 (630) {G0,W7,D2,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y ), alpha4( X
% 0.70/1.12 , Y ) }.
% 0.70/1.12 (631) {G0,W10,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aNormalFormOfIn0( Z, X, Y ), aElement0( Z ) }.
% 0.70/1.12 (632) {G0,W12,D2,L4,V3,M4} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aNormalFormOfIn0( Z, X, Y ), alpha5( X, Y, Z ) }.
% 0.70/1.12 (633) {G0,W14,D2,L5,V3,M5} { ! aElement0( X ), ! aRewritingSystem0( Y ), !
% 0.70/1.12 aElement0( Z ), ! alpha5( X, Y, Z ), aNormalFormOfIn0( Z, X, Y ) }.
% 0.70/1.12 (634) {G0,W8,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), sdtmndtasgtdt0( X, Y, Z )
% 0.70/1.12 }.
% 0.70/1.12 (635) {G0,W8,D2,L2,V4,M2} { ! alpha5( X, Y, Z ), ! aReductOfIn0( T, Z, Y )
% 0.70/1.12 }.
% 0.70/1.12 (636) {G0,W14,D3,L3,V3,M3} { ! sdtmndtasgtdt0( X, Y, Z ), aReductOfIn0(
% 0.70/1.12 skol9( Y, Z ), Z, Y ), alpha5( X, Y, Z ) }.
% 0.70/1.12 (637) {G0,W12,D3,L4,V2,M4} { ! aRewritingSystem0( X ), ! isTerminating0( X
% 0.70/1.12 ), ! aElement0( Y ), aNormalFormOfIn0( skol10( X, Y ), Y, X ) }.
% 0.70/1.12 (638) {G0,W2,D2,L1,V0,M1} { aRewritingSystem0( xR ) }.
% 0.70/1.12 (639) {G0,W24,D3,L7,V4,M7} { ! aElement0( Z ), ! aElement0( X ), !
% 0.70/1.12 aElement0( Y ), ! aReductOfIn0( X, Z, xR ), ! aReductOfIn0( Y, Z, xR ), Y
% 0.70/1.12 = skol11( T, Y ), alpha35( Y, skol11( T, Y ) ) }.
% 0.70/1.12 (640) {G0,W20,D3,L6,V4,M6} { ! aElement0( Z ), ! aElement0( X ), !
% 0.70/1.12 aElement0( Y ), ! aReductOfIn0( X, Z, xR ), ! aReductOfIn0( Y, Z, xR ),
% 0.70/1.12 sdtmndtasgtdt0( Y, xR, skol11( T, Y ) ) }.
% 0.70/1.12 (641) {G0,W19,D3,L6,V3,M6} { ! aElement0( Z ), ! aElement0( X ), !
% 0.70/1.12 aElement0( Y ), ! aReductOfIn0( X, Z, xR ), ! aReductOfIn0( Y, Z, xR ),
% 0.70/1.12 alpha26( X, skol11( X, Y ) ) }.
% 0.70/1.12 (642) {G0,W2,D2,L1,V0,M1} { isLocallyConfluent0( xR ) }.
% 0.70/1.12 (643) {G0,W1,D1,L1,V0,M1} { alpha18 }.
% 0.70/1.12 (644) {G0,W2,D2,L1,V0,M1} { isTerminating0( xR ) }.
% 0.70/1.12 (645) {G0,W6,D2,L2,V2,M2} { ! alpha35( X, Y ), alpha43( X, Y ) }.
% 0.70/1.12 (646) {G0,W7,D2,L2,V2,M2} { ! alpha35( X, Y ), sdtmndtplgtdt0( X, xR, Y )
% 0.70/1.12 }.
% 0.70/1.12 (647) {G0,W10,D2,L3,V2,M3} { ! alpha43( X, Y ), ! sdtmndtplgtdt0( X, xR, Y
% 0.70/1.12 ), alpha35( X, Y ) }.
% 0.70/1.12 (648) {G0,W10,D2,L3,V2,M3} { ! alpha43( X, Y ), aReductOfIn0( Y, X, xR ),
% 0.70/1.12 alpha52( X, Y ) }.
% 0.70/1.12 (649) {G0,W7,D2,L2,V2,M2} { ! aReductOfIn0( Y, X, xR ), alpha43( X, Y )
% 0.70/1.12 }.
% 0.70/1.12 (650) {G0,W6,D2,L2,V2,M2} { ! alpha52( X, Y ), alpha43( X, Y ) }.
% 0.70/1.12 (651) {G0,W7,D3,L2,V4,M2} { ! alpha52( X, Y ), aElement0( skol12( Z, T ) )
% 0.70/1.12 }.
% 0.70/1.12 (652) {G0,W9,D3,L2,V3,M2} { ! alpha52( X, Y ), sdtmndtplgtdt0( skol12( Z,
% 0.70/1.12 Y ), xR, Y ) }.
% 0.70/1.12 (653) {G0,W9,D3,L2,V2,M2} { ! alpha52( X, Y ), aReductOfIn0( skol12( X, Y
% 0.70/1.12 ), X, xR ) }.
% 0.70/1.12 (654) {G0,W13,D2,L4,V3,M4} { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( Z, xR, Y ), alpha52( X, Y ) }.
% 0.70/1.12 (655) {G0,W6,D2,L2,V2,M2} { ! alpha26( X, Y ), alpha36( X, Y ) }.
% 0.70/1.12 (656) {G0,W7,D2,L2,V2,M2} { ! alpha26( X, Y ), sdtmndtasgtdt0( X, xR, Y )
% 0.70/1.12 }.
% 0.70/1.12 (657) {G0,W10,D2,L3,V2,M3} { ! alpha36( X, Y ), ! sdtmndtasgtdt0( X, xR, Y
% 0.70/1.12 ), alpha26( X, Y ) }.
% 0.70/1.12 (658) {G0,W5,D2,L2,V2,M2} { ! alpha36( X, Y ), aElement0( Y ) }.
% 0.70/1.12 (659) {G0,W6,D2,L2,V2,M2} { ! alpha36( X, Y ), alpha44( X, Y ) }.
% 0.70/1.12 (660) {G0,W8,D2,L3,V2,M3} { ! aElement0( Y ), ! alpha44( X, Y ), alpha36(
% 0.70/1.12 X, Y ) }.
% 0.70/1.12 (661) {G0,W9,D2,L3,V2,M3} { ! alpha44( X, Y ), X = Y, alpha53( X, Y ) }.
% 0.70/1.12 (662) {G0,W6,D2,L2,V2,M2} { ! X = Y, alpha44( X, Y ) }.
% 0.70/1.12 (663) {G0,W6,D2,L2,V2,M2} { ! alpha53( X, Y ), alpha44( X, Y ) }.
% 0.70/1.12 (664) {G0,W6,D2,L2,V2,M2} { ! alpha53( X, Y ), alpha59( X, Y ) }.
% 0.70/1.12 (665) {G0,W7,D2,L2,V2,M2} { ! alpha53( X, Y ), sdtmndtplgtdt0( X, xR, Y )
% 0.70/1.12 }.
% 0.70/1.12 (666) {G0,W10,D2,L3,V2,M3} { ! alpha59( X, Y ), ! sdtmndtplgtdt0( X, xR, Y
% 0.70/1.12 ), alpha53( X, Y ) }.
% 0.70/1.12 (667) {G0,W10,D2,L3,V2,M3} { ! alpha59( X, Y ), aReductOfIn0( Y, X, xR ),
% 0.70/1.12 alpha64( X, Y ) }.
% 0.70/1.12 (668) {G0,W7,D2,L2,V2,M2} { ! aReductOfIn0( Y, X, xR ), alpha59( X, Y )
% 0.70/1.12 }.
% 0.70/1.12 (669) {G0,W6,D2,L2,V2,M2} { ! alpha64( X, Y ), alpha59( X, Y ) }.
% 0.70/1.12 (670) {G0,W7,D3,L2,V4,M2} { ! alpha64( X, Y ), aElement0( skol13( Z, T ) )
% 0.70/1.12 }.
% 0.70/1.12 (671) {G0,W9,D3,L2,V3,M2} { ! alpha64( X, Y ), sdtmndtplgtdt0( skol13( Z,
% 0.70/1.12 Y ), xR, Y ) }.
% 0.70/1.12 (672) {G0,W9,D3,L2,V2,M2} { ! alpha64( X, Y ), aReductOfIn0( skol13( X, Y
% 0.70/1.12 ), X, xR ) }.
% 0.70/1.12 (673) {G0,W13,D2,L4,V3,M4} { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( Z, xR, Y ), alpha64( X, Y ) }.
% 0.70/1.12 (674) {G0,W7,D2,L3,V2,M3} { ! alpha18, alpha27( X, Y ), iLess0( Y, X ) }.
% 0.70/1.12 (675) {G0,W4,D2,L2,V0,M2} { ! alpha27( skol14, skol33 ), alpha18 }.
% 0.70/1.12 (676) {G0,W4,D2,L2,V0,M2} { ! iLess0( skol33, skol14 ), alpha18 }.
% 0.70/1.12 (677) {G0,W9,D2,L3,V2,M3} { ! alpha27( X, Y ), alpha37( X, Y ), alpha45( X
% 0.70/1.12 , Y ) }.
% 0.70/1.12 (678) {G0,W6,D2,L2,V2,M2} { ! alpha37( X, Y ), alpha27( X, Y ) }.
% 0.70/1.12 (679) {G0,W6,D2,L2,V2,M2} { ! alpha45( X, Y ), alpha27( X, Y ) }.
% 0.70/1.12 (680) {G0,W6,D2,L2,V2,M2} { ! alpha45( X, Y ), alpha54( X, Y ) }.
% 0.70/1.12 (681) {G0,W7,D2,L2,V2,M2} { ! alpha45( X, Y ), ! sdtmndtplgtdt0( X, xR, Y
% 0.70/1.12 ) }.
% 0.70/1.12 (682) {G0,W10,D2,L3,V2,M3} { ! alpha54( X, Y ), sdtmndtplgtdt0( X, xR, Y )
% 0.70/1.12 , alpha45( X, Y ) }.
% 0.70/1.12 (683) {G0,W7,D2,L2,V2,M2} { ! alpha54( X, Y ), ! aReductOfIn0( Y, X, xR )
% 0.70/1.12 }.
% 0.70/1.12 (684) {G0,W6,D2,L2,V2,M2} { ! alpha54( X, Y ), alpha60( X, Y ) }.
% 0.70/1.12 (685) {G0,W10,D2,L3,V2,M3} { aReductOfIn0( Y, X, xR ), ! alpha60( X, Y ),
% 0.70/1.12 alpha54( X, Y ) }.
% 0.70/1.12 (686) {G0,W13,D2,L4,V3,M4} { ! alpha60( X, Y ), ! aElement0( Z ), !
% 0.70/1.12 aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y ) }.
% 0.70/1.12 (687) {G0,W7,D3,L2,V4,M2} { aElement0( skol15( Z, T ) ), alpha60( X, Y )
% 0.70/1.12 }.
% 0.70/1.12 (688) {G0,W9,D3,L2,V3,M2} { sdtmndtplgtdt0( skol15( Z, Y ), xR, Y ),
% 0.70/1.12 alpha60( X, Y ) }.
% 0.70/1.12 (689) {G0,W9,D3,L2,V2,M2} { aReductOfIn0( skol15( X, Y ), X, xR ), alpha60
% 0.70/1.12 ( X, Y ) }.
% 0.70/1.12 (690) {G0,W7,D2,L3,V2,M3} { ! alpha37( X, Y ), ! aElement0( X ), !
% 0.70/1.12 aElement0( Y ) }.
% 0.70/1.12 (691) {G0,W5,D2,L2,V2,M2} { aElement0( X ), alpha37( X, Y ) }.
% 0.70/1.12 (692) {G0,W5,D2,L2,V2,M2} { aElement0( Y ), alpha37( X, Y ) }.
% 0.70/1.12 (693) {G0,W2,D2,L1,V0,M1} { aElement0( xa ) }.
% 0.70/1.12 (694) {G0,W2,D2,L1,V0,M1} { aElement0( xb ) }.
% 0.70/1.12 (695) {G0,W2,D2,L1,V0,M1} { aElement0( xc ) }.
% 0.70/1.12 (696) {G0,W25,D3,L8,V4,M8} { ! aElement0( X ), ! aElement0( Y ), !
% 0.70/1.12 aElement0( Z ), alpha19( X, Y ), alpha28( X, Z ), ! iLess0( X, xa ), Z =
% 0.70/1.12 skol16( T, Z ), alpha46( Z, skol16( T, Z ) ) }.
% 0.70/1.12 (697) {G0,W21,D3,L7,V4,M7} { ! aElement0( X ), ! aElement0( Y ), !
% 0.70/1.12 aElement0( Z ), alpha19( X, Y ), alpha28( X, Z ), ! iLess0( X, xa ),
% 0.70/1.12 sdtmndtasgtdt0( Z, xR, skol16( T, Z ) ) }.
% 0.70/1.12 (698) {G0,W20,D3,L7,V3,M7} { ! aElement0( X ), ! aElement0( Y ), !
% 0.70/1.12 aElement0( Z ), alpha19( X, Y ), alpha28( X, Z ), ! iLess0( X, xa ),
% 0.70/1.12 alpha38( Y, skol16( Y, Z ) ) }.
% 0.70/1.12 (699) {G0,W6,D2,L2,V2,M2} { ! alpha46( X, Y ), alpha55( X, Y ) }.
% 0.70/1.12 (700) {G0,W7,D2,L2,V2,M2} { ! alpha46( X, Y ), sdtmndtplgtdt0( X, xR, Y )
% 0.70/1.12 }.
% 0.70/1.12 (701) {G0,W10,D2,L3,V2,M3} { ! alpha55( X, Y ), ! sdtmndtplgtdt0( X, xR, Y
% 0.70/1.12 ), alpha46( X, Y ) }.
% 0.70/1.12 (702) {G0,W10,D2,L3,V2,M3} { ! alpha55( X, Y ), aReductOfIn0( Y, X, xR ),
% 0.70/1.12 alpha61( X, Y ) }.
% 0.70/1.12 (703) {G0,W7,D2,L2,V2,M2} { ! aReductOfIn0( Y, X, xR ), alpha55( X, Y )
% 0.70/1.12 }.
% 0.70/1.12 (704) {G0,W6,D2,L2,V2,M2} { ! alpha61( X, Y ), alpha55( X, Y ) }.
% 0.70/1.12 (705) {G0,W7,D3,L2,V4,M2} { ! alpha61( X, Y ), aElement0( skol17( Z, T ) )
% 0.70/1.12 }.
% 0.70/1.12 (706) {G0,W9,D3,L2,V3,M2} { ! alpha61( X, Y ), sdtmndtplgtdt0( skol17( Z,
% 0.70/1.12 Y ), xR, Y ) }.
% 0.70/1.12 (707) {G0,W9,D3,L2,V2,M2} { ! alpha61( X, Y ), aReductOfIn0( skol17( X, Y
% 0.70/1.12 ), X, xR ) }.
% 0.70/1.12 (708) {G0,W13,D2,L4,V3,M4} { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( Z, xR, Y ), alpha61( X, Y ) }.
% 0.70/1.12 (709) {G0,W6,D2,L2,V2,M2} { ! alpha38( X, Y ), alpha47( X, Y ) }.
% 0.70/1.12 (710) {G0,W7,D2,L2,V2,M2} { ! alpha38( X, Y ), sdtmndtasgtdt0( X, xR, Y )
% 0.70/1.12 }.
% 0.70/1.12 (711) {G0,W10,D2,L3,V2,M3} { ! alpha47( X, Y ), ! sdtmndtasgtdt0( X, xR, Y
% 0.70/1.12 ), alpha38( X, Y ) }.
% 0.70/1.12 (712) {G0,W5,D2,L2,V2,M2} { ! alpha47( X, Y ), aElement0( Y ) }.
% 0.70/1.12 (713) {G0,W6,D2,L2,V2,M2} { ! alpha47( X, Y ), alpha56( X, Y ) }.
% 0.70/1.12 (714) {G0,W8,D2,L3,V2,M3} { ! aElement0( Y ), ! alpha56( X, Y ), alpha47(
% 0.70/1.12 X, Y ) }.
% 0.70/1.12 (715) {G0,W9,D2,L3,V2,M3} { ! alpha56( X, Y ), X = Y, alpha62( X, Y ) }.
% 0.70/1.12 (716) {G0,W6,D2,L2,V2,M2} { ! X = Y, alpha56( X, Y ) }.
% 0.70/1.12 (717) {G0,W6,D2,L2,V2,M2} { ! alpha62( X, Y ), alpha56( X, Y ) }.
% 0.70/1.12 (718) {G0,W6,D2,L2,V2,M2} { ! alpha62( X, Y ), alpha65( X, Y ) }.
% 0.70/1.12 (719) {G0,W7,D2,L2,V2,M2} { ! alpha62( X, Y ), sdtmndtplgtdt0( X, xR, Y )
% 0.70/1.12 }.
% 0.70/1.12 (720) {G0,W10,D2,L3,V2,M3} { ! alpha65( X, Y ), ! sdtmndtplgtdt0( X, xR, Y
% 0.70/1.12 ), alpha62( X, Y ) }.
% 0.70/1.12 (721) {G0,W10,D2,L3,V2,M3} { ! alpha65( X, Y ), aReductOfIn0( Y, X, xR ),
% 0.70/1.12 alpha66( X, Y ) }.
% 0.70/1.12 (722) {G0,W7,D2,L2,V2,M2} { ! aReductOfIn0( Y, X, xR ), alpha65( X, Y )
% 0.70/1.12 }.
% 0.70/1.12 (723) {G0,W6,D2,L2,V2,M2} { ! alpha66( X, Y ), alpha65( X, Y ) }.
% 0.70/1.12 (724) {G0,W7,D3,L2,V4,M2} { ! alpha66( X, Y ), aElement0( skol18( Z, T ) )
% 0.70/1.12 }.
% 0.70/1.12 (725) {G0,W9,D3,L2,V3,M2} { ! alpha66( X, Y ), sdtmndtplgtdt0( skol18( Z,
% 0.70/1.12 Y ), xR, Y ) }.
% 0.70/1.12 (726) {G0,W9,D3,L2,V2,M2} { ! alpha66( X, Y ), aReductOfIn0( skol18( X, Y
% 0.70/1.12 ), X, xR ) }.
% 0.70/1.12 (727) {G0,W13,D2,L4,V3,M4} { ! aElement0( Z ), ! aReductOfIn0( Z, X, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( Z, xR, Y ), alpha66( X, Y ) }.
% 0.70/1.12 (728) {G0,W6,D2,L2,V2,M2} { ! alpha28( X, Y ), alpha39( X, Y ) }.
% 0.70/1.12 (729) {G0,W7,D2,L2,V2,M2} { ! alpha28( X, Y ), ! sdtmndtasgtdt0( X, xR, Y
% 0.70/1.12 ) }.
% 0.70/1.12 (730) {G0,W10,D2,L3,V2,M3} { ! alpha39( X, Y ), sdtmndtasgtdt0( X, xR, Y )
% 0.70/1.12 , alpha28( X, Y ) }.
% 0.70/1.12 (731) {G0,W6,D2,L2,V2,M2} { ! alpha39( X, Y ), alpha48( X, Y ) }.
% 0.70/1.12 (732) {G0,W7,D2,L2,V2,M2} { ! alpha39( X, Y ), ! sdtmndtplgtdt0( X, xR, Y
% 0.70/1.12 ) }.
% 0.70/1.12 (733) {G0,W10,D2,L3,V2,M3} { ! alpha48( X, Y ), sdtmndtplgtdt0( X, xR, Y )
% 0.70/1.12 , alpha39( X, Y ) }.
% 0.70/1.12 (734) {G0,W6,D2,L2,V2,M2} { ! alpha48( X, Y ), alpha57( X, Y ) }.
% 0.70/1.12 (735) {G0,W6,D2,L2,V2,M2} { ! alpha48( X, Y ), alpha63( X, Y ) }.
% 0.70/1.12 (736) {G0,W9,D2,L3,V2,M3} { ! alpha57( X, Y ), ! alpha63( X, Y ), alpha48
% 0.70/1.12 ( X, Y ) }.
% 0.70/1.12 (737) {G0,W13,D2,L4,V3,M4} { ! alpha63( X, Y ), ! aElement0( Z ), !
% 0.70/1.12 aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y ) }.
% 0.70/1.12 (738) {G0,W7,D3,L2,V4,M2} { aElement0( skol19( Z, T ) ), alpha63( X, Y )
% 0.70/1.12 }.
% 0.70/1.12 (739) {G0,W9,D3,L2,V3,M2} { sdtmndtplgtdt0( skol19( Z, Y ), xR, Y ),
% 0.70/1.12 alpha63( X, Y ) }.
% 0.70/1.12 (740) {G0,W9,D3,L2,V2,M2} { aReductOfIn0( skol19( X, Y ), X, xR ), alpha63
% 0.70/1.12 ( X, Y ) }.
% 0.70/1.12 (741) {G0,W6,D2,L2,V2,M2} { ! alpha57( X, Y ), ! X = Y }.
% 0.70/1.12 (742) {G0,W7,D2,L2,V2,M2} { ! alpha57( X, Y ), ! aReductOfIn0( Y, X, xR )
% 0.70/1.12 }.
% 0.70/1.12 (743) {G0,W10,D2,L3,V2,M3} { X = Y, aReductOfIn0( Y, X, xR ), alpha57( X,
% 0.70/1.12 Y ) }.
% 0.70/1.12 (744) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), alpha29( X, Y ) }.
% 0.70/1.12 (745) {G0,W7,D2,L2,V2,M2} { ! alpha19( X, Y ), ! sdtmndtasgtdt0( X, xR, Y
% 0.70/1.12 ) }.
% 0.70/1.12 (746) {G0,W10,D2,L3,V2,M3} { ! alpha29( X, Y ), sdtmndtasgtdt0( X, xR, Y )
% 0.70/1.12 , alpha19( X, Y ) }.
% 0.70/1.12 (747) {G0,W6,D2,L2,V2,M2} { ! alpha29( X, Y ), alpha40( X, Y ) }.
% 0.70/1.12 (748) {G0,W7,D2,L2,V2,M2} { ! alpha29( X, Y ), ! sdtmndtplgtdt0( X, xR, Y
% 0.70/1.12 ) }.
% 0.70/1.12 (749) {G0,W10,D2,L3,V2,M3} { ! alpha40( X, Y ), sdtmndtplgtdt0( X, xR, Y )
% 0.70/1.12 , alpha29( X, Y ) }.
% 0.70/1.12 (750) {G0,W6,D2,L2,V2,M2} { ! alpha40( X, Y ), alpha49( X, Y ) }.
% 0.70/1.12 (751) {G0,W6,D2,L2,V2,M2} { ! alpha40( X, Y ), alpha58( X, Y ) }.
% 0.70/1.12 (752) {G0,W9,D2,L3,V2,M3} { ! alpha49( X, Y ), ! alpha58( X, Y ), alpha40
% 0.70/1.12 ( X, Y ) }.
% 0.70/1.12 (753) {G0,W13,D2,L4,V3,M4} { ! alpha58( X, Y ), ! aElement0( Z ), !
% 0.70/1.12 aReductOfIn0( Z, X, xR ), ! sdtmndtplgtdt0( Z, xR, Y ) }.
% 0.70/1.12 (754) {G0,W7,D3,L2,V4,M2} { aElement0( skol20( Z, T ) ), alpha58( X, Y )
% 0.70/1.12 }.
% 0.70/1.12 (755) {G0,W9,D3,L2,V3,M2} { sdtmndtplgtdt0( skol20( Z, Y ), xR, Y ),
% 0.70/1.12 alpha58( X, Y ) }.
% 0.70/1.12 (756) {G0,W9,D3,L2,V2,M2} { aReductOfIn0( skol20( X, Y ), X, xR ), alpha58
% 0.70/1.12 ( X, Y ) }.
% 0.70/1.12 (757) {G0,W6,D2,L2,V2,M2} { ! alpha49( X, Y ), ! X = Y }.
% 0.70/1.12 (758) {G0,W7,D2,L2,V2,M2} { ! alpha49( X, Y ), ! aReductOfIn0( Y, X, xR )
% 0.70/1.12 }.
% 0.70/1.12 (759) {G0,W10,D2,L3,V2,M3} { X = Y, aReductOfIn0( Y, X, xR ), alpha49( X,
% 0.70/1.12 Y ) }.
% 0.70/1.12 (760) {G0,W1,D1,L1,V0,M1} { alpha20 }.
% 0.70/1.12 (761) {G0,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xb ) }.
% 0.70/1.12 (762) {G0,W6,D2,L2,V0,M2} { aReductOfIn0( xc, xa, xR ), aElement0( skol21
% 0.70/1.12 ) }.
% 0.70/1.12 (763) {G0,W8,D2,L2,V0,M2} { aReductOfIn0( xc, xa, xR ), aReductOfIn0(
% 0.70/1.12 skol21, xa, xR ) }.
% 0.70/1.12 (764) {G0,W8,D2,L2,V0,M2} { aReductOfIn0( xc, xa, xR ), sdtmndtplgtdt0(
% 0.70/1.12 skol21, xR, xc ) }.
% 0.70/1.12 (765) {G0,W4,D2,L1,V0,M1} { sdtmndtplgtdt0( xa, xR, xc ) }.
% 0.70/1.12 (766) {G0,W6,D2,L3,V0,M3} { ! alpha20, aReductOfIn0( xb, xa, xR ), alpha30
% 0.70/1.12 }.
% 0.70/1.12 (767) {G0,W5,D2,L2,V0,M2} { ! aReductOfIn0( xb, xa, xR ), alpha20 }.
% 0.70/1.12 (768) {G0,W2,D1,L2,V0,M2} { ! alpha30, alpha20 }.
% 0.70/1.12 (769) {G0,W3,D2,L2,V0,M2} { ! alpha30, aElement0( skol22 ) }.
% 0.70/1.12 (770) {G0,W5,D2,L2,V0,M2} { ! alpha30, aReductOfIn0( skol22, xa, xR ) }.
% 0.70/1.12 (771) {G0,W5,D2,L2,V0,M2} { ! alpha30, sdtmndtplgtdt0( skol22, xR, xb )
% 0.70/1.12 }.
% 0.70/1.12 (772) {G0,W11,D2,L4,V1,M4} { ! aElement0( X ), ! aReductOfIn0( X, xa, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( X, xR, xb ), alpha30 }.
% 0.70/1.12 (773) {G0,W2,D2,L1,V0,M1} { aElement0( xu ) }.
% 0.70/1.12 (774) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xu, xa, xR ) }.
% 0.70/1.12 (775) {G0,W8,D2,L3,V0,M3} { xu = xb, aReductOfIn0( xb, xu, xR ), alpha21
% 0.70/1.12 }.
% 0.70/1.12 (776) {G0,W7,D2,L2,V0,M2} { xu = xb, sdtmndtplgtdt0( xu, xR, xb ) }.
% 0.70/1.12 (777) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xb ) }.
% 0.70/1.12 (778) {G0,W3,D2,L2,V0,M2} { ! alpha21, aElement0( skol23 ) }.
% 0.70/1.12 (779) {G0,W5,D2,L2,V0,M2} { ! alpha21, aReductOfIn0( skol23, xu, xR ) }.
% 0.70/1.12 (780) {G0,W5,D2,L2,V0,M2} { ! alpha21, sdtmndtplgtdt0( skol23, xR, xb )
% 0.70/1.12 }.
% 0.70/1.12 (781) {G0,W11,D2,L4,V1,M4} { ! aElement0( X ), ! aReductOfIn0( X, xu, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( X, xR, xb ), alpha21 }.
% 0.70/1.12 (782) {G0,W2,D2,L1,V0,M1} { aElement0( xv ) }.
% 0.70/1.12 (783) {G0,W4,D2,L1,V0,M1} { aReductOfIn0( xv, xa, xR ) }.
% 0.70/1.12 (784) {G0,W8,D2,L3,V0,M3} { xv = xc, aReductOfIn0( xc, xv, xR ), alpha22
% 0.70/1.12 }.
% 0.70/1.12 (785) {G0,W7,D2,L2,V0,M2} { xv = xc, sdtmndtplgtdt0( xv, xR, xc ) }.
% 0.70/1.12 (786) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xc ) }.
% 0.70/1.12 (787) {G0,W3,D2,L2,V0,M2} { ! alpha22, aElement0( skol24 ) }.
% 0.70/1.12 (788) {G0,W5,D2,L2,V0,M2} { ! alpha22, aReductOfIn0( skol24, xv, xR ) }.
% 0.70/1.12 (789) {G0,W5,D2,L2,V0,M2} { ! alpha22, sdtmndtplgtdt0( skol24, xR, xc )
% 0.70/1.12 }.
% 0.70/1.12 (790) {G0,W11,D2,L4,V1,M4} { ! aElement0( X ), ! aReductOfIn0( X, xv, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( X, xR, xc ), alpha22 }.
% 0.70/1.12 (791) {G0,W2,D2,L1,V0,M1} { aElement0( xw ) }.
% 0.70/1.12 (792) {G0,W1,D1,L1,V0,M1} { alpha23 }.
% 0.70/1.12 (793) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xu, xR, xw ) }.
% 0.70/1.12 (794) {G0,W8,D2,L3,V0,M3} { xv = xw, aReductOfIn0( xw, xv, xR ), alpha31
% 0.70/1.12 }.
% 0.70/1.12 (795) {G0,W7,D2,L2,V0,M2} { xv = xw, sdtmndtplgtdt0( xv, xR, xw ) }.
% 0.70/1.12 (796) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xv, xR, xw ) }.
% 0.70/1.12 (797) {G0,W3,D2,L2,V0,M2} { ! alpha31, aElement0( skol25 ) }.
% 0.70/1.12 (798) {G0,W5,D2,L2,V0,M2} { ! alpha31, aReductOfIn0( skol25, xv, xR ) }.
% 0.70/1.12 (799) {G0,W5,D2,L2,V0,M2} { ! alpha31, sdtmndtplgtdt0( skol25, xR, xw )
% 0.70/1.12 }.
% 0.70/1.12 (800) {G0,W11,D2,L4,V1,M4} { ! aElement0( X ), ! aReductOfIn0( X, xv, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( X, xR, xw ), alpha31 }.
% 0.70/1.12 (801) {G0,W5,D2,L3,V0,M3} { ! alpha23, xu = xw, alpha32 }.
% 0.70/1.12 (802) {G0,W4,D2,L2,V0,M2} { ! xu = xw, alpha23 }.
% 0.70/1.12 (803) {G0,W2,D1,L2,V0,M2} { ! alpha32, alpha23 }.
% 0.70/1.12 (804) {G0,W2,D1,L2,V0,M2} { ! alpha32, alpha41 }.
% 0.70/1.12 (805) {G0,W5,D2,L2,V0,M2} { ! alpha32, sdtmndtplgtdt0( xu, xR, xw ) }.
% 0.70/1.12 (806) {G0,W6,D2,L3,V0,M3} { ! alpha41, ! sdtmndtplgtdt0( xu, xR, xw ),
% 0.70/1.12 alpha32 }.
% 0.70/1.12 (807) {G0,W6,D2,L3,V0,M3} { ! alpha41, aReductOfIn0( xw, xu, xR ), alpha50
% 0.70/1.12 }.
% 0.70/1.12 (808) {G0,W5,D2,L2,V0,M2} { ! aReductOfIn0( xw, xu, xR ), alpha41 }.
% 0.70/1.12 (809) {G0,W2,D1,L2,V0,M2} { ! alpha50, alpha41 }.
% 0.70/1.12 (810) {G0,W3,D2,L2,V0,M2} { ! alpha50, aElement0( skol26 ) }.
% 0.70/1.12 (811) {G0,W5,D2,L2,V0,M2} { ! alpha50, aReductOfIn0( skol26, xu, xR ) }.
% 0.70/1.12 (812) {G0,W5,D2,L2,V0,M2} { ! alpha50, sdtmndtplgtdt0( skol26, xR, xw )
% 0.70/1.12 }.
% 0.70/1.12 (813) {G0,W11,D2,L4,V1,M4} { ! aElement0( X ), ! aReductOfIn0( X, xu, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( X, xR, xw ), alpha50 }.
% 0.70/1.12 (814) {G0,W2,D2,L1,V0,M1} { aElement0( xd ) }.
% 0.70/1.12 (815) {G0,W8,D2,L3,V0,M3} { xw = xd, aReductOfIn0( xd, xw, xR ), alpha24
% 0.70/1.12 }.
% 0.70/1.12 (816) {G0,W7,D2,L2,V0,M2} { xw = xd, sdtmndtplgtdt0( xw, xR, xd ) }.
% 0.70/1.12 (817) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xw, xR, xd ) }.
% 0.70/1.12 (818) {G0,W4,D2,L1,V1,M1} { ! aReductOfIn0( X, xd, xR ) }.
% 0.70/1.12 (819) {G0,W4,D2,L1,V0,M1} { aNormalFormOfIn0( xd, xw, xR ) }.
% 0.70/1.12 (820) {G0,W3,D2,L2,V0,M2} { ! alpha24, aElement0( skol27 ) }.
% 0.70/1.12 (821) {G0,W5,D2,L2,V0,M2} { ! alpha24, aReductOfIn0( skol27, xw, xR ) }.
% 0.70/1.12 (822) {G0,W5,D2,L2,V0,M2} { ! alpha24, sdtmndtplgtdt0( skol27, xR, xd )
% 0.70/1.12 }.
% 0.70/1.12 (823) {G0,W11,D2,L4,V1,M4} { ! aElement0( X ), ! aReductOfIn0( X, xw, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( X, xR, xd ), alpha24 }.
% 0.70/1.12 (824) {G0,W2,D2,L1,V0,M1} { aElement0( xx ) }.
% 0.70/1.12 (825) {G0,W1,D1,L1,V0,M1} { alpha25 }.
% 0.70/1.12 (826) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xb, xR, xx ) }.
% 0.70/1.12 (827) {G0,W8,D2,L3,V0,M3} { xd = xx, aReductOfIn0( xx, xd, xR ), alpha33
% 0.70/1.12 }.
% 0.70/1.12 (828) {G0,W7,D2,L2,V0,M2} { xd = xx, sdtmndtplgtdt0( xd, xR, xx ) }.
% 0.70/1.12 (829) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xd, xR, xx ) }.
% 0.70/1.12 (830) {G0,W3,D2,L2,V0,M2} { ! alpha33, aElement0( skol28 ) }.
% 0.70/1.12 (831) {G0,W5,D2,L2,V0,M2} { ! alpha33, aReductOfIn0( skol28, xd, xR ) }.
% 0.70/1.12 (832) {G0,W5,D2,L2,V0,M2} { ! alpha33, sdtmndtplgtdt0( skol28, xR, xx )
% 0.70/1.12 }.
% 0.70/1.12 (833) {G0,W11,D2,L4,V1,M4} { ! aElement0( X ), ! aReductOfIn0( X, xd, xR )
% 0.70/1.12 , ! sdtmndtplgtdt0( X, xR, xx ), alpha33 }.
% 0.70/1.12 (834) {G0,W5,D2,L3,V0,M3} { ! alpha25, xb = xx, alpha34 }.
% 0.70/1.12 (835) {G0,W4,D2,L2,V0,M2} { ! xb = xx, alpha25 }.
% 0.70/1.12 (836) {G0,W2,D1,L2,V0,M2} { ! alpha34, alpha25 }.
% 0.70/1.12 (837) {G0,W2,D1,L2,V0,M2} { ! alpha34, alpha42 }.
% 0.70/1.12 (838) {G0,W5,D2,L2,V0,M2} { ! alpha34, sdtmndtplgtdt0( xb, xR, xx ) }.
% 0.70/1.12 (839) {G0,W6,D2,L3,V0,M3} { ! alpha42, ! sdtmndtplgtdt0( xb, xR, xx ),
% 0.70/1.13 alpha34 }.
% 0.70/1.13 (840) {G0,W6,D2,L3,V0,M3} { ! alpha42, aReductOfIn0( xx, xb, xR ), alpha51
% 0.70/1.13 }.
% 0.70/1.13 (841) {G0,W5,D2,L2,V0,M2} { ! aReductOfIn0( xx, xb, xR ), alpha42 }.
% 0.70/1.13 (842) {G0,W2,D1,L2,V0,M2} { ! alpha51, alpha42 }.
% 0.70/1.13 (843) {G0,W3,D2,L2,V0,M2} { ! alpha51, aElement0( skol29 ) }.
% 0.70/1.13 (844) {G0,W5,D2,L2,V0,M2} { ! alpha51, aReductOfIn0( skol29, xb, xR ) }.
% 0.70/1.13 (845) {G0,W5,D2,L2,V0,M2} { ! alpha51, sdtmndtplgtdt0( skol29, xR, xx )
% 0.70/1.13 }.
% 0.70/1.13 (846) {G0,W11,D2,L4,V1,M4} { ! aElement0( X ), ! aReductOfIn0( X, xb, xR )
% 0.70/1.13 , ! sdtmndtplgtdt0( X, xR, xx ), alpha51 }.
% 0.70/1.13 (847) {G0,W3,D2,L1,V0,M1} { ! xb = xd }.
% 0.70/1.13 (848) {G0,W4,D2,L1,V0,M1} { ! aReductOfIn0( xd, xb, xR ) }.
% 0.70/1.13 (849) {G0,W10,D2,L3,V1,M3} { ! aElement0( X ), ! aReductOfIn0( X, xb, xR )
% 0.70/1.13 , ! sdtmndtplgtdt0( X, xR, xd ) }.
% 0.70/1.13 (850) {G0,W4,D2,L1,V0,M1} { ! sdtmndtplgtdt0( xb, xR, xd ) }.
% 0.70/1.13 (851) {G0,W4,D2,L1,V0,M1} { ! sdtmndtasgtdt0( xb, xR, xd ) }.
% 0.70/1.13
% 0.70/1.13
% 0.70/1.13 Total Proof:
% 0.70/1.13
% 0.70/1.13 *** allocated 22500 integers for termspace/termends
% 0.70/1.13 subsumption: (248) {G0,W4,D2,L1,V1,M1} I { ! aReductOfIn0( X, xd, xR ) }.
% 0.70/1.13 parent0: (818) {G0,W4,D2,L1,V1,M1} { ! aReductOfIn0( X, xd, xR ) }.
% 0.70/1.13 substitution0:
% 0.70/1.13 X := X
% 0.70/1.13 end
% 0.70/1.13 permutation0:
% 0.70/1.13 0 ==> 0
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 subsumption: (256) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xb, xR, xx ) }.
% 0.70/1.13 parent0: (826) {G0,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xb, xR, xx ) }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 permutation0:
% 0.70/1.13 0 ==> 0
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 resolution: (1117) {G1,W4,D2,L2,V0,M2} { xd = xx, alpha33 }.
% 0.70/1.13 parent0[0]: (248) {G0,W4,D2,L1,V1,M1} I { ! aReductOfIn0( X, xd, xR ) }.
% 0.70/1.13 parent1[1]: (827) {G0,W8,D2,L3,V0,M3} { xd = xx, aReductOfIn0( xx, xd, xR
% 0.70/1.13 ), alpha33 }.
% 0.70/1.13 substitution0:
% 0.70/1.13 X := xx
% 0.70/1.13 end
% 0.70/1.13 substitution1:
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 eqswap: (1118) {G1,W4,D2,L2,V0,M2} { xx = xd, alpha33 }.
% 0.70/1.13 parent0[0]: (1117) {G1,W4,D2,L2,V0,M2} { xd = xx, alpha33 }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 subsumption: (257) {G1,W4,D2,L2,V0,M2} I;r(248) { xx ==> xd, alpha33 }.
% 0.70/1.13 parent0: (1118) {G1,W4,D2,L2,V0,M2} { xx = xd, alpha33 }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 permutation0:
% 0.70/1.13 0 ==> 0
% 0.70/1.13 1 ==> 1
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 resolution: (1213) {G1,W1,D1,L1,V0,M1} { ! alpha33 }.
% 0.70/1.13 parent0[0]: (248) {G0,W4,D2,L1,V1,M1} I { ! aReductOfIn0( X, xd, xR ) }.
% 0.70/1.13 parent1[1]: (831) {G0,W5,D2,L2,V0,M2} { ! alpha33, aReductOfIn0( skol28,
% 0.70/1.13 xd, xR ) }.
% 0.70/1.13 substitution0:
% 0.70/1.13 X := skol28
% 0.70/1.13 end
% 0.70/1.13 substitution1:
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 subsumption: (261) {G1,W1,D1,L1,V0,M1} I;r(248) { ! alpha33 }.
% 0.70/1.13 parent0: (1213) {G1,W1,D1,L1,V0,M1} { ! alpha33 }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 permutation0:
% 0.70/1.13 0 ==> 0
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 *** allocated 33750 integers for termspace/termends
% 0.70/1.13 subsumption: (277) {G0,W4,D2,L1,V0,M1} I { ! sdtmndtasgtdt0( xb, xR, xd )
% 0.70/1.13 }.
% 0.70/1.13 parent0: (851) {G0,W4,D2,L1,V0,M1} { ! sdtmndtasgtdt0( xb, xR, xd ) }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 permutation0:
% 0.70/1.13 0 ==> 0
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 resolution: (1308) {G2,W3,D2,L1,V0,M1} { xx ==> xd }.
% 0.70/1.13 parent0[0]: (261) {G1,W1,D1,L1,V0,M1} I;r(248) { ! alpha33 }.
% 0.70/1.13 parent1[1]: (257) {G1,W4,D2,L2,V0,M2} I;r(248) { xx ==> xd, alpha33 }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 substitution1:
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 subsumption: (556) {G2,W3,D2,L1,V0,M1} S(257);r(261) { xx ==> xd }.
% 0.70/1.13 parent0: (1308) {G2,W3,D2,L1,V0,M1} { xx ==> xd }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 permutation0:
% 0.70/1.13 0 ==> 0
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 paramod: (1311) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xb, xR, xd ) }.
% 0.70/1.13 parent0[0]: (556) {G2,W3,D2,L1,V0,M1} S(257);r(261) { xx ==> xd }.
% 0.70/1.13 parent1[0; 3]: (256) {G0,W4,D2,L1,V0,M1} I { sdtmndtasgtdt0( xb, xR, xx )
% 0.70/1.13 }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 substitution1:
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 resolution: (1312) {G1,W0,D0,L0,V0,M0} { }.
% 0.70/1.13 parent0[0]: (277) {G0,W4,D2,L1,V0,M1} I { ! sdtmndtasgtdt0( xb, xR, xd )
% 0.70/1.13 }.
% 0.70/1.13 parent1[0]: (1311) {G1,W4,D2,L1,V0,M1} { sdtmndtasgtdt0( xb, xR, xd ) }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 substitution1:
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 subsumption: (559) {G3,W0,D0,L0,V0,M0} P(556,256);r(277) { }.
% 0.70/1.13 parent0: (1312) {G1,W0,D0,L0,V0,M0} { }.
% 0.70/1.13 substitution0:
% 0.70/1.13 end
% 0.70/1.13 permutation0:
% 0.70/1.13 end
% 0.70/1.13
% 0.70/1.13 Proof check complete!
% 0.70/1.13
% 0.70/1.13 Memory use:
% 0.70/1.13
% 0.70/1.13 space for terms: 12282
% 0.70/1.13 space for clauses: 27773
% 0.70/1.13
% 0.70/1.13
% 0.70/1.13 clauses generated: 825
% 0.70/1.13 clauses kept: 560
% 0.70/1.13 clauses selected: 63
% 0.70/1.13 clauses deleted: 2
% 0.70/1.13 clauses inuse deleted: 0
% 0.70/1.13
% 0.70/1.13 subsentry: 1977
% 0.70/1.13 literals s-matched: 1157
% 0.70/1.13 literals matched: 887
% 0.70/1.13 full subsumption: 244
% 0.70/1.13
% 0.70/1.13 checksum: 1319651383
% 0.70/1.13
% 0.70/1.13
% 0.70/1.13 Bliksem ended
%------------------------------------------------------------------------------