%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : LAT385+4 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n015.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 : Sun Jul 17 03:51:52 EDT 2022
% Result : Theorem 0.79s 1.18s
% Output : Refutation 0.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : LAT385+4 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Wed Jun 29 17:43:41 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.43/1.13 *** allocated 10000 integers for termspace/termends
% 0.43/1.13 *** allocated 10000 integers for clauses
% 0.43/1.13 *** allocated 10000 integers for justifications
% 0.43/1.13 Bliksem 1.12
% 0.43/1.13
% 0.43/1.13
% 0.43/1.13 Automatic Strategy Selection
% 0.43/1.13
% 0.43/1.13
% 0.43/1.13 Clauses:
% 0.43/1.13
% 0.43/1.13 { && }.
% 0.43/1.13 { && }.
% 0.43/1.13 { ! aSet0( X ), ! aElementOf0( Y, X ), aElement0( Y ) }.
% 0.43/1.13 { ! aSet0( X ), ! isEmpty0( X ), ! aElementOf0( Y, X ) }.
% 0.43/1.13 { ! aSet0( X ), aElementOf0( skol1( X ), X ), isEmpty0( X ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), aSet0( Y ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), alpha1( X, Y ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSet0( Y ), ! alpha1( X, Y ), aSubsetOf0( Y, X ) }.
% 0.43/1.13 { ! alpha1( X, Y ), ! aElementOf0( Z, Y ), aElementOf0( Z, X ) }.
% 0.43/1.13 { aElementOf0( skol2( Z, Y ), Y ), alpha1( X, Y ) }.
% 0.43/1.13 { ! aElementOf0( skol2( X, Y ), X ), alpha1( X, Y ) }.
% 0.43/1.13 { && }.
% 0.43/1.13 { ! aElement0( X ), sdtlseqdt0( X, X ) }.
% 0.43/1.13 { ! aElement0( X ), ! aElement0( Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y
% 0.43/1.13 , X ), X = Y }.
% 0.43/1.13 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), ! sdtlseqdt0( X, Y
% 0.43/1.13 ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aLowerBoundOfIn0( Z, Y, X ),
% 0.43/1.13 aElementOf0( Z, X ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aLowerBoundOfIn0( Z, Y, X ), alpha2
% 0.43/1.13 ( Y, Z ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aElementOf0( Z, X ), ! alpha2( Y, Z
% 0.43/1.13 ), aLowerBoundOfIn0( Z, Y, X ) }.
% 0.43/1.13 { ! alpha2( X, Y ), ! aElementOf0( Z, X ), sdtlseqdt0( Y, Z ) }.
% 0.43/1.13 { ! sdtlseqdt0( Y, skol3( Z, Y ) ), alpha2( X, Y ) }.
% 0.43/1.13 { aElementOf0( skol3( X, Y ), X ), alpha2( X, Y ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aUpperBoundOfIn0( Z, Y, X ),
% 0.43/1.13 aElementOf0( Z, X ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aUpperBoundOfIn0( Z, Y, X ), alpha3
% 0.43/1.13 ( Y, Z ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aElementOf0( Z, X ), ! alpha3( Y, Z
% 0.43/1.13 ), aUpperBoundOfIn0( Z, Y, X ) }.
% 0.43/1.13 { ! alpha3( X, Y ), ! aElementOf0( Z, X ), sdtlseqdt0( Z, Y ) }.
% 0.43/1.13 { ! sdtlseqdt0( skol4( Z, Y ), Y ), alpha3( X, Y ) }.
% 0.43/1.13 { aElementOf0( skol4( X, Y ), X ), alpha3( X, Y ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aInfimumOfIn0( Z, Y, X ),
% 0.43/1.13 aElementOf0( Z, X ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aInfimumOfIn0( Z, Y, X ), alpha4( X
% 0.43/1.13 , Y, Z ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aElementOf0( Z, X ), ! alpha4( X, Y
% 0.43/1.13 , Z ), aInfimumOfIn0( Z, Y, X ) }.
% 0.43/1.13 { ! alpha4( X, Y, Z ), aLowerBoundOfIn0( Z, Y, X ) }.
% 0.43/1.13 { ! alpha4( X, Y, Z ), alpha8( X, Y, Z ) }.
% 0.43/1.13 { ! aLowerBoundOfIn0( Z, Y, X ), ! alpha8( X, Y, Z ), alpha4( X, Y, Z ) }.
% 0.43/1.13 { ! alpha8( X, Y, Z ), ! aLowerBoundOfIn0( T, Y, X ), sdtlseqdt0( T, Z ) }
% 0.43/1.13 .
% 0.43/1.13 { ! sdtlseqdt0( skol5( T, U, Z ), Z ), alpha8( X, Y, Z ) }.
% 0.43/1.13 { aLowerBoundOfIn0( skol5( X, Y, Z ), Y, X ), alpha8( X, Y, Z ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aSupremumOfIn0( Z, Y, X ),
% 0.43/1.13 aElementOf0( Z, X ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aSupremumOfIn0( Z, Y, X ), alpha5(
% 0.43/1.13 X, Y, Z ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aElementOf0( Z, X ), ! alpha5( X, Y
% 0.43/1.13 , Z ), aSupremumOfIn0( Z, Y, X ) }.
% 0.43/1.13 { ! alpha5( X, Y, Z ), aUpperBoundOfIn0( Z, Y, X ) }.
% 0.43/1.13 { ! alpha5( X, Y, Z ), alpha9( X, Y, Z ) }.
% 0.43/1.13 { ! aUpperBoundOfIn0( Z, Y, X ), ! alpha9( X, Y, Z ), alpha5( X, Y, Z ) }.
% 0.43/1.13 { ! alpha9( X, Y, Z ), ! aUpperBoundOfIn0( T, Y, X ), sdtlseqdt0( Z, T ) }
% 0.43/1.13 .
% 0.43/1.13 { ! sdtlseqdt0( Z, skol6( T, U, Z ) ), alpha9( X, Y, Z ) }.
% 0.43/1.13 { aUpperBoundOfIn0( skol6( X, Y, Z ), Y, X ), alpha9( X, Y, Z ) }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aSupremumOfIn0( Z, Y, X ), !
% 0.43/1.13 aSupremumOfIn0( T, Y, X ), Z = T }.
% 0.43/1.13 { ! aSet0( X ), ! aSubsetOf0( Y, X ), ! aInfimumOfIn0( Z, Y, X ), !
% 0.43/1.13 aInfimumOfIn0( T, Y, X ), Z = T }.
% 0.43/1.13 { ! aCompleteLattice0( X ), aSet0( X ) }.
% 0.43/1.13 { ! aCompleteLattice0( X ), alpha6( X ) }.
% 0.43/1.13 { ! aSet0( X ), ! alpha6( X ), aCompleteLattice0( X ) }.
% 0.43/1.13 { ! alpha6( X ), ! aSubsetOf0( Y, X ), alpha10( X, Y ) }.
% 0.43/1.13 { aSubsetOf0( skol7( X ), X ), alpha6( X ) }.
% 0.43/1.13 { ! alpha10( X, skol7( X ) ), alpha6( X ) }.
% 0.43/1.13 { ! alpha10( X, Y ), aInfimumOfIn0( skol8( X, Y ), Y, X ) }.
% 0.43/1.13 { ! alpha10( X, Y ), aSupremumOfIn0( skol24( X, Y ), Y, X ) }.
% 0.43/1.13 { ! aInfimumOfIn0( Z, Y, X ), ! aSupremumOfIn0( T, Y, X ), alpha10( X, Y )
% 0.43/1.13 }.
% 0.43/1.13 { && }.
% 0.43/1.13 { ! aFunction0( X ), aSet0( szDzozmdt0( X ) ) }.
% 0.43/1.13 { ! aFunction0( X ), aSet0( szRzazndt0( X ) ) }.
% 0.43/1.13 { ! aFunction0( X ), ! aSet0( Y ), ! isOn0( X, Y ), szDzozmdt0( X ) =
% 0.43/1.13 szRzazndt0( X ) }.
% 0.43/1.13 { ! aFunction0( X ), ! aSet0( Y ), ! isOn0( X, Y ), szRzazndt0( X ) = Y }.
% 0.43/1.13 { ! aFunction0( X ), ! aSet0( Y ), ! szDzozmdt0( X ) = szRzazndt0( X ), !
% 0.43/1.13 szRzazndt0( X ) = Y, isOn0( X, Y ) }.
% 0.43/1.13 { ! aFunction0( X ), ! aElementOf0( Y, szDzozmdt0( X ) ), aElementOf0(
% 0.43/1.13 sdtlpdtrp0( X, Y ), szRzazndt0( X ) ) }.
% 0.43/1.13 { ! aFunction0( X ), ! aFixedPointOf0( Y, X ), aElementOf0( Y, szDzozmdt0(
% 0.43/1.13 X ) ) }.
% 0.43/1.13 { ! aFunction0( X ), ! aFixedPointOf0( Y, X ), sdtlpdtrp0( X, Y ) = Y }.
% 0.43/1.13 { ! aFunction0( X ), ! aElementOf0( Y, szDzozmdt0( X ) ), ! sdtlpdtrp0( X,
% 0.43/1.13 Y ) = Y, aFixedPointOf0( Y, X ) }.
% 0.43/1.13 { ! aFunction0( X ), ! isMonotone0( X ), ! alpha7( X, Y, Z ), alpha11( X, Y
% 0.43/1.13 , Z ) }.
% 0.43/1.13 { ! aFunction0( X ), alpha7( X, skol9( X ), skol25( X ) ), isMonotone0( X )
% 0.43/1.13 }.
% 0.43/1.13 { ! aFunction0( X ), ! alpha11( X, skol9( X ), skol25( X ) ), isMonotone0(
% 0.43/1.13 X ) }.
% 0.43/1.13 { ! alpha11( X, Y, Z ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( sdtlpdtrp0( X, Y
% 0.43/1.13 ), sdtlpdtrp0( X, Z ) ) }.
% 0.43/1.13 { sdtlseqdt0( Y, Z ), alpha11( X, Y, Z ) }.
% 0.43/1.13 { ! sdtlseqdt0( sdtlpdtrp0( X, Y ), sdtlpdtrp0( X, Z ) ), alpha11( X, Y, Z
% 0.43/1.13 ) }.
% 0.43/1.13 { ! alpha7( X, Y, Z ), aElementOf0( Y, szDzozmdt0( X ) ) }.
% 0.43/1.13 { ! alpha7( X, Y, Z ), aElementOf0( Z, szDzozmdt0( X ) ) }.
% 0.43/1.13 { ! aElementOf0( Y, szDzozmdt0( X ) ), ! aElementOf0( Z, szDzozmdt0( X ) )
% 0.43/1.13 , alpha7( X, Y, Z ) }.
% 0.43/1.13 { aSet0( xU ) }.
% 0.43/1.13 { alpha12( X ), alpha29( X, skol10( X ) ) }.
% 0.43/1.13 { alpha12( X ), alpha21( X ) }.
% 0.43/1.13 { aCompleteLattice0( xU ) }.
% 0.43/1.13 { aFunction0( xf ) }.
% 0.43/1.13 { ! aElementOf0( X, szDzozmdt0( xf ) ), ! aElementOf0( Y, szDzozmdt0( xf )
% 0.43/1.13 ), ! sdtlseqdt0( X, Y ), sdtlseqdt0( sdtlpdtrp0( xf, X ), sdtlpdtrp0( xf
% 0.43/1.13 , Y ) ) }.
% 0.43/1.13 { isMonotone0( xf ) }.
% 0.43/1.13 { szDzozmdt0( xf ) = szRzazndt0( xf ) }.
% 0.43/1.13 { szRzazndt0( xf ) = xU }.
% 0.43/1.13 { isOn0( xf, xU ) }.
% 0.43/1.13 { ! alpha29( X, Y ), alpha24( X, Y ) }.
% 0.43/1.13 { ! alpha29( X, Y ), alpha26( X, Y ) }.
% 0.43/1.13 { ! alpha29( X, Y ), aInfimumOfIn0( Y, X, xU ) }.
% 0.43/1.13 { ! alpha24( X, Y ), ! alpha26( X, Y ), ! aInfimumOfIn0( Y, X, xU ),
% 0.43/1.13 alpha29( X, Y ) }.
% 0.43/1.13 { ! alpha26( X, Y ), alpha30( X, Z ), sdtlseqdt0( Z, Y ) }.
% 0.43/1.13 { ! sdtlseqdt0( skol11( Z, Y ), Y ), alpha26( X, Y ) }.
% 0.43/1.13 { ! alpha30( X, skol11( X, Y ) ), alpha26( X, Y ) }.
% 0.43/1.13 { ! alpha30( X, Y ), alpha32( X, Y ) }.
% 0.43/1.13 { ! alpha30( X, Y ), ! aLowerBoundOfIn0( Y, X, xU ) }.
% 0.43/1.13 { ! alpha32( X, Y ), aLowerBoundOfIn0( Y, X, xU ), alpha30( X, Y ) }.
% 0.43/1.13 { ! alpha32( X, Y ), ! aElementOf0( Y, xU ), ! sdtlseqdt0( Y, skol12( Z, Y
% 0.43/1.13 ) ) }.
% 0.43/1.13 { ! alpha32( X, Y ), ! aElementOf0( Y, xU ), aElementOf0( skol12( X, Y ), X
% 0.43/1.13 ) }.
% 0.43/1.13 { aElementOf0( Y, xU ), alpha32( X, Y ) }.
% 0.43/1.13 { ! aElementOf0( Z, X ), sdtlseqdt0( Y, Z ), alpha32( X, Y ) }.
% 0.43/1.13 { ! alpha24( X, Y ), alpha27( X, Y ) }.
% 0.43/1.13 { ! alpha24( X, Y ), aLowerBoundOfIn0( Y, X, xU ) }.
% 0.43/1.13 { ! alpha27( X, Y ), ! aLowerBoundOfIn0( Y, X, xU ), alpha24( X, Y ) }.
% 0.43/1.13 { ! alpha27( X, Y ), alpha16( Y ) }.
% 0.43/1.13 { ! alpha27( X, Y ), ! aElementOf0( Z, X ), sdtlseqdt0( Y, Z ) }.
% 0.43/1.13 { ! alpha16( Y ), ! sdtlseqdt0( Y, skol13( Z, Y ) ), alpha27( X, Y ) }.
% 0.43/1.13 { ! alpha16( Y ), aElementOf0( skol13( X, Y ), X ), alpha27( X, Y ) }.
% 0.43/1.13 { ! alpha21( X ), alpha28( X, skol14( X ) ) }.
% 0.43/1.13 { ! alpha21( X ), aSupremumOfIn0( skol14( X ), X, xU ) }.
% 0.43/1.13 { ! alpha28( X, Y ), ! aSupremumOfIn0( Y, X, xU ), alpha21( X ) }.
% 0.43/1.13 { ! alpha28( X, Y ), alpha31( X, Y ) }.
% 0.43/1.13 { ! alpha28( X, Y ), alpha33( X, Y ) }.
% 0.43/1.13 { ! alpha31( X, Y ), ! alpha33( X, Y ), alpha28( X, Y ) }.
% 0.43/1.13 { ! alpha33( X, Y ), alpha35( X, Z ), sdtlseqdt0( Y, Z ) }.
% 0.43/1.13 { ! sdtlseqdt0( Y, skol15( Z, Y ) ), alpha33( X, Y ) }.
% 0.43/1.13 { ! alpha35( X, skol15( X, Y ) ), alpha33( X, Y ) }.
% 0.43/1.13 { ! alpha35( X, Y ), alpha36( X, Y ) }.
% 0.43/1.13 { ! alpha35( X, Y ), ! aUpperBoundOfIn0( Y, X, xU ) }.
% 0.43/1.13 { ! alpha36( X, Y ), aUpperBoundOfIn0( Y, X, xU ), alpha35( X, Y ) }.
% 0.43/1.13 { ! alpha36( X, Y ), ! aElementOf0( Y, xU ), ! sdtlseqdt0( skol16( Z, Y ),
% 0.43/1.13 Y ) }.
% 0.43/1.13 { ! alpha36( X, Y ), ! aElementOf0( Y, xU ), aElementOf0( skol16( X, Y ), X
% 0.43/1.13 ) }.
% 0.43/1.13 { aElementOf0( Y, xU ), alpha36( X, Y ) }.
% 0.43/1.13 { ! aElementOf0( Z, X ), sdtlseqdt0( Z, Y ), alpha36( X, Y ) }.
% 0.43/1.13 { ! alpha31( X, Y ), alpha34( X, Y ) }.
% 0.43/1.13 { ! alpha31( X, Y ), aUpperBoundOfIn0( Y, X, xU ) }.
% 0.43/1.13 { ! alpha34( X, Y ), ! aUpperBoundOfIn0( Y, X, xU ), alpha31( X, Y ) }.
% 0.43/1.13 { ! alpha34( X, Y ), alpha25( Y ) }.
% 0.43/1.13 { ! alpha34( X, Y ), ! aElementOf0( Z, X ), sdtlseqdt0( Z, Y ) }.
% 0.43/1.13 { ! alpha25( Y ), ! sdtlseqdt0( skol17( Z, Y ), Y ), alpha34( X, Y ) }.
% 0.43/1.13 { ! alpha25( Y ), aElementOf0( skol17( X, Y ), X ), alpha34( X, Y ) }.
% 0.43/1.13 { ! alpha25( X ), aElementOf0( X, xU ) }.
% 0.43/1.13 { ! alpha25( X ), aElementOf0( X, xU ) }.
% 0.43/1.13 { ! aElementOf0( X, xU ), ! aElementOf0( X, xU ), alpha25( X ) }.
% 0.43/1.13 { ! alpha16( X ), aElementOf0( X, xU ) }.
% 0.43/1.13 { ! alpha16( X ), aElementOf0( X, xU ) }.
% 0.43/1.13 { ! aElementOf0( X, xU ), ! aElementOf0( X, xU ), alpha16( X ) }.
% 0.43/1.13 { ! alpha12( X ), alpha17( X ) }.
% 0.43/1.13 { ! alpha12( X ), ! aSubsetOf0( X, xU ) }.
% 0.43/1.13 { ! alpha17( X ), aSubsetOf0( X, xU ), alpha12( X ) }.
% 0.43/1.13 { ! alpha17( X ), ! aSet0( X ), ! aElementOf0( skol18( Y ), xU ) }.
% 0.43/1.13 { ! alpha17( X ), ! aSet0( X ), aElementOf0( skol18( X ), X ) }.
% 0.43/1.13 { aSet0( X ), alpha17( X ) }.
% 0.43/1.13 { ! aElementOf0( Y, X ), aElementOf0( Y, xU ), alpha17( X ) }.
% 0.43/1.13 { aSet0( xS ) }.
% 0.43/1.13 { ! aElementOf0( X, xS ), alpha13( X ) }.
% 0.43/1.13 { ! aElementOf0( X, szDzozmdt0( xf ) ), ! sdtlpdtrp0( xf, X ) = X,
% 0.43/1.13 aElementOf0( X, xS ) }.
% 0.43/1.13 { ! aFixedPointOf0( X, xf ), aElementOf0( X, xS ) }.
% 0.43/1.13 { xS = cS1142( xf ) }.
% 0.43/1.13 { ! alpha13( X ), aElementOf0( X, szDzozmdt0( xf ) ) }.
% 0.43/1.13 { ! alpha13( X ), sdtlpdtrp0( xf, X ) = X }.
% 0.43/1.13 { ! alpha13( X ), aFixedPointOf0( X, xf ) }.
% 0.43/1.13 { ! aElementOf0( X, szDzozmdt0( xf ) ), ! sdtlpdtrp0( xf, X ) = X, !
% 0.43/1.13 aFixedPointOf0( X, xf ), alpha13( X ) }.
% 0.43/1.13 { aSet0( xT ) }.
% 0.43/1.13 { ! aElementOf0( X, xT ), aElementOf0( X, xS ) }.
% 0.43/1.13 { aSubsetOf0( xT, xS ) }.
% 0.43/1.13 { aSet0( xP ) }.
% 0.43/1.13 { ! aElementOf0( X, xP ), alpha14( X ) }.
% 0.43/1.13 { ! aElementOf0( X, xU ), ! sdtlseqdt0( sdtlpdtrp0( xf, X ), X ),
% 0.43/1.13 aElementOf0( skol19( Y ), xT ), aElementOf0( X, xP ) }.
% 0.43/1.13 { ! aElementOf0( X, xU ), ! sdtlseqdt0( sdtlpdtrp0( xf, X ), X ), !
% 0.43/1.13 sdtlseqdt0( skol19( X ), X ), aElementOf0( X, xP ) }.
% 0.43/1.13 { ! aElementOf0( X, xU ), ! sdtlseqdt0( sdtlpdtrp0( xf, X ), X ), !
% 0.43/1.13 aUpperBoundOfIn0( X, xT, xU ), aElementOf0( X, xP ) }.
% 0.43/1.13 { xP = cS1241( xU, xf, xT ) }.
% 0.43/1.13 { ! alpha14( X ), alpha18( X ) }.
% 0.43/1.13 { ! alpha14( X ), aUpperBoundOfIn0( X, xT, xU ) }.
% 0.43/1.13 { ! alpha18( X ), ! aUpperBoundOfIn0( X, xT, xU ), alpha14( X ) }.
% 0.43/1.13 { ! alpha18( X ), alpha22( X ) }.
% 0.43/1.13 { ! alpha18( X ), ! aElementOf0( Y, xT ), sdtlseqdt0( Y, X ) }.
% 0.43/1.13 { ! alpha22( X ), aElementOf0( skol20( Y ), xT ), alpha18( X ) }.
% 0.43/1.13 { ! alpha22( X ), ! sdtlseqdt0( skol20( X ), X ), alpha18( X ) }.
% 0.43/1.13 { ! alpha22( X ), aElementOf0( X, xU ) }.
% 0.43/1.13 { ! alpha22( X ), sdtlseqdt0( sdtlpdtrp0( xf, X ), X ) }.
% 0.43/1.13 { ! aElementOf0( X, xU ), ! sdtlseqdt0( sdtlpdtrp0( xf, X ), X ), alpha22(
% 0.43/1.13 X ) }.
% 0.43/1.13 { alpha15( X ), alpha19( skol21( Y ) ) }.
% 0.43/1.13 { alpha15( X ), aLowerBoundOfIn0( skol21( Y ), xP, xU ) }.
% 0.43/1.13 { alpha15( X ), ! sdtlseqdt0( skol21( X ), X ) }.
% 0.43/1.13 { ! aInfimumOfIn0( X, xP, xU ) }.
% 0.43/1.13 { ! alpha19( X ), aElementOf0( X, xU ) }.
% 0.43/1.13 { ! alpha19( X ), ! aElementOf0( Y, xP ), sdtlseqdt0( X, Y ) }.
% 0.43/1.13 { ! aElementOf0( X, xU ), aElementOf0( skol22( Y ), xP ), alpha19( X ) }.
% 0.43/1.13 { ! aElementOf0( X, xU ), ! sdtlseqdt0( X, skol22( X ) ), alpha19( X ) }.
% 0.43/1.13 { ! alpha15( X ), ! aElementOf0( X, xU ), alpha20( X ) }.
% 0.43/1.13 { aElementOf0( X, xU ), alpha15( X ) }.
% 0.43/1.13 { ! alpha20( X ), alpha15( X ) }.
% 0.43/1.13 { ! alpha20( X ), alpha23( X ) }.
% 0.43/1.13 { ! alpha20( X ), ! aLowerBoundOfIn0( X, xP, xU ) }.
% 0.43/1.13 { ! alpha23( X ), aLowerBoundOfIn0( X, xP, xU ), alpha20( X ) }.
% 0.43/1.13 { ! alpha23( X ), ! aElementOf0( X, xU ), aElementOf0( skol23( Y ), xP ) }
% 0.43/1.13 .
% 0.43/1.13 { ! alpha23( X ), ! aElementOf0( X, xU ), ! sdtlseqdt0( X, skol23( X ) ) }
% 0.43/1.13 .
% 0.43/1.13 { aElementOf0( X, xU ), alpha23( X ) }.
% 0.43/1.13 { ! aElementOf0( Y, xP ), sdtlseqdt0( X, Y ), alpha23( X ) }.
% 0.43/1.13
% 0.43/1.13 percentage equality = 0.033403, percentage horn = 0.819672
% 0.43/1.13 This is a problem with some equality
% 0.43/1.13
% 0.43/1.13
% 0.43/1.13
% 0.43/1.13 Options Used:
% 0.43/1.13
% 0.43/1.13 useres = 1
% 0.43/1.13 useparamod = 1
% 0.43/1.13 useeqrefl = 1
% 0.43/1.13 useeqfact = 1
% 0.43/1.13 usefactor = 1
% 0.43/1.13 usesimpsplitting = 0
% 0.43/1.13 usesimpdemod = 5
% 0.43/1.13 usesimpres = 3
% 0.43/1.13
% 0.43/1.13 resimpinuse = 1000
% 0.43/1.13 resimpclauses = 20000
% 0.43/1.13 substype = eqrewr
% 0.43/1.13 backwardsubs = 1
% 0.43/1.13 selectoldest = 5
% 0.43/1.13
% 0.43/1.13 litorderings [0] = split
% 0.43/1.13 litorderings [1] = extend the termordering, first sorting on arguments
% 0.43/1.13
% 0.43/1.13 termordering = kbo
% 0.43/1.13
% 0.43/1.13 litapriori = 0
% 0.79/1.18 termapriori = 1
% 0.79/1.18 litaposteriori = 0
% 0.79/1.18 termaposteriori = 0
% 0.79/1.18 demodaposteriori = 0
% 0.79/1.18 ordereqreflfact = 0
% 0.79/1.18
% 0.79/1.18 litselect = negord
% 0.79/1.18
% 0.79/1.18 maxweight = 15
% 0.79/1.18 maxdepth = 30000
% 0.79/1.18 maxlength = 115
% 0.79/1.18 maxnrvars = 195
% 0.79/1.18 excuselevel = 1
% 0.79/1.18 increasemaxweight = 1
% 0.79/1.18
% 0.79/1.18 maxselected = 10000000
% 0.79/1.18 maxnrclauses = 10000000
% 0.79/1.18
% 0.79/1.18 showgenerated = 0
% 0.79/1.18 showkept = 0
% 0.79/1.18 showselected = 0
% 0.79/1.18 showdeleted = 0
% 0.79/1.18 showresimp = 1
% 0.79/1.18 showstatus = 2000
% 0.79/1.18
% 0.79/1.18 prologoutput = 0
% 0.79/1.18 nrgoals = 5000000
% 0.79/1.18 totalproof = 1
% 0.79/1.18
% 0.79/1.18 Symbols occurring in the translation:
% 0.79/1.18
% 0.79/1.18 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.79/1.18 . [1, 2] (w:1, o:56, a:1, s:1, b:0),
% 0.79/1.18 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 0.79/1.18 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.79/1.18 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.79/1.18 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.79/1.18 aSet0 [36, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.79/1.18 aElement0 [37, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.79/1.18 aElementOf0 [39, 2] (w:1, o:80, a:1, s:1, b:0),
% 0.79/1.18 isEmpty0 [40, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.79/1.18 aSubsetOf0 [41, 2] (w:1, o:81, a:1, s:1, b:0),
% 0.79/1.18 sdtlseqdt0 [43, 2] (w:1, o:82, a:1, s:1, b:0),
% 0.79/1.18 aLowerBoundOfIn0 [44, 3] (w:1, o:113, a:1, s:1, b:0),
% 0.79/1.18 aUpperBoundOfIn0 [46, 3] (w:1, o:114, a:1, s:1, b:0),
% 0.79/1.18 aInfimumOfIn0 [47, 3] (w:1, o:115, a:1, s:1, b:0),
% 0.79/1.18 aSupremumOfIn0 [48, 3] (w:1, o:116, a:1, s:1, b:0),
% 0.79/1.18 aCompleteLattice0 [49, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.79/1.18 aFunction0 [50, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.79/1.18 szDzozmdt0 [51, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.79/1.18 szRzazndt0 [52, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.79/1.18 isOn0 [53, 2] (w:1, o:83, a:1, s:1, b:0),
% 0.79/1.18 sdtlpdtrp0 [54, 2] (w:1, o:84, a:1, s:1, b:0),
% 0.79/1.18 aFixedPointOf0 [55, 2] (w:1, o:85, a:1, s:1, b:0),
% 0.79/1.18 isMonotone0 [56, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.79/1.18 xU [57, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.79/1.18 xf [59, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.79/1.18 xS [60, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.79/1.18 cS1142 [61, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.79/1.18 xT [62, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.79/1.18 xP [63, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.79/1.18 cS1241 [64, 3] (w:1, o:117, a:1, s:1, b:0),
% 0.79/1.18 alpha1 [65, 2] (w:1, o:86, a:1, s:1, b:1),
% 0.79/1.18 alpha2 [66, 2] (w:1, o:88, a:1, s:1, b:1),
% 0.79/1.18 alpha3 [67, 2] (w:1, o:94, a:1, s:1, b:1),
% 0.79/1.18 alpha4 [68, 3] (w:1, o:118, a:1, s:1, b:1),
% 0.79/1.18 alpha5 [69, 3] (w:1, o:119, a:1, s:1, b:1),
% 0.79/1.18 alpha6 [70, 1] (w:1, o:30, a:1, s:1, b:1),
% 0.79/1.18 alpha7 [71, 3] (w:1, o:120, a:1, s:1, b:1),
% 0.79/1.18 alpha8 [72, 3] (w:1, o:121, a:1, s:1, b:1),
% 0.79/1.18 alpha9 [73, 3] (w:1, o:122, a:1, s:1, b:1),
% 0.79/1.18 alpha10 [74, 2] (w:1, o:87, a:1, s:1, b:1),
% 0.79/1.18 alpha11 [75, 3] (w:1, o:123, a:1, s:1, b:1),
% 0.79/1.18 alpha12 [76, 1] (w:1, o:31, a:1, s:1, b:1),
% 0.79/1.18 alpha13 [77, 1] (w:1, o:32, a:1, s:1, b:1),
% 0.79/1.18 alpha14 [78, 1] (w:1, o:33, a:1, s:1, b:1),
% 0.79/1.18 alpha15 [79, 1] (w:1, o:34, a:1, s:1, b:1),
% 0.79/1.18 alpha16 [80, 1] (w:1, o:35, a:1, s:1, b:1),
% 0.79/1.18 alpha17 [81, 1] (w:1, o:36, a:1, s:1, b:1),
% 0.79/1.18 alpha18 [82, 1] (w:1, o:37, a:1, s:1, b:1),
% 0.79/1.18 alpha19 [83, 1] (w:1, o:38, a:1, s:1, b:1),
% 0.79/1.18 alpha20 [84, 1] (w:1, o:39, a:1, s:1, b:1),
% 0.79/1.18 alpha21 [85, 1] (w:1, o:40, a:1, s:1, b:1),
% 0.79/1.18 alpha22 [86, 1] (w:1, o:41, a:1, s:1, b:1),
% 0.79/1.18 alpha23 [87, 1] (w:1, o:42, a:1, s:1, b:1),
% 0.79/1.18 alpha24 [88, 2] (w:1, o:89, a:1, s:1, b:1),
% 0.79/1.18 alpha25 [89, 1] (w:1, o:43, a:1, s:1, b:1),
% 0.79/1.18 alpha26 [90, 2] (w:1, o:90, a:1, s:1, b:1),
% 0.79/1.18 alpha27 [91, 2] (w:1, o:91, a:1, s:1, b:1),
% 0.79/1.18 alpha28 [92, 2] (w:1, o:92, a:1, s:1, b:1),
% 0.79/1.18 alpha29 [93, 2] (w:1, o:93, a:1, s:1, b:1),
% 0.79/1.18 alpha30 [94, 2] (w:1, o:95, a:1, s:1, b:1),
% 0.79/1.18 alpha31 [95, 2] (w:1, o:96, a:1, s:1, b:1),
% 0.79/1.18 alpha32 [96, 2] (w:1, o:97, a:1, s:1, b:1),
% 0.79/1.18 alpha33 [97, 2] (w:1, o:98, a:1, s:1, b:1),
% 0.79/1.18 alpha34 [98, 2] (w:1, o:99, a:1, s:1, b:1),
% 0.79/1.18 alpha35 [99, 2] (w:1, o:100, a:1, s:1, b:1),
% 0.79/1.18 alpha36 [100, 2] (w:1, o:101, a:1, s:1, b:1),
% 0.79/1.18 skol1 [101, 1] (w:1, o:44, a:1, s:1, b:1),
% 0.79/1.18 skol2 [102, 2] (w:1, o:108, a:1, s:1, b:1),
% 0.79/1.18 skol3 [103, 2] (w:1, o:110, a:1, s:1, b:1),
% 0.79/1.18 skol4 [104, 2] (w:1, o:111, a:1, s:1, b:1),
% 0.79/1.18 skol5 [105, 3] (w:1, o:124, a:1, s:1, b:1),
% 0.79/1.18 skol6 [106, 3] (w:1, o:125, a:1, s:1, b:1),
% 0.79/1.18 skol7 [107, 1] (w:1, o:45, a:1, s:1, b:1),
% 0.79/1.18 skol8 [108, 2] (w:1, o:112, a:1, s:1, b:1),
% 0.79/1.18 skol9 [109, 1] (w:1, o:46, a:1, s:1, b:1),
% 0.79/1.18 skol10 [110, 1] (w:1, o:47, a:1, s:1, b:1),
% 0.79/1.18 skol11 [111, 2] (w:1, o:102, a:1, s:1, b:1),
% 0.79/1.18 skol12 [112, 2] (w:1, o:103, a:1, s:1, b:1),
% 0.79/1.18 skol13 [113, 2] (w:1, o:104, a:1, s:1, b:1),
% 0.79/1.18 skol14 [114, 1] (w:1, o:48, a:1, s:1, b:1),
% 0.79/1.18 skol15 [115, 2] (w:1, o:105, a:1, s:1, b:1),
% 0.79/1.18 skol16 [116, 2] (w:1, o:106, a:1, s:1, b:1),
% 0.79/1.18 skol17 [117, 2] (w:1, o:107, a:1, s:1, b:1),
% 0.79/1.18 skol18 [118, 1] (w:1, o:49, a:1, s:1, b:1),
% 0.79/1.18 skol19 [119, 1] (w:1, o:50, a:1, s:1, b:1),
% 0.79/1.18 skol20 [120, 1] (w:1, o:51, a:1, s:1, b:1),
% 0.79/1.18 skol21 [121, 1] (w:1, o:52, a:1, s:1, b:1),
% 0.79/1.18 skol22 [122, 1] (w:1, o:53, a:1, s:1, b:1),
% 0.79/1.18 skol23 [123, 1] (w:1, o:54, a:1, s:1, b:1),
% 0.79/1.18 skol24 [124, 2] (w:1, o:109, a:1, s:1, b:1),
% 0.79/1.18 skol25 [125, 1] (w:1, o:55, a:1, s:1, b:1).
% 0.79/1.18
% 0.79/1.18
% 0.79/1.18 Starting Search:
% 0.79/1.18
% 0.79/1.18 *** allocated 15000 integers for clauses
% 0.79/1.18 *** allocated 22500 integers for clauses
% 0.79/1.18 *** allocated 33750 integers for clauses
% 0.79/1.18 *** allocated 15000 integers for termspace/termends
% 0.79/1.18 *** allocated 50625 integers for clauses
% 0.79/1.18 *** allocated 22500 integers for termspace/termends
% 0.79/1.18 Resimplifying inuse:
% 0.79/1.18 Done
% 0.79/1.18
% 0.79/1.18 *** allocated 75937 integers for clauses
% 0.79/1.18 *** allocated 33750 integers for termspace/termends
% 0.79/1.18 *** allocated 113905 integers for clauses
% 0.79/1.18
% 0.79/1.18 Bliksems!, er is een bewijs:
% 0.79/1.18 % SZS status Theorem
% 0.79/1.18 % SZS output start Refutation
% 0.79/1.18
% 0.79/1.18 (6) {G0,W10,D2,L4,V2,M4} I { ! aSet0( X ), ! aSet0( Y ), ! alpha1( X, Y ),
% 0.79/1.18 aSubsetOf0( Y, X ) }.
% 0.79/1.18 (8) {G0,W8,D3,L2,V3,M2} I { aElementOf0( skol2( Z, Y ), Y ), alpha1( X, Y )
% 0.79/1.18 }.
% 0.79/1.18 (9) {G0,W8,D3,L2,V2,M2} I { ! aElementOf0( skol2( X, Y ), X ), alpha1( X, Y
% 0.79/1.18 ) }.
% 0.79/1.18 (46) {G0,W4,D2,L2,V1,M2} I { ! aCompleteLattice0( X ), alpha6( X ) }.
% 0.79/1.18 (48) {G0,W8,D2,L3,V2,M3} I { ! alpha6( X ), ! aSubsetOf0( Y, X ), alpha10(
% 0.79/1.18 X, Y ) }.
% 0.79/1.18 (51) {G0,W9,D3,L2,V2,M2} I { ! alpha10( X, Y ), aInfimumOfIn0( skol8( X, Y
% 0.79/1.18 ), Y, X ) }.
% 0.79/1.18 (72) {G0,W2,D2,L1,V0,M1} I { aSet0( xU ) }.
% 0.79/1.18 (75) {G0,W2,D2,L1,V0,M1} I { aCompleteLattice0( xU ) }.
% 0.79/1.18 (126) {G0,W5,D2,L2,V1,M2} I { ! alpha25( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (127) {G0,W5,D2,L2,V1,M2} I;f { ! aElementOf0( X, xU ), alpha25( X ) }.
% 0.79/1.18 (128) {G0,W5,D2,L2,V1,M2} I { ! alpha16( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (129) {G0,W5,D2,L2,V1,M2} I;f { ! aElementOf0( X, xU ), alpha16( X ) }.
% 0.79/1.18 (149) {G0,W2,D2,L1,V0,M1} I { aSet0( xP ) }.
% 0.79/1.18 (150) {G0,W5,D2,L2,V1,M2} I { ! aElementOf0( X, xP ), alpha14( X ) }.
% 0.79/1.18 (155) {G0,W4,D2,L2,V1,M2} I { ! alpha14( X ), alpha18( X ) }.
% 0.79/1.18 (158) {G0,W4,D2,L2,V1,M2} I { ! alpha18( X ), alpha22( X ) }.
% 0.79/1.18 (162) {G0,W5,D2,L2,V1,M2} I { ! alpha22( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (168) {G0,W4,D2,L1,V1,M1} I { ! aInfimumOfIn0( X, xP, xU ) }.
% 0.79/1.18 (215) {G1,W2,D2,L1,V0,M1} R(46,75) { alpha6( xU ) }.
% 0.79/1.18 (501) {G1,W5,D2,L2,V1,M2} R(162,158) { aElementOf0( X, xU ), ! alpha18( X )
% 0.79/1.18 }.
% 0.79/1.18 (625) {G1,W5,D2,L2,V1,M2} R(150,155) { ! aElementOf0( X, xP ), alpha18( X )
% 0.79/1.18 }.
% 0.79/1.18 (891) {G2,W4,D2,L2,V1,M2} R(129,501) { alpha16( X ), ! alpha18( X ) }.
% 0.79/1.18 (938) {G3,W5,D2,L2,V1,M2} R(891,625) { alpha16( X ), ! aElementOf0( X, xP )
% 0.79/1.18 }.
% 0.79/1.18 (987) {G1,W4,D2,L2,V1,M2} R(127,128) { alpha25( X ), ! alpha16( X ) }.
% 0.79/1.18 (1005) {G4,W5,D2,L2,V1,M2} R(987,938) { alpha25( X ), ! aElementOf0( X, xP
% 0.79/1.18 ) }.
% 0.79/1.18 (1622) {G1,W3,D2,L1,V0,M1} R(51,168) { ! alpha10( xU, xP ) }.
% 0.79/1.18 (1626) {G2,W3,D2,L1,V0,M1} R(1622,48);r(215) { ! aSubsetOf0( xP, xU ) }.
% 0.79/1.18 (1627) {G3,W5,D2,L2,V0,M2} R(1626,6);r(72) { ! aSet0( xP ), ! alpha1( xU,
% 0.79/1.18 xP ) }.
% 0.79/1.18 (1630) {G4,W3,D2,L1,V0,M1} S(1627);r(149) { ! alpha1( xU, xP ) }.
% 0.79/1.18 (1634) {G5,W5,D3,L1,V1,M1} R(1630,8) { aElementOf0( skol2( X, xP ), xP )
% 0.79/1.18 }.
% 0.79/1.18 (1783) {G6,W4,D3,L1,V1,M1} R(1634,1005) { alpha25( skol2( X, xP ) ) }.
% 0.79/1.18 (1798) {G7,W5,D3,L1,V1,M1} R(1783,126) { aElementOf0( skol2( X, xP ), xU )
% 0.79/1.18 }.
% 0.79/1.18 (1861) {G8,W0,D0,L0,V0,M0} R(1798,9);r(1630) { }.
% 0.79/1.18
% 0.79/1.18
% 0.79/1.18 % SZS output end Refutation
% 0.79/1.18 found a proof!
% 0.79/1.18
% 0.79/1.18
% 0.79/1.18 Unprocessed initial clauses:
% 0.79/1.18
% 0.79/1.18 (1863) {G0,W1,D1,L1,V0,M1} { && }.
% 0.79/1.18 (1864) {G0,W1,D1,L1,V0,M1} { && }.
% 0.79/1.18 (1865) {G0,W7,D2,L3,V2,M3} { ! aSet0( X ), ! aElementOf0( Y, X ),
% 0.79/1.18 aElement0( Y ) }.
% 0.79/1.18 (1866) {G0,W7,D2,L3,V2,M3} { ! aSet0( X ), ! isEmpty0( X ), ! aElementOf0
% 0.79/1.18 ( Y, X ) }.
% 0.79/1.18 (1867) {G0,W8,D3,L3,V1,M3} { ! aSet0( X ), aElementOf0( skol1( X ), X ),
% 0.79/1.18 isEmpty0( X ) }.
% 0.79/1.18 (1868) {G0,W7,D2,L3,V2,M3} { ! aSet0( X ), ! aSubsetOf0( Y, X ), aSet0( Y
% 0.79/1.18 ) }.
% 0.79/1.18 (1869) {G0,W8,D2,L3,V2,M3} { ! aSet0( X ), ! aSubsetOf0( Y, X ), alpha1( X
% 0.79/1.18 , Y ) }.
% 0.79/1.18 (1870) {G0,W10,D2,L4,V2,M4} { ! aSet0( X ), ! aSet0( Y ), ! alpha1( X, Y )
% 0.79/1.18 , aSubsetOf0( Y, X ) }.
% 0.79/1.18 (1871) {G0,W9,D2,L3,V3,M3} { ! alpha1( X, Y ), ! aElementOf0( Z, Y ),
% 0.79/1.18 aElementOf0( Z, X ) }.
% 0.79/1.18 (1872) {G0,W8,D3,L2,V3,M2} { aElementOf0( skol2( Z, Y ), Y ), alpha1( X, Y
% 0.79/1.18 ) }.
% 0.79/1.18 (1873) {G0,W8,D3,L2,V2,M2} { ! aElementOf0( skol2( X, Y ), X ), alpha1( X
% 0.79/1.18 , Y ) }.
% 0.79/1.18 (1874) {G0,W1,D1,L1,V0,M1} { && }.
% 0.79/1.18 (1875) {G0,W5,D2,L2,V1,M2} { ! aElement0( X ), sdtlseqdt0( X, X ) }.
% 0.79/1.18 (1876) {G0,W13,D2,L5,V2,M5} { ! aElement0( X ), ! aElement0( Y ), !
% 0.79/1.18 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 0.79/1.18 (1877) {G0,W15,D2,L6,V3,M6} { ! aElement0( X ), ! aElement0( Y ), !
% 0.79/1.18 aElement0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X
% 0.79/1.18 , Z ) }.
% 0.79/1.18 (1878) {G0,W12,D2,L4,V3,M4} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aLowerBoundOfIn0( Z, Y, X ), aElementOf0( Z, X ) }.
% 0.79/1.18 (1879) {G0,W12,D2,L4,V3,M4} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aLowerBoundOfIn0( Z, Y, X ), alpha2( Y, Z ) }.
% 0.79/1.18 (1880) {G0,W15,D2,L5,V3,M5} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aElementOf0( Z, X ), ! alpha2( Y, Z ), aLowerBoundOfIn0( Z, Y, X ) }.
% 0.79/1.18 (1881) {G0,W9,D2,L3,V3,M3} { ! alpha2( X, Y ), ! aElementOf0( Z, X ),
% 0.79/1.18 sdtlseqdt0( Y, Z ) }.
% 0.79/1.18 (1882) {G0,W8,D3,L2,V3,M2} { ! sdtlseqdt0( Y, skol3( Z, Y ) ), alpha2( X,
% 0.79/1.18 Y ) }.
% 0.79/1.18 (1883) {G0,W8,D3,L2,V2,M2} { aElementOf0( skol3( X, Y ), X ), alpha2( X, Y
% 0.79/1.18 ) }.
% 0.79/1.18 (1884) {G0,W12,D2,L4,V3,M4} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aUpperBoundOfIn0( Z, Y, X ), aElementOf0( Z, X ) }.
% 0.79/1.18 (1885) {G0,W12,D2,L4,V3,M4} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aUpperBoundOfIn0( Z, Y, X ), alpha3( Y, Z ) }.
% 0.79/1.18 (1886) {G0,W15,D2,L5,V3,M5} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aElementOf0( Z, X ), ! alpha3( Y, Z ), aUpperBoundOfIn0( Z, Y, X ) }.
% 0.79/1.18 (1887) {G0,W9,D2,L3,V3,M3} { ! alpha3( X, Y ), ! aElementOf0( Z, X ),
% 0.79/1.18 sdtlseqdt0( Z, Y ) }.
% 0.79/1.18 (1888) {G0,W8,D3,L2,V3,M2} { ! sdtlseqdt0( skol4( Z, Y ), Y ), alpha3( X,
% 0.79/1.18 Y ) }.
% 0.79/1.18 (1889) {G0,W8,D3,L2,V2,M2} { aElementOf0( skol4( X, Y ), X ), alpha3( X, Y
% 0.79/1.18 ) }.
% 0.79/1.18 (1890) {G0,W12,D2,L4,V3,M4} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aInfimumOfIn0( Z, Y, X ), aElementOf0( Z, X ) }.
% 0.79/1.18 (1891) {G0,W13,D2,L4,V3,M4} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aInfimumOfIn0( Z, Y, X ), alpha4( X, Y, Z ) }.
% 0.79/1.18 (1892) {G0,W16,D2,L5,V3,M5} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aElementOf0( Z, X ), ! alpha4( X, Y, Z ), aInfimumOfIn0( Z, Y, X ) }.
% 0.79/1.18 (1893) {G0,W8,D2,L2,V3,M2} { ! alpha4( X, Y, Z ), aLowerBoundOfIn0( Z, Y,
% 0.79/1.18 X ) }.
% 0.79/1.18 (1894) {G0,W8,D2,L2,V3,M2} { ! alpha4( X, Y, Z ), alpha8( X, Y, Z ) }.
% 0.79/1.18 (1895) {G0,W12,D2,L3,V3,M3} { ! aLowerBoundOfIn0( Z, Y, X ), ! alpha8( X,
% 0.79/1.18 Y, Z ), alpha4( X, Y, Z ) }.
% 0.79/1.18 (1896) {G0,W11,D2,L3,V4,M3} { ! alpha8( X, Y, Z ), ! aLowerBoundOfIn0( T,
% 0.79/1.18 Y, X ), sdtlseqdt0( T, Z ) }.
% 0.79/1.18 (1897) {G0,W10,D3,L2,V5,M2} { ! sdtlseqdt0( skol5( T, U, Z ), Z ), alpha8
% 0.79/1.18 ( X, Y, Z ) }.
% 0.79/1.18 (1898) {G0,W11,D3,L2,V3,M2} { aLowerBoundOfIn0( skol5( X, Y, Z ), Y, X ),
% 0.79/1.18 alpha8( X, Y, Z ) }.
% 0.79/1.18 (1899) {G0,W12,D2,L4,V3,M4} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aSupremumOfIn0( Z, Y, X ), aElementOf0( Z, X ) }.
% 0.79/1.18 (1900) {G0,W13,D2,L4,V3,M4} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aSupremumOfIn0( Z, Y, X ), alpha5( X, Y, Z ) }.
% 0.79/1.18 (1901) {G0,W16,D2,L5,V3,M5} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aElementOf0( Z, X ), ! alpha5( X, Y, Z ), aSupremumOfIn0( Z, Y, X ) }.
% 0.79/1.18 (1902) {G0,W8,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), aUpperBoundOfIn0( Z, Y,
% 0.79/1.18 X ) }.
% 0.79/1.18 (1903) {G0,W8,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), alpha9( X, Y, Z ) }.
% 0.79/1.18 (1904) {G0,W12,D2,L3,V3,M3} { ! aUpperBoundOfIn0( Z, Y, X ), ! alpha9( X,
% 0.79/1.18 Y, Z ), alpha5( X, Y, Z ) }.
% 0.79/1.18 (1905) {G0,W11,D2,L3,V4,M3} { ! alpha9( X, Y, Z ), ! aUpperBoundOfIn0( T,
% 0.79/1.18 Y, X ), sdtlseqdt0( Z, T ) }.
% 0.79/1.18 (1906) {G0,W10,D3,L2,V5,M2} { ! sdtlseqdt0( Z, skol6( T, U, Z ) ), alpha9
% 0.79/1.18 ( X, Y, Z ) }.
% 0.79/1.18 (1907) {G0,W11,D3,L2,V3,M2} { aUpperBoundOfIn0( skol6( X, Y, Z ), Y, X ),
% 0.79/1.18 alpha9( X, Y, Z ) }.
% 0.79/1.18 (1908) {G0,W16,D2,L5,V4,M5} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aSupremumOfIn0( Z, Y, X ), ! aSupremumOfIn0( T, Y, X ), Z = T }.
% 0.79/1.18 (1909) {G0,W16,D2,L5,V4,M5} { ! aSet0( X ), ! aSubsetOf0( Y, X ), !
% 0.79/1.18 aInfimumOfIn0( Z, Y, X ), ! aInfimumOfIn0( T, Y, X ), Z = T }.
% 0.79/1.18 (1910) {G0,W4,D2,L2,V1,M2} { ! aCompleteLattice0( X ), aSet0( X ) }.
% 0.79/1.18 (1911) {G0,W4,D2,L2,V1,M2} { ! aCompleteLattice0( X ), alpha6( X ) }.
% 0.79/1.18 (1912) {G0,W6,D2,L3,V1,M3} { ! aSet0( X ), ! alpha6( X ),
% 0.79/1.18 aCompleteLattice0( X ) }.
% 0.79/1.18 (1913) {G0,W8,D2,L3,V2,M3} { ! alpha6( X ), ! aSubsetOf0( Y, X ), alpha10
% 0.79/1.18 ( X, Y ) }.
% 0.79/1.18 (1914) {G0,W6,D3,L2,V1,M2} { aSubsetOf0( skol7( X ), X ), alpha6( X ) }.
% 0.79/1.18 (1915) {G0,W6,D3,L2,V1,M2} { ! alpha10( X, skol7( X ) ), alpha6( X ) }.
% 0.79/1.18 (1916) {G0,W9,D3,L2,V2,M2} { ! alpha10( X, Y ), aInfimumOfIn0( skol8( X, Y
% 0.79/1.18 ), Y, X ) }.
% 0.79/1.18 (1917) {G0,W9,D3,L2,V2,M2} { ! alpha10( X, Y ), aSupremumOfIn0( skol24( X
% 0.79/1.18 , Y ), Y, X ) }.
% 0.79/1.18 (1918) {G0,W11,D2,L3,V4,M3} { ! aInfimumOfIn0( Z, Y, X ), ! aSupremumOfIn0
% 0.79/1.18 ( T, Y, X ), alpha10( X, Y ) }.
% 0.79/1.18 (1919) {G0,W1,D1,L1,V0,M1} { && }.
% 0.79/1.18 (1920) {G0,W5,D3,L2,V1,M2} { ! aFunction0( X ), aSet0( szDzozmdt0( X ) )
% 0.79/1.18 }.
% 0.79/1.18 (1921) {G0,W5,D3,L2,V1,M2} { ! aFunction0( X ), aSet0( szRzazndt0( X ) )
% 0.79/1.18 }.
% 0.79/1.18 (1922) {G0,W12,D3,L4,V2,M4} { ! aFunction0( X ), ! aSet0( Y ), ! isOn0( X
% 0.79/1.18 , Y ), szDzozmdt0( X ) = szRzazndt0( X ) }.
% 0.79/1.18 (1923) {G0,W11,D3,L4,V2,M4} { ! aFunction0( X ), ! aSet0( Y ), ! isOn0( X
% 0.79/1.18 , Y ), szRzazndt0( X ) = Y }.
% 0.79/1.18 (1924) {G0,W16,D3,L5,V2,M5} { ! aFunction0( X ), ! aSet0( Y ), !
% 0.79/1.18 szDzozmdt0( X ) = szRzazndt0( X ), ! szRzazndt0( X ) = Y, isOn0( X, Y )
% 0.79/1.18 }.
% 0.79/1.18 (1925) {G0,W12,D3,L3,V2,M3} { ! aFunction0( X ), ! aElementOf0( Y,
% 0.79/1.18 szDzozmdt0( X ) ), aElementOf0( sdtlpdtrp0( X, Y ), szRzazndt0( X ) ) }.
% 0.79/1.18 (1926) {G0,W9,D3,L3,V2,M3} { ! aFunction0( X ), ! aFixedPointOf0( Y, X ),
% 0.79/1.18 aElementOf0( Y, szDzozmdt0( X ) ) }.
% 0.79/1.18 (1927) {G0,W10,D3,L3,V2,M3} { ! aFunction0( X ), ! aFixedPointOf0( Y, X )
% 0.79/1.18 , sdtlpdtrp0( X, Y ) = Y }.
% 0.79/1.18 (1928) {G0,W14,D3,L4,V2,M4} { ! aFunction0( X ), ! aElementOf0( Y,
% 0.79/1.18 szDzozmdt0( X ) ), ! sdtlpdtrp0( X, Y ) = Y, aFixedPointOf0( Y, X ) }.
% 0.79/1.18 (1929) {G0,W12,D2,L4,V3,M4} { ! aFunction0( X ), ! isMonotone0( X ), !
% 0.79/1.18 alpha7( X, Y, Z ), alpha11( X, Y, Z ) }.
% 0.79/1.18 (1930) {G0,W10,D3,L3,V1,M3} { ! aFunction0( X ), alpha7( X, skol9( X ),
% 0.79/1.18 skol25( X ) ), isMonotone0( X ) }.
% 0.79/1.18 (1931) {G0,W10,D3,L3,V1,M3} { ! aFunction0( X ), ! alpha11( X, skol9( X )
% 0.79/1.18 , skol25( X ) ), isMonotone0( X ) }.
% 0.79/1.18 (1932) {G0,W14,D3,L3,V3,M3} { ! alpha11( X, Y, Z ), ! sdtlseqdt0( Y, Z ),
% 0.79/1.18 sdtlseqdt0( sdtlpdtrp0( X, Y ), sdtlpdtrp0( X, Z ) ) }.
% 0.79/1.18 (1933) {G0,W7,D2,L2,V3,M2} { sdtlseqdt0( Y, Z ), alpha11( X, Y, Z ) }.
% 0.79/1.18 (1934) {G0,W11,D3,L2,V3,M2} { ! sdtlseqdt0( sdtlpdtrp0( X, Y ), sdtlpdtrp0
% 0.79/1.18 ( X, Z ) ), alpha11( X, Y, Z ) }.
% 0.79/1.18 (1935) {G0,W8,D3,L2,V3,M2} { ! alpha7( X, Y, Z ), aElementOf0( Y,
% 0.79/1.18 szDzozmdt0( X ) ) }.
% 0.79/1.18 (1936) {G0,W8,D3,L2,V3,M2} { ! alpha7( X, Y, Z ), aElementOf0( Z,
% 0.79/1.18 szDzozmdt0( X ) ) }.
% 0.79/1.18 (1937) {G0,W12,D3,L3,V3,M3} { ! aElementOf0( Y, szDzozmdt0( X ) ), !
% 0.79/1.18 aElementOf0( Z, szDzozmdt0( X ) ), alpha7( X, Y, Z ) }.
% 0.79/1.18 (1938) {G0,W2,D2,L1,V0,M1} { aSet0( xU ) }.
% 0.79/1.18 (1939) {G0,W6,D3,L2,V1,M2} { alpha12( X ), alpha29( X, skol10( X ) ) }.
% 0.79/1.18 (1940) {G0,W4,D2,L2,V1,M2} { alpha12( X ), alpha21( X ) }.
% 0.79/1.18 (1941) {G0,W2,D2,L1,V0,M1} { aCompleteLattice0( xU ) }.
% 0.79/1.18 (1942) {G0,W2,D2,L1,V0,M1} { aFunction0( xf ) }.
% 0.79/1.18 (1943) {G0,W18,D3,L4,V2,M4} { ! aElementOf0( X, szDzozmdt0( xf ) ), !
% 0.79/1.18 aElementOf0( Y, szDzozmdt0( xf ) ), ! sdtlseqdt0( X, Y ), sdtlseqdt0(
% 0.79/1.18 sdtlpdtrp0( xf, X ), sdtlpdtrp0( xf, Y ) ) }.
% 0.79/1.18 (1944) {G0,W2,D2,L1,V0,M1} { isMonotone0( xf ) }.
% 0.79/1.18 (1945) {G0,W5,D3,L1,V0,M1} { szDzozmdt0( xf ) = szRzazndt0( xf ) }.
% 0.79/1.18 (1946) {G0,W4,D3,L1,V0,M1} { szRzazndt0( xf ) = xU }.
% 0.79/1.18 (1947) {G0,W3,D2,L1,V0,M1} { isOn0( xf, xU ) }.
% 0.79/1.18 (1948) {G0,W6,D2,L2,V2,M2} { ! alpha29( X, Y ), alpha24( X, Y ) }.
% 0.79/1.18 (1949) {G0,W6,D2,L2,V2,M2} { ! alpha29( X, Y ), alpha26( X, Y ) }.
% 0.79/1.18 (1950) {G0,W7,D2,L2,V2,M2} { ! alpha29( X, Y ), aInfimumOfIn0( Y, X, xU )
% 0.79/1.18 }.
% 0.79/1.18 (1951) {G0,W13,D2,L4,V2,M4} { ! alpha24( X, Y ), ! alpha26( X, Y ), !
% 0.79/1.18 aInfimumOfIn0( Y, X, xU ), alpha29( X, Y ) }.
% 0.79/1.18 (1952) {G0,W9,D2,L3,V3,M3} { ! alpha26( X, Y ), alpha30( X, Z ),
% 0.79/1.18 sdtlseqdt0( Z, Y ) }.
% 0.79/1.18 (1953) {G0,W8,D3,L2,V3,M2} { ! sdtlseqdt0( skol11( Z, Y ), Y ), alpha26( X
% 0.79/1.18 , Y ) }.
% 0.79/1.18 (1954) {G0,W8,D3,L2,V2,M2} { ! alpha30( X, skol11( X, Y ) ), alpha26( X, Y
% 0.79/1.18 ) }.
% 0.79/1.18 (1955) {G0,W6,D2,L2,V2,M2} { ! alpha30( X, Y ), alpha32( X, Y ) }.
% 0.79/1.18 (1956) {G0,W7,D2,L2,V2,M2} { ! alpha30( X, Y ), ! aLowerBoundOfIn0( Y, X,
% 0.79/1.18 xU ) }.
% 0.79/1.18 (1957) {G0,W10,D2,L3,V2,M3} { ! alpha32( X, Y ), aLowerBoundOfIn0( Y, X,
% 0.79/1.18 xU ), alpha30( X, Y ) }.
% 0.79/1.18 (1958) {G0,W11,D3,L3,V3,M3} { ! alpha32( X, Y ), ! aElementOf0( Y, xU ), !
% 0.79/1.18 sdtlseqdt0( Y, skol12( Z, Y ) ) }.
% 0.79/1.18 (1959) {G0,W11,D3,L3,V2,M3} { ! alpha32( X, Y ), ! aElementOf0( Y, xU ),
% 0.79/1.18 aElementOf0( skol12( X, Y ), X ) }.
% 0.79/1.18 (1960) {G0,W6,D2,L2,V2,M2} { aElementOf0( Y, xU ), alpha32( X, Y ) }.
% 0.79/1.18 (1961) {G0,W9,D2,L3,V3,M3} { ! aElementOf0( Z, X ), sdtlseqdt0( Y, Z ),
% 0.79/1.18 alpha32( X, Y ) }.
% 0.79/1.18 (1962) {G0,W6,D2,L2,V2,M2} { ! alpha24( X, Y ), alpha27( X, Y ) }.
% 0.79/1.18 (1963) {G0,W7,D2,L2,V2,M2} { ! alpha24( X, Y ), aLowerBoundOfIn0( Y, X, xU
% 0.79/1.18 ) }.
% 0.79/1.18 (1964) {G0,W10,D2,L3,V2,M3} { ! alpha27( X, Y ), ! aLowerBoundOfIn0( Y, X
% 0.79/1.18 , xU ), alpha24( X, Y ) }.
% 0.79/1.18 (1965) {G0,W5,D2,L2,V2,M2} { ! alpha27( X, Y ), alpha16( Y ) }.
% 0.79/1.18 (1966) {G0,W9,D2,L3,V3,M3} { ! alpha27( X, Y ), ! aElementOf0( Z, X ),
% 0.79/1.18 sdtlseqdt0( Y, Z ) }.
% 0.79/1.18 (1967) {G0,W10,D3,L3,V3,M3} { ! alpha16( Y ), ! sdtlseqdt0( Y, skol13( Z,
% 0.79/1.18 Y ) ), alpha27( X, Y ) }.
% 0.79/1.18 (1968) {G0,W10,D3,L3,V2,M3} { ! alpha16( Y ), aElementOf0( skol13( X, Y )
% 0.79/1.18 , X ), alpha27( X, Y ) }.
% 0.79/1.18 (1969) {G0,W6,D3,L2,V1,M2} { ! alpha21( X ), alpha28( X, skol14( X ) ) }.
% 0.79/1.18 (1970) {G0,W7,D3,L2,V1,M2} { ! alpha21( X ), aSupremumOfIn0( skol14( X ),
% 0.79/1.18 X, xU ) }.
% 0.79/1.18 (1971) {G0,W9,D2,L3,V2,M3} { ! alpha28( X, Y ), ! aSupremumOfIn0( Y, X, xU
% 0.79/1.18 ), alpha21( X ) }.
% 0.79/1.18 (1972) {G0,W6,D2,L2,V2,M2} { ! alpha28( X, Y ), alpha31( X, Y ) }.
% 0.79/1.18 (1973) {G0,W6,D2,L2,V2,M2} { ! alpha28( X, Y ), alpha33( X, Y ) }.
% 0.79/1.18 (1974) {G0,W9,D2,L3,V2,M3} { ! alpha31( X, Y ), ! alpha33( X, Y ), alpha28
% 0.79/1.18 ( X, Y ) }.
% 0.79/1.18 (1975) {G0,W9,D2,L3,V3,M3} { ! alpha33( X, Y ), alpha35( X, Z ),
% 0.79/1.18 sdtlseqdt0( Y, Z ) }.
% 0.79/1.18 (1976) {G0,W8,D3,L2,V3,M2} { ! sdtlseqdt0( Y, skol15( Z, Y ) ), alpha33( X
% 0.79/1.18 , Y ) }.
% 0.79/1.18 (1977) {G0,W8,D3,L2,V2,M2} { ! alpha35( X, skol15( X, Y ) ), alpha33( X, Y
% 0.79/1.18 ) }.
% 0.79/1.18 (1978) {G0,W6,D2,L2,V2,M2} { ! alpha35( X, Y ), alpha36( X, Y ) }.
% 0.79/1.18 (1979) {G0,W7,D2,L2,V2,M2} { ! alpha35( X, Y ), ! aUpperBoundOfIn0( Y, X,
% 0.79/1.18 xU ) }.
% 0.79/1.18 (1980) {G0,W10,D2,L3,V2,M3} { ! alpha36( X, Y ), aUpperBoundOfIn0( Y, X,
% 0.79/1.18 xU ), alpha35( X, Y ) }.
% 0.79/1.18 (1981) {G0,W11,D3,L3,V3,M3} { ! alpha36( X, Y ), ! aElementOf0( Y, xU ), !
% 0.79/1.18 sdtlseqdt0( skol16( Z, Y ), Y ) }.
% 0.79/1.18 (1982) {G0,W11,D3,L3,V2,M3} { ! alpha36( X, Y ), ! aElementOf0( Y, xU ),
% 0.79/1.18 aElementOf0( skol16( X, Y ), X ) }.
% 0.79/1.18 (1983) {G0,W6,D2,L2,V2,M2} { aElementOf0( Y, xU ), alpha36( X, Y ) }.
% 0.79/1.18 (1984) {G0,W9,D2,L3,V3,M3} { ! aElementOf0( Z, X ), sdtlseqdt0( Z, Y ),
% 0.79/1.18 alpha36( X, Y ) }.
% 0.79/1.18 (1985) {G0,W6,D2,L2,V2,M2} { ! alpha31( X, Y ), alpha34( X, Y ) }.
% 0.79/1.18 (1986) {G0,W7,D2,L2,V2,M2} { ! alpha31( X, Y ), aUpperBoundOfIn0( Y, X, xU
% 0.79/1.18 ) }.
% 0.79/1.18 (1987) {G0,W10,D2,L3,V2,M3} { ! alpha34( X, Y ), ! aUpperBoundOfIn0( Y, X
% 0.79/1.18 , xU ), alpha31( X, Y ) }.
% 0.79/1.18 (1988) {G0,W5,D2,L2,V2,M2} { ! alpha34( X, Y ), alpha25( Y ) }.
% 0.79/1.18 (1989) {G0,W9,D2,L3,V3,M3} { ! alpha34( X, Y ), ! aElementOf0( Z, X ),
% 0.79/1.18 sdtlseqdt0( Z, Y ) }.
% 0.79/1.18 (1990) {G0,W10,D3,L3,V3,M3} { ! alpha25( Y ), ! sdtlseqdt0( skol17( Z, Y )
% 0.79/1.18 , Y ), alpha34( X, Y ) }.
% 0.79/1.18 (1991) {G0,W10,D3,L3,V2,M3} { ! alpha25( Y ), aElementOf0( skol17( X, Y )
% 0.79/1.18 , X ), alpha34( X, Y ) }.
% 0.79/1.18 (1992) {G0,W5,D2,L2,V1,M2} { ! alpha25( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (1993) {G0,W5,D2,L2,V1,M2} { ! alpha25( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (1994) {G0,W8,D2,L3,V1,M3} { ! aElementOf0( X, xU ), ! aElementOf0( X, xU
% 0.79/1.18 ), alpha25( X ) }.
% 0.79/1.18 (1995) {G0,W5,D2,L2,V1,M2} { ! alpha16( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (1996) {G0,W5,D2,L2,V1,M2} { ! alpha16( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (1997) {G0,W8,D2,L3,V1,M3} { ! aElementOf0( X, xU ), ! aElementOf0( X, xU
% 0.79/1.18 ), alpha16( X ) }.
% 0.79/1.18 (1998) {G0,W4,D2,L2,V1,M2} { ! alpha12( X ), alpha17( X ) }.
% 0.79/1.18 (1999) {G0,W5,D2,L2,V1,M2} { ! alpha12( X ), ! aSubsetOf0( X, xU ) }.
% 0.79/1.18 (2000) {G0,W7,D2,L3,V1,M3} { ! alpha17( X ), aSubsetOf0( X, xU ), alpha12
% 0.79/1.18 ( X ) }.
% 0.79/1.18 (2001) {G0,W8,D3,L3,V2,M3} { ! alpha17( X ), ! aSet0( X ), ! aElementOf0(
% 0.79/1.18 skol18( Y ), xU ) }.
% 0.79/1.18 (2002) {G0,W8,D3,L3,V1,M3} { ! alpha17( X ), ! aSet0( X ), aElementOf0(
% 0.79/1.18 skol18( X ), X ) }.
% 0.79/1.18 (2003) {G0,W4,D2,L2,V1,M2} { aSet0( X ), alpha17( X ) }.
% 0.79/1.18 (2004) {G0,W8,D2,L3,V2,M3} { ! aElementOf0( Y, X ), aElementOf0( Y, xU ),
% 0.79/1.18 alpha17( X ) }.
% 0.79/1.18 (2005) {G0,W2,D2,L1,V0,M1} { aSet0( xS ) }.
% 0.79/1.18 (2006) {G0,W5,D2,L2,V1,M2} { ! aElementOf0( X, xS ), alpha13( X ) }.
% 0.79/1.18 (2007) {G0,W12,D3,L3,V1,M3} { ! aElementOf0( X, szDzozmdt0( xf ) ), !
% 0.79/1.18 sdtlpdtrp0( xf, X ) = X, aElementOf0( X, xS ) }.
% 0.79/1.18 (2008) {G0,W6,D2,L2,V1,M2} { ! aFixedPointOf0( X, xf ), aElementOf0( X, xS
% 0.79/1.18 ) }.
% 0.79/1.18 (2009) {G0,W4,D3,L1,V0,M1} { xS = cS1142( xf ) }.
% 0.79/1.18 (2010) {G0,W6,D3,L2,V1,M2} { ! alpha13( X ), aElementOf0( X, szDzozmdt0(
% 0.79/1.18 xf ) ) }.
% 0.79/1.18 (2011) {G0,W7,D3,L2,V1,M2} { ! alpha13( X ), sdtlpdtrp0( xf, X ) = X }.
% 0.79/1.18 (2012) {G0,W5,D2,L2,V1,M2} { ! alpha13( X ), aFixedPointOf0( X, xf ) }.
% 0.79/1.18 (2013) {G0,W14,D3,L4,V1,M4} { ! aElementOf0( X, szDzozmdt0( xf ) ), !
% 0.79/1.18 sdtlpdtrp0( xf, X ) = X, ! aFixedPointOf0( X, xf ), alpha13( X ) }.
% 0.79/1.18 (2014) {G0,W2,D2,L1,V0,M1} { aSet0( xT ) }.
% 0.79/1.18 (2015) {G0,W6,D2,L2,V1,M2} { ! aElementOf0( X, xT ), aElementOf0( X, xS )
% 0.79/1.18 }.
% 0.79/1.18 (2016) {G0,W3,D2,L1,V0,M1} { aSubsetOf0( xT, xS ) }.
% 0.79/1.18 (2017) {G0,W2,D2,L1,V0,M1} { aSet0( xP ) }.
% 0.79/1.18 (2018) {G0,W5,D2,L2,V1,M2} { ! aElementOf0( X, xP ), alpha14( X ) }.
% 0.79/1.18 (2019) {G0,W15,D3,L4,V2,M4} { ! aElementOf0( X, xU ), ! sdtlseqdt0(
% 0.79/1.18 sdtlpdtrp0( xf, X ), X ), aElementOf0( skol19( Y ), xT ), aElementOf0( X
% 0.79/1.18 , xP ) }.
% 0.79/1.18 (2020) {G0,W15,D3,L4,V1,M4} { ! aElementOf0( X, xU ), ! sdtlseqdt0(
% 0.79/1.18 sdtlpdtrp0( xf, X ), X ), ! sdtlseqdt0( skol19( X ), X ), aElementOf0( X
% 0.79/1.18 , xP ) }.
% 0.79/1.18 (2021) {G0,W15,D3,L4,V1,M4} { ! aElementOf0( X, xU ), ! sdtlseqdt0(
% 0.79/1.18 sdtlpdtrp0( xf, X ), X ), ! aUpperBoundOfIn0( X, xT, xU ), aElementOf0( X
% 0.79/1.18 , xP ) }.
% 0.79/1.18 (2022) {G0,W6,D3,L1,V0,M1} { xP = cS1241( xU, xf, xT ) }.
% 0.79/1.18 (2023) {G0,W4,D2,L2,V1,M2} { ! alpha14( X ), alpha18( X ) }.
% 0.79/1.18 (2024) {G0,W6,D2,L2,V1,M2} { ! alpha14( X ), aUpperBoundOfIn0( X, xT, xU )
% 0.79/1.18 }.
% 0.79/1.18 (2025) {G0,W8,D2,L3,V1,M3} { ! alpha18( X ), ! aUpperBoundOfIn0( X, xT, xU
% 0.79/1.18 ), alpha14( X ) }.
% 0.79/1.18 (2026) {G0,W4,D2,L2,V1,M2} { ! alpha18( X ), alpha22( X ) }.
% 0.79/1.18 (2027) {G0,W8,D2,L3,V2,M3} { ! alpha18( X ), ! aElementOf0( Y, xT ),
% 0.79/1.18 sdtlseqdt0( Y, X ) }.
% 0.79/1.18 (2028) {G0,W8,D3,L3,V2,M3} { ! alpha22( X ), aElementOf0( skol20( Y ), xT
% 0.79/1.18 ), alpha18( X ) }.
% 0.79/1.18 (2029) {G0,W8,D3,L3,V1,M3} { ! alpha22( X ), ! sdtlseqdt0( skol20( X ), X
% 0.79/1.18 ), alpha18( X ) }.
% 0.79/1.18 (2030) {G0,W5,D2,L2,V1,M2} { ! alpha22( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (2031) {G0,W7,D3,L2,V1,M2} { ! alpha22( X ), sdtlseqdt0( sdtlpdtrp0( xf, X
% 0.79/1.18 ), X ) }.
% 0.79/1.18 (2032) {G0,W10,D3,L3,V1,M3} { ! aElementOf0( X, xU ), ! sdtlseqdt0(
% 0.79/1.18 sdtlpdtrp0( xf, X ), X ), alpha22( X ) }.
% 0.79/1.18 (2033) {G0,W5,D3,L2,V2,M2} { alpha15( X ), alpha19( skol21( Y ) ) }.
% 0.79/1.18 (2034) {G0,W7,D3,L2,V2,M2} { alpha15( X ), aLowerBoundOfIn0( skol21( Y ),
% 0.79/1.18 xP, xU ) }.
% 0.79/1.18 (2035) {G0,W6,D3,L2,V1,M2} { alpha15( X ), ! sdtlseqdt0( skol21( X ), X )
% 0.79/1.18 }.
% 0.79/1.18 (2036) {G0,W4,D2,L1,V1,M1} { ! aInfimumOfIn0( X, xP, xU ) }.
% 0.79/1.18 (2037) {G0,W5,D2,L2,V1,M2} { ! alpha19( X ), aElementOf0( X, xU ) }.
% 0.79/1.18 (2038) {G0,W8,D2,L3,V2,M3} { ! alpha19( X ), ! aElementOf0( Y, xP ),
% 0.79/1.18 sdtlseqdt0( X, Y ) }.
% 0.79/1.18 (2039) {G0,W9,D3,L3,V2,M3} { ! aElementOf0( X, xU ), aElementOf0( skol22(
% 0.79/1.18 Y ), xP ), alpha19( X ) }.
% 0.79/1.18 (2040) {G0,W9,D3,L3,V1,M3} { ! aElementOf0( X, xU ), ! sdtlseqdt0( X,
% 0.79/1.18 skol22( X ) ), alpha19( X ) }.
% 0.79/1.18 (2041) {G0,W7,D2,L3,V1,M3} { ! alpha15( X ), ! aElementOf0( X, xU ),
% 0.81/1.18 alpha20( X ) }.
% 0.81/1.18 (2042) {G0,W5,D2,L2,V1,M2} { aElementOf0( X, xU ), alpha15( X ) }.
% 0.81/1.18 (2043) {G0,W4,D2,L2,V1,M2} { ! alpha20( X ), alpha15( X ) }.
% 0.81/1.18 (2044) {G0,W4,D2,L2,V1,M2} { ! alpha20( X ), alpha23( X ) }.
% 0.81/1.18 (2045) {G0,W6,D2,L2,V1,M2} { ! alpha20( X ), ! aLowerBoundOfIn0( X, xP, xU
% 0.81/1.18 ) }.
% 0.81/1.18 (2046) {G0,W8,D2,L3,V1,M3} { ! alpha23( X ), aLowerBoundOfIn0( X, xP, xU )
% 0.81/1.18 , alpha20( X ) }.
% 0.81/1.18 (2047) {G0,W9,D3,L3,V2,M3} { ! alpha23( X ), ! aElementOf0( X, xU ),
% 0.81/1.18 aElementOf0( skol23( Y ), xP ) }.
% 0.81/1.18 (2048) {G0,W9,D3,L3,V1,M3} { ! alpha23( X ), ! aElementOf0( X, xU ), !
% 0.81/1.18 sdtlseqdt0( X, skol23( X ) ) }.
% 0.81/1.18 (2049) {G0,W5,D2,L2,V1,M2} { aElementOf0( X, xU ), alpha23( X ) }.
% 0.81/1.18 (2050) {G0,W8,D2,L3,V2,M3} { ! aElementOf0( Y, xP ), sdtlseqdt0( X, Y ),
% 0.81/1.18 alpha23( X ) }.
% 0.81/1.18
% 0.81/1.18
% 0.81/1.18 Total Proof:
% 0.81/1.18
% 0.81/1.18 subsumption: (6) {G0,W10,D2,L4,V2,M4} I { ! aSet0( X ), ! aSet0( Y ), !
% 0.81/1.18 alpha1( X, Y ), aSubsetOf0( Y, X ) }.
% 0.81/1.18 parent0: (1870) {G0,W10,D2,L4,V2,M4} { ! aSet0( X ), ! aSet0( Y ), !
% 0.81/1.18 alpha1( X, Y ), aSubsetOf0( Y, X ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 Y := Y
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 2 ==> 2
% 0.81/1.18 3 ==> 3
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (8) {G0,W8,D3,L2,V3,M2} I { aElementOf0( skol2( Z, Y ), Y ),
% 0.81/1.18 alpha1( X, Y ) }.
% 0.81/1.18 parent0: (1872) {G0,W8,D3,L2,V3,M2} { aElementOf0( skol2( Z, Y ), Y ),
% 0.81/1.18 alpha1( X, Y ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 Y := Y
% 0.81/1.18 Z := Z
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (9) {G0,W8,D3,L2,V2,M2} I { ! aElementOf0( skol2( X, Y ), X )
% 0.81/1.18 , alpha1( X, Y ) }.
% 0.81/1.18 parent0: (1873) {G0,W8,D3,L2,V2,M2} { ! aElementOf0( skol2( X, Y ), X ),
% 0.81/1.18 alpha1( X, Y ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 Y := Y
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (46) {G0,W4,D2,L2,V1,M2} I { ! aCompleteLattice0( X ), alpha6
% 0.81/1.18 ( X ) }.
% 0.81/1.18 parent0: (1911) {G0,W4,D2,L2,V1,M2} { ! aCompleteLattice0( X ), alpha6( X
% 0.81/1.18 ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (48) {G0,W8,D2,L3,V2,M3} I { ! alpha6( X ), ! aSubsetOf0( Y, X
% 0.81/1.18 ), alpha10( X, Y ) }.
% 0.81/1.18 parent0: (1913) {G0,W8,D2,L3,V2,M3} { ! alpha6( X ), ! aSubsetOf0( Y, X )
% 0.81/1.18 , alpha10( X, Y ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 Y := Y
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 2 ==> 2
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (51) {G0,W9,D3,L2,V2,M2} I { ! alpha10( X, Y ), aInfimumOfIn0
% 0.81/1.18 ( skol8( X, Y ), Y, X ) }.
% 0.81/1.18 parent0: (1916) {G0,W9,D3,L2,V2,M2} { ! alpha10( X, Y ), aInfimumOfIn0(
% 0.81/1.18 skol8( X, Y ), Y, X ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 Y := Y
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (72) {G0,W2,D2,L1,V0,M1} I { aSet0( xU ) }.
% 0.81/1.18 parent0: (1938) {G0,W2,D2,L1,V0,M1} { aSet0( xU ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (75) {G0,W2,D2,L1,V0,M1} I { aCompleteLattice0( xU ) }.
% 0.81/1.18 parent0: (1941) {G0,W2,D2,L1,V0,M1} { aCompleteLattice0( xU ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (126) {G0,W5,D2,L2,V1,M2} I { ! alpha25( X ), aElementOf0( X,
% 0.81/1.18 xU ) }.
% 0.81/1.18 parent0: (1992) {G0,W5,D2,L2,V1,M2} { ! alpha25( X ), aElementOf0( X, xU )
% 0.81/1.18 }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 factor: (2184) {G0,W5,D2,L2,V1,M2} { ! aElementOf0( X, xU ), alpha25( X )
% 0.81/1.18 }.
% 0.81/1.18 parent0[0, 1]: (1994) {G0,W8,D2,L3,V1,M3} { ! aElementOf0( X, xU ), !
% 0.81/1.18 aElementOf0( X, xU ), alpha25( X ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (127) {G0,W5,D2,L2,V1,M2} I;f { ! aElementOf0( X, xU ),
% 0.81/1.18 alpha25( X ) }.
% 0.81/1.18 parent0: (2184) {G0,W5,D2,L2,V1,M2} { ! aElementOf0( X, xU ), alpha25( X )
% 0.81/1.18 }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (128) {G0,W5,D2,L2,V1,M2} I { ! alpha16( X ), aElementOf0( X,
% 0.81/1.18 xU ) }.
% 0.81/1.18 parent0: (1995) {G0,W5,D2,L2,V1,M2} { ! alpha16( X ), aElementOf0( X, xU )
% 0.81/1.18 }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 end
% 0.81/1.18 permutation0:
% 0.81/1.18 0 ==> 0
% 0.81/1.18 1 ==> 1
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 factor: (2237) {G0,W5,D2,L2,V1,M2} { ! aElementOf0( X, xU ), alpha16( X )
% 0.81/1.18 }.
% 0.81/1.18 parent0[0, 1]: (1997) {G0,W8,D2,L3,V1,M3} { ! aElementOf0( X, xU ), !
% 0.81/1.18 aElementOf0( X, xU ), alpha16( X ) }.
% 0.81/1.18 substitution0:
% 0.81/1.18 X := X
% 0.81/1.18 end
% 0.81/1.18
% 0.81/1.18 subsumption: (129) {G0,W5,D2,L2,V1,M2} I;f { ! aElementOf0( X, xU ),
% 0.81/1.19 alpha16( X ) }.
% 0.81/1.19 parent0: (2237) {G0,W5,D2,L2,V1,M2} { ! aElementOf0( X, xU ), alpha16( X )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (149) {G0,W2,D2,L1,V0,M1} I { aSet0( xP ) }.
% 0.81/1.19 parent0: (2017) {G0,W2,D2,L1,V0,M1} { aSet0( xP ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (150) {G0,W5,D2,L2,V1,M2} I { ! aElementOf0( X, xP ), alpha14
% 0.81/1.19 ( X ) }.
% 0.81/1.19 parent0: (2018) {G0,W5,D2,L2,V1,M2} { ! aElementOf0( X, xP ), alpha14( X )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 *** allocated 50625 integers for termspace/termends
% 0.81/1.19 subsumption: (155) {G0,W4,D2,L2,V1,M2} I { ! alpha14( X ), alpha18( X ) }.
% 0.81/1.19 parent0: (2023) {G0,W4,D2,L2,V1,M2} { ! alpha14( X ), alpha18( X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (158) {G0,W4,D2,L2,V1,M2} I { ! alpha18( X ), alpha22( X ) }.
% 0.81/1.19 parent0: (2026) {G0,W4,D2,L2,V1,M2} { ! alpha18( X ), alpha22( X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (162) {G0,W5,D2,L2,V1,M2} I { ! alpha22( X ), aElementOf0( X,
% 0.81/1.19 xU ) }.
% 0.81/1.19 parent0: (2030) {G0,W5,D2,L2,V1,M2} { ! alpha22( X ), aElementOf0( X, xU )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (168) {G0,W4,D2,L1,V1,M1} I { ! aInfimumOfIn0( X, xP, xU ) }.
% 0.81/1.19 parent0: (2036) {G0,W4,D2,L1,V1,M1} { ! aInfimumOfIn0( X, xP, xU ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2428) {G1,W2,D2,L1,V0,M1} { alpha6( xU ) }.
% 0.81/1.19 parent0[0]: (46) {G0,W4,D2,L2,V1,M2} I { ! aCompleteLattice0( X ), alpha6(
% 0.81/1.19 X ) }.
% 0.81/1.19 parent1[0]: (75) {G0,W2,D2,L1,V0,M1} I { aCompleteLattice0( xU ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := xU
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (215) {G1,W2,D2,L1,V0,M1} R(46,75) { alpha6( xU ) }.
% 0.81/1.19 parent0: (2428) {G1,W2,D2,L1,V0,M1} { alpha6( xU ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2429) {G1,W5,D2,L2,V1,M2} { aElementOf0( X, xU ), ! alpha18(
% 0.81/1.19 X ) }.
% 0.81/1.19 parent0[0]: (162) {G0,W5,D2,L2,V1,M2} I { ! alpha22( X ), aElementOf0( X,
% 0.81/1.19 xU ) }.
% 0.81/1.19 parent1[1]: (158) {G0,W4,D2,L2,V1,M2} I { ! alpha18( X ), alpha22( X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (501) {G1,W5,D2,L2,V1,M2} R(162,158) { aElementOf0( X, xU ), !
% 0.81/1.19 alpha18( X ) }.
% 0.81/1.19 parent0: (2429) {G1,W5,D2,L2,V1,M2} { aElementOf0( X, xU ), ! alpha18( X )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2430) {G1,W5,D2,L2,V1,M2} { alpha18( X ), ! aElementOf0( X,
% 0.81/1.19 xP ) }.
% 0.81/1.19 parent0[0]: (155) {G0,W4,D2,L2,V1,M2} I { ! alpha14( X ), alpha18( X ) }.
% 0.81/1.19 parent1[1]: (150) {G0,W5,D2,L2,V1,M2} I { ! aElementOf0( X, xP ), alpha14(
% 0.81/1.19 X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (625) {G1,W5,D2,L2,V1,M2} R(150,155) { ! aElementOf0( X, xP )
% 0.81/1.19 , alpha18( X ) }.
% 0.81/1.19 parent0: (2430) {G1,W5,D2,L2,V1,M2} { alpha18( X ), ! aElementOf0( X, xP )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 1
% 0.81/1.19 1 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2431) {G1,W4,D2,L2,V1,M2} { alpha16( X ), ! alpha18( X ) }.
% 0.81/1.19 parent0[0]: (129) {G0,W5,D2,L2,V1,M2} I;f { ! aElementOf0( X, xU ), alpha16
% 0.81/1.19 ( X ) }.
% 0.81/1.19 parent1[0]: (501) {G1,W5,D2,L2,V1,M2} R(162,158) { aElementOf0( X, xU ), !
% 0.81/1.19 alpha18( X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (891) {G2,W4,D2,L2,V1,M2} R(129,501) { alpha16( X ), ! alpha18
% 0.81/1.19 ( X ) }.
% 0.81/1.19 parent0: (2431) {G1,W4,D2,L2,V1,M2} { alpha16( X ), ! alpha18( X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2432) {G2,W5,D2,L2,V1,M2} { alpha16( X ), ! aElementOf0( X,
% 0.81/1.19 xP ) }.
% 0.81/1.19 parent0[1]: (891) {G2,W4,D2,L2,V1,M2} R(129,501) { alpha16( X ), ! alpha18
% 0.81/1.19 ( X ) }.
% 0.81/1.19 parent1[1]: (625) {G1,W5,D2,L2,V1,M2} R(150,155) { ! aElementOf0( X, xP ),
% 0.81/1.19 alpha18( X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (938) {G3,W5,D2,L2,V1,M2} R(891,625) { alpha16( X ), !
% 0.81/1.19 aElementOf0( X, xP ) }.
% 0.81/1.19 parent0: (2432) {G2,W5,D2,L2,V1,M2} { alpha16( X ), ! aElementOf0( X, xP )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2433) {G1,W4,D2,L2,V1,M2} { alpha25( X ), ! alpha16( X ) }.
% 0.81/1.19 parent0[0]: (127) {G0,W5,D2,L2,V1,M2} I;f { ! aElementOf0( X, xU ), alpha25
% 0.81/1.19 ( X ) }.
% 0.81/1.19 parent1[1]: (128) {G0,W5,D2,L2,V1,M2} I { ! alpha16( X ), aElementOf0( X,
% 0.81/1.19 xU ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (987) {G1,W4,D2,L2,V1,M2} R(127,128) { alpha25( X ), ! alpha16
% 0.81/1.19 ( X ) }.
% 0.81/1.19 parent0: (2433) {G1,W4,D2,L2,V1,M2} { alpha25( X ), ! alpha16( X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2434) {G2,W5,D2,L2,V1,M2} { alpha25( X ), ! aElementOf0( X,
% 0.81/1.19 xP ) }.
% 0.81/1.19 parent0[1]: (987) {G1,W4,D2,L2,V1,M2} R(127,128) { alpha25( X ), ! alpha16
% 0.81/1.19 ( X ) }.
% 0.81/1.19 parent1[0]: (938) {G3,W5,D2,L2,V1,M2} R(891,625) { alpha16( X ), !
% 0.81/1.19 aElementOf0( X, xP ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1005) {G4,W5,D2,L2,V1,M2} R(987,938) { alpha25( X ), !
% 0.81/1.19 aElementOf0( X, xP ) }.
% 0.81/1.19 parent0: (2434) {G2,W5,D2,L2,V1,M2} { alpha25( X ), ! aElementOf0( X, xP )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2435) {G1,W3,D2,L1,V0,M1} { ! alpha10( xU, xP ) }.
% 0.81/1.19 parent0[0]: (168) {G0,W4,D2,L1,V1,M1} I { ! aInfimumOfIn0( X, xP, xU ) }.
% 0.81/1.19 parent1[1]: (51) {G0,W9,D3,L2,V2,M2} I { ! alpha10( X, Y ), aInfimumOfIn0(
% 0.81/1.19 skol8( X, Y ), Y, X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := skol8( xU, xP )
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := xU
% 0.81/1.19 Y := xP
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1622) {G1,W3,D2,L1,V0,M1} R(51,168) { ! alpha10( xU, xP ) }.
% 0.81/1.19 parent0: (2435) {G1,W3,D2,L1,V0,M1} { ! alpha10( xU, xP ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2436) {G1,W5,D2,L2,V0,M2} { ! alpha6( xU ), ! aSubsetOf0( xP
% 0.81/1.19 , xU ) }.
% 0.81/1.19 parent0[0]: (1622) {G1,W3,D2,L1,V0,M1} R(51,168) { ! alpha10( xU, xP ) }.
% 0.81/1.19 parent1[2]: (48) {G0,W8,D2,L3,V2,M3} I { ! alpha6( X ), ! aSubsetOf0( Y, X
% 0.81/1.19 ), alpha10( X, Y ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := xU
% 0.81/1.19 Y := xP
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2437) {G2,W3,D2,L1,V0,M1} { ! aSubsetOf0( xP, xU ) }.
% 0.81/1.19 parent0[0]: (2436) {G1,W5,D2,L2,V0,M2} { ! alpha6( xU ), ! aSubsetOf0( xP
% 0.81/1.19 , xU ) }.
% 0.81/1.19 parent1[0]: (215) {G1,W2,D2,L1,V0,M1} R(46,75) { alpha6( xU ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1626) {G2,W3,D2,L1,V0,M1} R(1622,48);r(215) { ! aSubsetOf0(
% 0.81/1.19 xP, xU ) }.
% 0.81/1.19 parent0: (2437) {G2,W3,D2,L1,V0,M1} { ! aSubsetOf0( xP, xU ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2438) {G1,W7,D2,L3,V0,M3} { ! aSet0( xU ), ! aSet0( xP ), !
% 0.81/1.19 alpha1( xU, xP ) }.
% 0.81/1.19 parent0[0]: (1626) {G2,W3,D2,L1,V0,M1} R(1622,48);r(215) { ! aSubsetOf0( xP
% 0.81/1.19 , xU ) }.
% 0.81/1.19 parent1[3]: (6) {G0,W10,D2,L4,V2,M4} I { ! aSet0( X ), ! aSet0( Y ), !
% 0.81/1.19 alpha1( X, Y ), aSubsetOf0( Y, X ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := xU
% 0.81/1.19 Y := xP
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2439) {G1,W5,D2,L2,V0,M2} { ! aSet0( xP ), ! alpha1( xU, xP )
% 0.81/1.19 }.
% 0.81/1.19 parent0[0]: (2438) {G1,W7,D2,L3,V0,M3} { ! aSet0( xU ), ! aSet0( xP ), !
% 0.81/1.19 alpha1( xU, xP ) }.
% 0.81/1.19 parent1[0]: (72) {G0,W2,D2,L1,V0,M1} I { aSet0( xU ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1627) {G3,W5,D2,L2,V0,M2} R(1626,6);r(72) { ! aSet0( xP ), !
% 0.81/1.19 alpha1( xU, xP ) }.
% 0.81/1.19 parent0: (2439) {G1,W5,D2,L2,V0,M2} { ! aSet0( xP ), ! alpha1( xU, xP )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 1 ==> 1
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2440) {G1,W3,D2,L1,V0,M1} { ! alpha1( xU, xP ) }.
% 0.81/1.19 parent0[0]: (1627) {G3,W5,D2,L2,V0,M2} R(1626,6);r(72) { ! aSet0( xP ), !
% 0.81/1.19 alpha1( xU, xP ) }.
% 0.81/1.19 parent1[0]: (149) {G0,W2,D2,L1,V0,M1} I { aSet0( xP ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1630) {G4,W3,D2,L1,V0,M1} S(1627);r(149) { ! alpha1( xU, xP )
% 0.81/1.19 }.
% 0.81/1.19 parent0: (2440) {G1,W3,D2,L1,V0,M1} { ! alpha1( xU, xP ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2441) {G1,W5,D3,L1,V1,M1} { aElementOf0( skol2( X, xP ), xP )
% 0.81/1.19 }.
% 0.81/1.19 parent0[0]: (1630) {G4,W3,D2,L1,V0,M1} S(1627);r(149) { ! alpha1( xU, xP )
% 0.81/1.19 }.
% 0.81/1.19 parent1[1]: (8) {G0,W8,D3,L2,V3,M2} I { aElementOf0( skol2( Z, Y ), Y ),
% 0.81/1.19 alpha1( X, Y ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := xU
% 0.81/1.19 Y := xP
% 0.81/1.19 Z := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1634) {G5,W5,D3,L1,V1,M1} R(1630,8) { aElementOf0( skol2( X,
% 0.81/1.19 xP ), xP ) }.
% 0.81/1.19 parent0: (2441) {G1,W5,D3,L1,V1,M1} { aElementOf0( skol2( X, xP ), xP )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2442) {G5,W4,D3,L1,V1,M1} { alpha25( skol2( X, xP ) ) }.
% 0.81/1.19 parent0[1]: (1005) {G4,W5,D2,L2,V1,M2} R(987,938) { alpha25( X ), !
% 0.81/1.19 aElementOf0( X, xP ) }.
% 0.81/1.19 parent1[0]: (1634) {G5,W5,D3,L1,V1,M1} R(1630,8) { aElementOf0( skol2( X,
% 0.81/1.19 xP ), xP ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := skol2( X, xP )
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1783) {G6,W4,D3,L1,V1,M1} R(1634,1005) { alpha25( skol2( X,
% 0.81/1.19 xP ) ) }.
% 0.81/1.19 parent0: (2442) {G5,W4,D3,L1,V1,M1} { alpha25( skol2( X, xP ) ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2443) {G1,W5,D3,L1,V1,M1} { aElementOf0( skol2( X, xP ), xU )
% 0.81/1.19 }.
% 0.81/1.19 parent0[0]: (126) {G0,W5,D2,L2,V1,M2} I { ! alpha25( X ), aElementOf0( X,
% 0.81/1.19 xU ) }.
% 0.81/1.19 parent1[0]: (1783) {G6,W4,D3,L1,V1,M1} R(1634,1005) { alpha25( skol2( X, xP
% 0.81/1.19 ) ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := skol2( X, xP )
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1798) {G7,W5,D3,L1,V1,M1} R(1783,126) { aElementOf0( skol2( X
% 0.81/1.19 , xP ), xU ) }.
% 0.81/1.19 parent0: (2443) {G1,W5,D3,L1,V1,M1} { aElementOf0( skol2( X, xP ), xU )
% 0.81/1.19 }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := X
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 0 ==> 0
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2444) {G1,W3,D2,L1,V0,M1} { alpha1( xU, xP ) }.
% 0.81/1.19 parent0[0]: (9) {G0,W8,D3,L2,V2,M2} I { ! aElementOf0( skol2( X, Y ), X ),
% 0.81/1.19 alpha1( X, Y ) }.
% 0.81/1.19 parent1[0]: (1798) {G7,W5,D3,L1,V1,M1} R(1783,126) { aElementOf0( skol2( X
% 0.81/1.19 , xP ), xU ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 X := xU
% 0.81/1.19 Y := xP
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 X := xU
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 resolution: (2445) {G2,W0,D0,L0,V0,M0} { }.
% 0.81/1.19 parent0[0]: (1630) {G4,W3,D2,L1,V0,M1} S(1627);r(149) { ! alpha1( xU, xP )
% 0.81/1.19 }.
% 0.81/1.19 parent1[0]: (2444) {G1,W3,D2,L1,V0,M1} { alpha1( xU, xP ) }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 substitution1:
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 subsumption: (1861) {G8,W0,D0,L0,V0,M0} R(1798,9);r(1630) { }.
% 0.81/1.19 parent0: (2445) {G2,W0,D0,L0,V0,M0} { }.
% 0.81/1.19 substitution0:
% 0.81/1.19 end
% 0.81/1.19 permutation0:
% 0.81/1.19 end
% 0.81/1.19
% 0.81/1.19 Proof check complete!
% 0.81/1.19
% 0.81/1.19 Memory use:
% 0.81/1.19
% 0.81/1.19 space for terms: 28147
% 0.81/1.19 space for clauses: 81519
% 0.81/1.19
% 0.81/1.19
% 0.81/1.19 clauses generated: 4418
% 0.81/1.19 clauses kept: 1862
% 0.81/1.19 clauses selected: 276
% 0.81/1.19 clauses deleted: 3
% 0.81/1.19 clauses inuse deleted: 1
% 0.81/1.19
% 0.81/1.19 subsentry: 4790
% 0.81/1.19 literals s-matched: 3660
% 0.81/1.19 literals matched: 3406
% 0.81/1.19 full subsumption: 827
% 0.81/1.19
% 0.81/1.19 checksum: -2009454943
% 0.81/1.19
% 0.81/1.19
% 0.81/1.19 Bliksem ended
%------------------------------------------------------------------------------