%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : LAT301+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n025.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:50:23 EDT 2022
% Result : Theorem 52.29s 52.77s
% Output : Refutation 52.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : LAT301+1 : TPTP v8.1.0. Released v3.4.0.
% 0.10/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Thu Jun 30 06:36:08 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.67/1.11 *** allocated 10000 integers for termspace/termends
% 0.67/1.11 *** allocated 10000 integers for clauses
% 0.67/1.11 *** allocated 10000 integers for justifications
% 0.67/1.11 Bliksem 1.12
% 0.67/1.11
% 0.67/1.11
% 0.67/1.11 Automatic Strategy Selection
% 0.67/1.11
% 0.67/1.11
% 0.67/1.11 Clauses:
% 0.67/1.11
% 0.67/1.11 { ! v3_struct_0( skol1 ) }.
% 0.67/1.11 { v10_lattices( skol1 ) }.
% 0.67/1.11 { l3_lattices( skol1 ) }.
% 0.67/1.11 { m2_filter_2( skol27, skol1 ) }.
% 0.67/1.11 { v13_lattices( skol1 ) }.
% 0.67/1.11 { ! r2_hidden( k5_lattices( skol1 ), skol27 ) }.
% 0.67/1.11 { ! l3_lattices( X ), ! v3_lattices( X ), X = g3_lattices( u1_struct_0( X )
% 0.67/1.11 , u2_lattices( X ), u1_lattices( X ) ) }.
% 0.67/1.11 { ! r2_hidden( X, Y ), ! r2_hidden( Y, X ) }.
% 0.67/1.11 { ! v1_xboole_0( X ), v1_funct_1( X ) }.
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v10_lattices( X ), alpha1( X ) }
% 0.67/1.11 .
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v10_lattices( X ), v9_lattices( X
% 0.67/1.11 ) }.
% 0.67/1.11 { ! alpha1( X ), alpha7( X ) }.
% 0.67/1.11 { ! alpha1( X ), v8_lattices( X ) }.
% 0.67/1.11 { ! alpha7( X ), ! v8_lattices( X ), alpha1( X ) }.
% 0.67/1.11 { ! alpha7( X ), alpha13( X ) }.
% 0.67/1.11 { ! alpha7( X ), v7_lattices( X ) }.
% 0.67/1.11 { ! alpha13( X ), ! v7_lattices( X ), alpha7( X ) }.
% 0.67/1.11 { ! alpha13( X ), alpha15( X ) }.
% 0.67/1.11 { ! alpha13( X ), v6_lattices( X ) }.
% 0.67/1.11 { ! alpha15( X ), ! v6_lattices( X ), alpha13( X ) }.
% 0.67/1.11 { ! alpha15( X ), ! v3_struct_0( X ) }.
% 0.67/1.11 { ! alpha15( X ), v4_lattices( X ) }.
% 0.67/1.11 { ! alpha15( X ), v5_lattices( X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v4_lattices( X ), ! v5_lattices( X ), alpha15( X ) }
% 0.67/1.11 .
% 0.67/1.11 { ! m1_subset_1( X, k1_zfmisc_1( k2_zfmisc_1( Y, Z ) ) ), v1_relat_1( X ) }
% 0.67/1.11 .
% 0.67/1.11 { ! v1_relat_1( X ), ! v1_xboole_0( X ), ! v1_funct_1( X ), v1_relat_1( X )
% 0.67/1.11 }.
% 0.67/1.11 { ! v1_relat_1( X ), ! v1_xboole_0( X ), ! v1_funct_1( X ), v1_funct_1( X )
% 0.67/1.11 }.
% 0.67/1.11 { ! v1_relat_1( X ), ! v1_xboole_0( X ), ! v1_funct_1( X ), v2_funct_1( X )
% 0.67/1.11 }.
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v4_lattices( X ), ! v5_lattices(
% 0.67/1.11 X ), ! v6_lattices( X ), ! v7_lattices( X ), ! v8_lattices( X ), !
% 0.67/1.11 v9_lattices( X ), ! v3_struct_0( X ) }.
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v4_lattices( X ), ! v5_lattices(
% 0.67/1.11 X ), ! v6_lattices( X ), ! v7_lattices( X ), ! v8_lattices( X ), !
% 0.67/1.11 v9_lattices( X ), v10_lattices( X ) }.
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v13_lattices( X ), ! v14_lattices
% 0.67/1.11 ( X ), ! v3_struct_0( X ) }.
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v13_lattices( X ), ! v14_lattices
% 0.67/1.11 ( X ), v15_lattices( X ) }.
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v15_lattices( X ), ! v3_struct_0
% 0.67/1.11 ( X ) }.
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v15_lattices( X ), v13_lattices(
% 0.67/1.11 X ) }.
% 0.67/1.11 { ! l3_lattices( X ), v3_struct_0( X ), ! v15_lattices( X ), v14_lattices(
% 0.67/1.11 X ) }.
% 0.67/1.11 { ! l3_lattices( X ), k1_lattice2( X ) = g3_lattices( u1_struct_0( X ),
% 0.67/1.11 u1_lattices( X ), u2_lattices( X ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_subset_1
% 0.67/1.11 ( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), k7_filter_2( X, Y ) = Y }.
% 0.67/1.11 { ! v1_funct_1( Y ), ! v1_funct_2( Y, k2_zfmisc_1( X, X ), X ), !
% 0.67/1.11 m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), ! v1_funct_1( Z ), ! v1_funct_2
% 0.67/1.11 ( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Z, k2_zfmisc_1( X, X ), X )
% 0.67/1.11 , v3_lattices( g3_lattices( X, Y, Z ) ) }.
% 0.67/1.11 { ! v1_funct_1( Y ), ! v1_funct_2( Y, k2_zfmisc_1( X, X ), X ), !
% 0.67/1.11 m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), ! v1_funct_1( Z ), ! v1_funct_2
% 0.67/1.11 ( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Z, k2_zfmisc_1( X, X ), X )
% 0.67/1.11 , l3_lattices( g3_lattices( X, Y, Z ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2
% 0.67/1.11 ( Y, X ), m1_filter_2( k15_filter_2( X, Y ), k1_lattice2( X ) ) }.
% 0.67/1.11 { ! l3_lattices( X ), v3_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! l3_lattices( X ), l3_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { && }.
% 0.67/1.11 { && }.
% 0.67/1.11 { && }.
% 0.67/1.11 { v3_struct_0( X ), ! l1_lattices( X ), m1_subset_1( k5_lattices( X ),
% 0.67/1.11 u1_struct_0( X ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! l2_lattices( X ), m1_subset_1( k6_lattices( X ),
% 0.67/1.11 u1_struct_0( X ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_subset_1
% 0.67/1.11 ( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), m1_subset_1( k7_filter_2( X, Y )
% 0.67/1.11 , k1_zfmisc_1( u1_struct_0( k1_lattice2( X ) ) ) ) }.
% 0.67/1.11 { ! l1_lattices( X ), l1_struct_0( X ) }.
% 0.67/1.11 { && }.
% 0.67/1.11 { ! l2_lattices( X ), l1_struct_0( X ) }.
% 0.67/1.11 { ! l3_lattices( X ), l1_lattices( X ) }.
% 0.67/1.11 { ! l3_lattices( X ), l2_lattices( X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0
% 0.67/1.11 ( Y, X ), ! v1_xboole_0( Y ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0
% 0.67/1.11 ( Y, X ), m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_2
% 0.67/1.11 ( Y, X ), ! v1_xboole_0( Y ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_2
% 0.67/1.11 ( Y, X ), m2_lattice4( Y, X ) }.
% 0.67/1.11 { && }.
% 0.67/1.11 { && }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2
% 0.67/1.11 ( Y, X ), ! v1_xboole_0( Y ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2
% 0.67/1.11 ( Y, X ), m2_lattice4( Y, X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_lattice4
% 0.67/1.11 ( Y, X ), m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.67/1.11 { ! m2_relset_1( Z, X, Y ), m1_subset_1( Z, k1_zfmisc_1( k2_zfmisc_1( X, Y
% 0.67/1.11 ) ) ) }.
% 0.67/1.11 { ! l1_lattices( X ), v1_funct_1( u1_lattices( X ) ) }.
% 0.67/1.11 { ! l1_lattices( X ), v1_funct_2( u1_lattices( X ), k2_zfmisc_1(
% 0.67/1.11 u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! l1_lattices( X ), m2_relset_1( u1_lattices( X ), k2_zfmisc_1(
% 0.67/1.11 u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 0.67/1.11 { && }.
% 0.67/1.11 { ! l2_lattices( X ), v1_funct_1( u2_lattices( X ) ) }.
% 0.67/1.11 { ! l2_lattices( X ), v1_funct_2( u2_lattices( X ), k2_zfmisc_1(
% 0.67/1.11 u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! l2_lattices( X ), m2_relset_1( u2_lattices( X ), k2_zfmisc_1(
% 0.67/1.11 u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 0.67/1.11 { l1_lattices( skol2 ) }.
% 0.67/1.11 { l1_struct_0( skol3 ) }.
% 0.67/1.11 { l2_lattices( skol4 ) }.
% 0.67/1.11 { l3_lattices( skol5 ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m1_filter_0(
% 0.67/1.11 skol6( X ), X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m1_filter_2(
% 0.67/1.11 skol7( X ), X ) }.
% 0.67/1.11 { m1_relset_1( skol8( X, Y ), X, Y ) }.
% 0.67/1.11 { m1_subset_1( skol9( X ), X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m2_filter_2(
% 0.67/1.11 skol10( X ), X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m2_lattice4(
% 0.67/1.11 skol11( X ), X ) }.
% 0.67/1.11 { m2_relset_1( skol12( X, Y ), X, Y ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), v1_xboole_0( Y
% 0.67/1.11 ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_xboole_0(
% 0.67/1.11 k7_filter_2( X, Y ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! l3_lattices( X ), ! v3_struct_0( k1_lattice2( X ) ) }
% 0.67/1.11 .
% 0.67/1.11 { v3_struct_0( X ), ! l3_lattices( X ), v3_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! l1_struct_0( X ), ! v1_xboole_0( u1_struct_0( X ) ) }
% 0.67/1.11 .
% 0.67/1.11 { ! v1_xboole_0( k1_zfmisc_1( X ) ) }.
% 0.67/1.11 { v1_xboole_0( k1_xboole_0 ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v4_lattices( X ), ! l2_lattices( X ), alpha2( X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v4_lattices( X ), ! l2_lattices( X ), v1_partfun1(
% 0.67/1.11 u2_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ),
% 0.67/1.11 u1_struct_0( X ) ) }.
% 0.67/1.11 { ! alpha2( X ), alpha8( X ) }.
% 0.67/1.11 { ! alpha2( X ), v1_binop_1( u2_lattices( X ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! alpha8( X ), ! v1_binop_1( u2_lattices( X ), u1_struct_0( X ) ), alpha2
% 0.67/1.11 ( X ) }.
% 0.67/1.11 { ! alpha8( X ), v1_relat_1( u2_lattices( X ) ) }.
% 0.67/1.11 { ! alpha8( X ), v1_funct_1( u2_lattices( X ) ) }.
% 0.67/1.11 { ! alpha8( X ), v1_funct_2( u2_lattices( X ), k2_zfmisc_1( u1_struct_0( X
% 0.67/1.11 ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! v1_relat_1( u2_lattices( X ) ), ! v1_funct_1( u2_lattices( X ) ), !
% 0.67/1.11 v1_funct_2( u2_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0
% 0.67/1.11 ( X ) ), u1_struct_0( X ) ), alpha8( X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v5_lattices( X ), ! l2_lattices( X ), alpha3( X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v5_lattices( X ), ! l2_lattices( X ), v1_partfun1(
% 0.67/1.11 u2_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ),
% 0.67/1.11 u1_struct_0( X ) ) }.
% 0.67/1.11 { ! alpha3( X ), alpha9( X ) }.
% 0.67/1.11 { ! alpha3( X ), v2_binop_1( u2_lattices( X ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! alpha9( X ), ! v2_binop_1( u2_lattices( X ), u1_struct_0( X ) ), alpha3
% 0.67/1.11 ( X ) }.
% 0.67/1.11 { ! alpha9( X ), v1_relat_1( u2_lattices( X ) ) }.
% 0.67/1.11 { ! alpha9( X ), v1_funct_1( u2_lattices( X ) ) }.
% 0.67/1.11 { ! alpha9( X ), v1_funct_2( u2_lattices( X ), k2_zfmisc_1( u1_struct_0( X
% 0.67/1.11 ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! v1_relat_1( u2_lattices( X ) ), ! v1_funct_1( u2_lattices( X ) ), !
% 0.67/1.11 v1_funct_2( u2_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0
% 0.67/1.11 ( X ) ), u1_struct_0( X ) ), alpha9( X ) }.
% 0.67/1.11 { v1_xboole_0( X ), ! v1_funct_1( Y ), ! v1_funct_2( Y, k2_zfmisc_1( X, X )
% 0.67/1.11 , X ), ! m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), ! v1_funct_1( Z ), !
% 0.67/1.11 v1_funct_2( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Z, k2_zfmisc_1( X
% 0.67/1.11 , X ), X ), ! v3_struct_0( g3_lattices( X, Y, Z ) ) }.
% 0.67/1.11 { v1_xboole_0( X ), ! v1_funct_1( Y ), ! v1_funct_2( Y, k2_zfmisc_1( X, X )
% 0.67/1.11 , X ), ! m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), ! v1_funct_1( Z ), !
% 0.67/1.11 v1_funct_2( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Z, k2_zfmisc_1( X
% 0.67/1.11 , X ), X ), v3_lattices( g3_lattices( X, Y, Z ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v6_lattices( X ), ! l1_lattices( X ), alpha4( X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v6_lattices( X ), ! l1_lattices( X ), v1_partfun1(
% 0.67/1.11 u1_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ),
% 0.67/1.11 u1_struct_0( X ) ) }.
% 0.67/1.11 { ! alpha4( X ), alpha10( X ) }.
% 0.67/1.11 { ! alpha4( X ), v1_binop_1( u1_lattices( X ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! alpha10( X ), ! v1_binop_1( u1_lattices( X ), u1_struct_0( X ) ),
% 0.67/1.11 alpha4( X ) }.
% 0.67/1.11 { ! alpha10( X ), v1_relat_1( u1_lattices( X ) ) }.
% 0.67/1.11 { ! alpha10( X ), v1_funct_1( u1_lattices( X ) ) }.
% 0.67/1.11 { ! alpha10( X ), v1_funct_2( u1_lattices( X ), k2_zfmisc_1( u1_struct_0( X
% 0.67/1.11 ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! v1_relat_1( u1_lattices( X ) ), ! v1_funct_1( u1_lattices( X ) ), !
% 0.67/1.11 v1_funct_2( u1_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0
% 0.67/1.11 ( X ) ), u1_struct_0( X ) ), alpha10( X ) }.
% 0.67/1.11 { v1_xboole_0( X ), v1_xboole_0( Y ), ! v1_xboole_0( k2_zfmisc_1( X, Y ) )
% 0.67/1.11 }.
% 0.67/1.11 { v3_struct_0( X ), ! v7_lattices( X ), ! l1_lattices( X ), alpha5( X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v7_lattices( X ), ! l1_lattices( X ), v1_partfun1(
% 0.67/1.11 u1_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ),
% 0.67/1.11 u1_struct_0( X ) ) }.
% 0.67/1.11 { ! alpha5( X ), alpha11( X ) }.
% 0.67/1.11 { ! alpha5( X ), v2_binop_1( u1_lattices( X ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! alpha11( X ), ! v2_binop_1( u1_lattices( X ), u1_struct_0( X ) ),
% 0.67/1.11 alpha5( X ) }.
% 0.67/1.11 { ! alpha11( X ), v1_relat_1( u1_lattices( X ) ) }.
% 0.67/1.11 { ! alpha11( X ), v1_funct_1( u1_lattices( X ) ) }.
% 0.67/1.11 { ! alpha11( X ), v1_funct_2( u1_lattices( X ), k2_zfmisc_1( u1_struct_0( X
% 0.67/1.11 ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 0.67/1.11 { ! v1_relat_1( u1_lattices( X ) ), ! v1_funct_1( u1_lattices( X ) ), !
% 0.67/1.11 v1_funct_2( u1_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0
% 0.67/1.11 ( X ) ), u1_struct_0( X ) ), alpha11( X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), alpha6( X ) }
% 0.67/1.11 .
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), v10_lattices(
% 0.67/1.11 k1_lattice2( X ) ) }.
% 0.67/1.11 { ! alpha6( X ), alpha12( X ) }.
% 0.67/1.11 { ! alpha6( X ), v9_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! alpha12( X ), ! v9_lattices( k1_lattice2( X ) ), alpha6( X ) }.
% 0.67/1.11 { ! alpha12( X ), alpha14( X ) }.
% 0.67/1.11 { ! alpha12( X ), v8_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! alpha14( X ), ! v8_lattices( k1_lattice2( X ) ), alpha12( X ) }.
% 0.67/1.11 { ! alpha14( X ), alpha16( X ) }.
% 0.67/1.11 { ! alpha14( X ), v7_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! alpha16( X ), ! v7_lattices( k1_lattice2( X ) ), alpha14( X ) }.
% 0.67/1.11 { ! alpha16( X ), alpha17( X ) }.
% 0.67/1.11 { ! alpha16( X ), v6_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! alpha17( X ), ! v6_lattices( k1_lattice2( X ) ), alpha16( X ) }.
% 0.67/1.11 { ! alpha17( X ), alpha18( X ) }.
% 0.67/1.11 { ! alpha17( X ), v5_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! alpha18( X ), ! v5_lattices( k1_lattice2( X ) ), alpha17( X ) }.
% 0.67/1.11 { ! alpha18( X ), ! v3_struct_0( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! alpha18( X ), v3_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! alpha18( X ), v4_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { v3_struct_0( k1_lattice2( X ) ), ! v3_lattices( k1_lattice2( X ) ), !
% 0.67/1.11 v4_lattices( k1_lattice2( X ) ), alpha18( X ) }.
% 0.67/1.11 { ! v1_funct_1( Y ), ! v1_funct_2( Y, k2_zfmisc_1( X, X ), X ), !
% 0.67/1.11 m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), ! v1_funct_1( Z ), ! v1_funct_2
% 0.67/1.11 ( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Z, k2_zfmisc_1( X, X ), X )
% 0.67/1.11 , ! g3_lattices( X, Y, Z ) = g3_lattices( T, U, W ), X = T }.
% 0.67/1.11 { ! v1_funct_1( Y ), ! v1_funct_2( Y, k2_zfmisc_1( X, X ), X ), !
% 0.67/1.11 m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), ! v1_funct_1( Z ), ! v1_funct_2
% 0.67/1.11 ( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Z, k2_zfmisc_1( X, X ), X )
% 0.67/1.11 , ! g3_lattices( X, Y, Z ) = g3_lattices( T, U, W ), Y = U }.
% 0.67/1.11 { ! v1_funct_1( Y ), ! v1_funct_2( Y, k2_zfmisc_1( X, X ), X ), !
% 0.67/1.11 m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), ! v1_funct_1( Z ), ! v1_funct_2
% 0.67/1.11 ( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Z, k2_zfmisc_1( X, X ), X )
% 0.67/1.11 , ! g3_lattices( X, Y, Z ) = g3_lattices( T, U, W ), Z = W }.
% 0.67/1.11 { l3_lattices( skol13 ) }.
% 0.67/1.11 { ! v3_struct_0( skol13 ) }.
% 0.67/1.11 { v3_lattices( skol13 ) }.
% 0.67/1.11 { v4_lattices( skol13 ) }.
% 0.67/1.11 { v5_lattices( skol13 ) }.
% 0.67/1.11 { v6_lattices( skol13 ) }.
% 0.67/1.11 { v7_lattices( skol13 ) }.
% 0.67/1.11 { v8_lattices( skol13 ) }.
% 0.67/1.11 { v9_lattices( skol13 ) }.
% 0.67/1.11 { v10_lattices( skol13 ) }.
% 0.67/1.11 { v13_lattices( skol13 ) }.
% 0.67/1.11 { v14_lattices( skol13 ) }.
% 0.67/1.11 { v15_lattices( skol13 ) }.
% 0.67/1.11 { v1_relat_1( skol14 ) }.
% 0.67/1.11 { v1_funct_1( skol14 ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! v1_xboole_0
% 0.67/1.11 ( skol15( Y ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m2_lattice4(
% 0.67/1.11 skol15( X ), X ) }.
% 0.67/1.11 { v1_xboole_0( X ), ! v1_xboole_0( skol16( Y ) ) }.
% 0.67/1.11 { v1_xboole_0( X ), m1_subset_1( skol16( X ), k1_zfmisc_1( X ) ) }.
% 0.67/1.11 { v1_xboole_0( skol17 ) }.
% 0.67/1.11 { v1_relat_1( skol18 ) }.
% 0.67/1.11 { v1_xboole_0( skol18 ) }.
% 0.67/1.11 { v1_funct_1( skol18 ) }.
% 0.67/1.11 { v1_xboole_0( skol19( Y ) ) }.
% 0.67/1.11 { m1_subset_1( skol19( X ), k1_zfmisc_1( X ) ) }.
% 0.67/1.11 { ! v1_xboole_0( skol20 ) }.
% 0.67/1.11 { v1_relat_1( skol21 ) }.
% 0.67/1.11 { v1_funct_1( skol21 ) }.
% 0.67/1.11 { v2_funct_1( skol21 ) }.
% 0.67/1.11 { l3_lattices( skol22 ) }.
% 0.67/1.11 { v3_lattices( skol22 ) }.
% 0.67/1.11 { l1_struct_0( skol23 ) }.
% 0.67/1.11 { ! v3_struct_0( skol23 ) }.
% 0.67/1.11 { v3_struct_0( X ), ! l1_struct_0( X ), ! v1_xboole_0( skol24( Y ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! l1_struct_0( X ), m1_subset_1( skol24( X ),
% 0.67/1.11 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.67/1.11 { l3_lattices( skol25 ) }.
% 0.67/1.11 { ! v3_struct_0( skol25 ) }.
% 0.67/1.11 { v3_lattices( skol25 ) }.
% 0.67/1.11 { l3_lattices( skol26 ) }.
% 0.67/1.11 { ! v3_struct_0( skol26 ) }.
% 0.67/1.11 { v3_lattices( skol26 ) }.
% 0.67/1.11 { v4_lattices( skol26 ) }.
% 0.67/1.11 { v5_lattices( skol26 ) }.
% 0.67/1.11 { v6_lattices( skol26 ) }.
% 0.67/1.11 { v7_lattices( skol26 ) }.
% 0.67/1.11 { v8_lattices( skol26 ) }.
% 0.67/1.11 { v9_lattices( skol26 ) }.
% 0.67/1.11 { v10_lattices( skol26 ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2
% 0.67/1.11 ( Y, X ), k15_filter_2( X, Y ) = k7_filter_2( X, Y ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_2
% 0.67/1.11 ( Y, X ), m1_filter_0( Y, X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0
% 0.67/1.11 ( Y, X ), m1_filter_2( Y, X ) }.
% 0.67/1.11 { ! m2_relset_1( Z, X, Y ), m1_relset_1( Z, X, Y ) }.
% 0.67/1.11 { ! m1_relset_1( Z, X, Y ), m2_relset_1( Z, X, Y ) }.
% 0.67/1.11 { r1_tarski( X, X ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0
% 0.67/1.11 ( Y, X ), v3_struct_0( X ), ! v10_lattices( X ), ! v14_lattices( X ), !
% 0.67/1.11 l3_lattices( X ), r2_hidden( k6_lattices( X ), Y ) }.
% 0.67/1.11 { ! r2_hidden( X, Y ), m1_subset_1( X, Y ) }.
% 0.67/1.11 { ! m1_subset_1( X, Y ), v1_xboole_0( Y ), r2_hidden( X, Y ) }.
% 0.67/1.11 { ! m1_subset_1( X, k1_zfmisc_1( Y ) ), r1_tarski( X, Y ) }.
% 0.67/1.11 { ! r1_tarski( X, Y ), m1_subset_1( X, k1_zfmisc_1( Y ) ) }.
% 0.67/1.11 { ! r2_hidden( X, Z ), ! m1_subset_1( Z, k1_zfmisc_1( Y ) ), m1_subset_1( X
% 0.67/1.11 , Y ) }.
% 0.67/1.11 { ! r2_hidden( X, Y ), ! m1_subset_1( Y, k1_zfmisc_1( Z ) ), ! v1_xboole_0
% 0.67/1.11 ( Z ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! v13_lattices
% 0.67/1.11 ( X ), v14_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! v14_lattices
% 0.67/1.11 ( k1_lattice2( X ) ), v13_lattices( X ) }.
% 0.67/1.11 { ! v1_xboole_0( X ), X = k1_xboole_0 }.
% 0.67/1.11 { v3_struct_0( X ), ! v10_lattices( X ), ! v13_lattices( X ), ! l3_lattices
% 0.67/1.11 ( X ), k5_lattices( X ) = k6_lattices( k1_lattice2( X ) ) }.
% 0.67/1.11 { ! r2_hidden( X, Y ), ! v1_xboole_0( Y ) }.
% 0.67/1.11 { ! v1_xboole_0( X ), X = Y, ! v1_xboole_0( Y ) }.
% 0.67/1.11
% 0.67/1.11 percentage equality = 0.024528, percentage horn = 0.784314
% 0.67/1.11 This is a problem with some equality
% 0.67/1.11
% 0.67/1.11
% 0.67/1.11
% 0.67/1.11 Options Used:
% 0.67/1.11
% 0.67/1.11 useres = 1
% 0.67/1.11 useparamod = 1
% 0.67/1.11 useeqrefl = 1
% 2.91/3.29 useeqfact = 1
% 2.91/3.29 usefactor = 1
% 2.91/3.29 usesimpsplitting = 0
% 2.91/3.29 usesimpdemod = 5
% 2.91/3.29 usesimpres = 3
% 2.91/3.29
% 2.91/3.29 resimpinuse = 1000
% 2.91/3.29 resimpclauses = 20000
% 2.91/3.29 substype = eqrewr
% 2.91/3.29 backwardsubs = 1
% 2.91/3.29 selectoldest = 5
% 2.91/3.29
% 2.91/3.29 litorderings [0] = split
% 2.91/3.29 litorderings [1] = extend the termordering, first sorting on arguments
% 2.91/3.29
% 2.91/3.29 termordering = kbo
% 2.91/3.29
% 2.91/3.29 litapriori = 0
% 2.91/3.29 termapriori = 1
% 2.91/3.29 litaposteriori = 0
% 2.91/3.29 termaposteriori = 0
% 2.91/3.29 demodaposteriori = 0
% 2.91/3.29 ordereqreflfact = 0
% 2.91/3.29
% 2.91/3.29 litselect = negord
% 2.91/3.29
% 2.91/3.29 maxweight = 15
% 2.91/3.29 maxdepth = 30000
% 2.91/3.29 maxlength = 115
% 2.91/3.29 maxnrvars = 195
% 2.91/3.29 excuselevel = 1
% 2.91/3.29 increasemaxweight = 1
% 2.91/3.29
% 2.91/3.29 maxselected = 10000000
% 2.91/3.29 maxnrclauses = 10000000
% 2.91/3.29
% 2.91/3.29 showgenerated = 0
% 2.91/3.29 showkept = 0
% 2.91/3.29 showselected = 0
% 2.91/3.29 showdeleted = 0
% 2.91/3.29 showresimp = 1
% 2.91/3.29 showstatus = 2000
% 2.91/3.29
% 2.91/3.29 prologoutput = 0
% 2.91/3.29 nrgoals = 5000000
% 2.91/3.29 totalproof = 1
% 2.91/3.29
% 2.91/3.29 Symbols occurring in the translation:
% 2.91/3.29
% 2.91/3.29 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.91/3.29 . [1, 2] (w:1, o:88, a:1, s:1, b:0),
% 2.91/3.29 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 2.91/3.29 ! [4, 1] (w:0, o:29, a:1, s:1, b:0),
% 2.91/3.29 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.91/3.29 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.91/3.29 v3_struct_0 [36, 1] (w:1, o:40, a:1, s:1, b:0),
% 2.91/3.29 v10_lattices [37, 1] (w:1, o:41, a:1, s:1, b:0),
% 2.91/3.29 l3_lattices [38, 1] (w:1, o:48, a:1, s:1, b:0),
% 2.91/3.29 m2_filter_2 [40, 2] (w:1, o:115, a:1, s:1, b:0),
% 2.91/3.29 v13_lattices [41, 1] (w:1, o:49, a:1, s:1, b:0),
% 2.91/3.29 k5_lattices [42, 1] (w:1, o:42, a:1, s:1, b:0),
% 2.91/3.29 r2_hidden [43, 2] (w:1, o:117, a:1, s:1, b:0),
% 2.91/3.29 v3_lattices [44, 1] (w:1, o:50, a:1, s:1, b:0),
% 2.91/3.29 u1_struct_0 [45, 1] (w:1, o:34, a:1, s:1, b:0),
% 2.91/3.29 u2_lattices [46, 1] (w:1, o:36, a:1, s:1, b:0),
% 2.91/3.29 u1_lattices [47, 1] (w:1, o:35, a:1, s:1, b:0),
% 2.91/3.29 g3_lattices [48, 3] (w:1, o:126, a:1, s:1, b:0),
% 2.91/3.29 v1_xboole_0 [49, 1] (w:1, o:51, a:1, s:1, b:0),
% 2.91/3.29 v1_funct_1 [50, 1] (w:1, o:52, a:1, s:1, b:0),
% 2.91/3.29 v4_lattices [51, 1] (w:1, o:53, a:1, s:1, b:0),
% 2.91/3.29 v5_lattices [52, 1] (w:1, o:54, a:1, s:1, b:0),
% 2.91/3.29 v6_lattices [53, 1] (w:1, o:55, a:1, s:1, b:0),
% 2.91/3.29 v7_lattices [54, 1] (w:1, o:56, a:1, s:1, b:0),
% 2.91/3.29 v8_lattices [55, 1] (w:1, o:57, a:1, s:1, b:0),
% 2.91/3.29 v9_lattices [56, 1] (w:1, o:58, a:1, s:1, b:0),
% 2.91/3.29 k2_zfmisc_1 [58, 2] (w:1, o:119, a:1, s:1, b:0),
% 2.91/3.29 k1_zfmisc_1 [59, 1] (w:1, o:43, a:1, s:1, b:0),
% 2.91/3.29 m1_subset_1 [60, 2] (w:1, o:112, a:1, s:1, b:0),
% 2.91/3.29 v1_relat_1 [61, 1] (w:1, o:59, a:1, s:1, b:0),
% 2.91/3.29 v2_funct_1 [62, 1] (w:1, o:39, a:1, s:1, b:0),
% 2.91/3.29 v14_lattices [63, 1] (w:1, o:37, a:1, s:1, b:0),
% 2.91/3.29 v15_lattices [64, 1] (w:1, o:38, a:1, s:1, b:0),
% 2.91/3.29 k1_lattice2 [65, 1] (w:1, o:44, a:1, s:1, b:0),
% 2.91/3.29 k7_filter_2 [66, 2] (w:1, o:120, a:1, s:1, b:0),
% 2.91/3.29 v1_funct_2 [67, 3] (w:1, o:127, a:1, s:1, b:0),
% 2.91/3.29 m1_relset_1 [68, 3] (w:1, o:128, a:1, s:1, b:0),
% 2.91/3.29 k15_filter_2 [69, 2] (w:1, o:118, a:1, s:1, b:0),
% 2.91/3.29 m1_filter_2 [70, 2] (w:1, o:113, a:1, s:1, b:0),
% 2.91/3.29 l1_lattices [71, 1] (w:1, o:60, a:1, s:1, b:0),
% 2.91/3.29 l2_lattices [72, 1] (w:1, o:47, a:1, s:1, b:0),
% 2.91/3.29 k6_lattices [73, 1] (w:1, o:45, a:1, s:1, b:0),
% 2.91/3.29 l1_struct_0 [74, 1] (w:1, o:46, a:1, s:1, b:0),
% 2.91/3.29 m1_filter_0 [75, 2] (w:1, o:114, a:1, s:1, b:0),
% 2.91/3.29 m2_lattice4 [76, 2] (w:1, o:121, a:1, s:1, b:0),
% 2.91/3.29 m2_relset_1 [77, 3] (w:1, o:129, a:1, s:1, b:0),
% 2.91/3.29 k1_xboole_0 [78, 0] (w:1, o:9, a:1, s:1, b:0),
% 2.91/3.29 v1_binop_1 [79, 2] (w:1, o:122, a:1, s:1, b:0),
% 2.91/3.29 v1_partfun1 [80, 3] (w:1, o:130, a:1, s:1, b:0),
% 2.91/3.29 v2_binop_1 [81, 2] (w:1, o:123, a:1, s:1, b:0),
% 2.91/3.29 r1_tarski [85, 2] (w:1, o:116, a:1, s:1, b:0),
% 2.91/3.29 alpha1 [86, 1] (w:1, o:61, a:1, s:1, b:1),
% 2.91/3.29 alpha2 [87, 1] (w:1, o:71, a:1, s:1, b:1),
% 2.91/3.29 alpha3 [88, 1] (w:1, o:72, a:1, s:1, b:1),
% 2.91/3.29 alpha4 [89, 1] (w:1, o:73, a:1, s:1, b:1),
% 2.91/3.29 alpha5 [90, 1] (w:1, o:74, a:1, s:1, b:1),
% 2.91/3.29 alpha6 [91, 1] (w:1, o:75, a:1, s:1, b:1),
% 2.91/3.29 alpha7 [92, 1] (w:1, o:76, a:1, s:1, b:1),
% 2.91/3.29 alpha8 [93, 1] (w:1, o:77, a:1, s:1, b:1),
% 52.29/52.77 alpha9 [94, 1] (w:1, o:78, a:1, s:1, b:1),
% 52.29/52.77 alpha10 [95, 1] (w:1, o:62, a:1, s:1, b:1),
% 52.29/52.77 alpha11 [96, 1] (w:1, o:63, a:1, s:1, b:1),
% 52.29/52.77 alpha12 [97, 1] (w:1, o:64, a:1, s:1, b:1),
% 52.29/52.77 alpha13 [98, 1] (w:1, o:65, a:1, s:1, b:1),
% 52.29/52.77 alpha14 [99, 1] (w:1, o:66, a:1, s:1, b:1),
% 52.29/52.77 alpha15 [100, 1] (w:1, o:67, a:1, s:1, b:1),
% 52.29/52.77 alpha16 [101, 1] (w:1, o:68, a:1, s:1, b:1),
% 52.29/52.77 alpha17 [102, 1] (w:1, o:69, a:1, s:1, b:1),
% 52.29/52.77 alpha18 [103, 1] (w:1, o:70, a:1, s:1, b:1),
% 52.29/52.77 skol1 [104, 0] (w:1, o:13, a:1, s:1, b:1),
% 52.29/52.77 skol2 [105, 0] (w:1, o:18, a:1, s:1, b:1),
% 52.29/52.77 skol3 [106, 0] (w:1, o:26, a:1, s:1, b:1),
% 52.29/52.77 skol4 [107, 0] (w:1, o:27, a:1, s:1, b:1),
% 52.29/52.77 skol5 [108, 0] (w:1, o:28, a:1, s:1, b:1),
% 52.29/52.77 skol6 [109, 1] (w:1, o:79, a:1, s:1, b:1),
% 52.29/52.77 skol7 [110, 1] (w:1, o:80, a:1, s:1, b:1),
% 52.29/52.77 skol8 [111, 2] (w:1, o:124, a:1, s:1, b:1),
% 52.29/52.77 skol9 [112, 1] (w:1, o:81, a:1, s:1, b:1),
% 52.29/52.77 skol10 [113, 1] (w:1, o:82, a:1, s:1, b:1),
% 52.29/52.77 skol11 [114, 1] (w:1, o:83, a:1, s:1, b:1),
% 52.29/52.77 skol12 [115, 2] (w:1, o:125, a:1, s:1, b:1),
% 52.29/52.77 skol13 [116, 0] (w:1, o:14, a:1, s:1, b:1),
% 52.29/52.77 skol14 [117, 0] (w:1, o:15, a:1, s:1, b:1),
% 52.29/52.77 skol15 [118, 1] (w:1, o:84, a:1, s:1, b:1),
% 52.29/52.77 skol16 [119, 1] (w:1, o:85, a:1, s:1, b:1),
% 52.29/52.77 skol17 [120, 0] (w:1, o:16, a:1, s:1, b:1),
% 52.29/52.77 skol18 [121, 0] (w:1, o:17, a:1, s:1, b:1),
% 52.29/52.77 skol19 [122, 1] (w:1, o:86, a:1, s:1, b:1),
% 52.29/52.77 skol20 [123, 0] (w:1, o:19, a:1, s:1, b:1),
% 52.29/52.77 skol21 [124, 0] (w:1, o:20, a:1, s:1, b:1),
% 52.29/52.77 skol22 [125, 0] (w:1, o:21, a:1, s:1, b:1),
% 52.29/52.77 skol23 [126, 0] (w:1, o:22, a:1, s:1, b:1),
% 52.29/52.77 skol24 [127, 1] (w:1, o:87, a:1, s:1, b:1),
% 52.29/52.77 skol25 [128, 0] (w:1, o:23, a:1, s:1, b:1),
% 52.29/52.77 skol26 [129, 0] (w:1, o:24, a:1, s:1, b:1),
% 52.29/52.77 skol27 [130, 0] (w:1, o:25, a:1, s:1, b:1).
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Starting Search:
% 52.29/52.77
% 52.29/52.77 *** allocated 15000 integers for clauses
% 52.29/52.77 *** allocated 22500 integers for clauses
% 52.29/52.77 *** allocated 33750 integers for clauses
% 52.29/52.77 *** allocated 15000 integers for termspace/termends
% 52.29/52.77 *** allocated 50625 integers for clauses
% 52.29/52.77 *** allocated 22500 integers for termspace/termends
% 52.29/52.77 *** allocated 75937 integers for clauses
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 113905 integers for clauses
% 52.29/52.77 *** allocated 33750 integers for termspace/termends
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 3852
% 52.29/52.77 Kept: 2113
% 52.29/52.77 Inuse: 404
% 52.29/52.77 Deleted: 36
% 52.29/52.77 Deletedinuse: 0
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 170857 integers for clauses
% 52.29/52.77 *** allocated 50625 integers for termspace/termends
% 52.29/52.77 *** allocated 75937 integers for termspace/termends
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 113905 integers for termspace/termends
% 52.29/52.77 *** allocated 256285 integers for clauses
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 16126
% 52.29/52.77 Kept: 4113
% 52.29/52.77 Inuse: 531
% 52.29/52.77 Deleted: 64
% 52.29/52.77 Deletedinuse: 15
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 170857 integers for termspace/termends
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 384427 integers for clauses
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 22955
% 52.29/52.77 Kept: 6159
% 52.29/52.77 Inuse: 640
% 52.29/52.77 Deleted: 68
% 52.29/52.77 Deletedinuse: 17
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 43757
% 52.29/52.77 Kept: 8193
% 52.29/52.77 Inuse: 894
% 52.29/52.77 Deleted: 107
% 52.29/52.77 Deletedinuse: 18
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 576640 integers for clauses
% 52.29/52.77 *** allocated 256285 integers for termspace/termends
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 59975
% 52.29/52.77 Kept: 10193
% 52.29/52.77 Inuse: 1122
% 52.29/52.77 Deleted: 129
% 52.29/52.77 Deletedinuse: 18
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 78888
% 52.29/52.77 Kept: 12963
% 52.29/52.77 Inuse: 1298
% 52.29/52.77 Deleted: 138
% 52.29/52.77 Deletedinuse: 18
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 864960 integers for clauses
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 91775
% 52.29/52.77 Kept: 14968
% 52.29/52.77 Inuse: 1463
% 52.29/52.77 Deleted: 248
% 52.29/52.77 Deletedinuse: 121
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 384427 integers for termspace/termends
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 100689
% 52.29/52.77 Kept: 16983
% 52.29/52.77 Inuse: 1613
% 52.29/52.77 Deleted: 256
% 52.29/52.77 Deletedinuse: 121
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 111785
% 52.29/52.77 Kept: 19007
% 52.29/52.77 Inuse: 1798
% 52.29/52.77 Deleted: 294
% 52.29/52.77 Deletedinuse: 121
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying clauses:
% 52.29/52.77 *** allocated 1297440 integers for clauses
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 119372
% 52.29/52.77 Kept: 21025
% 52.29/52.77 Inuse: 1914
% 52.29/52.77 Deleted: 3659
% 52.29/52.77 Deletedinuse: 384
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 134783
% 52.29/52.77 Kept: 23067
% 52.29/52.77 Inuse: 2189
% 52.29/52.77 Deleted: 3674
% 52.29/52.77 Deletedinuse: 399
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 165924
% 52.29/52.77 Kept: 25069
% 52.29/52.77 Inuse: 2569
% 52.29/52.77 Deleted: 3693
% 52.29/52.77 Deletedinuse: 402
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 180843
% 52.29/52.77 Kept: 27077
% 52.29/52.77 Inuse: 2752
% 52.29/52.77 Deleted: 3694
% 52.29/52.77 Deletedinuse: 402
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 576640 integers for termspace/termends
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 201430
% 52.29/52.77 Kept: 29086
% 52.29/52.77 Inuse: 2967
% 52.29/52.77 Deleted: 3751
% 52.29/52.77 Deletedinuse: 402
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 1946160 integers for clauses
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 214212
% 52.29/52.77 Kept: 31261
% 52.29/52.77 Inuse: 3093
% 52.29/52.77 Deleted: 3752
% 52.29/52.77 Deletedinuse: 402
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 222706
% 52.29/52.77 Kept: 33906
% 52.29/52.77 Inuse: 3182
% 52.29/52.77 Deleted: 3752
% 52.29/52.77 Deletedinuse: 402
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 226023
% 52.29/52.77 Kept: 35906
% 52.29/52.77 Inuse: 3202
% 52.29/52.77 Deleted: 3752
% 52.29/52.77 Deletedinuse: 402
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 228409
% 52.29/52.77 Kept: 37930
% 52.29/52.77 Inuse: 3205
% 52.29/52.77 Deleted: 3752
% 52.29/52.77 Deletedinuse: 402
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 234817
% 52.29/52.77 Kept: 39930
% 52.29/52.77 Inuse: 3270
% 52.29/52.77 Deleted: 3752
% 52.29/52.77 Deletedinuse: 402
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying clauses:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 244352
% 52.29/52.77 Kept: 41941
% 52.29/52.77 Inuse: 3378
% 52.29/52.77 Deleted: 8134
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 261933
% 52.29/52.77 Kept: 43974
% 52.29/52.77 Inuse: 3539
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 2919240 integers for clauses
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 *** allocated 864960 integers for termspace/termends
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 276952
% 52.29/52.77 Kept: 45979
% 52.29/52.77 Inuse: 3655
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 287222
% 52.29/52.77 Kept: 47979
% 52.29/52.77 Inuse: 3736
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 396539
% 52.29/52.77 Kept: 49979
% 52.29/52.77 Inuse: 4021
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 418958
% 52.29/52.77 Kept: 52023
% 52.29/52.77 Inuse: 4215
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 460953
% 52.29/52.77 Kept: 54052
% 52.29/52.77 Inuse: 4395
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 480075
% 52.29/52.77 Kept: 56057
% 52.29/52.77 Inuse: 4519
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 493250
% 52.29/52.77 Kept: 58185
% 52.29/52.77 Inuse: 4586
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Intermediate Status:
% 52.29/52.77 Generated: 510305
% 52.29/52.77 Kept: 60203
% 52.29/52.77 Inuse: 4677
% 52.29/52.77 Deleted: 8136
% 52.29/52.77 Deletedinuse: 405
% 52.29/52.77
% 52.29/52.77 Resimplifying inuse:
% 52.29/52.77 Done
% 52.29/52.77
% 52.29/52.77 Resimplifying clauses:
% 52.29/52.77
% 52.29/52.77 Bliksems!, er is een bewijs:
% 52.29/52.77 % SZS status Theorem
% 52.29/52.77 % SZS output start Refutation
% 52.29/52.77
% 52.29/52.77 (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.29/52.77 (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.29/52.77 (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.29/52.77 (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol27, skol1 ) }.
% 52.29/52.77 (4) {G0,W2,D2,L1,V0,M1} I { v13_lattices( skol1 ) }.
% 52.29/52.77 (5) {G0,W4,D3,L1,V0,M1} I { ! r2_hidden( k5_lattices( skol1 ), skol27 ) }.
% 52.29/52.77 (31) {G0,W16,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 52.29/52.77 k7_filter_2( X, Y ) ==> Y }.
% 52.29/52.77 (34) {G0,W15,D3,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_filter_2( Y, X ), m1_filter_2( k15_filter_2( X, Y
% 52.29/52.77 ), k1_lattice2( X ) ) }.
% 52.29/52.77 (36) {G0,W5,D3,L2,V1,M2} I { ! l3_lattices( X ), l3_lattices( k1_lattice2(
% 52.29/52.77 X ) ) }.
% 52.29/52.77 (50) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 52.29/52.77 (51) {G0,W14,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y, k1_zfmisc_1(
% 52.29/52.77 u1_struct_0( X ) ) ) }.
% 52.29/52.77 (70) {G0,W7,D3,L3,V1,M3} I { v3_struct_0( X ), ! l3_lattices( X ), !
% 52.29/52.77 v3_struct_0( k1_lattice2( X ) ) }.
% 52.29/52.77 (113) {G0,W9,D3,L4,V1,M4} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), v10_lattices( k1_lattice2( X ) ) }.
% 52.29/52.77 (184) {G0,W16,D3,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_filter_2( Y, X ), k7_filter_2( X, Y ) ==>
% 52.29/52.77 k15_filter_2( X, Y ) }.
% 52.29/52.77 (185) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_filter_2( Y, X ), m1_filter_0( Y, X ) }.
% 52.29/52.77 (190) {G0,W15,D3,L6,V2,M6} I;f;f;f { v3_struct_0( X ), ! v10_lattices( X )
% 52.29/52.77 , ! l3_lattices( X ), ! m1_filter_0( Y, X ), ! v14_lattices( X ),
% 52.29/52.77 r2_hidden( k6_lattices( X ), Y ) }.
% 52.29/52.77 (197) {G0,W11,D3,L5,V1,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! v13_lattices( X ), v14_lattices( k1_lattice2( X ) )
% 52.29/52.77 }.
% 52.29/52.77 (200) {G0,W14,D4,L5,V1,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 v13_lattices( X ), ! l3_lattices( X ), k6_lattices( k1_lattice2( X ) )
% 52.29/52.77 ==> k5_lattices( X ) }.
% 52.29/52.77 (423) {G1,W10,D3,L3,V0,M3} R(34,3);r(0) { ! v10_lattices( skol1 ), !
% 52.29/52.77 l3_lattices( skol1 ), m1_filter_2( k15_filter_2( skol1, skol27 ),
% 52.29/52.77 k1_lattice2( skol1 ) ) }.
% 52.29/52.77 (457) {G1,W3,D3,L1,V0,M1} R(36,2) { l3_lattices( k1_lattice2( skol1 ) ) }.
% 52.29/52.77 (731) {G1,W7,D2,L3,V0,M3} R(50,3);r(0) { ! v10_lattices( skol1 ), !
% 52.29/52.77 l3_lattices( skol1 ), m2_lattice4( skol27, skol1 ) }.
% 52.29/52.77 (751) {G1,W14,D3,L5,V2,M5} R(51,31);f;f;f { v3_struct_0( X ), !
% 52.29/52.77 v10_lattices( X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ), k7_filter_2
% 52.29/52.77 ( X, Y ) ==> Y }.
% 52.29/52.77 (1099) {G1,W3,D3,L1,V0,M1} R(70,2);r(0) { ! v3_struct_0( k1_lattice2( skol1
% 52.29/52.77 ) ) }.
% 52.29/52.77 (2413) {G1,W5,D3,L2,V0,M2} R(113,2);r(0) { ! v10_lattices( skol1 ),
% 52.29/52.77 v10_lattices( k1_lattice2( skol1 ) ) }.
% 52.29/52.77 (4701) {G1,W11,D3,L3,V0,M3} R(184,3);r(0) { ! v10_lattices( skol1 ), !
% 52.29/52.77 l3_lattices( skol1 ), k7_filter_2( skol1, skol27 ) ==> k15_filter_2(
% 52.29/52.77 skol1, skol27 ) }.
% 52.29/52.77 (5443) {G1,W7,D3,L3,V0,M3} R(197,4);r(0) { ! v10_lattices( skol1 ), !
% 52.29/52.77 l3_lattices( skol1 ), v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.29/52.77 (5665) {G1,W10,D4,L3,V0,M3} R(200,4);r(0) { ! v10_lattices( skol1 ), !
% 52.29/52.77 l3_lattices( skol1 ), k6_lattices( k1_lattice2( skol1 ) ) ==> k5_lattices
% 52.29/52.77 ( skol1 ) }.
% 52.29/52.77 (8252) {G2,W3,D3,L1,V0,M1} S(2413);r(1) { v10_lattices( k1_lattice2( skol1
% 52.29/52.77 ) ) }.
% 52.29/52.77 (11705) {G2,W6,D3,L1,V0,M1} S(423);r(1);r(2) { m1_filter_2( k15_filter_2(
% 52.29/52.77 skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.29/52.77 (20666) {G2,W6,D4,L1,V0,M1} S(5665);r(1);r(2) { k6_lattices( k1_lattice2(
% 52.29/52.77 skol1 ) ) ==> k5_lattices( skol1 ) }.
% 52.29/52.77 (20723) {G2,W3,D3,L1,V0,M1} S(5443);r(1);r(2) { v14_lattices( k1_lattice2(
% 52.29/52.77 skol1 ) ) }.
% 52.29/52.77 (20759) {G2,W7,D3,L1,V0,M1} S(4701);r(1);r(2) { k7_filter_2( skol1, skol27
% 52.29/52.77 ) ==> k15_filter_2( skol1, skol27 ) }.
% 52.29/52.77 (20948) {G2,W3,D2,L1,V0,M1} S(731);r(1);r(2) { m2_lattice4( skol27, skol1 )
% 52.29/52.77 }.
% 52.29/52.77 (23131) {G3,W9,D3,L3,V0,M3} R(751,20948);d(20759);r(0) { ! v10_lattices(
% 52.29/52.77 skol1 ), ! l3_lattices( skol1 ), k15_filter_2( skol1, skol27 ) ==> skol27
% 52.29/52.77 }.
% 52.29/52.77 (30255) {G3,W12,D3,L3,V0,M3} R(11705,185);r(1099) { ! v10_lattices(
% 52.29/52.77 k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2( skol1 ) ),
% 52.29/52.77 m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.29/52.77 (41036) {G4,W6,D3,L1,V0,M1} S(30255);r(8252);r(457) { m1_filter_0(
% 52.29/52.77 k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.29/52.77 (41447) {G4,W5,D3,L1,V0,M1} S(23131);r(1);r(2) { k15_filter_2( skol1,
% 52.29/52.77 skol27 ) ==> skol27 }.
% 52.29/52.77 (42523) {G5,W4,D3,L1,V0,M1} S(41036);d(41447) { m1_filter_0( skol27,
% 52.29/52.77 k1_lattice2( skol1 ) ) }.
% 52.29/52.77 (42538) {G6,W13,D3,L4,V0,M4} R(42523,190);d(20666);r(1099) { ! v10_lattices
% 52.29/52.77 ( k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2( skol1 ) ), !
% 52.29/52.77 v14_lattices( k1_lattice2( skol1 ) ), r2_hidden( k5_lattices( skol1 ),
% 52.29/52.77 skol27 ) }.
% 52.29/52.77 (62922) {G7,W0,D0,L0,V0,M0} S(42538);r(8252);r(457);r(20723);r(5) { }.
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 % SZS output end Refutation
% 52.29/52.77 found a proof!
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Unprocessed initial clauses:
% 52.29/52.77
% 52.29/52.77 (62924) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol1 ) }.
% 52.29/52.77 (62925) {G0,W2,D2,L1,V0,M1} { v10_lattices( skol1 ) }.
% 52.29/52.77 (62926) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol1 ) }.
% 52.29/52.77 (62927) {G0,W3,D2,L1,V0,M1} { m2_filter_2( skol27, skol1 ) }.
% 52.29/52.77 (62928) {G0,W2,D2,L1,V0,M1} { v13_lattices( skol1 ) }.
% 52.29/52.77 (62929) {G0,W4,D3,L1,V0,M1} { ! r2_hidden( k5_lattices( skol1 ), skol27 )
% 52.29/52.77 }.
% 52.29/52.77 (62930) {G0,W13,D4,L3,V1,M3} { ! l3_lattices( X ), ! v3_lattices( X ), X =
% 52.29/52.77 g3_lattices( u1_struct_0( X ), u2_lattices( X ), u1_lattices( X ) ) }.
% 52.29/52.77 (62931) {G0,W6,D2,L2,V2,M2} { ! r2_hidden( X, Y ), ! r2_hidden( Y, X ) }.
% 52.29/52.77 (62932) {G0,W4,D2,L2,V1,M2} { ! v1_xboole_0( X ), v1_funct_1( X ) }.
% 52.29/52.77 (62933) {G0,W8,D2,L4,V1,M4} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v10_lattices( X ), alpha1( X ) }.
% 52.29/52.77 (62934) {G0,W8,D2,L4,V1,M4} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v10_lattices( X ), v9_lattices( X ) }.
% 52.29/52.77 (62935) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), alpha7( X ) }.
% 52.29/52.77 (62936) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v8_lattices( X ) }.
% 52.29/52.77 (62937) {G0,W6,D2,L3,V1,M3} { ! alpha7( X ), ! v8_lattices( X ), alpha1( X
% 52.29/52.77 ) }.
% 52.29/52.77 (62938) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), alpha13( X ) }.
% 52.29/52.77 (62939) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), v7_lattices( X ) }.
% 52.29/52.77 (62940) {G0,W6,D2,L3,V1,M3} { ! alpha13( X ), ! v7_lattices( X ), alpha7(
% 52.29/52.77 X ) }.
% 52.29/52.77 (62941) {G0,W4,D2,L2,V1,M2} { ! alpha13( X ), alpha15( X ) }.
% 52.29/52.77 (62942) {G0,W4,D2,L2,V1,M2} { ! alpha13( X ), v6_lattices( X ) }.
% 52.29/52.77 (62943) {G0,W6,D2,L3,V1,M3} { ! alpha15( X ), ! v6_lattices( X ), alpha13
% 52.29/52.77 ( X ) }.
% 52.29/52.77 (62944) {G0,W4,D2,L2,V1,M2} { ! alpha15( X ), ! v3_struct_0( X ) }.
% 52.29/52.77 (62945) {G0,W4,D2,L2,V1,M2} { ! alpha15( X ), v4_lattices( X ) }.
% 52.29/52.77 (62946) {G0,W4,D2,L2,V1,M2} { ! alpha15( X ), v5_lattices( X ) }.
% 52.29/52.77 (62947) {G0,W8,D2,L4,V1,M4} { v3_struct_0( X ), ! v4_lattices( X ), !
% 52.29/52.77 v5_lattices( X ), alpha15( X ) }.
% 52.29/52.77 (62948) {G0,W8,D4,L2,V3,M2} { ! m1_subset_1( X, k1_zfmisc_1( k2_zfmisc_1(
% 52.29/52.77 Y, Z ) ) ), v1_relat_1( X ) }.
% 52.29/52.77 (62949) {G0,W8,D2,L4,V1,M4} { ! v1_relat_1( X ), ! v1_xboole_0( X ), !
% 52.29/52.77 v1_funct_1( X ), v1_relat_1( X ) }.
% 52.29/52.77 (62950) {G0,W8,D2,L4,V1,M4} { ! v1_relat_1( X ), ! v1_xboole_0( X ), !
% 52.29/52.77 v1_funct_1( X ), v1_funct_1( X ) }.
% 52.29/52.77 (62951) {G0,W8,D2,L4,V1,M4} { ! v1_relat_1( X ), ! v1_xboole_0( X ), !
% 52.29/52.77 v1_funct_1( X ), v2_funct_1( X ) }.
% 52.29/52.77 (62952) {G0,W18,D2,L9,V1,M9} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v4_lattices( X ), ! v5_lattices( X ), ! v6_lattices( X ), ! v7_lattices(
% 52.29/52.77 X ), ! v8_lattices( X ), ! v9_lattices( X ), ! v3_struct_0( X ) }.
% 52.29/52.77 (62953) {G0,W18,D2,L9,V1,M9} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v4_lattices( X ), ! v5_lattices( X ), ! v6_lattices( X ), ! v7_lattices(
% 52.29/52.77 X ), ! v8_lattices( X ), ! v9_lattices( X ), v10_lattices( X ) }.
% 52.29/52.77 (62954) {G0,W10,D2,L5,V1,M5} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v13_lattices( X ), ! v14_lattices( X ), ! v3_struct_0( X ) }.
% 52.29/52.77 (62955) {G0,W10,D2,L5,V1,M5} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v13_lattices( X ), ! v14_lattices( X ), v15_lattices( X ) }.
% 52.29/52.77 (62956) {G0,W8,D2,L4,V1,M4} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v15_lattices( X ), ! v3_struct_0( X ) }.
% 52.29/52.77 (62957) {G0,W8,D2,L4,V1,M4} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v15_lattices( X ), v13_lattices( X ) }.
% 52.29/52.77 (62958) {G0,W8,D2,L4,V1,M4} { ! l3_lattices( X ), v3_struct_0( X ), !
% 52.29/52.77 v15_lattices( X ), v14_lattices( X ) }.
% 52.29/52.77 (62959) {G0,W12,D4,L2,V1,M2} { ! l3_lattices( X ), k1_lattice2( X ) =
% 52.29/52.77 g3_lattices( u1_struct_0( X ), u1_lattices( X ), u2_lattices( X ) ) }.
% 52.29/52.77 (62960) {G0,W16,D4,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 52.29/52.77 k7_filter_2( X, Y ) = Y }.
% 52.29/52.77 (62961) {G0,W33,D3,L7,V3,M7} { ! v1_funct_1( Y ), ! v1_funct_2( Y,
% 52.29/52.77 k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), !
% 52.29/52.77 v1_funct_1( Z ), ! v1_funct_2( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1
% 52.29/52.77 ( Z, k2_zfmisc_1( X, X ), X ), v3_lattices( g3_lattices( X, Y, Z ) ) }.
% 52.29/52.77 (62962) {G0,W33,D3,L7,V3,M7} { ! v1_funct_1( Y ), ! v1_funct_2( Y,
% 52.29/52.77 k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), !
% 52.29/52.77 v1_funct_1( Z ), ! v1_funct_2( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1
% 52.29/52.77 ( Z, k2_zfmisc_1( X, X ), X ), l3_lattices( g3_lattices( X, Y, Z ) ) }.
% 52.29/52.77 (62963) {G0,W15,D3,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_filter_2( Y, X ), m1_filter_2( k15_filter_2( X, Y
% 52.29/52.77 ), k1_lattice2( X ) ) }.
% 52.29/52.77 (62964) {G0,W5,D3,L2,V1,M2} { ! l3_lattices( X ), v3_lattices( k1_lattice2
% 52.29/52.77 ( X ) ) }.
% 52.29/52.77 (62965) {G0,W5,D3,L2,V1,M2} { ! l3_lattices( X ), l3_lattices( k1_lattice2
% 52.29/52.77 ( X ) ) }.
% 52.29/52.77 (62966) {G0,W1,D1,L1,V0,M1} { && }.
% 52.29/52.77 (62967) {G0,W1,D1,L1,V0,M1} { && }.
% 52.29/52.77 (62968) {G0,W1,D1,L1,V0,M1} { && }.
% 52.29/52.77 (62969) {G0,W9,D3,L3,V1,M3} { v3_struct_0( X ), ! l1_lattices( X ),
% 52.29/52.77 m1_subset_1( k5_lattices( X ), u1_struct_0( X ) ) }.
% 52.29/52.77 (62970) {G0,W9,D3,L3,V1,M3} { v3_struct_0( X ), ! l2_lattices( X ),
% 52.29/52.77 m1_subset_1( k6_lattices( X ), u1_struct_0( X ) ) }.
% 52.29/52.77 (62971) {G0,W19,D5,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 52.29/52.77 m1_subset_1( k7_filter_2( X, Y ), k1_zfmisc_1( u1_struct_0( k1_lattice2(
% 52.29/52.77 X ) ) ) ) }.
% 52.29/52.77 (62972) {G0,W4,D2,L2,V1,M2} { ! l1_lattices( X ), l1_struct_0( X ) }.
% 52.29/52.77 (62973) {G0,W1,D1,L1,V0,M1} { && }.
% 52.29/52.77 (62974) {G0,W4,D2,L2,V1,M2} { ! l2_lattices( X ), l1_struct_0( X ) }.
% 52.29/52.77 (62975) {G0,W4,D2,L2,V1,M2} { ! l3_lattices( X ), l1_lattices( X ) }.
% 52.29/52.77 (62976) {G0,W4,D2,L2,V1,M2} { ! l3_lattices( X ), l2_lattices( X ) }.
% 52.29/52.77 (62977) {G0,W11,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_filter_0( Y, X ), ! v1_xboole_0( Y ) }.
% 52.29/52.77 (62978) {G0,W14,D4,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_filter_0( Y, X ), m1_subset_1( Y, k1_zfmisc_1(
% 52.29/52.77 u1_struct_0( X ) ) ) }.
% 52.29/52.77 (62979) {G0,W11,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_filter_2( Y, X ), ! v1_xboole_0( Y ) }.
% 52.29/52.77 (62980) {G0,W12,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 52.29/52.77 (62981) {G0,W1,D1,L1,V0,M1} { && }.
% 52.29/52.77 (62982) {G0,W1,D1,L1,V0,M1} { && }.
% 52.29/52.77 (62983) {G0,W11,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_filter_2( Y, X ), ! v1_xboole_0( Y ) }.
% 52.29/52.77 (62984) {G0,W12,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 52.29/52.77 (62985) {G0,W14,D4,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y, k1_zfmisc_1(
% 52.29/52.77 u1_struct_0( X ) ) ) }.
% 52.29/52.77 (62986) {G0,W10,D4,L2,V3,M2} { ! m2_relset_1( Z, X, Y ), m1_subset_1( Z,
% 52.29/52.77 k1_zfmisc_1( k2_zfmisc_1( X, Y ) ) ) }.
% 52.29/52.77 (62987) {G0,W5,D3,L2,V1,M2} { ! l1_lattices( X ), v1_funct_1( u1_lattices
% 52.29/52.77 ( X ) ) }.
% 52.29/52.77 (62988) {G0,W12,D4,L2,V1,M2} { ! l1_lattices( X ), v1_funct_2( u1_lattices
% 52.29/52.77 ( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X
% 52.29/52.77 ) ) }.
% 52.29/52.77 (62989) {G0,W12,D4,L2,V1,M2} { ! l1_lattices( X ), m2_relset_1(
% 52.29/52.77 u1_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ),
% 52.29/52.77 u1_struct_0( X ) ) }.
% 52.29/52.77 (62990) {G0,W1,D1,L1,V0,M1} { && }.
% 52.29/52.77 (62991) {G0,W5,D3,L2,V1,M2} { ! l2_lattices( X ), v1_funct_1( u2_lattices
% 52.29/52.77 ( X ) ) }.
% 52.29/52.77 (62992) {G0,W12,D4,L2,V1,M2} { ! l2_lattices( X ), v1_funct_2( u2_lattices
% 52.29/52.77 ( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X
% 52.29/52.77 ) ) }.
% 52.29/52.77 (62993) {G0,W12,D4,L2,V1,M2} { ! l2_lattices( X ), m2_relset_1(
% 52.29/52.77 u2_lattices( X ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ),
% 52.29/52.77 u1_struct_0( X ) ) }.
% 52.29/52.77 (62994) {G0,W2,D2,L1,V0,M1} { l1_lattices( skol2 ) }.
% 52.29/52.77 (62995) {G0,W2,D2,L1,V0,M1} { l1_struct_0( skol3 ) }.
% 52.29/52.77 (62996) {G0,W2,D2,L1,V0,M1} { l2_lattices( skol4 ) }.
% 52.29/52.77 (62997) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol5 ) }.
% 52.29/52.77 (62998) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), m1_filter_0( skol6( X ), X ) }.
% 52.29/52.77 (62999) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), m1_filter_2( skol7( X ), X ) }.
% 52.29/52.77 (63000) {G0,W6,D3,L1,V2,M1} { m1_relset_1( skol8( X, Y ), X, Y ) }.
% 52.29/52.77 (63001) {G0,W4,D3,L1,V1,M1} { m1_subset_1( skol9( X ), X ) }.
% 52.29/52.77 (63002) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), m2_filter_2( skol10( X ), X ) }.
% 52.29/52.77 (63003) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), m2_lattice4( skol11( X ), X ) }.
% 52.29/52.77 (63004) {G0,W6,D3,L1,V2,M1} { m2_relset_1( skol12( X, Y ), X, Y ) }.
% 52.29/52.77 (63005) {G0,W17,D4,L6,V2,M6} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y, k1_zfmisc_1(
% 52.29/52.77 u1_struct_0( X ) ) ), ! v1_xboole_0( k7_filter_2( X, Y ) ) }.
% 52.29/52.77 (63006) {G0,W7,D3,L3,V1,M3} { v3_struct_0( X ), ! l3_lattices( X ), !
% 52.29/52.77 v3_struct_0( k1_lattice2( X ) ) }.
% 52.29/52.77 (63007) {G0,W7,D3,L3,V1,M3} { v3_struct_0( X ), ! l3_lattices( X ),
% 52.29/52.77 v3_lattices( k1_lattice2( X ) ) }.
% 52.29/52.77 (63008) {G0,W7,D3,L3,V1,M3} { v3_struct_0( X ), ! l1_struct_0( X ), !
% 52.29/52.77 v1_xboole_0( u1_struct_0( X ) ) }.
% 52.29/52.77 (63009) {G0,W3,D3,L1,V1,M1} { ! v1_xboole_0( k1_zfmisc_1( X ) ) }.
% 52.29/52.77 (63010) {G0,W2,D2,L1,V0,M1} { v1_xboole_0( k1_xboole_0 ) }.
% 52.29/52.77 (63011) {G0,W8,D2,L4,V1,M4} { v3_struct_0( X ), ! v4_lattices( X ), !
% 52.29/52.77 l2_lattices( X ), alpha2( X ) }.
% 52.29/52.77 (63012) {G0,W16,D4,L4,V1,M4} { v3_struct_0( X ), ! v4_lattices( X ), !
% 52.29/52.77 l2_lattices( X ), v1_partfun1( u2_lattices( X ), k2_zfmisc_1( u1_struct_0
% 52.29/52.77 ( X ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 52.29/52.77 (63013) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha8( X ) }.
% 52.29/52.77 (63014) {G0,W7,D3,L2,V1,M2} { ! alpha2( X ), v1_binop_1( u2_lattices( X )
% 52.29/52.77 , u1_struct_0( X ) ) }.
% 52.29/52.77 (63015) {G0,W9,D3,L3,V1,M3} { ! alpha8( X ), ! v1_binop_1( u2_lattices( X
% 52.29/52.77 ), u1_struct_0( X ) ), alpha2( X ) }.
% 52.29/52.77 (63016) {G0,W5,D3,L2,V1,M2} { ! alpha8( X ), v1_relat_1( u2_lattices( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63017) {G0,W5,D3,L2,V1,M2} { ! alpha8( X ), v1_funct_1( u2_lattices( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63018) {G0,W12,D4,L2,V1,M2} { ! alpha8( X ), v1_funct_2( u2_lattices( X )
% 52.29/52.77 , k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) )
% 52.29/52.77 }.
% 52.29/52.77 (63019) {G0,W18,D4,L4,V1,M4} { ! v1_relat_1( u2_lattices( X ) ), !
% 52.29/52.77 v1_funct_1( u2_lattices( X ) ), ! v1_funct_2( u2_lattices( X ),
% 52.29/52.77 k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) ),
% 52.29/52.77 alpha8( X ) }.
% 52.29/52.77 (63020) {G0,W8,D2,L4,V1,M4} { v3_struct_0( X ), ! v5_lattices( X ), !
% 52.29/52.77 l2_lattices( X ), alpha3( X ) }.
% 52.29/52.77 (63021) {G0,W16,D4,L4,V1,M4} { v3_struct_0( X ), ! v5_lattices( X ), !
% 52.29/52.77 l2_lattices( X ), v1_partfun1( u2_lattices( X ), k2_zfmisc_1( u1_struct_0
% 52.29/52.77 ( X ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 52.29/52.77 (63022) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha9( X ) }.
% 52.29/52.77 (63023) {G0,W7,D3,L2,V1,M2} { ! alpha3( X ), v2_binop_1( u2_lattices( X )
% 52.29/52.77 , u1_struct_0( X ) ) }.
% 52.29/52.77 (63024) {G0,W9,D3,L3,V1,M3} { ! alpha9( X ), ! v2_binop_1( u2_lattices( X
% 52.29/52.77 ), u1_struct_0( X ) ), alpha3( X ) }.
% 52.29/52.77 (63025) {G0,W5,D3,L2,V1,M2} { ! alpha9( X ), v1_relat_1( u2_lattices( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63026) {G0,W5,D3,L2,V1,M2} { ! alpha9( X ), v1_funct_1( u2_lattices( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63027) {G0,W12,D4,L2,V1,M2} { ! alpha9( X ), v1_funct_2( u2_lattices( X )
% 52.29/52.77 , k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) )
% 52.29/52.77 }.
% 52.29/52.77 (63028) {G0,W18,D4,L4,V1,M4} { ! v1_relat_1( u2_lattices( X ) ), !
% 52.29/52.77 v1_funct_1( u2_lattices( X ) ), ! v1_funct_2( u2_lattices( X ),
% 52.29/52.77 k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) ),
% 52.29/52.77 alpha9( X ) }.
% 52.29/52.77 (63029) {G0,W35,D3,L8,V3,M8} { v1_xboole_0( X ), ! v1_funct_1( Y ), !
% 52.29/52.77 v1_funct_2( Y, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Y, k2_zfmisc_1( X
% 52.29/52.77 , X ), X ), ! v1_funct_1( Z ), ! v1_funct_2( Z, k2_zfmisc_1( X, X ), X )
% 52.29/52.77 , ! m1_relset_1( Z, k2_zfmisc_1( X, X ), X ), ! v3_struct_0( g3_lattices
% 52.29/52.77 ( X, Y, Z ) ) }.
% 52.29/52.77 (63030) {G0,W35,D3,L8,V3,M8} { v1_xboole_0( X ), ! v1_funct_1( Y ), !
% 52.29/52.77 v1_funct_2( Y, k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Y, k2_zfmisc_1( X
% 52.29/52.77 , X ), X ), ! v1_funct_1( Z ), ! v1_funct_2( Z, k2_zfmisc_1( X, X ), X )
% 52.29/52.77 , ! m1_relset_1( Z, k2_zfmisc_1( X, X ), X ), v3_lattices( g3_lattices( X
% 52.29/52.77 , Y, Z ) ) }.
% 52.29/52.77 (63031) {G0,W8,D2,L4,V1,M4} { v3_struct_0( X ), ! v6_lattices( X ), !
% 52.29/52.77 l1_lattices( X ), alpha4( X ) }.
% 52.29/52.77 (63032) {G0,W16,D4,L4,V1,M4} { v3_struct_0( X ), ! v6_lattices( X ), !
% 52.29/52.77 l1_lattices( X ), v1_partfun1( u1_lattices( X ), k2_zfmisc_1( u1_struct_0
% 52.29/52.77 ( X ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 52.29/52.77 (63033) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), alpha10( X ) }.
% 52.29/52.77 (63034) {G0,W7,D3,L2,V1,M2} { ! alpha4( X ), v1_binop_1( u1_lattices( X )
% 52.29/52.77 , u1_struct_0( X ) ) }.
% 52.29/52.77 (63035) {G0,W9,D3,L3,V1,M3} { ! alpha10( X ), ! v1_binop_1( u1_lattices( X
% 52.29/52.77 ), u1_struct_0( X ) ), alpha4( X ) }.
% 52.29/52.77 (63036) {G0,W5,D3,L2,V1,M2} { ! alpha10( X ), v1_relat_1( u1_lattices( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63037) {G0,W5,D3,L2,V1,M2} { ! alpha10( X ), v1_funct_1( u1_lattices( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63038) {G0,W12,D4,L2,V1,M2} { ! alpha10( X ), v1_funct_2( u1_lattices( X
% 52.29/52.77 ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) )
% 52.29/52.77 }.
% 52.29/52.77 (63039) {G0,W18,D4,L4,V1,M4} { ! v1_relat_1( u1_lattices( X ) ), !
% 52.29/52.77 v1_funct_1( u1_lattices( X ) ), ! v1_funct_2( u1_lattices( X ),
% 52.29/52.77 k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) ),
% 52.29/52.77 alpha10( X ) }.
% 52.29/52.77 (63040) {G0,W8,D3,L3,V2,M3} { v1_xboole_0( X ), v1_xboole_0( Y ), !
% 52.29/52.77 v1_xboole_0( k2_zfmisc_1( X, Y ) ) }.
% 52.29/52.77 (63041) {G0,W8,D2,L4,V1,M4} { v3_struct_0( X ), ! v7_lattices( X ), !
% 52.29/52.77 l1_lattices( X ), alpha5( X ) }.
% 52.29/52.77 (63042) {G0,W16,D4,L4,V1,M4} { v3_struct_0( X ), ! v7_lattices( X ), !
% 52.29/52.77 l1_lattices( X ), v1_partfun1( u1_lattices( X ), k2_zfmisc_1( u1_struct_0
% 52.29/52.77 ( X ), u1_struct_0( X ) ), u1_struct_0( X ) ) }.
% 52.29/52.77 (63043) {G0,W4,D2,L2,V1,M2} { ! alpha5( X ), alpha11( X ) }.
% 52.29/52.77 (63044) {G0,W7,D3,L2,V1,M2} { ! alpha5( X ), v2_binop_1( u1_lattices( X )
% 52.29/52.77 , u1_struct_0( X ) ) }.
% 52.29/52.77 (63045) {G0,W9,D3,L3,V1,M3} { ! alpha11( X ), ! v2_binop_1( u1_lattices( X
% 52.29/52.77 ), u1_struct_0( X ) ), alpha5( X ) }.
% 52.29/52.77 (63046) {G0,W5,D3,L2,V1,M2} { ! alpha11( X ), v1_relat_1( u1_lattices( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63047) {G0,W5,D3,L2,V1,M2} { ! alpha11( X ), v1_funct_1( u1_lattices( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63048) {G0,W12,D4,L2,V1,M2} { ! alpha11( X ), v1_funct_2( u1_lattices( X
% 52.29/52.77 ), k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) )
% 52.29/52.77 }.
% 52.29/52.77 (63049) {G0,W18,D4,L4,V1,M4} { ! v1_relat_1( u1_lattices( X ) ), !
% 52.29/52.77 v1_funct_1( u1_lattices( X ) ), ! v1_funct_2( u1_lattices( X ),
% 52.29/52.77 k2_zfmisc_1( u1_struct_0( X ), u1_struct_0( X ) ), u1_struct_0( X ) ),
% 52.29/52.77 alpha11( X ) }.
% 52.29/52.77 (63050) {G0,W8,D2,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), alpha6( X ) }.
% 52.29/52.77 (63051) {G0,W9,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), v10_lattices( k1_lattice2( X ) ) }.
% 52.29/52.77 (63052) {G0,W4,D2,L2,V1,M2} { ! alpha6( X ), alpha12( X ) }.
% 52.29/52.77 (63053) {G0,W5,D3,L2,V1,M2} { ! alpha6( X ), v9_lattices( k1_lattice2( X )
% 52.29/52.77 ) }.
% 52.29/52.77 (63054) {G0,W7,D3,L3,V1,M3} { ! alpha12( X ), ! v9_lattices( k1_lattice2(
% 52.29/52.77 X ) ), alpha6( X ) }.
% 52.29/52.77 (63055) {G0,W4,D2,L2,V1,M2} { ! alpha12( X ), alpha14( X ) }.
% 52.29/52.77 (63056) {G0,W5,D3,L2,V1,M2} { ! alpha12( X ), v8_lattices( k1_lattice2( X
% 52.29/52.77 ) ) }.
% 52.29/52.77 (63057) {G0,W7,D3,L3,V1,M3} { ! alpha14( X ), ! v8_lattices( k1_lattice2(
% 52.29/52.77 X ) ), alpha12( X ) }.
% 52.29/52.77 (63058) {G0,W4,D2,L2,V1,M2} { ! alpha14( X ), alpha16( X ) }.
% 52.29/52.77 (63059) {G0,W5,D3,L2,V1,M2} { ! alpha14( X ), v7_lattices( k1_lattice2( X
% 52.29/52.77 ) ) }.
% 52.29/52.77 (63060) {G0,W7,D3,L3,V1,M3} { ! alpha16( X ), ! v7_lattices( k1_lattice2(
% 52.29/52.77 X ) ), alpha14( X ) }.
% 52.29/52.77 (63061) {G0,W4,D2,L2,V1,M2} { ! alpha16( X ), alpha17( X ) }.
% 52.29/52.77 (63062) {G0,W5,D3,L2,V1,M2} { ! alpha16( X ), v6_lattices( k1_lattice2( X
% 52.29/52.77 ) ) }.
% 52.29/52.77 (63063) {G0,W7,D3,L3,V1,M3} { ! alpha17( X ), ! v6_lattices( k1_lattice2(
% 52.29/52.77 X ) ), alpha16( X ) }.
% 52.29/52.77 (63064) {G0,W4,D2,L2,V1,M2} { ! alpha17( X ), alpha18( X ) }.
% 52.29/52.77 (63065) {G0,W5,D3,L2,V1,M2} { ! alpha17( X ), v5_lattices( k1_lattice2( X
% 52.29/52.77 ) ) }.
% 52.29/52.77 (63066) {G0,W7,D3,L3,V1,M3} { ! alpha18( X ), ! v5_lattices( k1_lattice2(
% 52.29/52.77 X ) ), alpha17( X ) }.
% 52.29/52.77 (63067) {G0,W5,D3,L2,V1,M2} { ! alpha18( X ), ! v3_struct_0( k1_lattice2(
% 52.29/52.77 X ) ) }.
% 52.29/52.77 (63068) {G0,W5,D3,L2,V1,M2} { ! alpha18( X ), v3_lattices( k1_lattice2( X
% 52.29/52.77 ) ) }.
% 52.29/52.77 (63069) {G0,W5,D3,L2,V1,M2} { ! alpha18( X ), v4_lattices( k1_lattice2( X
% 52.29/52.77 ) ) }.
% 52.29/52.77 (63070) {G0,W11,D3,L4,V1,M4} { v3_struct_0( k1_lattice2( X ) ), !
% 52.29/52.77 v3_lattices( k1_lattice2( X ) ), ! v4_lattices( k1_lattice2( X ) ),
% 52.29/52.77 alpha18( X ) }.
% 52.29/52.77 (63071) {G0,W40,D3,L8,V6,M8} { ! v1_funct_1( Y ), ! v1_funct_2( Y,
% 52.29/52.77 k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), !
% 52.29/52.77 v1_funct_1( Z ), ! v1_funct_2( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1
% 52.29/52.77 ( Z, k2_zfmisc_1( X, X ), X ), ! g3_lattices( X, Y, Z ) = g3_lattices( T
% 52.29/52.77 , U, W ), X = T }.
% 52.29/52.77 (63072) {G0,W40,D3,L8,V6,M8} { ! v1_funct_1( Y ), ! v1_funct_2( Y,
% 52.29/52.77 k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), !
% 52.29/52.77 v1_funct_1( Z ), ! v1_funct_2( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1
% 52.29/52.77 ( Z, k2_zfmisc_1( X, X ), X ), ! g3_lattices( X, Y, Z ) = g3_lattices( T
% 52.29/52.77 , U, W ), Y = U }.
% 52.29/52.77 (63073) {G0,W40,D3,L8,V6,M8} { ! v1_funct_1( Y ), ! v1_funct_2( Y,
% 52.29/52.77 k2_zfmisc_1( X, X ), X ), ! m1_relset_1( Y, k2_zfmisc_1( X, X ), X ), !
% 52.29/52.77 v1_funct_1( Z ), ! v1_funct_2( Z, k2_zfmisc_1( X, X ), X ), ! m1_relset_1
% 52.29/52.77 ( Z, k2_zfmisc_1( X, X ), X ), ! g3_lattices( X, Y, Z ) = g3_lattices( T
% 52.29/52.77 , U, W ), Z = W }.
% 52.29/52.77 (63074) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol13 ) }.
% 52.29/52.77 (63075) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol13 ) }.
% 52.29/52.77 (63076) {G0,W2,D2,L1,V0,M1} { v3_lattices( skol13 ) }.
% 52.29/52.77 (63077) {G0,W2,D2,L1,V0,M1} { v4_lattices( skol13 ) }.
% 52.29/52.77 (63078) {G0,W2,D2,L1,V0,M1} { v5_lattices( skol13 ) }.
% 52.29/52.77 (63079) {G0,W2,D2,L1,V0,M1} { v6_lattices( skol13 ) }.
% 52.29/52.77 (63080) {G0,W2,D2,L1,V0,M1} { v7_lattices( skol13 ) }.
% 52.29/52.77 (63081) {G0,W2,D2,L1,V0,M1} { v8_lattices( skol13 ) }.
% 52.29/52.77 (63082) {G0,W2,D2,L1,V0,M1} { v9_lattices( skol13 ) }.
% 52.29/52.77 (63083) {G0,W2,D2,L1,V0,M1} { v10_lattices( skol13 ) }.
% 52.29/52.77 (63084) {G0,W2,D2,L1,V0,M1} { v13_lattices( skol13 ) }.
% 52.29/52.77 (63085) {G0,W2,D2,L1,V0,M1} { v14_lattices( skol13 ) }.
% 52.29/52.77 (63086) {G0,W2,D2,L1,V0,M1} { v15_lattices( skol13 ) }.
% 52.29/52.77 (63087) {G0,W2,D2,L1,V0,M1} { v1_relat_1( skol14 ) }.
% 52.29/52.77 (63088) {G0,W2,D2,L1,V0,M1} { v1_funct_1( skol14 ) }.
% 52.29/52.77 (63089) {G0,W9,D3,L4,V2,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! v1_xboole_0( skol15( Y ) ) }.
% 52.29/52.77 (63090) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), m2_lattice4( skol15( X ), X ) }.
% 52.29/52.77 (63091) {G0,W5,D3,L2,V2,M2} { v1_xboole_0( X ), ! v1_xboole_0( skol16( Y )
% 52.29/52.77 ) }.
% 52.29/52.77 (63092) {G0,W7,D3,L2,V1,M2} { v1_xboole_0( X ), m1_subset_1( skol16( X ),
% 52.29/52.77 k1_zfmisc_1( X ) ) }.
% 52.29/52.77 (63093) {G0,W2,D2,L1,V0,M1} { v1_xboole_0( skol17 ) }.
% 52.29/52.77 (63094) {G0,W2,D2,L1,V0,M1} { v1_relat_1( skol18 ) }.
% 52.29/52.77 (63095) {G0,W2,D2,L1,V0,M1} { v1_xboole_0( skol18 ) }.
% 52.29/52.77 (63096) {G0,W2,D2,L1,V0,M1} { v1_funct_1( skol18 ) }.
% 52.29/52.77 (63097) {G0,W3,D3,L1,V1,M1} { v1_xboole_0( skol19( Y ) ) }.
% 52.29/52.77 (63098) {G0,W5,D3,L1,V1,M1} { m1_subset_1( skol19( X ), k1_zfmisc_1( X ) )
% 52.29/52.77 }.
% 52.29/52.77 (63099) {G0,W2,D2,L1,V0,M1} { ! v1_xboole_0( skol20 ) }.
% 52.29/52.77 (63100) {G0,W2,D2,L1,V0,M1} { v1_relat_1( skol21 ) }.
% 52.29/52.77 (63101) {G0,W2,D2,L1,V0,M1} { v1_funct_1( skol21 ) }.
% 52.29/52.77 (63102) {G0,W2,D2,L1,V0,M1} { v2_funct_1( skol21 ) }.
% 52.29/52.77 (63103) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol22 ) }.
% 52.29/52.77 (63104) {G0,W2,D2,L1,V0,M1} { v3_lattices( skol22 ) }.
% 52.29/52.77 (63105) {G0,W2,D2,L1,V0,M1} { l1_struct_0( skol23 ) }.
% 52.29/52.77 (63106) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol23 ) }.
% 52.29/52.77 (63107) {G0,W7,D3,L3,V2,M3} { v3_struct_0( X ), ! l1_struct_0( X ), !
% 52.29/52.77 v1_xboole_0( skol24( Y ) ) }.
% 52.29/52.77 (63108) {G0,W10,D4,L3,V1,M3} { v3_struct_0( X ), ! l1_struct_0( X ),
% 52.29/52.77 m1_subset_1( skol24( X ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 52.29/52.77 (63109) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol25 ) }.
% 52.29/52.77 (63110) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol25 ) }.
% 52.29/52.77 (63111) {G0,W2,D2,L1,V0,M1} { v3_lattices( skol25 ) }.
% 52.29/52.77 (63112) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol26 ) }.
% 52.29/52.77 (63113) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol26 ) }.
% 52.29/52.77 (63114) {G0,W2,D2,L1,V0,M1} { v3_lattices( skol26 ) }.
% 52.29/52.77 (63115) {G0,W2,D2,L1,V0,M1} { v4_lattices( skol26 ) }.
% 52.29/52.77 (63116) {G0,W2,D2,L1,V0,M1} { v5_lattices( skol26 ) }.
% 52.29/52.77 (63117) {G0,W2,D2,L1,V0,M1} { v6_lattices( skol26 ) }.
% 52.29/52.77 (63118) {G0,W2,D2,L1,V0,M1} { v7_lattices( skol26 ) }.
% 52.29/52.77 (63119) {G0,W2,D2,L1,V0,M1} { v8_lattices( skol26 ) }.
% 52.29/52.77 (63120) {G0,W2,D2,L1,V0,M1} { v9_lattices( skol26 ) }.
% 52.29/52.77 (63121) {G0,W2,D2,L1,V0,M1} { v10_lattices( skol26 ) }.
% 52.29/52.77 (63122) {G0,W16,D3,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m2_filter_2( Y, X ), k15_filter_2( X, Y ) =
% 52.29/52.77 k7_filter_2( X, Y ) }.
% 52.29/52.77 (63123) {G0,W12,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_filter_2( Y, X ), m1_filter_0( Y, X ) }.
% 52.29/52.77 (63124) {G0,W12,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_filter_0( Y, X ), m1_filter_2( Y, X ) }.
% 52.29/52.77 (63125) {G0,W8,D2,L2,V3,M2} { ! m2_relset_1( Z, X, Y ), m1_relset_1( Z, X
% 52.29/52.77 , Y ) }.
% 52.29/52.77 (63126) {G0,W8,D2,L2,V3,M2} { ! m1_relset_1( Z, X, Y ), m2_relset_1( Z, X
% 52.29/52.77 , Y ) }.
% 52.29/52.77 (63127) {G0,W3,D2,L1,V1,M1} { r1_tarski( X, X ) }.
% 52.29/52.77 (63128) {G0,W21,D3,L9,V2,M9} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! m1_filter_0( Y, X ), v3_struct_0( X ), ! v10_lattices
% 52.29/52.77 ( X ), ! v14_lattices( X ), ! l3_lattices( X ), r2_hidden( k6_lattices( X
% 52.29/52.77 ), Y ) }.
% 52.29/52.77 (63129) {G0,W6,D2,L2,V2,M2} { ! r2_hidden( X, Y ), m1_subset_1( X, Y ) }.
% 52.29/52.77 (63130) {G0,W8,D2,L3,V2,M3} { ! m1_subset_1( X, Y ), v1_xboole_0( Y ),
% 52.29/52.77 r2_hidden( X, Y ) }.
% 52.29/52.77 (63131) {G0,W7,D3,L2,V2,M2} { ! m1_subset_1( X, k1_zfmisc_1( Y ) ),
% 52.29/52.77 r1_tarski( X, Y ) }.
% 52.29/52.77 (63132) {G0,W7,D3,L2,V2,M2} { ! r1_tarski( X, Y ), m1_subset_1( X,
% 52.29/52.77 k1_zfmisc_1( Y ) ) }.
% 52.29/52.77 (63133) {G0,W10,D3,L3,V3,M3} { ! r2_hidden( X, Z ), ! m1_subset_1( Z,
% 52.29/52.77 k1_zfmisc_1( Y ) ), m1_subset_1( X, Y ) }.
% 52.29/52.77 (63134) {G0,W9,D3,L3,V3,M3} { ! r2_hidden( X, Y ), ! m1_subset_1( Y,
% 52.29/52.77 k1_zfmisc_1( Z ) ), ! v1_xboole_0( Z ) }.
% 52.29/52.77 (63135) {G0,W11,D3,L5,V1,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! v13_lattices( X ), v14_lattices( k1_lattice2( X ) )
% 52.29/52.77 }.
% 52.29/52.77 (63136) {G0,W11,D3,L5,V1,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 l3_lattices( X ), ! v14_lattices( k1_lattice2( X ) ), v13_lattices( X )
% 52.29/52.77 }.
% 52.29/52.77 (63137) {G0,W5,D2,L2,V1,M2} { ! v1_xboole_0( X ), X = k1_xboole_0 }.
% 52.29/52.77 (63138) {G0,W14,D4,L5,V1,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 52.29/52.77 v13_lattices( X ), ! l3_lattices( X ), k5_lattices( X ) = k6_lattices(
% 52.29/52.77 k1_lattice2( X ) ) }.
% 52.29/52.77 (63139) {G0,W5,D2,L2,V2,M2} { ! r2_hidden( X, Y ), ! v1_xboole_0( Y ) }.
% 52.29/52.77 (63140) {G0,W7,D2,L3,V2,M3} { ! v1_xboole_0( X ), X = Y, ! v1_xboole_0( Y
% 52.29/52.77 ) }.
% 52.29/52.77
% 52.29/52.77
% 52.29/52.77 Total Proof:
% 52.29/52.77
% 52.29/52.77 subsumption: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.29/52.77 parent0: (62924) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol1 ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.29/52.77 parent0: (62925) {G0,W2,D2,L1,V0,M1} { v10_lattices( skol1 ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.29/52.77 parent0: (62926) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol1 ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol27, skol1 ) }.
% 52.29/52.77 parent0: (62927) {G0,W3,D2,L1,V0,M1} { m2_filter_2( skol27, skol1 ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (4) {G0,W2,D2,L1,V0,M1} I { v13_lattices( skol1 ) }.
% 52.29/52.77 parent0: (62928) {G0,W2,D2,L1,V0,M1} { v13_lattices( skol1 ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (5) {G0,W4,D3,L1,V0,M1} I { ! r2_hidden( k5_lattices( skol1 )
% 52.29/52.77 , skol27 ) }.
% 52.29/52.77 parent0: (62929) {G0,W4,D3,L1,V0,M1} { ! r2_hidden( k5_lattices( skol1 ),
% 52.29/52.77 skol27 ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (31) {G0,W16,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.29/52.77 ( X ), ! l3_lattices( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X
% 52.29/52.77 ) ) ), k7_filter_2( X, Y ) ==> Y }.
% 52.29/52.77 parent0: (62960) {G0,W16,D4,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices(
% 52.29/52.77 X ), ! l3_lattices( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X )
% 52.29/52.77 ) ), k7_filter_2( X, Y ) = Y }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 Y := Y
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 1 ==> 1
% 52.29/52.77 2 ==> 2
% 52.29/52.77 3 ==> 3
% 52.29/52.77 4 ==> 4
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (34) {G0,W15,D3,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.29/52.77 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m1_filter_2(
% 52.29/52.77 k15_filter_2( X, Y ), k1_lattice2( X ) ) }.
% 52.29/52.77 parent0: (62963) {G0,W15,D3,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices(
% 52.29/52.77 X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m1_filter_2( k15_filter_2
% 52.29/52.77 ( X, Y ), k1_lattice2( X ) ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 Y := Y
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 1 ==> 1
% 52.29/52.77 2 ==> 2
% 52.29/52.77 3 ==> 3
% 52.29/52.77 4 ==> 4
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (36) {G0,W5,D3,L2,V1,M2} I { ! l3_lattices( X ), l3_lattices(
% 52.29/52.77 k1_lattice2( X ) ) }.
% 52.29/52.77 parent0: (62965) {G0,W5,D3,L2,V1,M2} { ! l3_lattices( X ), l3_lattices(
% 52.29/52.77 k1_lattice2( X ) ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 1 ==> 1
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (50) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.29/52.77 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 52.29/52.77 parent0: (62984) {G0,W12,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices(
% 52.29/52.77 X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 Y := Y
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 1 ==> 1
% 52.29/52.77 2 ==> 2
% 52.29/52.77 3 ==> 3
% 52.29/52.77 4 ==> 4
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (51) {G0,W14,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.29/52.77 ( X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y,
% 52.29/52.77 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 52.29/52.77 parent0: (62985) {G0,W14,D4,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices(
% 52.29/52.77 X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y,
% 52.29/52.77 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 Y := Y
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 1 ==> 1
% 52.29/52.77 2 ==> 2
% 52.29/52.77 3 ==> 3
% 52.29/52.77 4 ==> 4
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (70) {G0,W7,D3,L3,V1,M3} I { v3_struct_0( X ), ! l3_lattices(
% 52.29/52.77 X ), ! v3_struct_0( k1_lattice2( X ) ) }.
% 52.29/52.77 parent0: (63006) {G0,W7,D3,L3,V1,M3} { v3_struct_0( X ), ! l3_lattices( X
% 52.29/52.77 ), ! v3_struct_0( k1_lattice2( X ) ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 1 ==> 1
% 52.29/52.77 2 ==> 2
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (113) {G0,W9,D3,L4,V1,M4} I { v3_struct_0( X ), ! v10_lattices
% 52.29/52.77 ( X ), ! l3_lattices( X ), v10_lattices( k1_lattice2( X ) ) }.
% 52.29/52.77 parent0: (63051) {G0,W9,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X
% 52.29/52.77 ), ! l3_lattices( X ), v10_lattices( k1_lattice2( X ) ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 0
% 52.29/52.77 1 ==> 1
% 52.29/52.77 2 ==> 2
% 52.29/52.77 3 ==> 3
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 eqswap: (63334) {G0,W16,D3,L5,V2,M5} { k7_filter_2( X, Y ) = k15_filter_2
% 52.29/52.77 ( X, Y ), v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), !
% 52.29/52.77 m2_filter_2( Y, X ) }.
% 52.29/52.77 parent0[4]: (63122) {G0,W16,D3,L5,V2,M5} { v3_struct_0( X ), !
% 52.29/52.77 v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ),
% 52.29/52.77 k15_filter_2( X, Y ) = k7_filter_2( X, Y ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 Y := Y
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (184) {G0,W16,D3,L5,V2,M5} I { v3_struct_0( X ), !
% 52.29/52.77 v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), k7_filter_2
% 52.29/52.77 ( X, Y ) ==> k15_filter_2( X, Y ) }.
% 52.29/52.77 parent0: (63334) {G0,W16,D3,L5,V2,M5} { k7_filter_2( X, Y ) = k15_filter_2
% 52.29/52.77 ( X, Y ), v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), !
% 52.29/52.77 m2_filter_2( Y, X ) }.
% 52.29/52.77 substitution0:
% 52.29/52.77 X := X
% 52.29/52.77 Y := Y
% 52.29/52.77 end
% 52.29/52.77 permutation0:
% 52.29/52.77 0 ==> 4
% 52.29/52.77 1 ==> 0
% 52.29/52.77 2 ==> 1
% 52.29/52.77 3 ==> 2
% 52.29/52.77 4 ==> 3
% 52.29/52.77 end
% 52.29/52.77
% 52.29/52.77 subsumption: (185) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), !
% 52.29/52.77 v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_2( Y, X ), m1_filter_0
% 52.29/52.77 ( Y, X ) }.
% 52.29/52.77 parent0: (63123) {G0,W12,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices(
% 52.29/52.77 X ), ! l3_lattices( X ), ! m1_filter_2( Y, X ), m1_filter_0( Y, X ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77 permutation0:
% 52.37/52.77 0 ==> 0
% 52.37/52.77 1 ==> 1
% 52.37/52.77 2 ==> 2
% 52.37/52.77 3 ==> 3
% 52.37/52.77 4 ==> 4
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 factor: (63525) {G0,W19,D3,L8,V2,M8} { v3_struct_0( X ), ! v10_lattices( X
% 52.37/52.77 ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), ! v10_lattices( X ), !
% 52.37/52.77 v14_lattices( X ), ! l3_lattices( X ), r2_hidden( k6_lattices( X ), Y )
% 52.37/52.77 }.
% 52.37/52.77 parent0[0, 4]: (63128) {G0,W21,D3,L9,V2,M9} { v3_struct_0( X ), !
% 52.37/52.77 v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), v3_struct_0
% 52.37/52.77 ( X ), ! v10_lattices( X ), ! v14_lattices( X ), ! l3_lattices( X ),
% 52.37/52.77 r2_hidden( k6_lattices( X ), Y ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 factor: (63526) {G0,W17,D3,L7,V2,M7} { v3_struct_0( X ), ! v10_lattices( X
% 52.37/52.77 ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), ! v14_lattices( X ), !
% 52.37/52.77 l3_lattices( X ), r2_hidden( k6_lattices( X ), Y ) }.
% 52.37/52.77 parent0[1, 4]: (63525) {G0,W19,D3,L8,V2,M8} { v3_struct_0( X ), !
% 52.37/52.77 v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), !
% 52.37/52.77 v10_lattices( X ), ! v14_lattices( X ), ! l3_lattices( X ), r2_hidden(
% 52.37/52.77 k6_lattices( X ), Y ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 factor: (63527) {G0,W15,D3,L6,V2,M6} { v3_struct_0( X ), ! v10_lattices( X
% 52.37/52.77 ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), ! v14_lattices( X ),
% 52.37/52.77 r2_hidden( k6_lattices( X ), Y ) }.
% 52.37/52.77 parent0[2, 5]: (63526) {G0,W17,D3,L7,V2,M7} { v3_struct_0( X ), !
% 52.37/52.77 v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), !
% 52.37/52.77 v14_lattices( X ), ! l3_lattices( X ), r2_hidden( k6_lattices( X ), Y )
% 52.37/52.77 }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 subsumption: (190) {G0,W15,D3,L6,V2,M6} I;f;f;f { v3_struct_0( X ), !
% 52.37/52.77 v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), !
% 52.37/52.77 v14_lattices( X ), r2_hidden( k6_lattices( X ), Y ) }.
% 52.37/52.77 parent0: (63527) {G0,W15,D3,L6,V2,M6} { v3_struct_0( X ), ! v10_lattices(
% 52.37/52.77 X ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), ! v14_lattices( X ),
% 52.37/52.77 r2_hidden( k6_lattices( X ), Y ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77 permutation0:
% 52.37/52.77 0 ==> 0
% 52.37/52.77 1 ==> 1
% 52.37/52.77 2 ==> 2
% 52.37/52.77 3 ==> 3
% 52.37/52.77 4 ==> 4
% 52.37/52.77 5 ==> 5
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 subsumption: (197) {G0,W11,D3,L5,V1,M5} I { v3_struct_0( X ), !
% 52.37/52.77 v10_lattices( X ), ! l3_lattices( X ), ! v13_lattices( X ), v14_lattices
% 52.37/52.77 ( k1_lattice2( X ) ) }.
% 52.37/52.77 parent0: (63135) {G0,W11,D3,L5,V1,M5} { v3_struct_0( X ), ! v10_lattices(
% 52.37/52.77 X ), ! l3_lattices( X ), ! v13_lattices( X ), v14_lattices( k1_lattice2(
% 52.37/52.77 X ) ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 end
% 52.37/52.77 permutation0:
% 52.37/52.77 0 ==> 0
% 52.37/52.77 1 ==> 1
% 52.37/52.77 2 ==> 2
% 52.37/52.77 3 ==> 3
% 52.37/52.77 4 ==> 4
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 eqswap: (63725) {G0,W14,D4,L5,V1,M5} { k6_lattices( k1_lattice2( X ) ) =
% 52.37/52.77 k5_lattices( X ), v3_struct_0( X ), ! v10_lattices( X ), ! v13_lattices(
% 52.37/52.77 X ), ! l3_lattices( X ) }.
% 52.37/52.77 parent0[4]: (63138) {G0,W14,D4,L5,V1,M5} { v3_struct_0( X ), !
% 52.37/52.77 v10_lattices( X ), ! v13_lattices( X ), ! l3_lattices( X ), k5_lattices(
% 52.37/52.77 X ) = k6_lattices( k1_lattice2( X ) ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 subsumption: (200) {G0,W14,D4,L5,V1,M5} I { v3_struct_0( X ), !
% 52.37/52.77 v10_lattices( X ), ! v13_lattices( X ), ! l3_lattices( X ), k6_lattices(
% 52.37/52.77 k1_lattice2( X ) ) ==> k5_lattices( X ) }.
% 52.37/52.77 parent0: (63725) {G0,W14,D4,L5,V1,M5} { k6_lattices( k1_lattice2( X ) ) =
% 52.37/52.77 k5_lattices( X ), v3_struct_0( X ), ! v10_lattices( X ), ! v13_lattices(
% 52.37/52.77 X ), ! l3_lattices( X ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 end
% 52.37/52.77 permutation0:
% 52.37/52.77 0 ==> 4
% 52.37/52.77 1 ==> 0
% 52.37/52.77 2 ==> 1
% 52.37/52.77 3 ==> 2
% 52.37/52.77 4 ==> 3
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 resolution: (63726) {G1,W12,D3,L4,V0,M4} { v3_struct_0( skol1 ), !
% 52.37/52.77 v10_lattices( skol1 ), ! l3_lattices( skol1 ), m1_filter_2( k15_filter_2
% 52.37/52.77 ( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.77 parent0[3]: (34) {G0,W15,D3,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.77 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m1_filter_2(
% 52.37/52.77 k15_filter_2( X, Y ), k1_lattice2( X ) ) }.
% 52.37/52.77 parent1[0]: (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol27, skol1 ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := skol1
% 52.37/52.77 Y := skol27
% 52.37/52.77 end
% 52.37/52.77 substitution1:
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 resolution: (63727) {G1,W10,D3,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 52.37/52.77 l3_lattices( skol1 ), m1_filter_2( k15_filter_2( skol1, skol27 ),
% 52.37/52.77 k1_lattice2( skol1 ) ) }.
% 52.37/52.77 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.37/52.77 parent1[0]: (63726) {G1,W12,D3,L4,V0,M4} { v3_struct_0( skol1 ), !
% 52.37/52.77 v10_lattices( skol1 ), ! l3_lattices( skol1 ), m1_filter_2( k15_filter_2
% 52.37/52.77 ( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 end
% 52.37/52.77 substitution1:
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 subsumption: (423) {G1,W10,D3,L3,V0,M3} R(34,3);r(0) { ! v10_lattices(
% 52.37/52.77 skol1 ), ! l3_lattices( skol1 ), m1_filter_2( k15_filter_2( skol1, skol27
% 52.37/52.77 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.77 parent0: (63727) {G1,W10,D3,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 52.37/52.77 l3_lattices( skol1 ), m1_filter_2( k15_filter_2( skol1, skol27 ),
% 52.37/52.77 k1_lattice2( skol1 ) ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 end
% 52.37/52.77 permutation0:
% 52.37/52.77 0 ==> 0
% 52.37/52.77 1 ==> 1
% 52.37/52.77 2 ==> 2
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 resolution: (63728) {G1,W3,D3,L1,V0,M1} { l3_lattices( k1_lattice2( skol1
% 52.37/52.77 ) ) }.
% 52.37/52.77 parent0[0]: (36) {G0,W5,D3,L2,V1,M2} I { ! l3_lattices( X ), l3_lattices(
% 52.37/52.77 k1_lattice2( X ) ) }.
% 52.37/52.77 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := skol1
% 52.37/52.77 end
% 52.37/52.77 substitution1:
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 subsumption: (457) {G1,W3,D3,L1,V0,M1} R(36,2) { l3_lattices( k1_lattice2(
% 52.37/52.77 skol1 ) ) }.
% 52.37/52.77 parent0: (63728) {G1,W3,D3,L1,V0,M1} { l3_lattices( k1_lattice2( skol1 ) )
% 52.37/52.77 }.
% 52.37/52.77 substitution0:
% 52.37/52.77 end
% 52.37/52.77 permutation0:
% 52.37/52.77 0 ==> 0
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 resolution: (63729) {G1,W9,D2,L4,V0,M4} { v3_struct_0( skol1 ), !
% 52.37/52.77 v10_lattices( skol1 ), ! l3_lattices( skol1 ), m2_lattice4( skol27, skol1
% 52.37/52.77 ) }.
% 52.37/52.77 parent0[3]: (50) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.77 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 52.37/52.77 parent1[0]: (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol27, skol1 ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := skol1
% 52.37/52.77 Y := skol27
% 52.37/52.77 end
% 52.37/52.77 substitution1:
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 resolution: (63730) {G1,W7,D2,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 52.37/52.77 l3_lattices( skol1 ), m2_lattice4( skol27, skol1 ) }.
% 52.37/52.77 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.37/52.77 parent1[0]: (63729) {G1,W9,D2,L4,V0,M4} { v3_struct_0( skol1 ), !
% 52.37/52.77 v10_lattices( skol1 ), ! l3_lattices( skol1 ), m2_lattice4( skol27, skol1
% 52.37/52.77 ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 end
% 52.37/52.77 substitution1:
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 subsumption: (731) {G1,W7,D2,L3,V0,M3} R(50,3);r(0) { ! v10_lattices( skol1
% 52.37/52.77 ), ! l3_lattices( skol1 ), m2_lattice4( skol27, skol1 ) }.
% 52.37/52.77 parent0: (63730) {G1,W7,D2,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 52.37/52.77 l3_lattices( skol1 ), m2_lattice4( skol27, skol1 ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 end
% 52.37/52.77 permutation0:
% 52.37/52.77 0 ==> 0
% 52.37/52.77 1 ==> 1
% 52.37/52.77 2 ==> 2
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 eqswap: (63731) {G0,W16,D4,L5,V2,M5} { Y ==> k7_filter_2( X, Y ),
% 52.37/52.77 v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_subset_1
% 52.37/52.77 ( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 52.37/52.77 parent0[4]: (31) {G0,W16,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.77 ( X ), ! l3_lattices( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X
% 52.37/52.77 ) ) ), k7_filter_2( X, Y ) ==> Y }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 resolution: (63732) {G1,W20,D3,L8,V2,M8} { X ==> k7_filter_2( Y, X ),
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), v3_struct_0( Y
% 52.37/52.77 ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! m2_lattice4( X, Y ) }.
% 52.37/52.77 parent0[4]: (63731) {G0,W16,D4,L5,V2,M5} { Y ==> k7_filter_2( X, Y ),
% 52.37/52.77 v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m1_subset_1
% 52.37/52.77 ( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 52.37/52.77 parent1[4]: (51) {G0,W14,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.77 ( X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y,
% 52.37/52.77 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := Y
% 52.37/52.77 Y := X
% 52.37/52.77 end
% 52.37/52.77 substitution1:
% 52.37/52.77 X := Y
% 52.37/52.77 Y := X
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 factor: (63733) {G1,W18,D3,L7,V2,M7} { X ==> k7_filter_2( Y, X ),
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! v10_lattices
% 52.37/52.77 ( Y ), ! l3_lattices( Y ), ! m2_lattice4( X, Y ) }.
% 52.37/52.77 parent0[1, 4]: (63732) {G1,W20,D3,L8,V2,M8} { X ==> k7_filter_2( Y, X ),
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), v3_struct_0( Y
% 52.37/52.77 ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! m2_lattice4( X, Y ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 factor: (63734) {G1,W16,D3,L6,V2,M6} { X ==> k7_filter_2( Y, X ),
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! l3_lattices
% 52.37/52.77 ( Y ), ! m2_lattice4( X, Y ) }.
% 52.37/52.77 parent0[2, 4]: (63733) {G1,W18,D3,L7,V2,M7} { X ==> k7_filter_2( Y, X ),
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! v10_lattices
% 52.37/52.77 ( Y ), ! l3_lattices( Y ), ! m2_lattice4( X, Y ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 factor: (63735) {G1,W14,D3,L5,V2,M5} { X ==> k7_filter_2( Y, X ),
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! m2_lattice4
% 52.37/52.77 ( X, Y ) }.
% 52.37/52.77 parent0[3, 4]: (63734) {G1,W16,D3,L6,V2,M6} { X ==> k7_filter_2( Y, X ),
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! l3_lattices
% 52.37/52.77 ( Y ), ! m2_lattice4( X, Y ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 eqswap: (63736) {G1,W14,D3,L5,V2,M5} { k7_filter_2( Y, X ) ==> X,
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! m2_lattice4
% 52.37/52.77 ( X, Y ) }.
% 52.37/52.77 parent0[0]: (63735) {G1,W14,D3,L5,V2,M5} { X ==> k7_filter_2( Y, X ),
% 52.37/52.77 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! m2_lattice4
% 52.37/52.77 ( X, Y ) }.
% 52.37/52.77 substitution0:
% 52.37/52.77 X := X
% 52.37/52.77 Y := Y
% 52.37/52.77 end
% 52.37/52.77
% 52.37/52.77 subsumption: (751) {G1,W14,D3,L5,V2,M5} R(51,31);f;f;f { v3_struct_0( X ),
% 52.37/52.78 ! v10_lattices( X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ),
% 52.37/52.78 k7_filter_2( X, Y ) ==> Y }.
% 52.37/52.78 parent0: (63736) {G1,W14,D3,L5,V2,M5} { k7_filter_2( Y, X ) ==> X,
% 52.37/52.78 v3_struct_0( Y ), ! v10_lattices( Y ), ! l3_lattices( Y ), ! m2_lattice4
% 52.37/52.78 ( X, Y ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := Y
% 52.37/52.78 Y := X
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 4
% 52.37/52.78 1 ==> 0
% 52.37/52.78 2 ==> 1
% 52.37/52.78 3 ==> 2
% 52.37/52.78 4 ==> 3
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63740) {G1,W5,D3,L2,V0,M2} { v3_struct_0( skol1 ), !
% 52.37/52.78 v3_struct_0( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[1]: (70) {G0,W7,D3,L3,V1,M3} I { v3_struct_0( X ), ! l3_lattices( X
% 52.37/52.78 ), ! v3_struct_0( k1_lattice2( X ) ) }.
% 52.37/52.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := skol1
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63741) {G1,W3,D3,L1,V0,M1} { ! v3_struct_0( k1_lattice2(
% 52.37/52.78 skol1 ) ) }.
% 52.37/52.78 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.37/52.78 parent1[0]: (63740) {G1,W5,D3,L2,V0,M2} { v3_struct_0( skol1 ), !
% 52.37/52.78 v3_struct_0( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (1099) {G1,W3,D3,L1,V0,M1} R(70,2);r(0) { ! v3_struct_0(
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0: (63741) {G1,W3,D3,L1,V0,M1} { ! v3_struct_0( k1_lattice2( skol1 )
% 52.37/52.78 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63742) {G1,W7,D3,L3,V0,M3} { v3_struct_0( skol1 ), !
% 52.37/52.78 v10_lattices( skol1 ), v10_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[2]: (113) {G0,W9,D3,L4,V1,M4} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.78 ( X ), ! l3_lattices( X ), v10_lattices( k1_lattice2( X ) ) }.
% 52.37/52.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := skol1
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63743) {G1,W5,D3,L2,V0,M2} { ! v10_lattices( skol1 ),
% 52.37/52.78 v10_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.37/52.78 parent1[0]: (63742) {G1,W7,D3,L3,V0,M3} { v3_struct_0( skol1 ), !
% 52.37/52.78 v10_lattices( skol1 ), v10_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (2413) {G1,W5,D3,L2,V0,M2} R(113,2);r(0) { ! v10_lattices(
% 52.37/52.78 skol1 ), v10_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0: (63743) {G1,W5,D3,L2,V0,M2} { ! v10_lattices( skol1 ),
% 52.37/52.78 v10_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 1 ==> 1
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 eqswap: (63744) {G0,W16,D3,L5,V2,M5} { k15_filter_2( X, Y ) ==>
% 52.37/52.78 k7_filter_2( X, Y ), v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices
% 52.37/52.78 ( X ), ! m2_filter_2( Y, X ) }.
% 52.37/52.78 parent0[4]: (184) {G0,W16,D3,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.78 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), k7_filter_2( X, Y ) ==>
% 52.37/52.78 k15_filter_2( X, Y ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := X
% 52.37/52.78 Y := Y
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63745) {G1,W13,D3,L4,V0,M4} { k15_filter_2( skol1, skol27 )
% 52.37/52.78 ==> k7_filter_2( skol1, skol27 ), v3_struct_0( skol1 ), ! v10_lattices(
% 52.37/52.78 skol1 ), ! l3_lattices( skol1 ) }.
% 52.37/52.78 parent0[4]: (63744) {G0,W16,D3,L5,V2,M5} { k15_filter_2( X, Y ) ==>
% 52.37/52.78 k7_filter_2( X, Y ), v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices
% 52.37/52.78 ( X ), ! m2_filter_2( Y, X ) }.
% 52.37/52.78 parent1[0]: (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol27, skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := skol1
% 52.37/52.78 Y := skol27
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63746) {G1,W11,D3,L3,V0,M3} { k15_filter_2( skol1, skol27 )
% 52.37/52.78 ==> k7_filter_2( skol1, skol27 ), ! v10_lattices( skol1 ), ! l3_lattices
% 52.37/52.78 ( skol1 ) }.
% 52.37/52.78 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.37/52.78 parent1[1]: (63745) {G1,W13,D3,L4,V0,M4} { k15_filter_2( skol1, skol27 )
% 52.37/52.78 ==> k7_filter_2( skol1, skol27 ), v3_struct_0( skol1 ), ! v10_lattices(
% 52.37/52.78 skol1 ), ! l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 eqswap: (63747) {G1,W11,D3,L3,V0,M3} { k7_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 k15_filter_2( skol1, skol27 ), ! v10_lattices( skol1 ), ! l3_lattices(
% 52.37/52.78 skol1 ) }.
% 52.37/52.78 parent0[0]: (63746) {G1,W11,D3,L3,V0,M3} { k15_filter_2( skol1, skol27 )
% 52.37/52.78 ==> k7_filter_2( skol1, skol27 ), ! v10_lattices( skol1 ), ! l3_lattices
% 52.37/52.78 ( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (4701) {G1,W11,D3,L3,V0,M3} R(184,3);r(0) { ! v10_lattices(
% 52.37/52.78 skol1 ), ! l3_lattices( skol1 ), k7_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 k15_filter_2( skol1, skol27 ) }.
% 52.37/52.78 parent0: (63747) {G1,W11,D3,L3,V0,M3} { k7_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 k15_filter_2( skol1, skol27 ), ! v10_lattices( skol1 ), ! l3_lattices(
% 52.37/52.78 skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 2
% 52.37/52.78 1 ==> 0
% 52.37/52.78 2 ==> 1
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63748) {G1,W9,D3,L4,V0,M4} { v3_struct_0( skol1 ), !
% 52.37/52.78 v10_lattices( skol1 ), ! l3_lattices( skol1 ), v14_lattices( k1_lattice2
% 52.37/52.78 ( skol1 ) ) }.
% 52.37/52.78 parent0[3]: (197) {G0,W11,D3,L5,V1,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.78 ( X ), ! l3_lattices( X ), ! v13_lattices( X ), v14_lattices( k1_lattice2
% 52.37/52.78 ( X ) ) }.
% 52.37/52.78 parent1[0]: (4) {G0,W2,D2,L1,V0,M1} I { v13_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := skol1
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63749) {G1,W7,D3,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 52.37/52.78 l3_lattices( skol1 ), v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.37/52.78 parent1[0]: (63748) {G1,W9,D3,L4,V0,M4} { v3_struct_0( skol1 ), !
% 52.37/52.78 v10_lattices( skol1 ), ! l3_lattices( skol1 ), v14_lattices( k1_lattice2
% 52.37/52.78 ( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (5443) {G1,W7,D3,L3,V0,M3} R(197,4);r(0) { ! v10_lattices(
% 52.37/52.78 skol1 ), ! l3_lattices( skol1 ), v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0: (63749) {G1,W7,D3,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 52.37/52.78 l3_lattices( skol1 ), v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 1 ==> 1
% 52.37/52.78 2 ==> 2
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 eqswap: (63750) {G0,W14,D4,L5,V1,M5} { k5_lattices( X ) ==> k6_lattices(
% 52.37/52.78 k1_lattice2( X ) ), v3_struct_0( X ), ! v10_lattices( X ), ! v13_lattices
% 52.37/52.78 ( X ), ! l3_lattices( X ) }.
% 52.37/52.78 parent0[4]: (200) {G0,W14,D4,L5,V1,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.78 ( X ), ! v13_lattices( X ), ! l3_lattices( X ), k6_lattices( k1_lattice2
% 52.37/52.78 ( X ) ) ==> k5_lattices( X ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := X
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63751) {G1,W12,D4,L4,V0,M4} { k5_lattices( skol1 ) ==>
% 52.37/52.78 k6_lattices( k1_lattice2( skol1 ) ), v3_struct_0( skol1 ), ! v10_lattices
% 52.37/52.78 ( skol1 ), ! l3_lattices( skol1 ) }.
% 52.37/52.78 parent0[3]: (63750) {G0,W14,D4,L5,V1,M5} { k5_lattices( X ) ==>
% 52.37/52.78 k6_lattices( k1_lattice2( X ) ), v3_struct_0( X ), ! v10_lattices( X ), !
% 52.37/52.78 v13_lattices( X ), ! l3_lattices( X ) }.
% 52.37/52.78 parent1[0]: (4) {G0,W2,D2,L1,V0,M1} I { v13_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := skol1
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63752) {G1,W10,D4,L3,V0,M3} { k5_lattices( skol1 ) ==>
% 52.37/52.78 k6_lattices( k1_lattice2( skol1 ) ), ! v10_lattices( skol1 ), !
% 52.37/52.78 l3_lattices( skol1 ) }.
% 52.37/52.78 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.37/52.78 parent1[1]: (63751) {G1,W12,D4,L4,V0,M4} { k5_lattices( skol1 ) ==>
% 52.37/52.78 k6_lattices( k1_lattice2( skol1 ) ), v3_struct_0( skol1 ), ! v10_lattices
% 52.37/52.78 ( skol1 ), ! l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 eqswap: (63753) {G1,W10,D4,L3,V0,M3} { k6_lattices( k1_lattice2( skol1 ) )
% 52.37/52.78 ==> k5_lattices( skol1 ), ! v10_lattices( skol1 ), ! l3_lattices( skol1
% 52.37/52.78 ) }.
% 52.37/52.78 parent0[0]: (63752) {G1,W10,D4,L3,V0,M3} { k5_lattices( skol1 ) ==>
% 52.37/52.78 k6_lattices( k1_lattice2( skol1 ) ), ! v10_lattices( skol1 ), !
% 52.37/52.78 l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (5665) {G1,W10,D4,L3,V0,M3} R(200,4);r(0) { ! v10_lattices(
% 52.37/52.78 skol1 ), ! l3_lattices( skol1 ), k6_lattices( k1_lattice2( skol1 ) ) ==>
% 52.37/52.78 k5_lattices( skol1 ) }.
% 52.37/52.78 parent0: (63753) {G1,W10,D4,L3,V0,M3} { k6_lattices( k1_lattice2( skol1 )
% 52.37/52.78 ) ==> k5_lattices( skol1 ), ! v10_lattices( skol1 ), ! l3_lattices(
% 52.37/52.78 skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 2
% 52.37/52.78 1 ==> 0
% 52.37/52.78 2 ==> 1
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63754) {G1,W3,D3,L1,V0,M1} { v10_lattices( k1_lattice2( skol1
% 52.37/52.78 ) ) }.
% 52.37/52.78 parent0[0]: (2413) {G1,W5,D3,L2,V0,M2} R(113,2);r(0) { ! v10_lattices(
% 52.37/52.78 skol1 ), v10_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (8252) {G2,W3,D3,L1,V0,M1} S(2413);r(1) { v10_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0: (63754) {G1,W3,D3,L1,V0,M1} { v10_lattices( k1_lattice2( skol1 )
% 52.37/52.78 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63755) {G1,W8,D3,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 m1_filter_2( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (423) {G1,W10,D3,L3,V0,M3} R(34,3);r(0) { ! v10_lattices( skol1
% 52.37/52.78 ), ! l3_lattices( skol1 ), m1_filter_2( k15_filter_2( skol1, skol27 ),
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63756) {G1,W6,D3,L1,V0,M1} { m1_filter_2( k15_filter_2( skol1
% 52.37/52.78 , skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (63755) {G1,W8,D3,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 m1_filter_2( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (11705) {G2,W6,D3,L1,V0,M1} S(423);r(1);r(2) { m1_filter_2(
% 52.37/52.78 k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0: (63756) {G1,W6,D3,L1,V0,M1} { m1_filter_2( k15_filter_2( skol1,
% 52.37/52.78 skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63758) {G1,W8,D4,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 k6_lattices( k1_lattice2( skol1 ) ) ==> k5_lattices( skol1 ) }.
% 52.37/52.78 parent0[0]: (5665) {G1,W10,D4,L3,V0,M3} R(200,4);r(0) { ! v10_lattices(
% 52.37/52.78 skol1 ), ! l3_lattices( skol1 ), k6_lattices( k1_lattice2( skol1 ) ) ==>
% 52.37/52.78 k5_lattices( skol1 ) }.
% 52.37/52.78 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63759) {G1,W6,D4,L1,V0,M1} { k6_lattices( k1_lattice2( skol1
% 52.37/52.78 ) ) ==> k5_lattices( skol1 ) }.
% 52.37/52.78 parent0[0]: (63758) {G1,W8,D4,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 k6_lattices( k1_lattice2( skol1 ) ) ==> k5_lattices( skol1 ) }.
% 52.37/52.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (20666) {G2,W6,D4,L1,V0,M1} S(5665);r(1);r(2) { k6_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ) ==> k5_lattices( skol1 ) }.
% 52.37/52.78 parent0: (63759) {G1,W6,D4,L1,V0,M1} { k6_lattices( k1_lattice2( skol1 ) )
% 52.37/52.78 ==> k5_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63761) {G1,W5,D3,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (5443) {G1,W7,D3,L3,V0,M3} R(197,4);r(0) { ! v10_lattices(
% 52.37/52.78 skol1 ), ! l3_lattices( skol1 ), v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63762) {G1,W3,D3,L1,V0,M1} { v14_lattices( k1_lattice2( skol1
% 52.37/52.78 ) ) }.
% 52.37/52.78 parent0[0]: (63761) {G1,W5,D3,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (20723) {G2,W3,D3,L1,V0,M1} S(5443);r(1);r(2) { v14_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0: (63762) {G1,W3,D3,L1,V0,M1} { v14_lattices( k1_lattice2( skol1 )
% 52.37/52.78 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63764) {G1,W9,D3,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 k7_filter_2( skol1, skol27 ) ==> k15_filter_2( skol1, skol27 ) }.
% 52.37/52.78 parent0[0]: (4701) {G1,W11,D3,L3,V0,M3} R(184,3);r(0) { ! v10_lattices(
% 52.37/52.78 skol1 ), ! l3_lattices( skol1 ), k7_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 k15_filter_2( skol1, skol27 ) }.
% 52.37/52.78 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63765) {G1,W7,D3,L1,V0,M1} { k7_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 k15_filter_2( skol1, skol27 ) }.
% 52.37/52.78 parent0[0]: (63764) {G1,W9,D3,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 k7_filter_2( skol1, skol27 ) ==> k15_filter_2( skol1, skol27 ) }.
% 52.37/52.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (20759) {G2,W7,D3,L1,V0,M1} S(4701);r(1);r(2) { k7_filter_2(
% 52.37/52.78 skol1, skol27 ) ==> k15_filter_2( skol1, skol27 ) }.
% 52.37/52.78 parent0: (63765) {G1,W7,D3,L1,V0,M1} { k7_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 k15_filter_2( skol1, skol27 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63767) {G1,W5,D2,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 m2_lattice4( skol27, skol1 ) }.
% 52.37/52.78 parent0[0]: (731) {G1,W7,D2,L3,V0,M3} R(50,3);r(0) { ! v10_lattices( skol1
% 52.37/52.78 ), ! l3_lattices( skol1 ), m2_lattice4( skol27, skol1 ) }.
% 52.37/52.78 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63768) {G1,W3,D2,L1,V0,M1} { m2_lattice4( skol27, skol1 ) }.
% 52.37/52.78 parent0[0]: (63767) {G1,W5,D2,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 m2_lattice4( skol27, skol1 ) }.
% 52.37/52.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (20948) {G2,W3,D2,L1,V0,M1} S(731);r(1);r(2) { m2_lattice4(
% 52.37/52.78 skol27, skol1 ) }.
% 52.37/52.78 parent0: (63768) {G1,W3,D2,L1,V0,M1} { m2_lattice4( skol27, skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 eqswap: (63769) {G1,W14,D3,L5,V2,M5} { Y ==> k7_filter_2( X, Y ),
% 52.37/52.78 v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_lattice4
% 52.37/52.78 ( Y, X ) }.
% 52.37/52.78 parent0[4]: (751) {G1,W14,D3,L5,V2,M5} R(51,31);f;f;f { v3_struct_0( X ), !
% 52.37/52.78 v10_lattices( X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ),
% 52.37/52.78 k7_filter_2( X, Y ) ==> Y }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := X
% 52.37/52.78 Y := Y
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63771) {G2,W11,D3,L4,V0,M4} { skol27 ==> k7_filter_2( skol1,
% 52.37/52.78 skol27 ), v3_struct_0( skol1 ), ! v10_lattices( skol1 ), ! l3_lattices(
% 52.37/52.78 skol1 ) }.
% 52.37/52.78 parent0[4]: (63769) {G1,W14,D3,L5,V2,M5} { Y ==> k7_filter_2( X, Y ),
% 52.37/52.78 v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_lattice4
% 52.37/52.78 ( Y, X ) }.
% 52.37/52.78 parent1[0]: (20948) {G2,W3,D2,L1,V0,M1} S(731);r(1);r(2) { m2_lattice4(
% 52.37/52.78 skol27, skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := skol1
% 52.37/52.78 Y := skol27
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 paramod: (63772) {G3,W11,D3,L4,V0,M4} { skol27 ==> k15_filter_2( skol1,
% 52.37/52.78 skol27 ), v3_struct_0( skol1 ), ! v10_lattices( skol1 ), ! l3_lattices(
% 52.37/52.78 skol1 ) }.
% 52.37/52.78 parent0[0]: (20759) {G2,W7,D3,L1,V0,M1} S(4701);r(1);r(2) { k7_filter_2(
% 52.37/52.78 skol1, skol27 ) ==> k15_filter_2( skol1, skol27 ) }.
% 52.37/52.78 parent1[0; 2]: (63771) {G2,W11,D3,L4,V0,M4} { skol27 ==> k7_filter_2(
% 52.37/52.78 skol1, skol27 ), v3_struct_0( skol1 ), ! v10_lattices( skol1 ), !
% 52.37/52.78 l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63773) {G1,W9,D3,L3,V0,M3} { skol27 ==> k15_filter_2( skol1,
% 52.37/52.78 skol27 ), ! v10_lattices( skol1 ), ! l3_lattices( skol1 ) }.
% 52.37/52.78 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 52.37/52.78 parent1[1]: (63772) {G3,W11,D3,L4,V0,M4} { skol27 ==> k15_filter_2( skol1
% 52.37/52.78 , skol27 ), v3_struct_0( skol1 ), ! v10_lattices( skol1 ), ! l3_lattices
% 52.37/52.78 ( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 eqswap: (63774) {G1,W9,D3,L3,V0,M3} { k15_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 skol27, ! v10_lattices( skol1 ), ! l3_lattices( skol1 ) }.
% 52.37/52.78 parent0[0]: (63773) {G1,W9,D3,L3,V0,M3} { skol27 ==> k15_filter_2( skol1,
% 52.37/52.78 skol27 ), ! v10_lattices( skol1 ), ! l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (23131) {G3,W9,D3,L3,V0,M3} R(751,20948);d(20759);r(0) { !
% 52.37/52.78 v10_lattices( skol1 ), ! l3_lattices( skol1 ), k15_filter_2( skol1,
% 52.37/52.78 skol27 ) ==> skol27 }.
% 52.37/52.78 parent0: (63774) {G1,W9,D3,L3,V0,M3} { k15_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 skol27, ! v10_lattices( skol1 ), ! l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 2
% 52.37/52.78 1 ==> 0
% 52.37/52.78 2 ==> 1
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63775) {G1,W15,D3,L4,V0,M4} { v3_struct_0( k1_lattice2( skol1
% 52.37/52.78 ) ), ! v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2
% 52.37/52.78 ( skol1 ) ), m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2(
% 52.37/52.78 skol1 ) ) }.
% 52.37/52.78 parent0[3]: (185) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 52.37/52.78 ( X ), ! l3_lattices( X ), ! m1_filter_2( Y, X ), m1_filter_0( Y, X ) }.
% 52.37/52.78 parent1[0]: (11705) {G2,W6,D3,L1,V0,M1} S(423);r(1);r(2) { m1_filter_2(
% 52.37/52.78 k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := k1_lattice2( skol1 )
% 52.37/52.78 Y := k15_filter_2( skol1, skol27 )
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63776) {G2,W12,D3,L3,V0,M3} { ! v10_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ), ! l3_lattices( k1_lattice2( skol1 ) ), m1_filter_0(
% 52.37/52.78 k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (1099) {G1,W3,D3,L1,V0,M1} R(70,2);r(0) { ! v3_struct_0(
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent1[0]: (63775) {G1,W15,D3,L4,V0,M4} { v3_struct_0( k1_lattice2( skol1
% 52.37/52.78 ) ), ! v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2
% 52.37/52.78 ( skol1 ) ), m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2(
% 52.37/52.78 skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (30255) {G3,W12,D3,L3,V0,M3} R(11705,185);r(1099) { !
% 52.37/52.78 v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2( skol1 )
% 52.37/52.78 ), m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) )
% 52.37/52.78 }.
% 52.37/52.78 parent0: (63776) {G2,W12,D3,L3,V0,M3} { ! v10_lattices( k1_lattice2( skol1
% 52.37/52.78 ) ), ! l3_lattices( k1_lattice2( skol1 ) ), m1_filter_0( k15_filter_2(
% 52.37/52.78 skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 1 ==> 1
% 52.37/52.78 2 ==> 2
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63777) {G3,W9,D3,L2,V0,M2} { ! l3_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ), m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1
% 52.37/52.78 ) ) }.
% 52.37/52.78 parent0[0]: (30255) {G3,W12,D3,L3,V0,M3} R(11705,185);r(1099) { !
% 52.37/52.78 v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2( skol1 )
% 52.37/52.78 ), m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) )
% 52.37/52.78 }.
% 52.37/52.78 parent1[0]: (8252) {G2,W3,D3,L1,V0,M1} S(2413);r(1) { v10_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63778) {G2,W6,D3,L1,V0,M1} { m1_filter_0( k15_filter_2( skol1
% 52.37/52.78 , skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (63777) {G3,W9,D3,L2,V0,M2} { ! l3_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ), m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1
% 52.37/52.78 ) ) }.
% 52.37/52.78 parent1[0]: (457) {G1,W3,D3,L1,V0,M1} R(36,2) { l3_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (41036) {G4,W6,D3,L1,V0,M1} S(30255);r(8252);r(457) {
% 52.37/52.78 m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0: (63778) {G2,W6,D3,L1,V0,M1} { m1_filter_0( k15_filter_2( skol1,
% 52.37/52.78 skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63780) {G1,W7,D3,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 k15_filter_2( skol1, skol27 ) ==> skol27 }.
% 52.37/52.78 parent0[0]: (23131) {G3,W9,D3,L3,V0,M3} R(751,20948);d(20759);r(0) { !
% 52.37/52.78 v10_lattices( skol1 ), ! l3_lattices( skol1 ), k15_filter_2( skol1,
% 52.37/52.78 skol27 ) ==> skol27 }.
% 52.37/52.78 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63781) {G1,W5,D3,L1,V0,M1} { k15_filter_2( skol1, skol27 )
% 52.37/52.78 ==> skol27 }.
% 52.37/52.78 parent0[0]: (63780) {G1,W7,D3,L2,V0,M2} { ! l3_lattices( skol1 ),
% 52.37/52.78 k15_filter_2( skol1, skol27 ) ==> skol27 }.
% 52.37/52.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (41447) {G4,W5,D3,L1,V0,M1} S(23131);r(1);r(2) { k15_filter_2
% 52.37/52.78 ( skol1, skol27 ) ==> skol27 }.
% 52.37/52.78 parent0: (63781) {G1,W5,D3,L1,V0,M1} { k15_filter_2( skol1, skol27 ) ==>
% 52.37/52.78 skol27 }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 paramod: (63784) {G5,W4,D3,L1,V0,M1} { m1_filter_0( skol27, k1_lattice2(
% 52.37/52.78 skol1 ) ) }.
% 52.37/52.78 parent0[0]: (41447) {G4,W5,D3,L1,V0,M1} S(23131);r(1);r(2) { k15_filter_2(
% 52.37/52.78 skol1, skol27 ) ==> skol27 }.
% 52.37/52.78 parent1[0; 1]: (41036) {G4,W6,D3,L1,V0,M1} S(30255);r(8252);r(457) {
% 52.37/52.78 m1_filter_0( k15_filter_2( skol1, skol27 ), k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (42523) {G5,W4,D3,L1,V0,M1} S(41036);d(41447) { m1_filter_0(
% 52.37/52.78 skol27, k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0: (63784) {G5,W4,D3,L1,V0,M1} { m1_filter_0( skol27, k1_lattice2(
% 52.37/52.78 skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 0
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63786) {G1,W17,D4,L5,V0,M5} { v3_struct_0( k1_lattice2( skol1
% 52.37/52.78 ) ), ! v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2
% 52.37/52.78 ( skol1 ) ), ! v14_lattices( k1_lattice2( skol1 ) ), r2_hidden(
% 52.37/52.78 k6_lattices( k1_lattice2( skol1 ) ), skol27 ) }.
% 52.37/52.78 parent0[3]: (190) {G0,W15,D3,L6,V2,M6} I;f;f;f { v3_struct_0( X ), !
% 52.37/52.78 v10_lattices( X ), ! l3_lattices( X ), ! m1_filter_0( Y, X ), !
% 52.37/52.78 v14_lattices( X ), r2_hidden( k6_lattices( X ), Y ) }.
% 52.37/52.78 parent1[0]: (42523) {G5,W4,D3,L1,V0,M1} S(41036);d(41447) { m1_filter_0(
% 52.37/52.78 skol27, k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 X := k1_lattice2( skol1 )
% 52.37/52.78 Y := skol27
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 paramod: (63787) {G2,W16,D3,L5,V0,M5} { r2_hidden( k5_lattices( skol1 ),
% 52.37/52.78 skol27 ), v3_struct_0( k1_lattice2( skol1 ) ), ! v10_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2( skol1 ) ), !
% 52.37/52.78 v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (20666) {G2,W6,D4,L1,V0,M1} S(5665);r(1);r(2) { k6_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ) ==> k5_lattices( skol1 ) }.
% 52.37/52.78 parent1[4; 1]: (63786) {G1,W17,D4,L5,V0,M5} { v3_struct_0( k1_lattice2(
% 52.37/52.78 skol1 ) ), ! v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ), ! v14_lattices( k1_lattice2( skol1 ) ), r2_hidden
% 52.37/52.78 ( k6_lattices( k1_lattice2( skol1 ) ), skol27 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63788) {G2,W13,D3,L4,V0,M4} { r2_hidden( k5_lattices( skol1 )
% 52.37/52.78 , skol27 ), ! v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ), ! v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent0[0]: (1099) {G1,W3,D3,L1,V0,M1} R(70,2);r(0) { ! v3_struct_0(
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 parent1[1]: (63787) {G2,W16,D3,L5,V0,M5} { r2_hidden( k5_lattices( skol1 )
% 52.37/52.78 , skol27 ), v3_struct_0( k1_lattice2( skol1 ) ), ! v10_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2( skol1 ) ), !
% 52.37/52.78 v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (42538) {G6,W13,D3,L4,V0,M4} R(42523,190);d(20666);r(1099) { !
% 52.37/52.78 v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2( skol1
% 52.37/52.78 ) ), ! v14_lattices( k1_lattice2( skol1 ) ), r2_hidden( k5_lattices(
% 52.37/52.78 skol1 ), skol27 ) }.
% 52.37/52.78 parent0: (63788) {G2,W13,D3,L4,V0,M4} { r2_hidden( k5_lattices( skol1 ),
% 52.37/52.78 skol27 ), ! v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ), ! v14_lattices( k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 0 ==> 3
% 52.37/52.78 1 ==> 0
% 52.37/52.78 2 ==> 1
% 52.37/52.78 3 ==> 2
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63789) {G3,W10,D3,L3,V0,M3} { ! l3_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ), ! v14_lattices( k1_lattice2( skol1 ) ), r2_hidden( k5_lattices
% 52.37/52.78 ( skol1 ), skol27 ) }.
% 52.37/52.78 parent0[0]: (42538) {G6,W13,D3,L4,V0,M4} R(42523,190);d(20666);r(1099) { !
% 52.37/52.78 v10_lattices( k1_lattice2( skol1 ) ), ! l3_lattices( k1_lattice2( skol1 )
% 52.37/52.78 ), ! v14_lattices( k1_lattice2( skol1 ) ), r2_hidden( k5_lattices( skol1
% 52.37/52.78 ), skol27 ) }.
% 52.37/52.78 parent1[0]: (8252) {G2,W3,D3,L1,V0,M1} S(2413);r(1) { v10_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63790) {G2,W7,D3,L2,V0,M2} { ! v14_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ), r2_hidden( k5_lattices( skol1 ), skol27 ) }.
% 52.37/52.78 parent0[0]: (63789) {G3,W10,D3,L3,V0,M3} { ! l3_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ), ! v14_lattices( k1_lattice2( skol1 ) ), r2_hidden( k5_lattices
% 52.37/52.78 ( skol1 ), skol27 ) }.
% 52.37/52.78 parent1[0]: (457) {G1,W3,D3,L1,V0,M1} R(36,2) { l3_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63791) {G3,W4,D3,L1,V0,M1} { r2_hidden( k5_lattices( skol1 )
% 52.37/52.78 , skol27 ) }.
% 52.37/52.78 parent0[0]: (63790) {G2,W7,D3,L2,V0,M2} { ! v14_lattices( k1_lattice2(
% 52.37/52.78 skol1 ) ), r2_hidden( k5_lattices( skol1 ), skol27 ) }.
% 52.37/52.78 parent1[0]: (20723) {G2,W3,D3,L1,V0,M1} S(5443);r(1);r(2) { v14_lattices(
% 52.37/52.78 k1_lattice2( skol1 ) ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 resolution: (63792) {G1,W0,D0,L0,V0,M0} { }.
% 52.37/52.78 parent0[0]: (5) {G0,W4,D3,L1,V0,M1} I { ! r2_hidden( k5_lattices( skol1 ),
% 52.37/52.78 skol27 ) }.
% 52.37/52.78 parent1[0]: (63791) {G3,W4,D3,L1,V0,M1} { r2_hidden( k5_lattices( skol1 )
% 52.37/52.78 , skol27 ) }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 substitution1:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 subsumption: (62922) {G7,W0,D0,L0,V0,M0} S(42538);r(8252);r(457);r(20723);r
% 52.37/52.78 (5) { }.
% 52.37/52.78 parent0: (63792) {G1,W0,D0,L0,V0,M0} { }.
% 52.37/52.78 substitution0:
% 52.37/52.78 end
% 52.37/52.78 permutation0:
% 52.37/52.78 end
% 52.37/52.78
% 52.37/52.78 Proof check complete!
% 52.37/52.78
% 52.37/52.78 Memory use:
% 52.37/52.78
% 52.37/52.78 space for terms: 792130
% 52.37/52.78 space for clauses: 2638271
% 52.37/52.78
% 52.37/52.78
% 52.37/52.78 clauses generated: 522576
% 52.37/52.78 clauses kept: 62923
% 52.37/52.78 clauses selected: 4742
% 52.37/52.78 clauses deleted: 11040
% 52.37/52.78 clauses inuse deleted: 405
% 52.37/52.78
% 52.37/52.78 subsentry: 452634
% 52.37/52.78 literals s-matched: 239872
% 52.37/52.78 literals matched: 232611
% 52.37/52.78 full subsumption: 39745
% 52.37/52.78
% 52.37/52.78 checksum: -888220728
% 52.37/52.78
% 52.37/52.78
% 52.37/52.78 Bliksem ended
%------------------------------------------------------------------------------