%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : TOP024+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n022.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 : Thu Jul 21 21:20:17 EDT 2022
% Result : Theorem 4.39s 4.75s
% Output : Refutation 4.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : TOP024+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Sun May 29 05:06:08 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.46/1.11 *** allocated 10000 integers for termspace/termends
% 0.46/1.11 *** allocated 10000 integers for clauses
% 0.46/1.11 *** allocated 10000 integers for justifications
% 0.46/1.11 Bliksem 1.12
% 0.46/1.11
% 0.46/1.11
% 0.46/1.11 Automatic Strategy Selection
% 0.46/1.11
% 0.46/1.11
% 0.46/1.11 Clauses:
% 0.46/1.11
% 0.46/1.11 { ! v3_struct_0( skol1 ) }.
% 0.46/1.11 { v2_pre_topc( skol1 ) }.
% 0.46/1.11 { l1_pre_topc( skol1 ) }.
% 0.46/1.11 { m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 0.46/1.11 { v1_tsp_2( skol17, skol1 ) }.
% 0.46/1.11 { ! v1_tops_1( skol17, skol1 ) }.
% 0.46/1.11 { ! r2_hidden( X, Y ), ! r2_hidden( Y, X ) }.
% 0.46/1.11 { ! v1_membered( X ), ! m1_subset_1( Y, X ), v1_xcmplx_0( Y ) }.
% 0.46/1.11 { ! v2_membered( X ), ! m1_subset_1( Y, X ), v1_xcmplx_0( Y ) }.
% 0.46/1.11 { ! v2_membered( X ), ! m1_subset_1( Y, X ), v1_xreal_0( Y ) }.
% 0.46/1.11 { ! v3_membered( X ), ! m1_subset_1( Y, X ), v1_xcmplx_0( Y ) }.
% 0.46/1.11 { ! v3_membered( X ), ! m1_subset_1( Y, X ), v1_xreal_0( Y ) }.
% 0.46/1.11 { ! v3_membered( X ), ! m1_subset_1( Y, X ), v1_rat_1( Y ) }.
% 0.46/1.11 { ! v4_membered( X ), ! m1_subset_1( Y, X ), alpha1( Y ) }.
% 0.46/1.11 { ! v4_membered( X ), ! m1_subset_1( Y, X ), v1_rat_1( Y ) }.
% 0.46/1.11 { ! alpha1( X ), v1_xcmplx_0( X ) }.
% 0.46/1.11 { ! alpha1( X ), v1_xreal_0( X ) }.
% 0.46/1.11 { ! alpha1( X ), v1_int_1( X ) }.
% 0.46/1.11 { ! v1_xcmplx_0( X ), ! v1_xreal_0( X ), ! v1_int_1( X ), alpha1( X ) }.
% 0.46/1.11 { ! v5_membered( X ), ! m1_subset_1( Y, X ), alpha2( Y ) }.
% 0.46/1.11 { ! v5_membered( X ), ! m1_subset_1( Y, X ), v1_rat_1( Y ) }.
% 0.46/1.11 { ! alpha2( X ), alpha10( X ) }.
% 0.46/1.11 { ! alpha2( X ), v1_int_1( X ) }.
% 0.46/1.11 { ! alpha10( X ), ! v1_int_1( X ), alpha2( X ) }.
% 0.46/1.11 { ! alpha10( X ), v1_xcmplx_0( X ) }.
% 0.46/1.11 { ! alpha10( X ), v4_ordinal2( X ) }.
% 0.46/1.11 { ! alpha10( X ), v1_xreal_0( X ) }.
% 0.46/1.11 { ! v1_xcmplx_0( X ), ! v4_ordinal2( X ), ! v1_xreal_0( X ), alpha10( X ) }
% 0.46/1.11 .
% 0.46/1.11 { ! v1_xboole_0( X ), alpha3( X ) }.
% 0.46/1.11 { ! v1_xboole_0( X ), v5_membered( X ) }.
% 0.46/1.11 { ! alpha3( X ), alpha11( X ) }.
% 0.46/1.11 { ! alpha3( X ), v4_membered( X ) }.
% 0.46/1.11 { ! alpha11( X ), ! v4_membered( X ), alpha3( X ) }.
% 0.46/1.11 { ! alpha11( X ), v1_membered( X ) }.
% 0.46/1.11 { ! alpha11( X ), v2_membered( X ) }.
% 0.46/1.11 { ! alpha11( X ), v3_membered( X ) }.
% 0.46/1.11 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha11( X )
% 0.46/1.11 }.
% 0.46/1.11 { ! v1_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), v1_membered( Y
% 0.46/1.11 ) }.
% 0.46/1.11 { ! v2_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), v1_membered( Y
% 0.46/1.11 ) }.
% 0.46/1.11 { ! v2_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), v2_membered( Y
% 0.46/1.11 ) }.
% 0.46/1.11 { ! v3_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), v1_membered( Y
% 0.46/1.11 ) }.
% 0.46/1.11 { ! v3_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), v2_membered( Y
% 0.46/1.11 ) }.
% 0.46/1.11 { ! v3_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), v3_membered( Y
% 0.46/1.11 ) }.
% 0.46/1.11 { ! v4_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), alpha4( Y ) }.
% 0.46/1.11 { ! v4_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), v4_membered( Y
% 0.46/1.11 ) }.
% 0.46/1.11 { ! alpha4( X ), v1_membered( X ) }.
% 0.46/1.11 { ! alpha4( X ), v2_membered( X ) }.
% 0.46/1.11 { ! alpha4( X ), v3_membered( X ) }.
% 0.46/1.11 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha4( X ) }
% 0.46/1.11 .
% 0.46/1.11 { ! v5_membered( X ), v4_membered( X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), ! v1_xboole_0( Y ), v3_pre_topc( Y, X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), ! v1_xboole_0( Y ), v4_pre_topc( Y, X ) }.
% 0.46/1.11 { ! v5_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), alpha5( Y ) }.
% 0.46/1.11 { ! v5_membered( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), v5_membered( Y
% 0.46/1.11 ) }.
% 0.46/1.11 { ! alpha5( X ), alpha12( X ) }.
% 0.46/1.11 { ! alpha5( X ), v4_membered( X ) }.
% 0.46/1.11 { ! alpha12( X ), ! v4_membered( X ), alpha5( X ) }.
% 0.46/1.11 { ! alpha12( X ), v1_membered( X ) }.
% 0.46/1.11 { ! alpha12( X ), v2_membered( X ) }.
% 0.46/1.11 { ! alpha12( X ), v3_membered( X ) }.
% 0.46/1.11 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha12( X )
% 0.46/1.11 }.
% 0.46/1.11 { ! v4_membered( X ), v3_membered( X ) }.
% 0.46/1.11 { ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 0.46/1.11 ! v1_xboole_0( Y ), v2_tops_1( Y, X ) }.
% 0.46/1.11 { ! v3_membered( X ), v2_membered( X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), ! v1_xboole_0( Y ), v3_tops_1( Y, X ) }.
% 0.46/1.11 { ! v2_membered( X ), v1_membered( X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), ! v3_tops_1( Y, X ), v2_tops_1( Y, X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), ! v4_pre_topc( Y, X ), ! v2_tops_1( Y, X ),
% 0.46/1.11 v2_tops_1( Y, X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), ! v4_pre_topc( Y, X ), ! v2_tops_1( Y, X ),
% 0.46/1.11 v3_tops_1( Y, X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), ! v3_pre_topc( Y, X ), ! v3_tops_1( Y, X ), alpha6
% 0.46/1.11 ( X, Y ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), ! v3_pre_topc( Y, X ), ! v3_tops_1( Y, X ),
% 0.46/1.11 v3_tops_1( Y, X ) }.
% 0.46/1.11 { ! alpha6( X, Y ), alpha13( X, Y ) }.
% 0.46/1.11 { ! alpha6( X, Y ), v2_tops_1( Y, X ) }.
% 0.46/1.11 { ! alpha13( X, Y ), ! v2_tops_1( Y, X ), alpha6( X, Y ) }.
% 0.46/1.11 { ! alpha13( X, Y ), alpha16( X, Y ) }.
% 0.46/1.11 { ! alpha13( X, Y ), v5_membered( Y ) }.
% 0.46/1.11 { ! alpha16( X, Y ), ! v5_membered( Y ), alpha13( X, Y ) }.
% 0.46/1.11 { ! alpha16( X, Y ), alpha19( X, Y ) }.
% 0.46/1.11 { ! alpha16( X, Y ), v4_membered( Y ) }.
% 0.46/1.11 { ! alpha19( X, Y ), ! v4_membered( Y ), alpha16( X, Y ) }.
% 0.46/1.11 { ! alpha19( X, Y ), alpha22( X, Y ) }.
% 0.46/1.11 { ! alpha19( X, Y ), v3_membered( Y ) }.
% 0.46/1.11 { ! alpha22( X, Y ), ! v3_membered( Y ), alpha19( X, Y ) }.
% 0.46/1.11 { ! alpha22( X, Y ), alpha25( X, Y ) }.
% 0.46/1.11 { ! alpha22( X, Y ), v2_membered( Y ) }.
% 0.46/1.11 { ! alpha25( X, Y ), ! v2_membered( Y ), alpha22( X, Y ) }.
% 0.46/1.11 { ! alpha25( X, Y ), alpha27( X, Y ) }.
% 0.46/1.11 { ! alpha25( X, Y ), v1_membered( Y ) }.
% 0.46/1.11 { ! alpha27( X, Y ), ! v1_membered( Y ), alpha25( X, Y ) }.
% 0.46/1.11 { ! alpha27( X, Y ), v1_xboole_0( Y ) }.
% 0.46/1.11 { ! alpha27( X, Y ), v3_pre_topc( Y, X ) }.
% 0.46/1.11 { ! alpha27( X, Y ), v4_pre_topc( Y, X ) }.
% 0.46/1.11 { ! v1_xboole_0( Y ), ! v3_pre_topc( Y, X ), ! v4_pre_topc( Y, X ), alpha27
% 0.46/1.11 ( X, Y ) }.
% 0.46/1.11 { ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 0.46/1.11 ! v1_tops_1( Y, X ), k6_pre_topc( X, Y ) = u1_struct_0( X ) }.
% 0.46/1.11 { ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 0.46/1.11 ! k6_pre_topc( X, Y ) = u1_struct_0( X ), v1_tops_1( Y, X ) }.
% 0.46/1.11 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1(
% 0.46/1.11 Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tsp_2( Y, X ), v1_tsp_1( Y, X
% 0.46/1.11 ) }.
% 0.46/1.11 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1(
% 0.46/1.11 Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tsp_2( Y, X ), k3_tex_4( X, Y
% 0.46/1.11 ) = u1_struct_0( X ) }.
% 0.46/1.11 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1(
% 0.46/1.11 Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tsp_1( Y, X ), ! k3_tex_4( X,
% 0.46/1.11 Y ) = u1_struct_0( X ), v1_tsp_2( Y, X ) }.
% 0.46/1.11 { && }.
% 0.46/1.11 { && }.
% 0.46/1.11 { ! l1_struct_0( X ), m1_subset_1( k2_pre_topc( X ), k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ) }.
% 0.46/1.11 { v3_struct_0( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), m1_subset_1( k3_tex_4( X, Y ), k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 0.46/1.11 m1_subset_1( k6_pre_topc( X, Y ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! l1_pre_topc( X ), l1_struct_0( X ) }.
% 0.46/1.11 { && }.
% 0.46/1.11 { && }.
% 0.46/1.11 { && }.
% 0.46/1.11 { l1_pre_topc( skol2 ) }.
% 0.46/1.11 { l1_struct_0( skol3 ) }.
% 0.46/1.11 { m1_subset_1( skol4( X ), X ) }.
% 0.46/1.11 { v3_struct_0( X ), ! l1_struct_0( X ), ! v1_xboole_0( u1_struct_0( X ) ) }
% 0.46/1.11 .
% 0.46/1.11 { ! v1_xboole_0( k1_zfmisc_1( X ) ) }.
% 0.46/1.11 { v3_struct_0( X ), ! l1_struct_0( X ), ! v1_xboole_0( k2_pre_topc( X ) ) }
% 0.46/1.11 .
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 0.46/1.11 u1_struct_0( X ) ) ), v4_pre_topc( k6_pre_topc( X, Y ), X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), v4_pre_topc( k2_pre_topc( X ), X
% 0.46/1.11 ) }.
% 0.46/1.11 { v1_xboole_0( k1_xboole_0 ) }.
% 0.46/1.11 { v1_membered( k1_xboole_0 ) }.
% 0.46/1.11 { v2_membered( k1_xboole_0 ) }.
% 0.46/1.11 { v3_membered( k1_xboole_0 ) }.
% 0.46/1.11 { v4_membered( k1_xboole_0 ) }.
% 0.46/1.11 { v5_membered( k1_xboole_0 ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), v3_pre_topc( k2_pre_topc( X ), X
% 0.46/1.11 ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), v4_pre_topc( k2_pre_topc( X ), X
% 0.46/1.11 ) }.
% 0.46/1.11 { ! l1_pre_topc( X ), v1_tops_1( k2_pre_topc( X ), X ) }.
% 0.46/1.11 { ! v1_xboole_0( skol5 ) }.
% 0.46/1.11 { v1_membered( skol5 ) }.
% 0.46/1.11 { v2_membered( skol5 ) }.
% 0.46/1.11 { v3_membered( skol5 ) }.
% 0.46/1.11 { v4_membered( skol5 ) }.
% 0.46/1.11 { v5_membered( skol5 ) }.
% 0.46/1.11 { v1_xboole_0( X ), ! v1_xboole_0( skol6( Y ) ) }.
% 0.46/1.11 { v1_xboole_0( X ), m1_subset_1( skol6( X ), k1_zfmisc_1( X ) ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), m1_subset_1( skol7( X ),
% 0.46/1.11 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), v3_pre_topc( skol7( X ), X ) }.
% 0.46/1.11 { v1_xboole_0( skol8( Y ) ) }.
% 0.46/1.11 { m1_subset_1( skol8( X ), k1_zfmisc_1( X ) ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), m1_subset_1( skol9( X ),
% 0.46/1.11 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), v3_pre_topc( skol9( X ), X ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), v4_pre_topc( skol9( X ), X ) }.
% 0.46/1.11 { l1_struct_0( skol10 ) }.
% 0.46/1.11 { ! v3_struct_0( skol10 ) }.
% 0.46/1.11 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), alpha7( X,
% 0.46/1.11 skol11( X ) ) }.
% 0.46/1.11 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), v4_pre_topc(
% 0.46/1.11 skol11( X ), X ) }.
% 0.46/1.11 { ! alpha7( X, Y ), m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! alpha7( X, Y ), ! v1_xboole_0( Y ) }.
% 0.46/1.11 { ! alpha7( X, Y ), v3_pre_topc( Y, X ) }.
% 0.46/1.11 { ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), v1_xboole_0( Y ), !
% 0.46/1.11 v3_pre_topc( Y, X ), alpha7( X, Y ) }.
% 0.46/1.11 { ! l1_pre_topc( X ), alpha8( X, skol12( X ) ) }.
% 0.46/1.11 { ! l1_pre_topc( X ), v2_tops_1( skol12( X ), X ) }.
% 0.46/1.11 { ! alpha8( X, Y ), alpha14( X, Y ) }.
% 0.46/1.11 { ! alpha8( X, Y ), v5_membered( Y ) }.
% 0.46/1.11 { ! alpha14( X, Y ), ! v5_membered( Y ), alpha8( X, Y ) }.
% 0.46/1.11 { ! alpha14( X, Y ), alpha17( X, Y ) }.
% 0.46/1.11 { ! alpha14( X, Y ), v4_membered( Y ) }.
% 0.46/1.11 { ! alpha17( X, Y ), ! v4_membered( Y ), alpha14( X, Y ) }.
% 0.46/1.11 { ! alpha17( X, Y ), alpha20( X, Y ) }.
% 0.46/1.11 { ! alpha17( X, Y ), v3_membered( Y ) }.
% 0.46/1.11 { ! alpha20( X, Y ), ! v3_membered( Y ), alpha17( X, Y ) }.
% 0.46/1.11 { ! alpha20( X, Y ), alpha23( X, Y ) }.
% 0.46/1.11 { ! alpha20( X, Y ), v2_membered( Y ) }.
% 0.46/1.11 { ! alpha23( X, Y ), ! v2_membered( Y ), alpha20( X, Y ) }.
% 0.46/1.11 { ! alpha23( X, Y ), m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! alpha23( X, Y ), v1_xboole_0( Y ) }.
% 0.46/1.11 { ! alpha23( X, Y ), v1_membered( Y ) }.
% 0.46/1.11 { ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_xboole_0( Y ),
% 0.46/1.11 ! v1_membered( Y ), alpha23( X, Y ) }.
% 0.46/1.11 { v3_struct_0( X ), ! l1_struct_0( X ), ! v1_xboole_0( skol13( Y ) ) }.
% 0.46/1.11 { v3_struct_0( X ), ! l1_struct_0( X ), m1_subset_1( skol13( X ),
% 0.46/1.11 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), alpha9( X, skol14( X ) ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), v3_tops_1( skol14( X ), X ) }.
% 0.46/1.11 { ! alpha9( X, Y ), alpha15( X, Y ) }.
% 0.46/1.11 { ! alpha9( X, Y ), v2_tops_1( Y, X ) }.
% 0.46/1.11 { ! alpha15( X, Y ), ! v2_tops_1( Y, X ), alpha9( X, Y ) }.
% 0.46/1.11 { ! alpha15( X, Y ), alpha18( X, Y ) }.
% 0.46/1.11 { ! alpha15( X, Y ), v5_membered( Y ) }.
% 0.46/1.11 { ! alpha18( X, Y ), ! v5_membered( Y ), alpha15( X, Y ) }.
% 0.46/1.11 { ! alpha18( X, Y ), alpha21( X, Y ) }.
% 0.46/1.11 { ! alpha18( X, Y ), v4_membered( Y ) }.
% 0.46/1.11 { ! alpha21( X, Y ), ! v4_membered( Y ), alpha18( X, Y ) }.
% 0.46/1.11 { ! alpha21( X, Y ), alpha24( X, Y ) }.
% 0.46/1.11 { ! alpha21( X, Y ), v3_membered( Y ) }.
% 0.46/1.11 { ! alpha24( X, Y ), ! v3_membered( Y ), alpha21( X, Y ) }.
% 0.46/1.11 { ! alpha24( X, Y ), alpha26( X, Y ) }.
% 0.46/1.11 { ! alpha24( X, Y ), v2_membered( Y ) }.
% 0.46/1.11 { ! alpha26( X, Y ), ! v2_membered( Y ), alpha24( X, Y ) }.
% 0.46/1.11 { ! alpha26( X, Y ), alpha28( X, Y ) }.
% 0.46/1.11 { ! alpha26( X, Y ), v1_membered( Y ) }.
% 0.46/1.11 { ! alpha28( X, Y ), ! v1_membered( Y ), alpha26( X, Y ) }.
% 0.46/1.11 { ! alpha28( X, Y ), alpha29( X, Y ) }.
% 0.46/1.11 { ! alpha28( X, Y ), v4_pre_topc( Y, X ) }.
% 0.46/1.11 { ! alpha29( X, Y ), ! v4_pre_topc( Y, X ), alpha28( X, Y ) }.
% 0.46/1.11 { ! alpha29( X, Y ), m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! alpha29( X, Y ), v1_xboole_0( Y ) }.
% 0.46/1.11 { ! alpha29( X, Y ), v3_pre_topc( Y, X ) }.
% 0.46/1.11 { ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_xboole_0( Y ),
% 0.46/1.11 ! v3_pre_topc( Y, X ), alpha29( X, Y ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), m1_subset_1( skol15( X ),
% 0.46/1.11 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.46/1.11 { ! v2_pre_topc( X ), ! l1_pre_topc( X ), v4_pre_topc( skol15( X ), X ) }.
% 0.46/1.11 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! v1_xboole_0(
% 0.46/1.11 skol16( Y ) ) }.
% 0.46/1.11 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), m1_subset_1(
% 0.46/1.11 skol16( X ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 1.27/1.61 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), v4_pre_topc(
% 1.27/1.61 skol16( X ), X ) }.
% 1.27/1.61 { r1_tarski( X, X ) }.
% 1.27/1.61 { ! l1_struct_0( X ), k2_pre_topc( X ) = u1_struct_0( X ) }.
% 1.27/1.61 { ! r2_hidden( X, Y ), m1_subset_1( X, Y ) }.
% 1.27/1.61 { ! m1_subset_1( X, Y ), v1_xboole_0( Y ), r2_hidden( X, Y ) }.
% 1.27/1.61 { ! m1_subset_1( X, k1_zfmisc_1( Y ) ), r1_tarski( X, Y ) }.
% 1.27/1.61 { ! r1_tarski( X, Y ), m1_subset_1( X, k1_zfmisc_1( Y ) ) }.
% 1.27/1.61 { ! r2_hidden( X, Z ), ! m1_subset_1( Z, k1_zfmisc_1( Y ) ), m1_subset_1( X
% 1.27/1.61 , Y ) }.
% 1.27/1.61 { ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 1.27/1.61 ! v4_pre_topc( Y, X ), k6_pre_topc( X, Y ) = Y }.
% 1.27/1.61 { ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 1.27/1.61 ! v2_pre_topc( X ), ! k6_pre_topc( X, Y ) = Y, v4_pre_topc( Y, X ) }.
% 1.27/1.61 { ! r2_hidden( X, Y ), ! m1_subset_1( Y, k1_zfmisc_1( Z ) ), ! v1_xboole_0
% 1.27/1.61 ( Z ) }.
% 1.27/1.61 { v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), ! m1_subset_1(
% 1.27/1.61 Y, k1_zfmisc_1( u1_struct_0( X ) ) ), k6_pre_topc( X, k3_tex_4( X, Y ) )
% 1.27/1.61 = k6_pre_topc( X, Y ) }.
% 1.27/1.61 { ! v1_xboole_0( X ), X = k1_xboole_0 }.
% 1.27/1.61 { ! r2_hidden( X, Y ), ! v1_xboole_0( Y ) }.
% 1.27/1.61 { ! v1_xboole_0( X ), X = Y, ! v1_xboole_0( Y ) }.
% 1.27/1.61
% 1.27/1.61 percentage equality = 0.019120, percentage horn = 0.936893
% 1.27/1.61 This is a problem with some equality
% 1.27/1.61
% 1.27/1.61
% 1.27/1.61
% 1.27/1.61 Options Used:
% 1.27/1.61
% 1.27/1.61 useres = 1
% 1.27/1.61 useparamod = 1
% 1.27/1.61 useeqrefl = 1
% 1.27/1.61 useeqfact = 1
% 1.27/1.61 usefactor = 1
% 1.27/1.61 usesimpsplitting = 0
% 1.27/1.61 usesimpdemod = 5
% 1.27/1.61 usesimpres = 3
% 1.27/1.61
% 1.27/1.61 resimpinuse = 1000
% 1.27/1.61 resimpclauses = 20000
% 1.27/1.61 substype = eqrewr
% 1.27/1.61 backwardsubs = 1
% 1.27/1.61 selectoldest = 5
% 1.27/1.61
% 1.27/1.61 litorderings [0] = split
% 1.27/1.61 litorderings [1] = extend the termordering, first sorting on arguments
% 1.27/1.61
% 1.27/1.61 termordering = kbo
% 1.27/1.61
% 1.27/1.61 litapriori = 0
% 1.27/1.61 termapriori = 1
% 1.27/1.61 litaposteriori = 0
% 1.27/1.61 termaposteriori = 0
% 1.27/1.61 demodaposteriori = 0
% 1.27/1.61 ordereqreflfact = 0
% 1.27/1.61
% 1.27/1.61 litselect = negord
% 1.27/1.61
% 1.27/1.61 maxweight = 15
% 1.27/1.61 maxdepth = 30000
% 1.27/1.61 maxlength = 115
% 1.27/1.61 maxnrvars = 195
% 1.27/1.61 excuselevel = 1
% 1.27/1.61 increasemaxweight = 1
% 1.27/1.61
% 1.27/1.61 maxselected = 10000000
% 1.27/1.61 maxnrclauses = 10000000
% 1.27/1.61
% 1.27/1.61 showgenerated = 0
% 1.27/1.61 showkept = 0
% 1.27/1.61 showselected = 0
% 1.27/1.61 showdeleted = 0
% 1.27/1.61 showresimp = 1
% 1.27/1.61 showstatus = 2000
% 1.27/1.61
% 1.27/1.61 prologoutput = 0
% 1.27/1.61 nrgoals = 5000000
% 1.27/1.61 totalproof = 1
% 1.27/1.61
% 1.27/1.61 Symbols occurring in the translation:
% 1.27/1.61
% 1.27/1.61 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.27/1.61 . [1, 2] (w:1, o:58, a:1, s:1, b:0),
% 1.27/1.61 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 1.27/1.61 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 1.27/1.61 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.27/1.61 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.27/1.61 v3_struct_0 [36, 1] (w:1, o:30, a:1, s:1, b:0),
% 1.27/1.61 v2_pre_topc [37, 1] (w:1, o:28, a:1, s:1, b:0),
% 1.27/1.61 l1_pre_topc [38, 1] (w:1, o:33, a:1, s:1, b:0),
% 1.27/1.61 u1_struct_0 [40, 1] (w:1, o:21, a:1, s:1, b:0),
% 1.27/1.61 k1_zfmisc_1 [41, 1] (w:1, o:31, a:1, s:1, b:0),
% 1.27/1.61 m1_subset_1 [42, 2] (w:1, o:82, a:1, s:1, b:0),
% 1.27/1.61 v1_tsp_2 [43, 2] (w:1, o:84, a:1, s:1, b:0),
% 1.27/1.61 v1_tops_1 [44, 2] (w:1, o:85, a:1, s:1, b:0),
% 1.27/1.61 r2_hidden [45, 2] (w:1, o:87, a:1, s:1, b:0),
% 1.27/1.61 v1_membered [46, 1] (w:1, o:22, a:1, s:1, b:0),
% 1.27/1.61 v1_xcmplx_0 [47, 1] (w:1, o:24, a:1, s:1, b:0),
% 1.27/1.61 v2_membered [48, 1] (w:1, o:29, a:1, s:1, b:0),
% 1.27/1.61 v1_xreal_0 [49, 1] (w:1, o:25, a:1, s:1, b:0),
% 1.27/1.61 v3_membered [50, 1] (w:1, o:34, a:1, s:1, b:0),
% 1.27/1.61 v1_rat_1 [51, 1] (w:1, o:26, a:1, s:1, b:0),
% 1.27/1.61 v4_membered [52, 1] (w:1, o:35, a:1, s:1, b:0),
% 1.27/1.61 v1_int_1 [53, 1] (w:1, o:27, a:1, s:1, b:0),
% 1.27/1.61 v5_membered [54, 1] (w:1, o:37, a:1, s:1, b:0),
% 1.27/1.61 v4_ordinal2 [55, 1] (w:1, o:36, a:1, s:1, b:0),
% 1.27/1.61 v1_xboole_0 [56, 1] (w:1, o:23, a:1, s:1, b:0),
% 1.27/1.61 v3_pre_topc [57, 2] (w:1, o:89, a:1, s:1, b:0),
% 1.27/1.61 v4_pre_topc [58, 2] (w:1, o:91, a:1, s:1, b:0),
% 1.27/1.61 v2_tops_1 [59, 2] (w:1, o:88, a:1, s:1, b:0),
% 1.27/1.61 v3_tops_1 [60, 2] (w:1, o:90, a:1, s:1, b:0),
% 1.27/1.61 k6_pre_topc [61, 2] (w:1, o:92, a:1, s:1, b:0),
% 1.27/1.61 v1_tsp_1 [62, 2] (w:1, o:83, a:1, s:1, b:0),
% 1.27/1.61 k3_tex_4 [63, 2] (w:1, o:93, a:1, s:1, b:0),
% 1.27/1.61 l1_struct_0 [64, 1] (w:1, o:38, a:1, s:1, b:0),
% 4.39/4.75 k2_pre_topc [65, 1] (w:1, o:32, a:1, s:1, b:0),
% 4.39/4.75 k1_xboole_0 [66, 0] (w:1, o:8, a:1, s:1, b:0),
% 4.39/4.75 r1_tarski [67, 2] (w:1, o:86, a:1, s:1, b:0),
% 4.39/4.75 alpha1 [69, 1] (w:1, o:39, a:1, s:1, b:1),
% 4.39/4.75 alpha2 [70, 1] (w:1, o:43, a:1, s:1, b:1),
% 4.39/4.75 alpha3 [71, 1] (w:1, o:44, a:1, s:1, b:1),
% 4.39/4.75 alpha4 [72, 1] (w:1, o:45, a:1, s:1, b:1),
% 4.39/4.75 alpha5 [73, 1] (w:1, o:46, a:1, s:1, b:1),
% 4.39/4.75 alpha6 [74, 2] (w:1, o:94, a:1, s:1, b:1),
% 4.39/4.75 alpha7 [75, 2] (w:1, o:95, a:1, s:1, b:1),
% 4.39/4.75 alpha8 [76, 2] (w:1, o:96, a:1, s:1, b:1),
% 4.39/4.75 alpha9 [77, 2] (w:1, o:97, a:1, s:1, b:1),
% 4.39/4.75 alpha10 [78, 1] (w:1, o:40, a:1, s:1, b:1),
% 4.39/4.75 alpha11 [79, 1] (w:1, o:41, a:1, s:1, b:1),
% 4.39/4.75 alpha12 [80, 1] (w:1, o:42, a:1, s:1, b:1),
% 4.39/4.75 alpha13 [81, 2] (w:1, o:98, a:1, s:1, b:1),
% 4.39/4.75 alpha14 [82, 2] (w:1, o:99, a:1, s:1, b:1),
% 4.39/4.75 alpha15 [83, 2] (w:1, o:100, a:1, s:1, b:1),
% 4.39/4.75 alpha16 [84, 2] (w:1, o:101, a:1, s:1, b:1),
% 4.39/4.75 alpha17 [85, 2] (w:1, o:102, a:1, s:1, b:1),
% 4.39/4.75 alpha18 [86, 2] (w:1, o:103, a:1, s:1, b:1),
% 4.39/4.75 alpha19 [87, 2] (w:1, o:104, a:1, s:1, b:1),
% 4.39/4.75 alpha20 [88, 2] (w:1, o:105, a:1, s:1, b:1),
% 4.39/4.75 alpha21 [89, 2] (w:1, o:106, a:1, s:1, b:1),
% 4.39/4.75 alpha22 [90, 2] (w:1, o:107, a:1, s:1, b:1),
% 4.39/4.75 alpha23 [91, 2] (w:1, o:108, a:1, s:1, b:1),
% 4.39/4.75 alpha24 [92, 2] (w:1, o:109, a:1, s:1, b:1),
% 4.39/4.75 alpha25 [93, 2] (w:1, o:110, a:1, s:1, b:1),
% 4.39/4.75 alpha26 [94, 2] (w:1, o:111, a:1, s:1, b:1),
% 4.39/4.75 alpha27 [95, 2] (w:1, o:112, a:1, s:1, b:1),
% 4.39/4.75 alpha28 [96, 2] (w:1, o:113, a:1, s:1, b:1),
% 4.39/4.75 alpha29 [97, 2] (w:1, o:114, a:1, s:1, b:1),
% 4.39/4.75 skol1 [98, 0] (w:1, o:10, a:1, s:1, b:1),
% 4.39/4.75 skol2 [99, 0] (w:1, o:13, a:1, s:1, b:1),
% 4.39/4.75 skol3 [100, 0] (w:1, o:14, a:1, s:1, b:1),
% 4.39/4.75 skol4 [101, 1] (w:1, o:47, a:1, s:1, b:1),
% 4.39/4.75 skol5 [102, 0] (w:1, o:15, a:1, s:1, b:1),
% 4.39/4.75 skol6 [103, 1] (w:1, o:48, a:1, s:1, b:1),
% 4.39/4.75 skol7 [104, 1] (w:1, o:49, a:1, s:1, b:1),
% 4.39/4.75 skol8 [105, 1] (w:1, o:50, a:1, s:1, b:1),
% 4.39/4.75 skol9 [106, 1] (w:1, o:51, a:1, s:1, b:1),
% 4.39/4.75 skol10 [107, 0] (w:1, o:11, a:1, s:1, b:1),
% 4.39/4.75 skol11 [108, 1] (w:1, o:52, a:1, s:1, b:1),
% 4.39/4.75 skol12 [109, 1] (w:1, o:53, a:1, s:1, b:1),
% 4.39/4.75 skol13 [110, 1] (w:1, o:54, a:1, s:1, b:1),
% 4.39/4.75 skol14 [111, 1] (w:1, o:55, a:1, s:1, b:1),
% 4.39/4.75 skol15 [112, 1] (w:1, o:56, a:1, s:1, b:1),
% 4.39/4.75 skol16 [113, 1] (w:1, o:57, a:1, s:1, b:1),
% 4.39/4.75 skol17 [114, 0] (w:1, o:12, a:1, s:1, b:1).
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Starting Search:
% 4.39/4.75
% 4.39/4.75 *** allocated 15000 integers for clauses
% 4.39/4.75 *** allocated 22500 integers for clauses
% 4.39/4.75 *** allocated 33750 integers for clauses
% 4.39/4.75 *** allocated 15000 integers for termspace/termends
% 4.39/4.75 *** allocated 50625 integers for clauses
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 22500 integers for termspace/termends
% 4.39/4.75 *** allocated 75937 integers for clauses
% 4.39/4.75 *** allocated 113905 integers for clauses
% 4.39/4.75 *** allocated 33750 integers for termspace/termends
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 4489
% 4.39/4.75 Kept: 2004
% 4.39/4.75 Inuse: 515
% 4.39/4.75 Deleted: 11
% 4.39/4.75 Deletedinuse: 5
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 170857 integers for clauses
% 4.39/4.75 *** allocated 50625 integers for termspace/termends
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 9589
% 4.39/4.75 Kept: 4007
% 4.39/4.75 Inuse: 804
% 4.39/4.75 Deleted: 107
% 4.39/4.75 Deletedinuse: 98
% 4.39/4.75
% 4.39/4.75 *** allocated 256285 integers for clauses
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 75937 integers for termspace/termends
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 14137
% 4.39/4.75 Kept: 6024
% 4.39/4.75 Inuse: 996
% 4.39/4.75 Deleted: 123
% 4.39/4.75 Deletedinuse: 105
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 384427 integers for clauses
% 4.39/4.75 *** allocated 113905 integers for termspace/termends
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 22531
% 4.39/4.75 Kept: 8027
% 4.39/4.75 Inuse: 1259
% 4.39/4.75 Deleted: 138
% 4.39/4.75 Deletedinuse: 107
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 576640 integers for clauses
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 31906
% 4.39/4.75 Kept: 10028
% 4.39/4.75 Inuse: 1531
% 4.39/4.75 Deleted: 160
% 4.39/4.75 Deletedinuse: 113
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 170857 integers for termspace/termends
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 40803
% 4.39/4.75 Kept: 12433
% 4.39/4.75 Inuse: 1688
% 4.39/4.75 Deleted: 165
% 4.39/4.75 Deletedinuse: 115
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 48176
% 4.39/4.75 Kept: 14915
% 4.39/4.75 Inuse: 1697
% 4.39/4.75 Deleted: 167
% 4.39/4.75 Deletedinuse: 117
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 864960 integers for clauses
% 4.39/4.75 *** allocated 256285 integers for termspace/termends
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 59295
% 4.39/4.75 Kept: 16920
% 4.39/4.75 Inuse: 1828
% 4.39/4.75 Deleted: 180
% 4.39/4.75 Deletedinuse: 117
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 68393
% 4.39/4.75 Kept: 19271
% 4.39/4.75 Inuse: 1887
% 4.39/4.75 Deleted: 219
% 4.39/4.75 Deletedinuse: 147
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying clauses:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 75629
% 4.39/4.75 Kept: 21282
% 4.39/4.75 Inuse: 1959
% 4.39/4.75 Deleted: 1807
% 4.39/4.75 Deletedinuse: 147
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 92572
% 4.39/4.75 Kept: 23359
% 4.39/4.75 Inuse: 2128
% 4.39/4.75 Deleted: 1808
% 4.39/4.75 Deletedinuse: 148
% 4.39/4.75
% 4.39/4.75 *** allocated 384427 integers for termspace/termends
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 1297440 integers for clauses
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 129020
% 4.39/4.75 Kept: 25376
% 4.39/4.75 Inuse: 2571
% 4.39/4.75 Deleted: 1815
% 4.39/4.75 Deletedinuse: 150
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 139919
% 4.39/4.75 Kept: 27405
% 4.39/4.75 Inuse: 2670
% 4.39/4.75 Deleted: 1816
% 4.39/4.75 Deletedinuse: 150
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 151689
% 4.39/4.75 Kept: 29411
% 4.39/4.75 Inuse: 2764
% 4.39/4.75 Deleted: 1816
% 4.39/4.75 Deletedinuse: 150
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 170152
% 4.39/4.75 Kept: 31412
% 4.39/4.75 Inuse: 2903
% 4.39/4.75 Deleted: 1816
% 4.39/4.75 Deletedinuse: 150
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 184641
% 4.39/4.75 Kept: 33420
% 4.39/4.75 Inuse: 2992
% 4.39/4.75 Deleted: 1816
% 4.39/4.75 Deletedinuse: 150
% 4.39/4.75
% 4.39/4.75 *** allocated 576640 integers for termspace/termends
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 194703
% 4.39/4.75 Kept: 35453
% 4.39/4.75 Inuse: 3053
% 4.39/4.75 Deleted: 1816
% 4.39/4.75 Deletedinuse: 150
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 *** allocated 1946160 integers for clauses
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 207406
% 4.39/4.75 Kept: 37533
% 4.39/4.75 Inuse: 3137
% 4.39/4.75 Deleted: 1817
% 4.39/4.75 Deletedinuse: 150
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Intermediate Status:
% 4.39/4.75 Generated: 213867
% 4.39/4.75 Kept: 39542
% 4.39/4.75 Inuse: 3216
% 4.39/4.75 Deleted: 1817
% 4.39/4.75 Deletedinuse: 150
% 4.39/4.75
% 4.39/4.75 Resimplifying inuse:
% 4.39/4.75 Done
% 4.39/4.75
% 4.39/4.75 Resimplifying clauses:
% 4.39/4.75
% 4.39/4.75 Bliksems!, er is een bewijs:
% 4.39/4.75 % SZS status Theorem
% 4.39/4.75 % SZS output start Refutation
% 4.39/4.75
% 4.39/4.75 (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 4.39/4.75 (1) {G0,W2,D2,L1,V0,M1} I { v2_pre_topc( skol1 ) }.
% 4.39/4.75 (2) {G0,W2,D2,L1,V0,M1} I { l1_pre_topc( skol1 ) }.
% 4.39/4.75 (3) {G0,W5,D4,L1,V0,M1} I { m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0(
% 4.39/4.75 skol1 ) ) ) }.
% 4.39/4.75 (4) {G0,W3,D2,L1,V0,M1} I { v1_tsp_2( skol17, skol1 ) }.
% 4.39/4.75 (5) {G0,W3,D2,L1,V0,M1} I { ! v1_tops_1( skol17, skol1 ) }.
% 4.39/4.75 (91) {G0,W16,D4,L4,V2,M4} I { ! l1_pre_topc( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tops_1( Y, X ), k6_pre_topc( X, Y
% 4.39/4.75 ) ==> u1_struct_0( X ) }.
% 4.39/4.75 (92) {G0,W16,D4,L4,V2,M4} I { ! l1_pre_topc( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ), ! k6_pre_topc( X, Y ) ==> u1_struct_0
% 4.39/4.75 ( X ), v1_tops_1( Y, X ) }.
% 4.39/4.75 (94) {G0,W20,D4,L6,V2,M6} I { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), !
% 4.39/4.75 v1_tsp_2( Y, X ), k3_tex_4( X, Y ) ==> u1_struct_0( X ) }.
% 4.39/4.75 (100) {G0,W4,D2,L2,V1,M2} I { ! l1_pre_topc( X ), l1_struct_0( X ) }.
% 4.39/4.75 (116) {G0,W6,D3,L2,V1,M2} I { ! l1_pre_topc( X ), v1_tops_1( k2_pre_topc( X
% 4.39/4.75 ), X ) }.
% 4.39/4.75 (192) {G0,W3,D2,L1,V1,M1} I { r1_tarski( X, X ) }.
% 4.39/4.75 (193) {G0,W7,D3,L2,V1,M2} I { ! l1_struct_0( X ), k2_pre_topc( X ) ==>
% 4.39/4.75 u1_struct_0( X ) }.
% 4.39/4.75 (197) {G0,W7,D3,L2,V2,M2} I { ! r1_tarski( X, Y ), m1_subset_1( X,
% 4.39/4.75 k1_zfmisc_1( Y ) ) }.
% 4.39/4.75 (202) {G0,W20,D4,L5,V2,M5} I { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 4.39/4.75 k6_pre_topc( X, k3_tex_4( X, Y ) ) ==> k6_pre_topc( X, Y ) }.
% 4.39/4.75 (1026) {G1,W11,D4,L2,V0,M2} R(92,5);r(2) { ! m1_subset_1( skol17,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.75 u1_struct_0( skol1 ) }.
% 4.39/4.75 (1046) {G1,W15,D4,L4,V0,M4} R(94,4);r(0) { ! v2_pre_topc( skol1 ), !
% 4.39/4.75 l1_pre_topc( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0(
% 4.39/4.75 skol1 ) ) ), k3_tex_4( skol1, skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.75 (2578) {G1,W6,D3,L2,V1,M2} P(193,116);r(100) { ! l1_pre_topc( X ),
% 4.39/4.75 v1_tops_1( u1_struct_0( X ), X ) }.
% 4.39/4.75 (2759) {G1,W4,D3,L1,V1,M1} R(197,192) { m1_subset_1( X, k1_zfmisc_1( X ) )
% 4.39/4.75 }.
% 4.39/4.75 (2766) {G2,W9,D4,L2,V1,M2} R(2759,91);r(2578) { ! l1_pre_topc( X ),
% 4.39/4.75 k6_pre_topc( X, u1_struct_0( X ) ) ==> u1_struct_0( X ) }.
% 4.39/4.75 (20372) {G2,W6,D3,L1,V0,M1} S(1046);r(1);r(2);r(3) { k3_tex_4( skol1,
% 4.39/4.75 skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.75 (20376) {G2,W6,D3,L1,V0,M1} S(1026);r(3) { ! k6_pre_topc( skol1, skol17 )
% 4.39/4.75 ==> u1_struct_0( skol1 ) }.
% 4.39/4.75 (36572) {G3,W15,D4,L4,V0,M4} P(20372,202);d(2766);r(0) { ! v2_pre_topc(
% 4.39/4.75 skol1 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( skol1 ) ) ), k6_pre_topc( skol1, skol17 ) ==> u1_struct_0(
% 4.39/4.75 skol1 ) }.
% 4.39/4.75 (40430) {G4,W0,D0,L0,V0,M0} S(36572);r(1);r(2);r(3);r(20376) { }.
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 % SZS output end Refutation
% 4.39/4.75 found a proof!
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Unprocessed initial clauses:
% 4.39/4.75
% 4.39/4.75 (40432) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol1 ) }.
% 4.39/4.75 (40433) {G0,W2,D2,L1,V0,M1} { v2_pre_topc( skol1 ) }.
% 4.39/4.75 (40434) {G0,W2,D2,L1,V0,M1} { l1_pre_topc( skol1 ) }.
% 4.39/4.75 (40435) {G0,W5,D4,L1,V0,M1} { m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 (40436) {G0,W3,D2,L1,V0,M1} { v1_tsp_2( skol17, skol1 ) }.
% 4.39/4.75 (40437) {G0,W3,D2,L1,V0,M1} { ! v1_tops_1( skol17, skol1 ) }.
% 4.39/4.75 (40438) {G0,W6,D2,L2,V2,M2} { ! r2_hidden( X, Y ), ! r2_hidden( Y, X ) }.
% 4.39/4.75 (40439) {G0,W7,D2,L3,V2,M3} { ! v1_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 v1_xcmplx_0( Y ) }.
% 4.39/4.75 (40440) {G0,W7,D2,L3,V2,M3} { ! v2_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 v1_xcmplx_0( Y ) }.
% 4.39/4.75 (40441) {G0,W7,D2,L3,V2,M3} { ! v2_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 v1_xreal_0( Y ) }.
% 4.39/4.75 (40442) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 v1_xcmplx_0( Y ) }.
% 4.39/4.75 (40443) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 v1_xreal_0( Y ) }.
% 4.39/4.75 (40444) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 v1_rat_1( Y ) }.
% 4.39/4.75 (40445) {G0,W7,D2,L3,V2,M3} { ! v4_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 alpha1( Y ) }.
% 4.39/4.75 (40446) {G0,W7,D2,L3,V2,M3} { ! v4_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 v1_rat_1( Y ) }.
% 4.39/4.75 (40447) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_xcmplx_0( X ) }.
% 4.39/4.75 (40448) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_xreal_0( X ) }.
% 4.39/4.75 (40449) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_int_1( X ) }.
% 4.39/4.75 (40450) {G0,W8,D2,L4,V1,M4} { ! v1_xcmplx_0( X ), ! v1_xreal_0( X ), !
% 4.39/4.75 v1_int_1( X ), alpha1( X ) }.
% 4.39/4.75 (40451) {G0,W7,D2,L3,V2,M3} { ! v5_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 alpha2( Y ) }.
% 4.39/4.75 (40452) {G0,W7,D2,L3,V2,M3} { ! v5_membered( X ), ! m1_subset_1( Y, X ),
% 4.39/4.75 v1_rat_1( Y ) }.
% 4.39/4.75 (40453) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha10( X ) }.
% 4.39/4.75 (40454) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), v1_int_1( X ) }.
% 4.39/4.75 (40455) {G0,W6,D2,L3,V1,M3} { ! alpha10( X ), ! v1_int_1( X ), alpha2( X )
% 4.39/4.75 }.
% 4.39/4.75 (40456) {G0,W4,D2,L2,V1,M2} { ! alpha10( X ), v1_xcmplx_0( X ) }.
% 4.39/4.75 (40457) {G0,W4,D2,L2,V1,M2} { ! alpha10( X ), v4_ordinal2( X ) }.
% 4.39/4.75 (40458) {G0,W4,D2,L2,V1,M2} { ! alpha10( X ), v1_xreal_0( X ) }.
% 4.39/4.75 (40459) {G0,W8,D2,L4,V1,M4} { ! v1_xcmplx_0( X ), ! v4_ordinal2( X ), !
% 4.39/4.75 v1_xreal_0( X ), alpha10( X ) }.
% 4.39/4.75 (40460) {G0,W4,D2,L2,V1,M2} { ! v1_xboole_0( X ), alpha3( X ) }.
% 4.39/4.75 (40461) {G0,W4,D2,L2,V1,M2} { ! v1_xboole_0( X ), v5_membered( X ) }.
% 4.39/4.75 (40462) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha11( X ) }.
% 4.39/4.75 (40463) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), v4_membered( X ) }.
% 4.39/4.75 (40464) {G0,W6,D2,L3,V1,M3} { ! alpha11( X ), ! v4_membered( X ), alpha3(
% 4.39/4.75 X ) }.
% 4.39/4.75 (40465) {G0,W4,D2,L2,V1,M2} { ! alpha11( X ), v1_membered( X ) }.
% 4.39/4.75 (40466) {G0,W4,D2,L2,V1,M2} { ! alpha11( X ), v2_membered( X ) }.
% 4.39/4.75 (40467) {G0,W4,D2,L2,V1,M2} { ! alpha11( X ), v3_membered( X ) }.
% 4.39/4.75 (40468) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 4.39/4.75 v3_membered( X ), alpha11( X ) }.
% 4.39/4.75 (40469) {G0,W8,D3,L3,V2,M3} { ! v1_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), v1_membered( Y ) }.
% 4.39/4.75 (40470) {G0,W8,D3,L3,V2,M3} { ! v2_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), v1_membered( Y ) }.
% 4.39/4.75 (40471) {G0,W8,D3,L3,V2,M3} { ! v2_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), v2_membered( Y ) }.
% 4.39/4.75 (40472) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), v1_membered( Y ) }.
% 4.39/4.75 (40473) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), v2_membered( Y ) }.
% 4.39/4.75 (40474) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), v3_membered( Y ) }.
% 4.39/4.75 (40475) {G0,W8,D3,L3,V2,M3} { ! v4_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), alpha4( Y ) }.
% 4.39/4.75 (40476) {G0,W8,D3,L3,V2,M3} { ! v4_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), v4_membered( Y ) }.
% 4.39/4.75 (40477) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v1_membered( X ) }.
% 4.39/4.75 (40478) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v2_membered( X ) }.
% 4.39/4.75 (40479) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v3_membered( X ) }.
% 4.39/4.75 (40480) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 4.39/4.75 v3_membered( X ), alpha4( X ) }.
% 4.39/4.75 (40481) {G0,W4,D2,L2,V1,M2} { ! v5_membered( X ), v4_membered( X ) }.
% 4.39/4.75 (40482) {G0,W14,D4,L5,V2,M5} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_xboole_0( Y ),
% 4.39/4.75 v3_pre_topc( Y, X ) }.
% 4.39/4.75 (40483) {G0,W14,D4,L5,V2,M5} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_xboole_0( Y ),
% 4.39/4.75 v4_pre_topc( Y, X ) }.
% 4.39/4.75 (40484) {G0,W8,D3,L3,V2,M3} { ! v5_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), alpha5( Y ) }.
% 4.39/4.75 (40485) {G0,W8,D3,L3,V2,M3} { ! v5_membered( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( X ) ), v5_membered( Y ) }.
% 4.39/4.75 (40486) {G0,W4,D2,L2,V1,M2} { ! alpha5( X ), alpha12( X ) }.
% 4.39/4.75 (40487) {G0,W4,D2,L2,V1,M2} { ! alpha5( X ), v4_membered( X ) }.
% 4.39/4.75 (40488) {G0,W6,D2,L3,V1,M3} { ! alpha12( X ), ! v4_membered( X ), alpha5(
% 4.39/4.75 X ) }.
% 4.39/4.75 (40489) {G0,W4,D2,L2,V1,M2} { ! alpha12( X ), v1_membered( X ) }.
% 4.39/4.75 (40490) {G0,W4,D2,L2,V1,M2} { ! alpha12( X ), v2_membered( X ) }.
% 4.39/4.75 (40491) {G0,W4,D2,L2,V1,M2} { ! alpha12( X ), v3_membered( X ) }.
% 4.39/4.75 (40492) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 4.39/4.75 v3_membered( X ), alpha12( X ) }.
% 4.39/4.75 (40493) {G0,W4,D2,L2,V1,M2} { ! v4_membered( X ), v3_membered( X ) }.
% 4.39/4.75 (40494) {G0,W12,D4,L4,V2,M4} { ! l1_pre_topc( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_xboole_0( Y ), v2_tops_1( Y, X )
% 4.39/4.75 }.
% 4.39/4.75 (40495) {G0,W4,D2,L2,V1,M2} { ! v3_membered( X ), v2_membered( X ) }.
% 4.39/4.75 (40496) {G0,W14,D4,L5,V2,M5} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_xboole_0( Y ),
% 4.39/4.75 v3_tops_1( Y, X ) }.
% 4.39/4.75 (40497) {G0,W4,D2,L2,V1,M2} { ! v2_membered( X ), v1_membered( X ) }.
% 4.39/4.75 (40498) {G0,W15,D4,L5,V2,M5} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v3_tops_1( Y, X ),
% 4.39/4.75 v2_tops_1( Y, X ) }.
% 4.39/4.75 (40499) {G0,W18,D4,L6,V2,M6} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v4_pre_topc( Y, X )
% 4.39/4.75 , ! v2_tops_1( Y, X ), v2_tops_1( Y, X ) }.
% 4.39/4.75 (40500) {G0,W18,D4,L6,V2,M6} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v4_pre_topc( Y, X )
% 4.39/4.75 , ! v2_tops_1( Y, X ), v3_tops_1( Y, X ) }.
% 4.39/4.75 (40501) {G0,W18,D4,L6,V2,M6} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v3_pre_topc( Y, X )
% 4.39/4.75 , ! v3_tops_1( Y, X ), alpha6( X, Y ) }.
% 4.39/4.75 (40502) {G0,W18,D4,L6,V2,M6} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v3_pre_topc( Y, X )
% 4.39/4.75 , ! v3_tops_1( Y, X ), v3_tops_1( Y, X ) }.
% 4.39/4.75 (40503) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), alpha13( X, Y ) }.
% 4.39/4.75 (40504) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), v2_tops_1( Y, X ) }.
% 4.39/4.75 (40505) {G0,W9,D2,L3,V2,M3} { ! alpha13( X, Y ), ! v2_tops_1( Y, X ),
% 4.39/4.75 alpha6( X, Y ) }.
% 4.39/4.75 (40506) {G0,W6,D2,L2,V2,M2} { ! alpha13( X, Y ), alpha16( X, Y ) }.
% 4.39/4.75 (40507) {G0,W5,D2,L2,V2,M2} { ! alpha13( X, Y ), v5_membered( Y ) }.
% 4.39/4.75 (40508) {G0,W8,D2,L3,V2,M3} { ! alpha16( X, Y ), ! v5_membered( Y ),
% 4.39/4.75 alpha13( X, Y ) }.
% 4.39/4.75 (40509) {G0,W6,D2,L2,V2,M2} { ! alpha16( X, Y ), alpha19( X, Y ) }.
% 4.39/4.75 (40510) {G0,W5,D2,L2,V2,M2} { ! alpha16( X, Y ), v4_membered( Y ) }.
% 4.39/4.75 (40511) {G0,W8,D2,L3,V2,M3} { ! alpha19( X, Y ), ! v4_membered( Y ),
% 4.39/4.75 alpha16( X, Y ) }.
% 4.39/4.75 (40512) {G0,W6,D2,L2,V2,M2} { ! alpha19( X, Y ), alpha22( X, Y ) }.
% 4.39/4.75 (40513) {G0,W5,D2,L2,V2,M2} { ! alpha19( X, Y ), v3_membered( Y ) }.
% 4.39/4.75 (40514) {G0,W8,D2,L3,V2,M3} { ! alpha22( X, Y ), ! v3_membered( Y ),
% 4.39/4.75 alpha19( X, Y ) }.
% 4.39/4.75 (40515) {G0,W6,D2,L2,V2,M2} { ! alpha22( X, Y ), alpha25( X, Y ) }.
% 4.39/4.75 (40516) {G0,W5,D2,L2,V2,M2} { ! alpha22( X, Y ), v2_membered( Y ) }.
% 4.39/4.75 (40517) {G0,W8,D2,L3,V2,M3} { ! alpha25( X, Y ), ! v2_membered( Y ),
% 4.39/4.75 alpha22( X, Y ) }.
% 4.39/4.75 (40518) {G0,W6,D2,L2,V2,M2} { ! alpha25( X, Y ), alpha27( X, Y ) }.
% 4.39/4.75 (40519) {G0,W5,D2,L2,V2,M2} { ! alpha25( X, Y ), v1_membered( Y ) }.
% 4.39/4.75 (40520) {G0,W8,D2,L3,V2,M3} { ! alpha27( X, Y ), ! v1_membered( Y ),
% 4.39/4.75 alpha25( X, Y ) }.
% 4.39/4.75 (40521) {G0,W5,D2,L2,V2,M2} { ! alpha27( X, Y ), v1_xboole_0( Y ) }.
% 4.39/4.75 (40522) {G0,W6,D2,L2,V2,M2} { ! alpha27( X, Y ), v3_pre_topc( Y, X ) }.
% 4.39/4.75 (40523) {G0,W6,D2,L2,V2,M2} { ! alpha27( X, Y ), v4_pre_topc( Y, X ) }.
% 4.39/4.75 (40524) {G0,W11,D2,L4,V2,M4} { ! v1_xboole_0( Y ), ! v3_pre_topc( Y, X ),
% 4.39/4.75 ! v4_pre_topc( Y, X ), alpha27( X, Y ) }.
% 4.39/4.75 (40525) {G0,W16,D4,L4,V2,M4} { ! l1_pre_topc( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tops_1( Y, X ), k6_pre_topc( X, Y
% 4.39/4.75 ) = u1_struct_0( X ) }.
% 4.39/4.75 (40526) {G0,W16,D4,L4,V2,M4} { ! l1_pre_topc( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ), ! k6_pre_topc( X, Y ) = u1_struct_0( X
% 4.39/4.75 ), v1_tops_1( Y, X ) }.
% 4.39/4.75 (40527) {G0,W17,D4,L6,V2,M6} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), !
% 4.39/4.75 v1_tsp_2( Y, X ), v1_tsp_1( Y, X ) }.
% 4.39/4.75 (40528) {G0,W20,D4,L6,V2,M6} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), !
% 4.39/4.75 v1_tsp_2( Y, X ), k3_tex_4( X, Y ) = u1_struct_0( X ) }.
% 4.39/4.75 (40529) {G0,W23,D4,L7,V2,M7} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), !
% 4.39/4.75 v1_tsp_1( Y, X ), ! k3_tex_4( X, Y ) = u1_struct_0( X ), v1_tsp_2( Y, X )
% 4.39/4.75 }.
% 4.39/4.75 (40530) {G0,W1,D1,L1,V0,M1} { && }.
% 4.39/4.75 (40531) {G0,W1,D1,L1,V0,M1} { && }.
% 4.39/4.75 (40532) {G0,W8,D4,L2,V1,M2} { ! l1_struct_0( X ), m1_subset_1( k2_pre_topc
% 4.39/4.75 ( X ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40533) {G0,W16,D4,L4,V2,M4} { v3_struct_0( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), m1_subset_1( k3_tex_4
% 4.39/4.75 ( X, Y ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40534) {G0,W14,D4,L3,V2,M3} { ! l1_pre_topc( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ), m1_subset_1( k6_pre_topc( X, Y ),
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40535) {G0,W4,D2,L2,V1,M2} { ! l1_pre_topc( X ), l1_struct_0( X ) }.
% 4.39/4.75 (40536) {G0,W1,D1,L1,V0,M1} { && }.
% 4.39/4.75 (40537) {G0,W1,D1,L1,V0,M1} { && }.
% 4.39/4.75 (40538) {G0,W1,D1,L1,V0,M1} { && }.
% 4.39/4.75 (40539) {G0,W2,D2,L1,V0,M1} { l1_pre_topc( skol2 ) }.
% 4.39/4.75 (40540) {G0,W2,D2,L1,V0,M1} { l1_struct_0( skol3 ) }.
% 4.39/4.75 (40541) {G0,W4,D3,L1,V1,M1} { m1_subset_1( skol4( X ), X ) }.
% 4.39/4.75 (40542) {G0,W7,D3,L3,V1,M3} { v3_struct_0( X ), ! l1_struct_0( X ), !
% 4.39/4.75 v1_xboole_0( u1_struct_0( X ) ) }.
% 4.39/4.75 (40543) {G0,W3,D3,L1,V1,M1} { ! v1_xboole_0( k1_zfmisc_1( X ) ) }.
% 4.39/4.75 (40544) {G0,W7,D3,L3,V1,M3} { v3_struct_0( X ), ! l1_struct_0( X ), !
% 4.39/4.75 v1_xboole_0( k2_pre_topc( X ) ) }.
% 4.39/4.75 (40545) {G0,W14,D4,L4,V2,M4} { ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), v4_pre_topc(
% 4.39/4.75 k6_pre_topc( X, Y ), X ) }.
% 4.39/4.75 (40546) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 v4_pre_topc( k2_pre_topc( X ), X ) }.
% 4.39/4.75 (40547) {G0,W2,D2,L1,V0,M1} { v1_xboole_0( k1_xboole_0 ) }.
% 4.39/4.75 (40548) {G0,W2,D2,L1,V0,M1} { v1_membered( k1_xboole_0 ) }.
% 4.39/4.75 (40549) {G0,W2,D2,L1,V0,M1} { v2_membered( k1_xboole_0 ) }.
% 4.39/4.75 (40550) {G0,W2,D2,L1,V0,M1} { v3_membered( k1_xboole_0 ) }.
% 4.39/4.75 (40551) {G0,W2,D2,L1,V0,M1} { v4_membered( k1_xboole_0 ) }.
% 4.39/4.75 (40552) {G0,W2,D2,L1,V0,M1} { v5_membered( k1_xboole_0 ) }.
% 4.39/4.75 (40553) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 v3_pre_topc( k2_pre_topc( X ), X ) }.
% 4.39/4.75 (40554) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 v4_pre_topc( k2_pre_topc( X ), X ) }.
% 4.39/4.75 (40555) {G0,W6,D3,L2,V1,M2} { ! l1_pre_topc( X ), v1_tops_1( k2_pre_topc(
% 4.39/4.75 X ), X ) }.
% 4.39/4.75 (40556) {G0,W2,D2,L1,V0,M1} { ! v1_xboole_0( skol5 ) }.
% 4.39/4.75 (40557) {G0,W2,D2,L1,V0,M1} { v1_membered( skol5 ) }.
% 4.39/4.75 (40558) {G0,W2,D2,L1,V0,M1} { v2_membered( skol5 ) }.
% 4.39/4.75 (40559) {G0,W2,D2,L1,V0,M1} { v3_membered( skol5 ) }.
% 4.39/4.75 (40560) {G0,W2,D2,L1,V0,M1} { v4_membered( skol5 ) }.
% 4.39/4.75 (40561) {G0,W2,D2,L1,V0,M1} { v5_membered( skol5 ) }.
% 4.39/4.75 (40562) {G0,W5,D3,L2,V2,M2} { v1_xboole_0( X ), ! v1_xboole_0( skol6( Y )
% 4.39/4.75 ) }.
% 4.39/4.75 (40563) {G0,W7,D3,L2,V1,M2} { v1_xboole_0( X ), m1_subset_1( skol6( X ),
% 4.39/4.75 k1_zfmisc_1( X ) ) }.
% 4.39/4.75 (40564) {G0,W10,D4,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 m1_subset_1( skol7( X ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40565) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 v3_pre_topc( skol7( X ), X ) }.
% 4.39/4.75 (40566) {G0,W3,D3,L1,V1,M1} { v1_xboole_0( skol8( Y ) ) }.
% 4.39/4.75 (40567) {G0,W5,D3,L1,V1,M1} { m1_subset_1( skol8( X ), k1_zfmisc_1( X ) )
% 4.39/4.75 }.
% 4.39/4.75 (40568) {G0,W10,D4,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 m1_subset_1( skol9( X ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40569) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 v3_pre_topc( skol9( X ), X ) }.
% 4.39/4.75 (40570) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 v4_pre_topc( skol9( X ), X ) }.
% 4.39/4.75 (40571) {G0,W2,D2,L1,V0,M1} { l1_struct_0( skol10 ) }.
% 4.39/4.75 (40572) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol10 ) }.
% 4.39/4.75 (40573) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), alpha7( X, skol11( X ) ) }.
% 4.39/4.75 (40574) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), v4_pre_topc( skol11( X ), X ) }.
% 4.39/4.75 (40575) {G0,W8,D4,L2,V2,M2} { ! alpha7( X, Y ), m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40576) {G0,W5,D2,L2,V2,M2} { ! alpha7( X, Y ), ! v1_xboole_0( Y ) }.
% 4.39/4.75 (40577) {G0,W6,D2,L2,V2,M2} { ! alpha7( X, Y ), v3_pre_topc( Y, X ) }.
% 4.39/4.75 (40578) {G0,W13,D4,L4,V2,M4} { ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0
% 4.39/4.75 ( X ) ) ), v1_xboole_0( Y ), ! v3_pre_topc( Y, X ), alpha7( X, Y ) }.
% 4.39/4.75 (40579) {G0,W6,D3,L2,V1,M2} { ! l1_pre_topc( X ), alpha8( X, skol12( X ) )
% 4.39/4.75 }.
% 4.39/4.75 (40580) {G0,W6,D3,L2,V1,M2} { ! l1_pre_topc( X ), v2_tops_1( skol12( X ),
% 4.39/4.75 X ) }.
% 4.39/4.75 (40581) {G0,W6,D2,L2,V2,M2} { ! alpha8( X, Y ), alpha14( X, Y ) }.
% 4.39/4.75 (40582) {G0,W5,D2,L2,V2,M2} { ! alpha8( X, Y ), v5_membered( Y ) }.
% 4.39/4.75 (40583) {G0,W8,D2,L3,V2,M3} { ! alpha14( X, Y ), ! v5_membered( Y ),
% 4.39/4.75 alpha8( X, Y ) }.
% 4.39/4.75 (40584) {G0,W6,D2,L2,V2,M2} { ! alpha14( X, Y ), alpha17( X, Y ) }.
% 4.39/4.75 (40585) {G0,W5,D2,L2,V2,M2} { ! alpha14( X, Y ), v4_membered( Y ) }.
% 4.39/4.75 (40586) {G0,W8,D2,L3,V2,M3} { ! alpha17( X, Y ), ! v4_membered( Y ),
% 4.39/4.75 alpha14( X, Y ) }.
% 4.39/4.75 (40587) {G0,W6,D2,L2,V2,M2} { ! alpha17( X, Y ), alpha20( X, Y ) }.
% 4.39/4.75 (40588) {G0,W5,D2,L2,V2,M2} { ! alpha17( X, Y ), v3_membered( Y ) }.
% 4.39/4.75 (40589) {G0,W8,D2,L3,V2,M3} { ! alpha20( X, Y ), ! v3_membered( Y ),
% 4.39/4.75 alpha17( X, Y ) }.
% 4.39/4.75 (40590) {G0,W6,D2,L2,V2,M2} { ! alpha20( X, Y ), alpha23( X, Y ) }.
% 4.39/4.75 (40591) {G0,W5,D2,L2,V2,M2} { ! alpha20( X, Y ), v2_membered( Y ) }.
% 4.39/4.75 (40592) {G0,W8,D2,L3,V2,M3} { ! alpha23( X, Y ), ! v2_membered( Y ),
% 4.39/4.75 alpha20( X, Y ) }.
% 4.39/4.75 (40593) {G0,W8,D4,L2,V2,M2} { ! alpha23( X, Y ), m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40594) {G0,W5,D2,L2,V2,M2} { ! alpha23( X, Y ), v1_xboole_0( Y ) }.
% 4.39/4.75 (40595) {G0,W5,D2,L2,V2,M2} { ! alpha23( X, Y ), v1_membered( Y ) }.
% 4.39/4.75 (40596) {G0,W12,D4,L4,V2,M4} { ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0
% 4.39/4.75 ( X ) ) ), ! v1_xboole_0( Y ), ! v1_membered( Y ), alpha23( X, Y ) }.
% 4.39/4.75 (40597) {G0,W7,D3,L3,V2,M3} { v3_struct_0( X ), ! l1_struct_0( X ), !
% 4.39/4.75 v1_xboole_0( skol13( Y ) ) }.
% 4.39/4.75 (40598) {G0,W10,D4,L3,V1,M3} { v3_struct_0( X ), ! l1_struct_0( X ),
% 4.39/4.75 m1_subset_1( skol13( X ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40599) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 alpha9( X, skol14( X ) ) }.
% 4.39/4.75 (40600) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 v3_tops_1( skol14( X ), X ) }.
% 4.39/4.75 (40601) {G0,W6,D2,L2,V2,M2} { ! alpha9( X, Y ), alpha15( X, Y ) }.
% 4.39/4.75 (40602) {G0,W6,D2,L2,V2,M2} { ! alpha9( X, Y ), v2_tops_1( Y, X ) }.
% 4.39/4.75 (40603) {G0,W9,D2,L3,V2,M3} { ! alpha15( X, Y ), ! v2_tops_1( Y, X ),
% 4.39/4.75 alpha9( X, Y ) }.
% 4.39/4.75 (40604) {G0,W6,D2,L2,V2,M2} { ! alpha15( X, Y ), alpha18( X, Y ) }.
% 4.39/4.75 (40605) {G0,W5,D2,L2,V2,M2} { ! alpha15( X, Y ), v5_membered( Y ) }.
% 4.39/4.75 (40606) {G0,W8,D2,L3,V2,M3} { ! alpha18( X, Y ), ! v5_membered( Y ),
% 4.39/4.75 alpha15( X, Y ) }.
% 4.39/4.75 (40607) {G0,W6,D2,L2,V2,M2} { ! alpha18( X, Y ), alpha21( X, Y ) }.
% 4.39/4.75 (40608) {G0,W5,D2,L2,V2,M2} { ! alpha18( X, Y ), v4_membered( Y ) }.
% 4.39/4.75 (40609) {G0,W8,D2,L3,V2,M3} { ! alpha21( X, Y ), ! v4_membered( Y ),
% 4.39/4.75 alpha18( X, Y ) }.
% 4.39/4.75 (40610) {G0,W6,D2,L2,V2,M2} { ! alpha21( X, Y ), alpha24( X, Y ) }.
% 4.39/4.75 (40611) {G0,W5,D2,L2,V2,M2} { ! alpha21( X, Y ), v3_membered( Y ) }.
% 4.39/4.75 (40612) {G0,W8,D2,L3,V2,M3} { ! alpha24( X, Y ), ! v3_membered( Y ),
% 4.39/4.75 alpha21( X, Y ) }.
% 4.39/4.75 (40613) {G0,W6,D2,L2,V2,M2} { ! alpha24( X, Y ), alpha26( X, Y ) }.
% 4.39/4.75 (40614) {G0,W5,D2,L2,V2,M2} { ! alpha24( X, Y ), v2_membered( Y ) }.
% 4.39/4.75 (40615) {G0,W8,D2,L3,V2,M3} { ! alpha26( X, Y ), ! v2_membered( Y ),
% 4.39/4.75 alpha24( X, Y ) }.
% 4.39/4.75 (40616) {G0,W6,D2,L2,V2,M2} { ! alpha26( X, Y ), alpha28( X, Y ) }.
% 4.39/4.75 (40617) {G0,W5,D2,L2,V2,M2} { ! alpha26( X, Y ), v1_membered( Y ) }.
% 4.39/4.75 (40618) {G0,W8,D2,L3,V2,M3} { ! alpha28( X, Y ), ! v1_membered( Y ),
% 4.39/4.75 alpha26( X, Y ) }.
% 4.39/4.75 (40619) {G0,W6,D2,L2,V2,M2} { ! alpha28( X, Y ), alpha29( X, Y ) }.
% 4.39/4.75 (40620) {G0,W6,D2,L2,V2,M2} { ! alpha28( X, Y ), v4_pre_topc( Y, X ) }.
% 4.39/4.75 (40621) {G0,W9,D2,L3,V2,M3} { ! alpha29( X, Y ), ! v4_pre_topc( Y, X ),
% 4.39/4.75 alpha28( X, Y ) }.
% 4.39/4.75 (40622) {G0,W8,D4,L2,V2,M2} { ! alpha29( X, Y ), m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40623) {G0,W5,D2,L2,V2,M2} { ! alpha29( X, Y ), v1_xboole_0( Y ) }.
% 4.39/4.75 (40624) {G0,W6,D2,L2,V2,M2} { ! alpha29( X, Y ), v3_pre_topc( Y, X ) }.
% 4.39/4.75 (40625) {G0,W13,D4,L4,V2,M4} { ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0
% 4.39/4.75 ( X ) ) ), ! v1_xboole_0( Y ), ! v3_pre_topc( Y, X ), alpha29( X, Y ) }.
% 4.39/4.75 (40626) {G0,W10,D4,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 m1_subset_1( skol15( X ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.75 (40627) {G0,W8,D3,L3,V1,M3} { ! v2_pre_topc( X ), ! l1_pre_topc( X ),
% 4.39/4.75 v4_pre_topc( skol15( X ), X ) }.
% 4.39/4.75 (40628) {G0,W9,D3,L4,V2,M4} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), ! v1_xboole_0( skol16( Y ) ) }.
% 4.39/4.75 (40629) {G0,W12,D4,L4,V1,M4} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), m1_subset_1( skol16( X ), k1_zfmisc_1( u1_struct_0( X )
% 4.39/4.75 ) ) }.
% 4.39/4.75 (40630) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), v4_pre_topc( skol16( X ), X ) }.
% 4.39/4.75 (40631) {G0,W3,D2,L1,V1,M1} { r1_tarski( X, X ) }.
% 4.39/4.75 (40632) {G0,W7,D3,L2,V1,M2} { ! l1_struct_0( X ), k2_pre_topc( X ) =
% 4.39/4.75 u1_struct_0( X ) }.
% 4.39/4.75 (40633) {G0,W6,D2,L2,V2,M2} { ! r2_hidden( X, Y ), m1_subset_1( X, Y ) }.
% 4.39/4.75 (40634) {G0,W8,D2,L3,V2,M3} { ! m1_subset_1( X, Y ), v1_xboole_0( Y ),
% 4.39/4.75 r2_hidden( X, Y ) }.
% 4.39/4.75 (40635) {G0,W7,D3,L2,V2,M2} { ! m1_subset_1( X, k1_zfmisc_1( Y ) ),
% 4.39/4.75 r1_tarski( X, Y ) }.
% 4.39/4.75 (40636) {G0,W7,D3,L2,V2,M2} { ! r1_tarski( X, Y ), m1_subset_1( X,
% 4.39/4.75 k1_zfmisc_1( Y ) ) }.
% 4.39/4.75 (40637) {G0,W10,D3,L3,V3,M3} { ! r2_hidden( X, Z ), ! m1_subset_1( Z,
% 4.39/4.75 k1_zfmisc_1( Y ) ), m1_subset_1( X, Y ) }.
% 4.39/4.75 (40638) {G0,W15,D4,L4,V2,M4} { ! l1_pre_topc( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ), ! v4_pre_topc( Y, X ), k6_pre_topc( X
% 4.39/4.75 , Y ) = Y }.
% 4.39/4.75 (40639) {G0,W17,D4,L5,V2,M5} { ! l1_pre_topc( X ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( u1_struct_0( X ) ) ), ! v2_pre_topc( X ), ! k6_pre_topc( X,
% 4.39/4.75 Y ) = Y, v4_pre_topc( Y, X ) }.
% 4.39/4.75 (40640) {G0,W9,D3,L3,V3,M3} { ! r2_hidden( X, Y ), ! m1_subset_1( Y,
% 4.39/4.75 k1_zfmisc_1( Z ) ), ! v1_xboole_0( Z ) }.
% 4.39/4.75 (40641) {G0,W20,D4,L5,V2,M5} { v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.75 l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ),
% 4.39/4.75 k6_pre_topc( X, k3_tex_4( X, Y ) ) = k6_pre_topc( X, Y ) }.
% 4.39/4.75 (40642) {G0,W5,D2,L2,V1,M2} { ! v1_xboole_0( X ), X = k1_xboole_0 }.
% 4.39/4.75 (40643) {G0,W5,D2,L2,V2,M2} { ! r2_hidden( X, Y ), ! v1_xboole_0( Y ) }.
% 4.39/4.75 (40644) {G0,W7,D2,L3,V2,M3} { ! v1_xboole_0( X ), X = Y, ! v1_xboole_0( Y
% 4.39/4.75 ) }.
% 4.39/4.75
% 4.39/4.75
% 4.39/4.75 Total Proof:
% 4.39/4.75
% 4.39/4.75 subsumption: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 4.39/4.75 parent0: (40432) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol1 ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { v2_pre_topc( skol1 ) }.
% 4.39/4.75 parent0: (40433) {G0,W2,D2,L1,V0,M1} { v2_pre_topc( skol1 ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { l1_pre_topc( skol1 ) }.
% 4.39/4.75 parent0: (40434) {G0,W2,D2,L1,V0,M1} { l1_pre_topc( skol1 ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (3) {G0,W5,D4,L1,V0,M1} I { m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 parent0: (40435) {G0,W5,D4,L1,V0,M1} { m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (4) {G0,W3,D2,L1,V0,M1} I { v1_tsp_2( skol17, skol1 ) }.
% 4.39/4.75 parent0: (40436) {G0,W3,D2,L1,V0,M1} { v1_tsp_2( skol17, skol1 ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (5) {G0,W3,D2,L1,V0,M1} I { ! v1_tops_1( skol17, skol1 ) }.
% 4.39/4.75 parent0: (40437) {G0,W3,D2,L1,V0,M1} { ! v1_tops_1( skol17, skol1 ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (91) {G0,W16,D4,L4,V2,M4} I { ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tops_1( Y, X ),
% 4.39/4.75 k6_pre_topc( X, Y ) ==> u1_struct_0( X ) }.
% 4.39/4.75 parent0: (40525) {G0,W16,D4,L4,V2,M4} { ! l1_pre_topc( X ), ! m1_subset_1
% 4.39/4.75 ( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tops_1( Y, X ), k6_pre_topc
% 4.39/4.75 ( X, Y ) = u1_struct_0( X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := Y
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 1 ==> 1
% 4.39/4.75 2 ==> 2
% 4.39/4.75 3 ==> 3
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (92) {G0,W16,D4,L4,V2,M4} I { ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! k6_pre_topc( X, Y )
% 4.39/4.75 ==> u1_struct_0( X ), v1_tops_1( Y, X ) }.
% 4.39/4.75 parent0: (40526) {G0,W16,D4,L4,V2,M4} { ! l1_pre_topc( X ), ! m1_subset_1
% 4.39/4.75 ( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! k6_pre_topc( X, Y ) =
% 4.39/4.75 u1_struct_0( X ), v1_tops_1( Y, X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := Y
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 1 ==> 1
% 4.39/4.75 2 ==> 2
% 4.39/4.75 3 ==> 3
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (94) {G0,W20,D4,L6,V2,M6} I { v3_struct_0( X ), ! v2_pre_topc
% 4.39/4.75 ( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X
% 4.39/4.75 ) ) ), ! v1_tsp_2( Y, X ), k3_tex_4( X, Y ) ==> u1_struct_0( X ) }.
% 4.39/4.75 parent0: (40528) {G0,W20,D4,L6,V2,M6} { v3_struct_0( X ), ! v2_pre_topc( X
% 4.39/4.75 ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) )
% 4.39/4.75 ), ! v1_tsp_2( Y, X ), k3_tex_4( X, Y ) = u1_struct_0( X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := Y
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 1 ==> 1
% 4.39/4.75 2 ==> 2
% 4.39/4.75 3 ==> 3
% 4.39/4.75 4 ==> 4
% 4.39/4.75 5 ==> 5
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (100) {G0,W4,D2,L2,V1,M2} I { ! l1_pre_topc( X ), l1_struct_0
% 4.39/4.75 ( X ) }.
% 4.39/4.75 parent0: (40535) {G0,W4,D2,L2,V1,M2} { ! l1_pre_topc( X ), l1_struct_0( X
% 4.39/4.75 ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 1 ==> 1
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (116) {G0,W6,D3,L2,V1,M2} I { ! l1_pre_topc( X ), v1_tops_1(
% 4.39/4.75 k2_pre_topc( X ), X ) }.
% 4.39/4.75 parent0: (40555) {G0,W6,D3,L2,V1,M2} { ! l1_pre_topc( X ), v1_tops_1(
% 4.39/4.75 k2_pre_topc( X ), X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 1 ==> 1
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (192) {G0,W3,D2,L1,V1,M1} I { r1_tarski( X, X ) }.
% 4.39/4.75 parent0: (40631) {G0,W3,D2,L1,V1,M1} { r1_tarski( X, X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (193) {G0,W7,D3,L2,V1,M2} I { ! l1_struct_0( X ), k2_pre_topc
% 4.39/4.75 ( X ) ==> u1_struct_0( X ) }.
% 4.39/4.75 parent0: (40632) {G0,W7,D3,L2,V1,M2} { ! l1_struct_0( X ), k2_pre_topc( X
% 4.39/4.75 ) = u1_struct_0( X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 1 ==> 1
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (197) {G0,W7,D3,L2,V2,M2} I { ! r1_tarski( X, Y ), m1_subset_1
% 4.39/4.75 ( X, k1_zfmisc_1( Y ) ) }.
% 4.39/4.75 parent0: (40636) {G0,W7,D3,L2,V2,M2} { ! r1_tarski( X, Y ), m1_subset_1( X
% 4.39/4.75 , k1_zfmisc_1( Y ) ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := Y
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 1 ==> 1
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (202) {G0,W20,D4,L5,V2,M5} I { v3_struct_0( X ), ! v2_pre_topc
% 4.39/4.75 ( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X
% 4.39/4.75 ) ) ), k6_pre_topc( X, k3_tex_4( X, Y ) ) ==> k6_pre_topc( X, Y ) }.
% 4.39/4.75 parent0: (40641) {G0,W20,D4,L5,V2,M5} { v3_struct_0( X ), ! v2_pre_topc( X
% 4.39/4.75 ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) )
% 4.39/4.75 ), k6_pre_topc( X, k3_tex_4( X, Y ) ) = k6_pre_topc( X, Y ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := Y
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 1 ==> 1
% 4.39/4.75 2 ==> 2
% 4.39/4.75 3 ==> 3
% 4.39/4.75 4 ==> 4
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 eqswap: (40690) {G0,W16,D4,L4,V2,M4} { ! u1_struct_0( X ) ==> k6_pre_topc
% 4.39/4.75 ( X, Y ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0
% 4.39/4.75 ( X ) ) ), v1_tops_1( Y, X ) }.
% 4.39/4.75 parent0[2]: (92) {G0,W16,D4,L4,V2,M4} I { ! l1_pre_topc( X ), ! m1_subset_1
% 4.39/4.75 ( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! k6_pre_topc( X, Y ) ==>
% 4.39/4.75 u1_struct_0( X ), v1_tops_1( Y, X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := Y
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 resolution: (40691) {G1,W13,D4,L3,V0,M3} { ! u1_struct_0( skol1 ) ==>
% 4.39/4.75 k6_pre_topc( skol1, skol17 ), ! l1_pre_topc( skol1 ), ! m1_subset_1(
% 4.39/4.75 skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 parent0[0]: (5) {G0,W3,D2,L1,V0,M1} I { ! v1_tops_1( skol17, skol1 ) }.
% 4.39/4.75 parent1[3]: (40690) {G0,W16,D4,L4,V2,M4} { ! u1_struct_0( X ) ==>
% 4.39/4.75 k6_pre_topc( X, Y ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( X ) ) ), v1_tops_1( Y, X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 substitution1:
% 4.39/4.75 X := skol1
% 4.39/4.75 Y := skol17
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 resolution: (40692) {G1,W11,D4,L2,V0,M2} { ! u1_struct_0( skol1 ) ==>
% 4.39/4.75 k6_pre_topc( skol1, skol17 ), ! m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 parent0[1]: (40691) {G1,W13,D4,L3,V0,M3} { ! u1_struct_0( skol1 ) ==>
% 4.39/4.75 k6_pre_topc( skol1, skol17 ), ! l1_pre_topc( skol1 ), ! m1_subset_1(
% 4.39/4.75 skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l1_pre_topc( skol1 ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 substitution1:
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 eqswap: (40693) {G1,W11,D4,L2,V0,M2} { ! k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.75 u1_struct_0( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0(
% 4.39/4.75 skol1 ) ) ) }.
% 4.39/4.75 parent0[0]: (40692) {G1,W11,D4,L2,V0,M2} { ! u1_struct_0( skol1 ) ==>
% 4.39/4.75 k6_pre_topc( skol1, skol17 ), ! m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (1026) {G1,W11,D4,L2,V0,M2} R(92,5);r(2) { ! m1_subset_1(
% 4.39/4.75 skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! k6_pre_topc( skol1,
% 4.39/4.75 skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.75 parent0: (40693) {G1,W11,D4,L2,V0,M2} { ! k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.75 u1_struct_0( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0(
% 4.39/4.75 skol1 ) ) ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 1
% 4.39/4.75 1 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 eqswap: (40694) {G0,W20,D4,L6,V2,M6} { u1_struct_0( X ) ==> k3_tex_4( X, Y
% 4.39/4.75 ), v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tsp_2( Y, X ) }.
% 4.39/4.75 parent0[5]: (94) {G0,W20,D4,L6,V2,M6} I { v3_struct_0( X ), ! v2_pre_topc(
% 4.39/4.75 X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X )
% 4.39/4.75 ) ), ! v1_tsp_2( Y, X ), k3_tex_4( X, Y ) ==> u1_struct_0( X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := Y
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 resolution: (40695) {G1,W17,D4,L5,V0,M5} { u1_struct_0( skol1 ) ==>
% 4.39/4.75 k3_tex_4( skol1, skol17 ), v3_struct_0( skol1 ), ! v2_pre_topc( skol1 ),
% 4.39/4.75 ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0(
% 4.39/4.75 skol1 ) ) ) }.
% 4.39/4.75 parent0[5]: (40694) {G0,W20,D4,L6,V2,M6} { u1_struct_0( X ) ==> k3_tex_4(
% 4.39/4.75 X, Y ), v3_struct_0( X ), ! v2_pre_topc( X ), ! l1_pre_topc( X ), !
% 4.39/4.75 m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tsp_2( Y, X ) }.
% 4.39/4.75 parent1[0]: (4) {G0,W3,D2,L1,V0,M1} I { v1_tsp_2( skol17, skol1 ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := skol1
% 4.39/4.75 Y := skol17
% 4.39/4.75 end
% 4.39/4.75 substitution1:
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 resolution: (40696) {G1,W15,D4,L4,V0,M4} { u1_struct_0( skol1 ) ==>
% 4.39/4.75 k3_tex_4( skol1, skol17 ), ! v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 )
% 4.39/4.75 , ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 4.39/4.75 parent1[1]: (40695) {G1,W17,D4,L5,V0,M5} { u1_struct_0( skol1 ) ==>
% 4.39/4.75 k3_tex_4( skol1, skol17 ), v3_struct_0( skol1 ), ! v2_pre_topc( skol1 ),
% 4.39/4.75 ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0(
% 4.39/4.75 skol1 ) ) ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 substitution1:
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 eqswap: (40697) {G1,W15,D4,L4,V0,M4} { k3_tex_4( skol1, skol17 ) ==>
% 4.39/4.75 u1_struct_0( skol1 ), ! v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 ), !
% 4.39/4.75 m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 parent0[0]: (40696) {G1,W15,D4,L4,V0,M4} { u1_struct_0( skol1 ) ==>
% 4.39/4.75 k3_tex_4( skol1, skol17 ), ! v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 )
% 4.39/4.75 , ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (1046) {G1,W15,D4,L4,V0,M4} R(94,4);r(0) { ! v2_pre_topc(
% 4.39/4.75 skol1 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( skol1 ) ) ), k3_tex_4( skol1, skol17 ) ==> u1_struct_0(
% 4.39/4.75 skol1 ) }.
% 4.39/4.75 parent0: (40697) {G1,W15,D4,L4,V0,M4} { k3_tex_4( skol1, skol17 ) ==>
% 4.39/4.75 u1_struct_0( skol1 ), ! v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 ), !
% 4.39/4.75 m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 3
% 4.39/4.75 1 ==> 0
% 4.39/4.75 2 ==> 1
% 4.39/4.75 3 ==> 2
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 paramod: (40699) {G1,W8,D3,L3,V1,M3} { v1_tops_1( u1_struct_0( X ), X ), !
% 4.39/4.75 l1_struct_0( X ), ! l1_pre_topc( X ) }.
% 4.39/4.75 parent0[1]: (193) {G0,W7,D3,L2,V1,M2} I { ! l1_struct_0( X ), k2_pre_topc(
% 4.39/4.75 X ) ==> u1_struct_0( X ) }.
% 4.39/4.75 parent1[1; 1]: (116) {G0,W6,D3,L2,V1,M2} I { ! l1_pre_topc( X ), v1_tops_1
% 4.39/4.75 ( k2_pre_topc( X ), X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75 substitution1:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 resolution: (40700) {G1,W8,D3,L3,V1,M3} { v1_tops_1( u1_struct_0( X ), X )
% 4.39/4.75 , ! l1_pre_topc( X ), ! l1_pre_topc( X ) }.
% 4.39/4.75 parent0[1]: (40699) {G1,W8,D3,L3,V1,M3} { v1_tops_1( u1_struct_0( X ), X )
% 4.39/4.75 , ! l1_struct_0( X ), ! l1_pre_topc( X ) }.
% 4.39/4.75 parent1[1]: (100) {G0,W4,D2,L2,V1,M2} I { ! l1_pre_topc( X ), l1_struct_0(
% 4.39/4.75 X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75 substitution1:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 factor: (40701) {G1,W6,D3,L2,V1,M2} { v1_tops_1( u1_struct_0( X ), X ), !
% 4.39/4.75 l1_pre_topc( X ) }.
% 4.39/4.75 parent0[1, 2]: (40700) {G1,W8,D3,L3,V1,M3} { v1_tops_1( u1_struct_0( X ),
% 4.39/4.75 X ), ! l1_pre_topc( X ), ! l1_pre_topc( X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (2578) {G1,W6,D3,L2,V1,M2} P(193,116);r(100) { ! l1_pre_topc(
% 4.39/4.75 X ), v1_tops_1( u1_struct_0( X ), X ) }.
% 4.39/4.75 parent0: (40701) {G1,W6,D3,L2,V1,M2} { v1_tops_1( u1_struct_0( X ), X ), !
% 4.39/4.75 l1_pre_topc( X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 1
% 4.39/4.75 1 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 resolution: (40702) {G1,W4,D3,L1,V1,M1} { m1_subset_1( X, k1_zfmisc_1( X )
% 4.39/4.75 ) }.
% 4.39/4.75 parent0[0]: (197) {G0,W7,D3,L2,V2,M2} I { ! r1_tarski( X, Y ), m1_subset_1
% 4.39/4.75 ( X, k1_zfmisc_1( Y ) ) }.
% 4.39/4.75 parent1[0]: (192) {G0,W3,D2,L1,V1,M1} I { r1_tarski( X, X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := X
% 4.39/4.75 end
% 4.39/4.75 substitution1:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 subsumption: (2759) {G1,W4,D3,L1,V1,M1} R(197,192) { m1_subset_1( X,
% 4.39/4.75 k1_zfmisc_1( X ) ) }.
% 4.39/4.75 parent0: (40702) {G1,W4,D3,L1,V1,M1} { m1_subset_1( X, k1_zfmisc_1( X ) )
% 4.39/4.75 }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 end
% 4.39/4.75 permutation0:
% 4.39/4.75 0 ==> 0
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 eqswap: (40703) {G0,W16,D4,L4,V2,M4} { u1_struct_0( X ) ==> k6_pre_topc( X
% 4.39/4.75 , Y ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X
% 4.39/4.75 ) ) ), ! v1_tops_1( Y, X ) }.
% 4.39/4.75 parent0[3]: (91) {G0,W16,D4,L4,V2,M4} I { ! l1_pre_topc( X ), ! m1_subset_1
% 4.39/4.75 ( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v1_tops_1( Y, X ), k6_pre_topc
% 4.39/4.75 ( X, Y ) ==> u1_struct_0( X ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := Y
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 resolution: (40704) {G1,W13,D4,L3,V1,M3} { u1_struct_0( X ) ==>
% 4.39/4.75 k6_pre_topc( X, u1_struct_0( X ) ), ! l1_pre_topc( X ), ! v1_tops_1(
% 4.39/4.75 u1_struct_0( X ), X ) }.
% 4.39/4.75 parent0[2]: (40703) {G0,W16,D4,L4,V2,M4} { u1_struct_0( X ) ==>
% 4.39/4.75 k6_pre_topc( X, Y ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1(
% 4.39/4.75 u1_struct_0( X ) ) ), ! v1_tops_1( Y, X ) }.
% 4.39/4.75 parent1[0]: (2759) {G1,W4,D3,L1,V1,M1} R(197,192) { m1_subset_1( X,
% 4.39/4.75 k1_zfmisc_1( X ) ) }.
% 4.39/4.75 substitution0:
% 4.39/4.75 X := X
% 4.39/4.75 Y := u1_struct_0( X )
% 4.39/4.75 end
% 4.39/4.75 substitution1:
% 4.39/4.75 X := u1_struct_0( X )
% 4.39/4.75 end
% 4.39/4.75
% 4.39/4.75 resolution: (40705) {G2,W11,D4,L3,V1,M3} { u1_struct_0( X ) ==>
% 4.39/4.75 k6_pre_topc( X, u1_struct_0( X ) ), ! l1_pre_topc( X ), ! l1_pre_topc( X
% 4.39/4.75 ) }.
% 4.39/4.75 parent0[2]: (40704) {G1,W13,D4,L3,V1,M3} { u1_struct_0( X ) ==>
% 4.39/4.75 k6_pre_topc( X, u1_struct_0( X ) ), ! l1_pre_topc( X ), ! v1_tops_1(
% 4.39/4.75 u1_struct_0( X ), X ) }.
% 4.39/4.76 parent1[1]: (2578) {G1,W6,D3,L2,V1,M2} P(193,116);r(100) { ! l1_pre_topc( X
% 4.39/4.76 ), v1_tops_1( u1_struct_0( X ), X ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 X := X
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 X := X
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 eqswap: (40706) {G2,W11,D4,L3,V1,M3} { k6_pre_topc( X, u1_struct_0( X ) )
% 4.39/4.76 ==> u1_struct_0( X ), ! l1_pre_topc( X ), ! l1_pre_topc( X ) }.
% 4.39/4.76 parent0[0]: (40705) {G2,W11,D4,L3,V1,M3} { u1_struct_0( X ) ==>
% 4.39/4.76 k6_pre_topc( X, u1_struct_0( X ) ), ! l1_pre_topc( X ), ! l1_pre_topc( X
% 4.39/4.76 ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 X := X
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 factor: (40707) {G2,W9,D4,L2,V1,M2} { k6_pre_topc( X, u1_struct_0( X ) )
% 4.39/4.76 ==> u1_struct_0( X ), ! l1_pre_topc( X ) }.
% 4.39/4.76 parent0[1, 2]: (40706) {G2,W11,D4,L3,V1,M3} { k6_pre_topc( X, u1_struct_0
% 4.39/4.76 ( X ) ) ==> u1_struct_0( X ), ! l1_pre_topc( X ), ! l1_pre_topc( X ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 X := X
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 subsumption: (2766) {G2,W9,D4,L2,V1,M2} R(2759,91);r(2578) { ! l1_pre_topc
% 4.39/4.76 ( X ), k6_pre_topc( X, u1_struct_0( X ) ) ==> u1_struct_0( X ) }.
% 4.39/4.76 parent0: (40707) {G2,W9,D4,L2,V1,M2} { k6_pre_topc( X, u1_struct_0( X ) )
% 4.39/4.76 ==> u1_struct_0( X ), ! l1_pre_topc( X ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 X := X
% 4.39/4.76 end
% 4.39/4.76 permutation0:
% 4.39/4.76 0 ==> 1
% 4.39/4.76 1 ==> 0
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40710) {G1,W13,D4,L3,V0,M3} { ! l1_pre_topc( skol1 ), !
% 4.39/4.76 m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k3_tex_4(
% 4.39/4.76 skol1, skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0[0]: (1046) {G1,W15,D4,L4,V0,M4} R(94,4);r(0) { ! v2_pre_topc( skol1
% 4.39/4.76 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.76 u1_struct_0( skol1 ) ) ), k3_tex_4( skol1, skol17 ) ==> u1_struct_0(
% 4.39/4.76 skol1 ) }.
% 4.39/4.76 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v2_pre_topc( skol1 ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40711) {G1,W11,D4,L2,V0,M2} { ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k3_tex_4( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0[0]: (40710) {G1,W13,D4,L3,V0,M3} { ! l1_pre_topc( skol1 ), !
% 4.39/4.76 m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k3_tex_4(
% 4.39/4.76 skol1, skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l1_pre_topc( skol1 ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40712) {G1,W6,D3,L1,V0,M1} { k3_tex_4( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0[0]: (40711) {G1,W11,D4,L2,V0,M2} { ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k3_tex_4( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 parent1[0]: (3) {G0,W5,D4,L1,V0,M1} I { m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.76 u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 subsumption: (20372) {G2,W6,D3,L1,V0,M1} S(1046);r(1);r(2);r(3) { k3_tex_4
% 4.39/4.76 ( skol1, skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0: (40712) {G1,W6,D3,L1,V0,M1} { k3_tex_4( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 permutation0:
% 4.39/4.76 0 ==> 0
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40715) {G1,W6,D3,L1,V0,M1} { ! k6_pre_topc( skol1, skol17 )
% 4.39/4.76 ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0[0]: (1026) {G1,W11,D4,L2,V0,M2} R(92,5);r(2) { ! m1_subset_1(
% 4.39/4.76 skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! k6_pre_topc( skol1,
% 4.39/4.76 skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent1[0]: (3) {G0,W5,D4,L1,V0,M1} I { m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.76 u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 subsumption: (20376) {G2,W6,D3,L1,V0,M1} S(1026);r(3) { ! k6_pre_topc(
% 4.39/4.76 skol1, skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0: (40715) {G1,W6,D3,L1,V0,M1} { ! k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 permutation0:
% 4.39/4.76 0 ==> 0
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 eqswap: (40718) {G0,W20,D4,L5,V2,M5} { k6_pre_topc( X, Y ) ==> k6_pre_topc
% 4.39/4.76 ( X, k3_tex_4( X, Y ) ), v3_struct_0( X ), ! v2_pre_topc( X ), !
% 4.39/4.76 l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 4.39/4.76 parent0[4]: (202) {G0,W20,D4,L5,V2,M5} I { v3_struct_0( X ), ! v2_pre_topc
% 4.39/4.76 ( X ), ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X
% 4.39/4.76 ) ) ), k6_pre_topc( X, k3_tex_4( X, Y ) ) ==> k6_pre_topc( X, Y ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 X := X
% 4.39/4.76 Y := Y
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 paramod: (40720) {G1,W19,D4,L5,V0,M5} { k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 k6_pre_topc( skol1, u1_struct_0( skol1 ) ), v3_struct_0( skol1 ), !
% 4.39/4.76 v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 parent0[0]: (20372) {G2,W6,D3,L1,V0,M1} S(1046);r(1);r(2);r(3) { k3_tex_4(
% 4.39/4.76 skol1, skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent1[0; 6]: (40718) {G0,W20,D4,L5,V2,M5} { k6_pre_topc( X, Y ) ==>
% 4.39/4.76 k6_pre_topc( X, k3_tex_4( X, Y ) ), v3_struct_0( X ), ! v2_pre_topc( X )
% 4.39/4.76 , ! l1_pre_topc( X ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) )
% 4.39/4.76 }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 X := skol1
% 4.39/4.76 Y := skol17
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 paramod: (40721) {G2,W19,D4,L6,V0,M6} { k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ), ! l1_pre_topc( skol1 ), v3_struct_0( skol1 ), !
% 4.39/4.76 v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 parent0[1]: (2766) {G2,W9,D4,L2,V1,M2} R(2759,91);r(2578) { ! l1_pre_topc(
% 4.39/4.76 X ), k6_pre_topc( X, u1_struct_0( X ) ) ==> u1_struct_0( X ) }.
% 4.39/4.76 parent1[0; 4]: (40720) {G1,W19,D4,L5,V0,M5} { k6_pre_topc( skol1, skol17 )
% 4.39/4.76 ==> k6_pre_topc( skol1, u1_struct_0( skol1 ) ), v3_struct_0( skol1 ), !
% 4.39/4.76 v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 X := skol1
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 factor: (40722) {G2,W17,D4,L5,V0,M5} { k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ), ! l1_pre_topc( skol1 ), v3_struct_0( skol1 ), !
% 4.39/4.76 v2_pre_topc( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0(
% 4.39/4.76 skol1 ) ) ) }.
% 4.39/4.76 parent0[1, 4]: (40721) {G2,W19,D4,L6,V0,M6} { k6_pre_topc( skol1, skol17 )
% 4.39/4.76 ==> u1_struct_0( skol1 ), ! l1_pre_topc( skol1 ), v3_struct_0( skol1 ),
% 4.39/4.76 ! v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40723) {G1,W15,D4,L4,V0,M4} { k6_pre_topc( skol1, skol17 )
% 4.39/4.76 ==> u1_struct_0( skol1 ), ! l1_pre_topc( skol1 ), ! v2_pre_topc( skol1 )
% 4.39/4.76 , ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 4.39/4.76 parent1[2]: (40722) {G2,W17,D4,L5,V0,M5} { k6_pre_topc( skol1, skol17 )
% 4.39/4.76 ==> u1_struct_0( skol1 ), ! l1_pre_topc( skol1 ), v3_struct_0( skol1 ), !
% 4.39/4.76 v2_pre_topc( skol1 ), ! m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0(
% 4.39/4.76 skol1 ) ) ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 subsumption: (36572) {G3,W15,D4,L4,V0,M4} P(20372,202);d(2766);r(0) { !
% 4.39/4.76 v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0: (40723) {G1,W15,D4,L4,V0,M4} { k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ), ! l1_pre_topc( skol1 ), ! v2_pre_topc( skol1 ), !
% 4.39/4.76 m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 permutation0:
% 4.39/4.76 0 ==> 3
% 4.39/4.76 1 ==> 1
% 4.39/4.76 2 ==> 0
% 4.39/4.76 3 ==> 2
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40727) {G1,W13,D4,L3,V0,M3} { ! l1_pre_topc( skol1 ), !
% 4.39/4.76 m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k6_pre_topc(
% 4.39/4.76 skol1, skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0[0]: (36572) {G3,W15,D4,L4,V0,M4} P(20372,202);d(2766);r(0) { !
% 4.39/4.76 v2_pre_topc( skol1 ), ! l1_pre_topc( skol1 ), ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v2_pre_topc( skol1 ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40728) {G1,W11,D4,L2,V0,M2} { ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0[0]: (40727) {G1,W13,D4,L3,V0,M3} { ! l1_pre_topc( skol1 ), !
% 4.39/4.76 m1_subset_1( skol17, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k6_pre_topc(
% 4.39/4.76 skol1, skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l1_pre_topc( skol1 ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40729) {G1,W6,D3,L1,V0,M1} { k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 parent0[0]: (40728) {G1,W11,D4,L2,V0,M2} { ! m1_subset_1( skol17,
% 4.39/4.76 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 parent1[0]: (3) {G0,W5,D4,L1,V0,M1} I { m1_subset_1( skol17, k1_zfmisc_1(
% 4.39/4.76 u1_struct_0( skol1 ) ) ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 resolution: (40730) {G2,W0,D0,L0,V0,M0} { }.
% 4.39/4.76 parent0[0]: (20376) {G2,W6,D3,L1,V0,M1} S(1026);r(3) { ! k6_pre_topc( skol1
% 4.39/4.76 , skol17 ) ==> u1_struct_0( skol1 ) }.
% 4.39/4.76 parent1[0]: (40729) {G1,W6,D3,L1,V0,M1} { k6_pre_topc( skol1, skol17 ) ==>
% 4.39/4.76 u1_struct_0( skol1 ) }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 substitution1:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 subsumption: (40430) {G4,W0,D0,L0,V0,M0} S(36572);r(1);r(2);r(3);r(20376)
% 4.39/4.76 { }.
% 4.39/4.76 parent0: (40730) {G2,W0,D0,L0,V0,M0} { }.
% 4.39/4.76 substitution0:
% 4.39/4.76 end
% 4.39/4.76 permutation0:
% 4.39/4.76 end
% 4.39/4.76
% 4.39/4.76 Proof check complete!
% 4.39/4.76
% 4.39/4.76 Memory use:
% 4.39/4.76
% 4.39/4.76 space for terms: 458618
% 4.39/4.76 space for clauses: 1421916
% 4.39/4.76
% 4.39/4.76
% 4.39/4.76 clauses generated: 216397
% 4.39/4.76 clauses kept: 40431
% 4.39/4.76 clauses selected: 3242
% 4.39/4.76 clauses deleted: 1857
% 4.39/4.76 clauses inuse deleted: 150
% 4.39/4.76
% 4.39/4.76 subsentry: 411037
% 4.39/4.76 literals s-matched: 293416
% 4.39/4.76 literals matched: 270522
% 4.39/4.76 full subsumption: 15401
% 4.39/4.76
% 4.39/4.76 checksum: 1021566516
% 4.39/4.76
% 4.39/4.76
% 4.39/4.76 Bliksem ended
%------------------------------------------------------------------------------