%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SEU326+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n007.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 : Tue Jul 19 07:12:29 EDT 2022
% Result : Theorem 1.75s 2.15s
% Output : Refutation 1.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU326+1 : TPTP v8.1.0. Released v3.3.0.
% 0.04/0.14 % Command : bliksem %s
% 0.14/0.35 % Computer : n007.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % DateTime : Sun Jun 19 18:51:44 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.77/1.17 *** allocated 10000 integers for termspace/termends
% 0.77/1.17 *** allocated 10000 integers for clauses
% 0.77/1.17 *** allocated 10000 integers for justifications
% 0.77/1.17 Bliksem 1.12
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Automatic Strategy Selection
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Clauses:
% 0.77/1.17
% 0.77/1.17 { ! in( X, Y ), ! in( Y, X ) }.
% 0.77/1.17 { ! v1_membered( X ), ! element( Y, X ), v1_xcmplx_0( Y ) }.
% 0.77/1.17 { ! v2_membered( X ), ! element( Y, X ), v1_xcmplx_0( Y ) }.
% 0.77/1.17 { ! v2_membered( X ), ! element( Y, X ), v1_xreal_0( Y ) }.
% 0.77/1.17 { ! v3_membered( X ), ! element( Y, X ), v1_xcmplx_0( Y ) }.
% 0.77/1.17 { ! v3_membered( X ), ! element( Y, X ), v1_xreal_0( Y ) }.
% 0.77/1.17 { ! v3_membered( X ), ! element( Y, X ), v1_rat_1( Y ) }.
% 0.77/1.17 { ! v4_membered( X ), ! element( Y, X ), alpha1( Y ) }.
% 0.77/1.17 { ! v4_membered( X ), ! element( Y, X ), v1_rat_1( Y ) }.
% 0.77/1.17 { ! alpha1( X ), v1_xcmplx_0( X ) }.
% 0.77/1.17 { ! alpha1( X ), v1_xreal_0( X ) }.
% 0.77/1.17 { ! alpha1( X ), v1_int_1( X ) }.
% 0.77/1.17 { ! v1_xcmplx_0( X ), ! v1_xreal_0( X ), ! v1_int_1( X ), alpha1( X ) }.
% 0.77/1.17 { ! v5_membered( X ), ! element( Y, X ), alpha2( Y ) }.
% 0.77/1.17 { ! v5_membered( X ), ! element( Y, X ), v1_rat_1( Y ) }.
% 0.77/1.17 { ! alpha2( X ), alpha7( X ) }.
% 0.77/1.17 { ! alpha2( X ), v1_int_1( X ) }.
% 0.77/1.17 { ! alpha7( X ), ! v1_int_1( X ), alpha2( X ) }.
% 0.77/1.17 { ! alpha7( X ), v1_xcmplx_0( X ) }.
% 0.77/1.17 { ! alpha7( X ), natural( X ) }.
% 0.77/1.17 { ! alpha7( X ), v1_xreal_0( X ) }.
% 0.77/1.17 { ! v1_xcmplx_0( X ), ! natural( X ), ! v1_xreal_0( X ), alpha7( X ) }.
% 0.77/1.17 { ! empty( X ), alpha3( X ) }.
% 0.77/1.17 { ! empty( X ), v5_membered( X ) }.
% 0.77/1.17 { ! alpha3( X ), alpha8( X ) }.
% 0.77/1.17 { ! alpha3( X ), v4_membered( X ) }.
% 0.77/1.17 { ! alpha8( X ), ! v4_membered( X ), alpha3( X ) }.
% 0.77/1.17 { ! alpha8( X ), v1_membered( X ) }.
% 0.77/1.17 { ! alpha8( X ), v2_membered( X ) }.
% 0.77/1.17 { ! alpha8( X ), v3_membered( X ) }.
% 0.77/1.17 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha8( X ) }
% 0.77/1.17 .
% 0.77/1.17 { ! v1_membered( X ), ! element( Y, powerset( X ) ), v1_membered( Y ) }.
% 0.77/1.17 { ! v2_membered( X ), ! element( Y, powerset( X ) ), v1_membered( Y ) }.
% 0.77/1.17 { ! v2_membered( X ), ! element( Y, powerset( X ) ), v2_membered( Y ) }.
% 0.77/1.17 { ! v3_membered( X ), ! element( Y, powerset( X ) ), v1_membered( Y ) }.
% 0.77/1.17 { ! v3_membered( X ), ! element( Y, powerset( X ) ), v2_membered( Y ) }.
% 0.77/1.17 { ! v3_membered( X ), ! element( Y, powerset( X ) ), v3_membered( Y ) }.
% 0.77/1.17 { ! v4_membered( X ), ! element( Y, powerset( X ) ), alpha4( Y ) }.
% 0.77/1.17 { ! v4_membered( X ), ! element( Y, powerset( X ) ), v4_membered( Y ) }.
% 0.77/1.17 { ! alpha4( X ), v1_membered( X ) }.
% 0.77/1.17 { ! alpha4( X ), v2_membered( X ) }.
% 0.77/1.17 { ! alpha4( X ), v3_membered( X ) }.
% 0.77/1.17 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha4( X ) }
% 0.77/1.17 .
% 0.77/1.17 { ! v5_membered( X ), v4_membered( X ) }.
% 0.77/1.17 { ! v5_membered( X ), ! element( Y, powerset( X ) ), alpha5( Y ) }.
% 0.77/1.17 { ! v5_membered( X ), ! element( Y, powerset( X ) ), v5_membered( Y ) }.
% 0.77/1.17 { ! alpha5( X ), alpha9( X ) }.
% 0.77/1.17 { ! alpha5( X ), v4_membered( X ) }.
% 0.77/1.17 { ! alpha9( X ), ! v4_membered( X ), alpha5( X ) }.
% 0.77/1.17 { ! alpha9( X ), v1_membered( X ) }.
% 0.77/1.17 { ! alpha9( X ), v2_membered( X ) }.
% 0.77/1.17 { ! alpha9( X ), v3_membered( X ) }.
% 0.77/1.17 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha9( X ) }
% 0.77/1.17 .
% 0.77/1.17 { ! v4_membered( X ), v3_membered( X ) }.
% 0.77/1.17 { ! v3_membered( X ), v2_membered( X ) }.
% 0.77/1.17 { ! v2_membered( X ), v1_membered( X ) }.
% 0.77/1.17 { && }.
% 0.77/1.17 { && }.
% 0.77/1.17 { ! element( Y, powerset( powerset( X ) ) ), element(
% 0.77/1.17 complements_of_subsets( X, Y ), powerset( powerset( X ) ) ) }.
% 0.77/1.17 { && }.
% 0.77/1.17 { element( skol1( X ), X ) }.
% 0.77/1.17 { ! empty( powerset( X ) ) }.
% 0.77/1.17 { empty( empty_set ) }.
% 0.77/1.17 { v1_membered( empty_set ) }.
% 0.77/1.17 { v2_membered( empty_set ) }.
% 0.77/1.17 { v3_membered( empty_set ) }.
% 0.77/1.17 { v4_membered( empty_set ) }.
% 0.77/1.17 { v5_membered( empty_set ) }.
% 0.77/1.17 { ! element( Y, powerset( powerset( X ) ) ), complements_of_subsets( X,
% 0.77/1.17 complements_of_subsets( X, Y ) ) = Y }.
% 0.77/1.17 { ! empty( skol2 ) }.
% 0.77/1.17 { v1_membered( skol2 ) }.
% 0.77/1.17 { v2_membered( skol2 ) }.
% 0.77/1.17 { v3_membered( skol2 ) }.
% 0.77/1.17 { v4_membered( skol2 ) }.
% 0.77/1.17 { v5_membered( skol2 ) }.
% 0.77/1.17 { empty( X ), ! empty( skol3( Y ) ) }.
% 0.77/1.17 { empty( X ), element( skol3( X ), powerset( X ) ) }.
% 0.77/1.17 { empty( skol4( Y ) ) }.
% 0.77/1.17 { element( skol4( X ), powerset( X ) ) }.
% 0.77/1.17 { subset( X, X ) }.
% 0.77/1.17 { element( skol6, powerset( powerset( skol5 ) ) ) }.
% 0.77/1.17 { alpha6( skol5, skol6 ), ! complements_of_subsets( skol5, skol6 ) =
% 0.77/1.17 empty_set }.
% 0.77/1.17 { alpha6( skol5, skol6 ), skol6 = empty_set }.
% 0.77/1.17 { ! alpha6( X, Y ), ! Y = empty_set }.
% 1.75/2.15 { ! alpha6( X, Y ), complements_of_subsets( X, Y ) = empty_set }.
% 1.75/2.15 { Y = empty_set, ! complements_of_subsets( X, Y ) = empty_set, alpha6( X, Y
% 1.75/2.15 ) }.
% 1.75/2.15 { ! in( X, Y ), element( X, Y ) }.
% 1.75/2.15 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 1.75/2.15 { ! element( X, powerset( Y ) ), subset( X, Y ) }.
% 1.75/2.15 { ! subset( X, Y ), element( X, powerset( Y ) ) }.
% 1.75/2.15 { ! element( Y, powerset( powerset( X ) ) ), Y = empty_set, !
% 1.75/2.15 complements_of_subsets( X, Y ) = empty_set }.
% 1.75/2.15 { ! in( X, Z ), ! element( Z, powerset( Y ) ), element( X, Y ) }.
% 1.75/2.15 { ! in( X, Y ), ! element( Y, powerset( Z ) ), ! empty( Z ) }.
% 1.75/2.15 { ! empty( X ), X = empty_set }.
% 1.75/2.15 { ! in( X, Y ), ! empty( Y ) }.
% 1.75/2.15 { ! empty( X ), X = Y, ! empty( Y ) }.
% 1.75/2.15
% 1.75/2.15 percentage equality = 0.052885, percentage horn = 0.957447
% 1.75/2.15 This is a problem with some equality
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Options Used:
% 1.75/2.15
% 1.75/2.15 useres = 1
% 1.75/2.15 useparamod = 1
% 1.75/2.15 useeqrefl = 1
% 1.75/2.15 useeqfact = 1
% 1.75/2.15 usefactor = 1
% 1.75/2.15 usesimpsplitting = 0
% 1.75/2.15 usesimpdemod = 5
% 1.75/2.15 usesimpres = 3
% 1.75/2.15
% 1.75/2.15 resimpinuse = 1000
% 1.75/2.15 resimpclauses = 20000
% 1.75/2.15 substype = eqrewr
% 1.75/2.15 backwardsubs = 1
% 1.75/2.15 selectoldest = 5
% 1.75/2.15
% 1.75/2.15 litorderings [0] = split
% 1.75/2.15 litorderings [1] = extend the termordering, first sorting on arguments
% 1.75/2.15
% 1.75/2.15 termordering = kbo
% 1.75/2.15
% 1.75/2.15 litapriori = 0
% 1.75/2.15 termapriori = 1
% 1.75/2.15 litaposteriori = 0
% 1.75/2.15 termaposteriori = 0
% 1.75/2.15 demodaposteriori = 0
% 1.75/2.15 ordereqreflfact = 0
% 1.75/2.15
% 1.75/2.15 litselect = negord
% 1.75/2.15
% 1.75/2.15 maxweight = 15
% 1.75/2.15 maxdepth = 30000
% 1.75/2.15 maxlength = 115
% 1.75/2.15 maxnrvars = 195
% 1.75/2.15 excuselevel = 1
% 1.75/2.15 increasemaxweight = 1
% 1.75/2.15
% 1.75/2.15 maxselected = 10000000
% 1.75/2.15 maxnrclauses = 10000000
% 1.75/2.15
% 1.75/2.15 showgenerated = 0
% 1.75/2.15 showkept = 0
% 1.75/2.15 showselected = 0
% 1.75/2.15 showdeleted = 0
% 1.75/2.15 showresimp = 1
% 1.75/2.15 showstatus = 2000
% 1.75/2.15
% 1.75/2.15 prologoutput = 0
% 1.75/2.15 nrgoals = 5000000
% 1.75/2.15 totalproof = 1
% 1.75/2.15
% 1.75/2.15 Symbols occurring in the translation:
% 1.75/2.15
% 1.75/2.15 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.75/2.15 . [1, 2] (w:1, o:41, a:1, s:1, b:0),
% 1.75/2.15 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 1.75/2.15 ! [4, 1] (w:0, o:13, a:1, s:1, b:0),
% 1.75/2.15 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.75/2.15 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.75/2.15 in [37, 2] (w:1, o:65, a:1, s:1, b:0),
% 1.75/2.15 v1_membered [38, 1] (w:1, o:18, a:1, s:1, b:0),
% 1.75/2.15 element [39, 2] (w:1, o:66, a:1, s:1, b:0),
% 1.75/2.15 v1_xcmplx_0 [40, 1] (w:1, o:19, a:1, s:1, b:0),
% 1.75/2.15 v2_membered [41, 1] (w:1, o:23, a:1, s:1, b:0),
% 1.75/2.15 v1_xreal_0 [42, 1] (w:1, o:20, a:1, s:1, b:0),
% 1.75/2.15 v3_membered [43, 1] (w:1, o:24, a:1, s:1, b:0),
% 1.75/2.15 v1_rat_1 [44, 1] (w:1, o:21, a:1, s:1, b:0),
% 1.75/2.15 v4_membered [45, 1] (w:1, o:25, a:1, s:1, b:0),
% 1.75/2.15 v1_int_1 [46, 1] (w:1, o:22, a:1, s:1, b:0),
% 1.75/2.15 v5_membered [47, 1] (w:1, o:26, a:1, s:1, b:0),
% 1.75/2.15 natural [48, 1] (w:1, o:27, a:1, s:1, b:0),
% 1.75/2.15 empty [49, 1] (w:1, o:28, a:1, s:1, b:0),
% 1.75/2.15 powerset [50, 1] (w:1, o:29, a:1, s:1, b:0),
% 1.75/2.15 complements_of_subsets [51, 2] (w:1, o:67, a:1, s:1, b:0),
% 1.75/2.15 empty_set [52, 0] (w:1, o:8, a:1, s:1, b:0),
% 1.75/2.15 subset [53, 2] (w:1, o:68, a:1, s:1, b:0),
% 1.75/2.15 alpha1 [55, 1] (w:1, o:30, a:1, s:1, b:1),
% 1.75/2.15 alpha2 [56, 1] (w:1, o:31, a:1, s:1, b:1),
% 1.75/2.15 alpha3 [57, 1] (w:1, o:32, a:1, s:1, b:1),
% 1.75/2.15 alpha4 [58, 1] (w:1, o:33, a:1, s:1, b:1),
% 1.75/2.15 alpha5 [59, 1] (w:1, o:34, a:1, s:1, b:1),
% 1.75/2.15 alpha6 [60, 2] (w:1, o:69, a:1, s:1, b:1),
% 1.75/2.15 alpha7 [61, 1] (w:1, o:35, a:1, s:1, b:1),
% 1.75/2.15 alpha8 [62, 1] (w:1, o:36, a:1, s:1, b:1),
% 1.75/2.15 alpha9 [63, 1] (w:1, o:37, a:1, s:1, b:1),
% 1.75/2.15 skol1 [64, 1] (w:1, o:38, a:1, s:1, b:1),
% 1.75/2.15 skol2 [65, 0] (w:1, o:10, a:1, s:1, b:1),
% 1.75/2.15 skol3 [66, 1] (w:1, o:39, a:1, s:1, b:1),
% 1.75/2.15 skol4 [67, 1] (w:1, o:40, a:1, s:1, b:1),
% 1.75/2.15 skol5 [68, 0] (w:1, o:11, a:1, s:1, b:1),
% 1.75/2.15 skol6 [69, 0] (w:1, o:12, a:1, s:1, b:1).
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Starting Search:
% 1.75/2.15
% 1.75/2.15 *** allocated 15000 integers for clauses
% 1.75/2.15 *** allocated 22500 integers for clauses
% 1.75/2.15 *** allocated 33750 integers for clauses
% 1.75/2.15 *** allocated 50625 integers for clauses
% 1.75/2.15 *** allocated 15000 integers for termspace/termends
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15 *** allocated 75937 integers for clauses
% 1.75/2.15 *** allocated 22500 integers for termspace/termends
% 1.75/2.15 *** allocated 113905 integers for clauses
% 1.75/2.15
% 1.75/2.15 Intermediate Status:
% 1.75/2.15 Generated: 7144
% 1.75/2.15 Kept: 2002
% 1.75/2.15 Inuse: 466
% 1.75/2.15 Deleted: 67
% 1.75/2.15 Deletedinuse: 18
% 1.75/2.15
% 1.75/2.15 *** allocated 33750 integers for termspace/termends
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15 *** allocated 170857 integers for clauses
% 1.75/2.15 *** allocated 50625 integers for termspace/termends
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Intermediate Status:
% 1.75/2.15 Generated: 18843
% 1.75/2.15 Kept: 4011
% 1.75/2.15 Inuse: 779
% 1.75/2.15 Deleted: 85
% 1.75/2.15 Deletedinuse: 22
% 1.75/2.15
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15 *** allocated 256285 integers for clauses
% 1.75/2.15 *** allocated 75937 integers for termspace/termends
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Intermediate Status:
% 1.75/2.15 Generated: 29111
% 1.75/2.15 Kept: 6012
% 1.75/2.15 Inuse: 970
% 1.75/2.15 Deleted: 105
% 1.75/2.15 Deletedinuse: 22
% 1.75/2.15
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15 *** allocated 384427 integers for clauses
% 1.75/2.15 *** allocated 113905 integers for termspace/termends
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Intermediate Status:
% 1.75/2.15 Generated: 40562
% 1.75/2.15 Kept: 8138
% 1.75/2.15 Inuse: 1091
% 1.75/2.15 Deleted: 108
% 1.75/2.15 Deletedinuse: 23
% 1.75/2.15
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15 *** allocated 576640 integers for clauses
% 1.75/2.15 *** allocated 170857 integers for termspace/termends
% 1.75/2.15
% 1.75/2.15 Intermediate Status:
% 1.75/2.15 Generated: 48813
% 1.75/2.15 Kept: 10166
% 1.75/2.15 Inuse: 1176
% 1.75/2.15 Deleted: 113
% 1.75/2.15 Deletedinuse: 23
% 1.75/2.15
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15 Resimplifying inuse:
% 1.75/2.15 Done
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Bliksems!, er is een bewijs:
% 1.75/2.15 % SZS status Theorem
% 1.75/2.15 % SZS output start Refutation
% 1.75/2.15
% 1.75/2.15 (57) {G0,W12,D4,L2,V2,M2} I { ! element( Y, powerset( powerset( X ) ) ),
% 1.75/2.15 element( complements_of_subsets( X, Y ), powerset( powerset( X ) ) ) }.
% 1.75/2.15 (66) {G0,W12,D4,L2,V2,M2} I { ! element( Y, powerset( powerset( X ) ) ),
% 1.75/2.15 complements_of_subsets( X, complements_of_subsets( X, Y ) ) ==> Y }.
% 1.75/2.15 (75) {G0,W3,D3,L1,V1,M1} I { empty( skol4( Y ) ) }.
% 1.75/2.15 (76) {G0,W5,D3,L1,V1,M1} I { element( skol4( X ), powerset( X ) ) }.
% 1.75/2.15 (78) {G0,W5,D4,L1,V0,M1} I { element( skol6, powerset( powerset( skol5 ) )
% 1.75/2.15 ) }.
% 1.75/2.15 (79) {G0,W8,D3,L2,V0,M2} I { alpha6( skol5, skol6 ), !
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) ==> empty_set }.
% 1.75/2.15 (80) {G0,W6,D2,L2,V0,M2} I { alpha6( skol5, skol6 ), skol6 ==> empty_set
% 1.75/2.15 }.
% 1.75/2.15 (81) {G0,W6,D2,L2,V2,M2} I { ! alpha6( X, Y ), ! Y = empty_set }.
% 1.75/2.15 (82) {G0,W8,D3,L2,V2,M2} I { ! alpha6( X, Y ), complements_of_subsets( X, Y
% 1.75/2.15 ) ==> empty_set }.
% 1.75/2.15 (88) {G0,W13,D4,L3,V2,M3} I { ! element( Y, powerset( powerset( X ) ) ), Y
% 1.75/2.15 = empty_set, ! complements_of_subsets( X, Y ) ==> empty_set }.
% 1.75/2.15 (91) {G0,W5,D2,L2,V1,M2} I { ! empty( X ), X = empty_set }.
% 1.75/2.15 (95) {G1,W3,D2,L1,V1,M1} Q(81) { ! alpha6( X, empty_set ) }.
% 1.75/2.15 (322) {G1,W4,D3,L1,V1,M1} R(91,75) { skol4( X ) ==> empty_set }.
% 1.75/2.15 (337) {G2,W4,D3,L1,V1,M1} S(76);d(322) { element( empty_set, powerset( X )
% 1.75/2.15 ) }.
% 1.75/2.15 (404) {G3,W7,D4,L1,V1,M1} R(57,337) { element( complements_of_subsets( X,
% 1.75/2.15 empty_set ), powerset( powerset( X ) ) ) }.
% 1.75/2.15 (424) {G3,W7,D4,L1,V1,M1} R(66,337) { complements_of_subsets( X,
% 1.75/2.15 complements_of_subsets( X, empty_set ) ) ==> empty_set }.
% 1.75/2.15 (528) {G1,W8,D3,L2,V0,M2} S(79);d(80) { alpha6( skol5, skol6 ), !
% 1.75/2.15 complements_of_subsets( skol5, empty_set ) ==> empty_set }.
% 1.75/2.15 (538) {G1,W8,D3,L2,V0,M2} R(82,80) { complements_of_subsets( skol5, skol6 )
% 1.75/2.15 ==> empty_set, skol6 ==> empty_set }.
% 1.75/2.15 (769) {G2,W3,D2,L1,V0,M1} R(88,78);d(538);q { skol6 ==> empty_set }.
% 1.75/2.15 (5422) {G4,W5,D3,L1,V1,M1} R(404,88);d(424);q { complements_of_subsets( X,
% 1.75/2.15 empty_set ) ==> empty_set }.
% 1.75/2.15 (12081) {G5,W0,D0,L0,V0,M0} S(528);d(769);d(5422);q;r(95) { }.
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 % SZS output end Refutation
% 1.75/2.15 found a proof!
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Unprocessed initial clauses:
% 1.75/2.15
% 1.75/2.15 (12083) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 1.75/2.15 (12084) {G0,W7,D2,L3,V2,M3} { ! v1_membered( X ), ! element( Y, X ),
% 1.75/2.15 v1_xcmplx_0( Y ) }.
% 1.75/2.15 (12085) {G0,W7,D2,L3,V2,M3} { ! v2_membered( X ), ! element( Y, X ),
% 1.75/2.15 v1_xcmplx_0( Y ) }.
% 1.75/2.15 (12086) {G0,W7,D2,L3,V2,M3} { ! v2_membered( X ), ! element( Y, X ),
% 1.75/2.15 v1_xreal_0( Y ) }.
% 1.75/2.15 (12087) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! element( Y, X ),
% 1.75/2.15 v1_xcmplx_0( Y ) }.
% 1.75/2.15 (12088) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! element( Y, X ),
% 1.75/2.15 v1_xreal_0( Y ) }.
% 1.75/2.15 (12089) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! element( Y, X ),
% 1.75/2.15 v1_rat_1( Y ) }.
% 1.75/2.15 (12090) {G0,W7,D2,L3,V2,M3} { ! v4_membered( X ), ! element( Y, X ),
% 1.75/2.15 alpha1( Y ) }.
% 1.75/2.15 (12091) {G0,W7,D2,L3,V2,M3} { ! v4_membered( X ), ! element( Y, X ),
% 1.75/2.15 v1_rat_1( Y ) }.
% 1.75/2.15 (12092) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_xcmplx_0( X ) }.
% 1.75/2.15 (12093) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_xreal_0( X ) }.
% 1.75/2.15 (12094) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_int_1( X ) }.
% 1.75/2.15 (12095) {G0,W8,D2,L4,V1,M4} { ! v1_xcmplx_0( X ), ! v1_xreal_0( X ), !
% 1.75/2.15 v1_int_1( X ), alpha1( X ) }.
% 1.75/2.15 (12096) {G0,W7,D2,L3,V2,M3} { ! v5_membered( X ), ! element( Y, X ),
% 1.75/2.15 alpha2( Y ) }.
% 1.75/2.15 (12097) {G0,W7,D2,L3,V2,M3} { ! v5_membered( X ), ! element( Y, X ),
% 1.75/2.15 v1_rat_1( Y ) }.
% 1.75/2.15 (12098) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha7( X ) }.
% 1.75/2.15 (12099) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), v1_int_1( X ) }.
% 1.75/2.15 (12100) {G0,W6,D2,L3,V1,M3} { ! alpha7( X ), ! v1_int_1( X ), alpha2( X )
% 1.75/2.15 }.
% 1.75/2.15 (12101) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), v1_xcmplx_0( X ) }.
% 1.75/2.15 (12102) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), natural( X ) }.
% 1.75/2.15 (12103) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), v1_xreal_0( X ) }.
% 1.75/2.15 (12104) {G0,W8,D2,L4,V1,M4} { ! v1_xcmplx_0( X ), ! natural( X ), !
% 1.75/2.15 v1_xreal_0( X ), alpha7( X ) }.
% 1.75/2.15 (12105) {G0,W4,D2,L2,V1,M2} { ! empty( X ), alpha3( X ) }.
% 1.75/2.15 (12106) {G0,W4,D2,L2,V1,M2} { ! empty( X ), v5_membered( X ) }.
% 1.75/2.15 (12107) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha8( X ) }.
% 1.75/2.15 (12108) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), v4_membered( X ) }.
% 1.75/2.15 (12109) {G0,W6,D2,L3,V1,M3} { ! alpha8( X ), ! v4_membered( X ), alpha3( X
% 1.75/2.15 ) }.
% 1.75/2.15 (12110) {G0,W4,D2,L2,V1,M2} { ! alpha8( X ), v1_membered( X ) }.
% 1.75/2.15 (12111) {G0,W4,D2,L2,V1,M2} { ! alpha8( X ), v2_membered( X ) }.
% 1.75/2.15 (12112) {G0,W4,D2,L2,V1,M2} { ! alpha8( X ), v3_membered( X ) }.
% 1.75/2.15 (12113) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 1.75/2.15 v3_membered( X ), alpha8( X ) }.
% 1.75/2.15 (12114) {G0,W8,D3,L3,V2,M3} { ! v1_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), v1_membered( Y ) }.
% 1.75/2.15 (12115) {G0,W8,D3,L3,V2,M3} { ! v2_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), v1_membered( Y ) }.
% 1.75/2.15 (12116) {G0,W8,D3,L3,V2,M3} { ! v2_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), v2_membered( Y ) }.
% 1.75/2.15 (12117) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), v1_membered( Y ) }.
% 1.75/2.15 (12118) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), v2_membered( Y ) }.
% 1.75/2.15 (12119) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), v3_membered( Y ) }.
% 1.75/2.15 (12120) {G0,W8,D3,L3,V2,M3} { ! v4_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), alpha4( Y ) }.
% 1.75/2.15 (12121) {G0,W8,D3,L3,V2,M3} { ! v4_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), v4_membered( Y ) }.
% 1.75/2.15 (12122) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v1_membered( X ) }.
% 1.75/2.15 (12123) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v2_membered( X ) }.
% 1.75/2.15 (12124) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v3_membered( X ) }.
% 1.75/2.15 (12125) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 1.75/2.15 v3_membered( X ), alpha4( X ) }.
% 1.75/2.15 (12126) {G0,W4,D2,L2,V1,M2} { ! v5_membered( X ), v4_membered( X ) }.
% 1.75/2.15 (12127) {G0,W8,D3,L3,V2,M3} { ! v5_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), alpha5( Y ) }.
% 1.75/2.15 (12128) {G0,W8,D3,L3,V2,M3} { ! v5_membered( X ), ! element( Y, powerset(
% 1.75/2.15 X ) ), v5_membered( Y ) }.
% 1.75/2.15 (12129) {G0,W4,D2,L2,V1,M2} { ! alpha5( X ), alpha9( X ) }.
% 1.75/2.15 (12130) {G0,W4,D2,L2,V1,M2} { ! alpha5( X ), v4_membered( X ) }.
% 1.75/2.15 (12131) {G0,W6,D2,L3,V1,M3} { ! alpha9( X ), ! v4_membered( X ), alpha5( X
% 1.75/2.15 ) }.
% 1.75/2.15 (12132) {G0,W4,D2,L2,V1,M2} { ! alpha9( X ), v1_membered( X ) }.
% 1.75/2.15 (12133) {G0,W4,D2,L2,V1,M2} { ! alpha9( X ), v2_membered( X ) }.
% 1.75/2.15 (12134) {G0,W4,D2,L2,V1,M2} { ! alpha9( X ), v3_membered( X ) }.
% 1.75/2.15 (12135) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 1.75/2.15 v3_membered( X ), alpha9( X ) }.
% 1.75/2.15 (12136) {G0,W4,D2,L2,V1,M2} { ! v4_membered( X ), v3_membered( X ) }.
% 1.75/2.15 (12137) {G0,W4,D2,L2,V1,M2} { ! v3_membered( X ), v2_membered( X ) }.
% 1.75/2.15 (12138) {G0,W4,D2,L2,V1,M2} { ! v2_membered( X ), v1_membered( X ) }.
% 1.75/2.15 (12139) {G0,W1,D1,L1,V0,M1} { && }.
% 1.75/2.15 (12140) {G0,W1,D1,L1,V0,M1} { && }.
% 1.75/2.15 (12141) {G0,W12,D4,L2,V2,M2} { ! element( Y, powerset( powerset( X ) ) ),
% 1.75/2.15 element( complements_of_subsets( X, Y ), powerset( powerset( X ) ) ) }.
% 1.75/2.15 (12142) {G0,W1,D1,L1,V0,M1} { && }.
% 1.75/2.15 (12143) {G0,W4,D3,L1,V1,M1} { element( skol1( X ), X ) }.
% 1.75/2.15 (12144) {G0,W3,D3,L1,V1,M1} { ! empty( powerset( X ) ) }.
% 1.75/2.15 (12145) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 1.75/2.15 (12146) {G0,W2,D2,L1,V0,M1} { v1_membered( empty_set ) }.
% 1.75/2.15 (12147) {G0,W2,D2,L1,V0,M1} { v2_membered( empty_set ) }.
% 1.75/2.15 (12148) {G0,W2,D2,L1,V0,M1} { v3_membered( empty_set ) }.
% 1.75/2.15 (12149) {G0,W2,D2,L1,V0,M1} { v4_membered( empty_set ) }.
% 1.75/2.15 (12150) {G0,W2,D2,L1,V0,M1} { v5_membered( empty_set ) }.
% 1.75/2.15 (12151) {G0,W12,D4,L2,V2,M2} { ! element( Y, powerset( powerset( X ) ) ),
% 1.75/2.15 complements_of_subsets( X, complements_of_subsets( X, Y ) ) = Y }.
% 1.75/2.15 (12152) {G0,W2,D2,L1,V0,M1} { ! empty( skol2 ) }.
% 1.75/2.15 (12153) {G0,W2,D2,L1,V0,M1} { v1_membered( skol2 ) }.
% 1.75/2.15 (12154) {G0,W2,D2,L1,V0,M1} { v2_membered( skol2 ) }.
% 1.75/2.15 (12155) {G0,W2,D2,L1,V0,M1} { v3_membered( skol2 ) }.
% 1.75/2.15 (12156) {G0,W2,D2,L1,V0,M1} { v4_membered( skol2 ) }.
% 1.75/2.15 (12157) {G0,W2,D2,L1,V0,M1} { v5_membered( skol2 ) }.
% 1.75/2.15 (12158) {G0,W5,D3,L2,V2,M2} { empty( X ), ! empty( skol3( Y ) ) }.
% 1.75/2.15 (12159) {G0,W7,D3,L2,V1,M2} { empty( X ), element( skol3( X ), powerset( X
% 1.75/2.15 ) ) }.
% 1.75/2.15 (12160) {G0,W3,D3,L1,V1,M1} { empty( skol4( Y ) ) }.
% 1.75/2.15 (12161) {G0,W5,D3,L1,V1,M1} { element( skol4( X ), powerset( X ) ) }.
% 1.75/2.15 (12162) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 1.75/2.15 (12163) {G0,W5,D4,L1,V0,M1} { element( skol6, powerset( powerset( skol5 )
% 1.75/2.15 ) ) }.
% 1.75/2.15 (12164) {G0,W8,D3,L2,V0,M2} { alpha6( skol5, skol6 ), !
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) = empty_set }.
% 1.75/2.15 (12165) {G0,W6,D2,L2,V0,M2} { alpha6( skol5, skol6 ), skol6 = empty_set
% 1.75/2.15 }.
% 1.75/2.15 (12166) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), ! Y = empty_set }.
% 1.75/2.15 (12167) {G0,W8,D3,L2,V2,M2} { ! alpha6( X, Y ), complements_of_subsets( X
% 1.75/2.15 , Y ) = empty_set }.
% 1.75/2.15 (12168) {G0,W11,D3,L3,V2,M3} { Y = empty_set, ! complements_of_subsets( X
% 1.75/2.15 , Y ) = empty_set, alpha6( X, Y ) }.
% 1.75/2.15 (12169) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 1.75/2.15 (12170) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y )
% 1.75/2.15 }.
% 1.75/2.15 (12171) {G0,W7,D3,L2,V2,M2} { ! element( X, powerset( Y ) ), subset( X, Y
% 1.75/2.15 ) }.
% 1.75/2.15 (12172) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X, powerset( Y )
% 1.75/2.15 ) }.
% 1.75/2.15 (12173) {G0,W13,D4,L3,V2,M3} { ! element( Y, powerset( powerset( X ) ) ),
% 1.75/2.15 Y = empty_set, ! complements_of_subsets( X, Y ) = empty_set }.
% 1.75/2.15 (12174) {G0,W10,D3,L3,V3,M3} { ! in( X, Z ), ! element( Z, powerset( Y ) )
% 1.75/2.15 , element( X, Y ) }.
% 1.75/2.15 (12175) {G0,W9,D3,L3,V3,M3} { ! in( X, Y ), ! element( Y, powerset( Z ) )
% 1.75/2.15 , ! empty( Z ) }.
% 1.75/2.15 (12176) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 1.75/2.15 (12177) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 1.75/2.15 (12178) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Total Proof:
% 1.75/2.15
% 1.75/2.15 subsumption: (57) {G0,W12,D4,L2,V2,M2} I { ! element( Y, powerset( powerset
% 1.75/2.15 ( X ) ) ), element( complements_of_subsets( X, Y ), powerset( powerset( X
% 1.75/2.15 ) ) ) }.
% 1.75/2.15 parent0: (12141) {G0,W12,D4,L2,V2,M2} { ! element( Y, powerset( powerset(
% 1.75/2.15 X ) ) ), element( complements_of_subsets( X, Y ), powerset( powerset( X )
% 1.75/2.15 ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := Y
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (66) {G0,W12,D4,L2,V2,M2} I { ! element( Y, powerset( powerset
% 1.75/2.15 ( X ) ) ), complements_of_subsets( X, complements_of_subsets( X, Y ) )
% 1.75/2.15 ==> Y }.
% 1.75/2.15 parent0: (12151) {G0,W12,D4,L2,V2,M2} { ! element( Y, powerset( powerset(
% 1.75/2.15 X ) ) ), complements_of_subsets( X, complements_of_subsets( X, Y ) ) = Y
% 1.75/2.15 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := Y
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (75) {G0,W3,D3,L1,V1,M1} I { empty( skol4( Y ) ) }.
% 1.75/2.15 parent0: (12160) {G0,W3,D3,L1,V1,M1} { empty( skol4( Y ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := Z
% 1.75/2.15 Y := Y
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (76) {G0,W5,D3,L1,V1,M1} I { element( skol4( X ), powerset( X
% 1.75/2.15 ) ) }.
% 1.75/2.15 parent0: (12161) {G0,W5,D3,L1,V1,M1} { element( skol4( X ), powerset( X )
% 1.75/2.15 ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (78) {G0,W5,D4,L1,V0,M1} I { element( skol6, powerset(
% 1.75/2.15 powerset( skol5 ) ) ) }.
% 1.75/2.15 parent0: (12163) {G0,W5,D4,L1,V0,M1} { element( skol6, powerset( powerset
% 1.75/2.15 ( skol5 ) ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (79) {G0,W8,D3,L2,V0,M2} I { alpha6( skol5, skol6 ), !
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) ==> empty_set }.
% 1.75/2.15 parent0: (12164) {G0,W8,D3,L2,V0,M2} { alpha6( skol5, skol6 ), !
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) = empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (80) {G0,W6,D2,L2,V0,M2} I { alpha6( skol5, skol6 ), skol6 ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 parent0: (12165) {G0,W6,D2,L2,V0,M2} { alpha6( skol5, skol6 ), skol6 =
% 1.75/2.15 empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (81) {G0,W6,D2,L2,V2,M2} I { ! alpha6( X, Y ), ! Y = empty_set
% 1.75/2.15 }.
% 1.75/2.15 parent0: (12166) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), ! Y = empty_set
% 1.75/2.15 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := Y
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (82) {G0,W8,D3,L2,V2,M2} I { ! alpha6( X, Y ),
% 1.75/2.15 complements_of_subsets( X, Y ) ==> empty_set }.
% 1.75/2.15 parent0: (12167) {G0,W8,D3,L2,V2,M2} { ! alpha6( X, Y ),
% 1.75/2.15 complements_of_subsets( X, Y ) = empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := Y
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (88) {G0,W13,D4,L3,V2,M3} I { ! element( Y, powerset( powerset
% 1.75/2.15 ( X ) ) ), Y = empty_set, ! complements_of_subsets( X, Y ) ==> empty_set
% 1.75/2.15 }.
% 1.75/2.15 parent0: (12173) {G0,W13,D4,L3,V2,M3} { ! element( Y, powerset( powerset(
% 1.75/2.15 X ) ) ), Y = empty_set, ! complements_of_subsets( X, Y ) = empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := Y
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 2 ==> 2
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (91) {G0,W5,D2,L2,V1,M2} I { ! empty( X ), X = empty_set }.
% 1.75/2.15 parent0: (12176) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12231) {G0,W6,D2,L2,V2,M2} { ! empty_set = X, ! alpha6( Y, X )
% 1.75/2.15 }.
% 1.75/2.15 parent0[1]: (81) {G0,W6,D2,L2,V2,M2} I { ! alpha6( X, Y ), ! Y = empty_set
% 1.75/2.15 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := Y
% 1.75/2.15 Y := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqrefl: (12232) {G0,W3,D2,L1,V1,M1} { ! alpha6( X, empty_set ) }.
% 1.75/2.15 parent0[0]: (12231) {G0,W6,D2,L2,V2,M2} { ! empty_set = X, ! alpha6( Y, X
% 1.75/2.15 ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := empty_set
% 1.75/2.15 Y := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (95) {G1,W3,D2,L1,V1,M1} Q(81) { ! alpha6( X, empty_set ) }.
% 1.75/2.15 parent0: (12232) {G0,W3,D2,L1,V1,M1} { ! alpha6( X, empty_set ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12233) {G0,W5,D2,L2,V1,M2} { empty_set = X, ! empty( X ) }.
% 1.75/2.15 parent0[1]: (91) {G0,W5,D2,L2,V1,M2} I { ! empty( X ), X = empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 resolution: (12234) {G1,W4,D3,L1,V1,M1} { empty_set = skol4( X ) }.
% 1.75/2.15 parent0[1]: (12233) {G0,W5,D2,L2,V1,M2} { empty_set = X, ! empty( X ) }.
% 1.75/2.15 parent1[0]: (75) {G0,W3,D3,L1,V1,M1} I { empty( skol4( Y ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := skol4( X )
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 X := Y
% 1.75/2.15 Y := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12235) {G1,W4,D3,L1,V1,M1} { skol4( X ) = empty_set }.
% 1.75/2.15 parent0[0]: (12234) {G1,W4,D3,L1,V1,M1} { empty_set = skol4( X ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (322) {G1,W4,D3,L1,V1,M1} R(91,75) { skol4( X ) ==> empty_set
% 1.75/2.15 }.
% 1.75/2.15 parent0: (12235) {G1,W4,D3,L1,V1,M1} { skol4( X ) = empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 paramod: (12237) {G1,W4,D3,L1,V1,M1} { element( empty_set, powerset( X ) )
% 1.75/2.15 }.
% 1.75/2.15 parent0[0]: (322) {G1,W4,D3,L1,V1,M1} R(91,75) { skol4( X ) ==> empty_set
% 1.75/2.15 }.
% 1.75/2.15 parent1[0; 1]: (76) {G0,W5,D3,L1,V1,M1} I { element( skol4( X ), powerset(
% 1.75/2.15 X ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (337) {G2,W4,D3,L1,V1,M1} S(76);d(322) { element( empty_set,
% 1.75/2.15 powerset( X ) ) }.
% 1.75/2.15 parent0: (12237) {G1,W4,D3,L1,V1,M1} { element( empty_set, powerset( X ) )
% 1.75/2.15 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 resolution: (12238) {G1,W7,D4,L1,V1,M1} { element( complements_of_subsets
% 1.75/2.15 ( X, empty_set ), powerset( powerset( X ) ) ) }.
% 1.75/2.15 parent0[0]: (57) {G0,W12,D4,L2,V2,M2} I { ! element( Y, powerset( powerset
% 1.75/2.15 ( X ) ) ), element( complements_of_subsets( X, Y ), powerset( powerset( X
% 1.75/2.15 ) ) ) }.
% 1.75/2.15 parent1[0]: (337) {G2,W4,D3,L1,V1,M1} S(76);d(322) { element( empty_set,
% 1.75/2.15 powerset( X ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := empty_set
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 X := powerset( X )
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (404) {G3,W7,D4,L1,V1,M1} R(57,337) { element(
% 1.75/2.15 complements_of_subsets( X, empty_set ), powerset( powerset( X ) ) ) }.
% 1.75/2.15 parent0: (12238) {G1,W7,D4,L1,V1,M1} { element( complements_of_subsets( X
% 1.75/2.15 , empty_set ), powerset( powerset( X ) ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12239) {G0,W12,D4,L2,V2,M2} { Y ==> complements_of_subsets( X,
% 1.75/2.15 complements_of_subsets( X, Y ) ), ! element( Y, powerset( powerset( X ) )
% 1.75/2.15 ) }.
% 1.75/2.15 parent0[1]: (66) {G0,W12,D4,L2,V2,M2} I { ! element( Y, powerset( powerset
% 1.75/2.15 ( X ) ) ), complements_of_subsets( X, complements_of_subsets( X, Y ) )
% 1.75/2.15 ==> Y }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := Y
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 resolution: (12240) {G1,W7,D4,L1,V1,M1} { empty_set ==>
% 1.75/2.15 complements_of_subsets( X, complements_of_subsets( X, empty_set ) ) }.
% 1.75/2.15 parent0[1]: (12239) {G0,W12,D4,L2,V2,M2} { Y ==> complements_of_subsets( X
% 1.75/2.15 , complements_of_subsets( X, Y ) ), ! element( Y, powerset( powerset( X )
% 1.75/2.15 ) ) }.
% 1.75/2.15 parent1[0]: (337) {G2,W4,D3,L1,V1,M1} S(76);d(322) { element( empty_set,
% 1.75/2.15 powerset( X ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := empty_set
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 X := powerset( X )
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12241) {G1,W7,D4,L1,V1,M1} { complements_of_subsets( X,
% 1.75/2.15 complements_of_subsets( X, empty_set ) ) ==> empty_set }.
% 1.75/2.15 parent0[0]: (12240) {G1,W7,D4,L1,V1,M1} { empty_set ==>
% 1.75/2.15 complements_of_subsets( X, complements_of_subsets( X, empty_set ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (424) {G3,W7,D4,L1,V1,M1} R(66,337) { complements_of_subsets(
% 1.75/2.15 X, complements_of_subsets( X, empty_set ) ) ==> empty_set }.
% 1.75/2.15 parent0: (12241) {G1,W7,D4,L1,V1,M1} { complements_of_subsets( X,
% 1.75/2.15 complements_of_subsets( X, empty_set ) ) ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 paramod: (12245) {G1,W11,D3,L3,V0,M3} { ! complements_of_subsets( skol5,
% 1.75/2.15 empty_set ) ==> empty_set, alpha6( skol5, skol6 ), alpha6( skol5, skol6 )
% 1.75/2.15 }.
% 1.75/2.15 parent0[1]: (80) {G0,W6,D2,L2,V0,M2} I { alpha6( skol5, skol6 ), skol6 ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 parent1[1; 4]: (79) {G0,W8,D3,L2,V0,M2} I { alpha6( skol5, skol6 ), !
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 factor: (12269) {G1,W8,D3,L2,V0,M2} { ! complements_of_subsets( skol5,
% 1.75/2.15 empty_set ) ==> empty_set, alpha6( skol5, skol6 ) }.
% 1.75/2.15 parent0[1, 2]: (12245) {G1,W11,D3,L3,V0,M3} { ! complements_of_subsets(
% 1.75/2.15 skol5, empty_set ) ==> empty_set, alpha6( skol5, skol6 ), alpha6( skol5,
% 1.75/2.15 skol6 ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (528) {G1,W8,D3,L2,V0,M2} S(79);d(80) { alpha6( skol5, skol6 )
% 1.75/2.15 , ! complements_of_subsets( skol5, empty_set ) ==> empty_set }.
% 1.75/2.15 parent0: (12269) {G1,W8,D3,L2,V0,M2} { ! complements_of_subsets( skol5,
% 1.75/2.15 empty_set ) ==> empty_set, alpha6( skol5, skol6 ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 1
% 1.75/2.15 1 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12270) {G0,W8,D3,L2,V2,M2} { empty_set ==> complements_of_subsets
% 1.75/2.15 ( X, Y ), ! alpha6( X, Y ) }.
% 1.75/2.15 parent0[1]: (82) {G0,W8,D3,L2,V2,M2} I { ! alpha6( X, Y ),
% 1.75/2.15 complements_of_subsets( X, Y ) ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 Y := Y
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12271) {G0,W6,D2,L2,V0,M2} { empty_set ==> skol6, alpha6( skol5,
% 1.75/2.15 skol6 ) }.
% 1.75/2.15 parent0[1]: (80) {G0,W6,D2,L2,V0,M2} I { alpha6( skol5, skol6 ), skol6 ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 resolution: (12272) {G1,W8,D3,L2,V0,M2} { empty_set ==>
% 1.75/2.15 complements_of_subsets( skol5, skol6 ), empty_set ==> skol6 }.
% 1.75/2.15 parent0[1]: (12270) {G0,W8,D3,L2,V2,M2} { empty_set ==>
% 1.75/2.15 complements_of_subsets( X, Y ), ! alpha6( X, Y ) }.
% 1.75/2.15 parent1[1]: (12271) {G0,W6,D2,L2,V0,M2} { empty_set ==> skol6, alpha6(
% 1.75/2.15 skol5, skol6 ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := skol5
% 1.75/2.15 Y := skol6
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12274) {G1,W8,D3,L2,V0,M2} { skol6 ==> empty_set, empty_set ==>
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) }.
% 1.75/2.15 parent0[1]: (12272) {G1,W8,D3,L2,V0,M2} { empty_set ==>
% 1.75/2.15 complements_of_subsets( skol5, skol6 ), empty_set ==> skol6 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12275) {G1,W8,D3,L2,V0,M2} { complements_of_subsets( skol5, skol6
% 1.75/2.15 ) ==> empty_set, skol6 ==> empty_set }.
% 1.75/2.15 parent0[1]: (12274) {G1,W8,D3,L2,V0,M2} { skol6 ==> empty_set, empty_set
% 1.75/2.15 ==> complements_of_subsets( skol5, skol6 ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (538) {G1,W8,D3,L2,V0,M2} R(82,80) { complements_of_subsets(
% 1.75/2.15 skol5, skol6 ) ==> empty_set, skol6 ==> empty_set }.
% 1.75/2.15 parent0: (12275) {G1,W8,D3,L2,V0,M2} { complements_of_subsets( skol5,
% 1.75/2.15 skol6 ) ==> empty_set, skol6 ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 1 ==> 1
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12276) {G0,W13,D4,L3,V2,M3} { empty_set = X, ! element( X,
% 1.75/2.15 powerset( powerset( Y ) ) ), ! complements_of_subsets( Y, X ) ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 parent0[1]: (88) {G0,W13,D4,L3,V2,M3} I { ! element( Y, powerset( powerset
% 1.75/2.15 ( X ) ) ), Y = empty_set, ! complements_of_subsets( X, Y ) ==> empty_set
% 1.75/2.15 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := Y
% 1.75/2.15 Y := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12280) {G1,W8,D3,L2,V0,M2} { empty_set ==> skol6,
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) ==> empty_set }.
% 1.75/2.15 parent0[1]: (538) {G1,W8,D3,L2,V0,M2} R(82,80) { complements_of_subsets(
% 1.75/2.15 skol5, skol6 ) ==> empty_set, skol6 ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 resolution: (12282) {G1,W8,D3,L2,V0,M2} { empty_set = skol6, !
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) ==> empty_set }.
% 1.75/2.15 parent0[1]: (12276) {G0,W13,D4,L3,V2,M3} { empty_set = X, ! element( X,
% 1.75/2.15 powerset( powerset( Y ) ) ), ! complements_of_subsets( Y, X ) ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 parent1[0]: (78) {G0,W5,D4,L1,V0,M1} I { element( skol6, powerset( powerset
% 1.75/2.15 ( skol5 ) ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := skol6
% 1.75/2.15 Y := skol5
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 paramod: (12297) {G2,W9,D2,L3,V0,M3} { ! empty_set ==> empty_set,
% 1.75/2.15 empty_set ==> skol6, empty_set = skol6 }.
% 1.75/2.15 parent0[1]: (12280) {G1,W8,D3,L2,V0,M2} { empty_set ==> skol6,
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) ==> empty_set }.
% 1.75/2.15 parent1[1; 2]: (12282) {G1,W8,D3,L2,V0,M2} { empty_set = skol6, !
% 1.75/2.15 complements_of_subsets( skol5, skol6 ) ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 factor: (12298) {G2,W6,D2,L2,V0,M2} { ! empty_set ==> empty_set, empty_set
% 1.75/2.15 ==> skol6 }.
% 1.75/2.15 parent0[1, 2]: (12297) {G2,W9,D2,L3,V0,M3} { ! empty_set ==> empty_set,
% 1.75/2.15 empty_set ==> skol6, empty_set = skol6 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqrefl: (12299) {G0,W3,D2,L1,V0,M1} { empty_set ==> skol6 }.
% 1.75/2.15 parent0[0]: (12298) {G2,W6,D2,L2,V0,M2} { ! empty_set ==> empty_set,
% 1.75/2.15 empty_set ==> skol6 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12300) {G0,W3,D2,L1,V0,M1} { skol6 ==> empty_set }.
% 1.75/2.15 parent0[0]: (12299) {G0,W3,D2,L1,V0,M1} { empty_set ==> skol6 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (769) {G2,W3,D2,L1,V0,M1} R(88,78);d(538);q { skol6 ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 parent0: (12300) {G0,W3,D2,L1,V0,M1} { skol6 ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12301) {G0,W13,D4,L3,V2,M3} { empty_set = X, ! element( X,
% 1.75/2.15 powerset( powerset( Y ) ) ), ! complements_of_subsets( Y, X ) ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 parent0[1]: (88) {G0,W13,D4,L3,V2,M3} I { ! element( Y, powerset( powerset
% 1.75/2.15 ( X ) ) ), Y = empty_set, ! complements_of_subsets( X, Y ) ==> empty_set
% 1.75/2.15 }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := Y
% 1.75/2.15 Y := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 resolution: (12305) {G1,W12,D4,L2,V1,M2} { empty_set =
% 1.75/2.15 complements_of_subsets( X, empty_set ), ! complements_of_subsets( X,
% 1.75/2.15 complements_of_subsets( X, empty_set ) ) ==> empty_set }.
% 1.75/2.15 parent0[1]: (12301) {G0,W13,D4,L3,V2,M3} { empty_set = X, ! element( X,
% 1.75/2.15 powerset( powerset( Y ) ) ), ! complements_of_subsets( Y, X ) ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 parent1[0]: (404) {G3,W7,D4,L1,V1,M1} R(57,337) { element(
% 1.75/2.15 complements_of_subsets( X, empty_set ), powerset( powerset( X ) ) ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := complements_of_subsets( X, empty_set )
% 1.75/2.15 Y := X
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 paramod: (12306) {G2,W8,D3,L2,V1,M2} { ! empty_set ==> empty_set,
% 1.75/2.15 empty_set = complements_of_subsets( X, empty_set ) }.
% 1.75/2.15 parent0[0]: (424) {G3,W7,D4,L1,V1,M1} R(66,337) { complements_of_subsets( X
% 1.75/2.15 , complements_of_subsets( X, empty_set ) ) ==> empty_set }.
% 1.75/2.15 parent1[1; 2]: (12305) {G1,W12,D4,L2,V1,M2} { empty_set =
% 1.75/2.15 complements_of_subsets( X, empty_set ), ! complements_of_subsets( X,
% 1.75/2.15 complements_of_subsets( X, empty_set ) ) ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqrefl: (12307) {G0,W5,D3,L1,V1,M1} { empty_set = complements_of_subsets(
% 1.75/2.15 X, empty_set ) }.
% 1.75/2.15 parent0[0]: (12306) {G2,W8,D3,L2,V1,M2} { ! empty_set ==> empty_set,
% 1.75/2.15 empty_set = complements_of_subsets( X, empty_set ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqswap: (12308) {G0,W5,D3,L1,V1,M1} { complements_of_subsets( X, empty_set
% 1.75/2.15 ) = empty_set }.
% 1.75/2.15 parent0[0]: (12307) {G0,W5,D3,L1,V1,M1} { empty_set =
% 1.75/2.15 complements_of_subsets( X, empty_set ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (5422) {G4,W5,D3,L1,V1,M1} R(404,88);d(424);q {
% 1.75/2.15 complements_of_subsets( X, empty_set ) ==> empty_set }.
% 1.75/2.15 parent0: (12308) {G0,W5,D3,L1,V1,M1} { complements_of_subsets( X,
% 1.75/2.15 empty_set ) = empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := X
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 0 ==> 0
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 paramod: (12312) {G2,W8,D3,L2,V0,M2} { alpha6( skol5, empty_set ), !
% 1.75/2.15 complements_of_subsets( skol5, empty_set ) ==> empty_set }.
% 1.75/2.15 parent0[0]: (769) {G2,W3,D2,L1,V0,M1} R(88,78);d(538);q { skol6 ==>
% 1.75/2.15 empty_set }.
% 1.75/2.15 parent1[0; 2]: (528) {G1,W8,D3,L2,V0,M2} S(79);d(80) { alpha6( skol5, skol6
% 1.75/2.15 ), ! complements_of_subsets( skol5, empty_set ) ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 paramod: (12313) {G3,W6,D2,L2,V0,M2} { ! empty_set ==> empty_set, alpha6(
% 1.75/2.15 skol5, empty_set ) }.
% 1.75/2.15 parent0[0]: (5422) {G4,W5,D3,L1,V1,M1} R(404,88);d(424);q {
% 1.75/2.15 complements_of_subsets( X, empty_set ) ==> empty_set }.
% 1.75/2.15 parent1[1; 2]: (12312) {G2,W8,D3,L2,V0,M2} { alpha6( skol5, empty_set ), !
% 1.75/2.15 complements_of_subsets( skol5, empty_set ) ==> empty_set }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := skol5
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 eqrefl: (12314) {G0,W3,D2,L1,V0,M1} { alpha6( skol5, empty_set ) }.
% 1.75/2.15 parent0[0]: (12313) {G3,W6,D2,L2,V0,M2} { ! empty_set ==> empty_set,
% 1.75/2.15 alpha6( skol5, empty_set ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 resolution: (12315) {G1,W0,D0,L0,V0,M0} { }.
% 1.75/2.15 parent0[0]: (95) {G1,W3,D2,L1,V1,M1} Q(81) { ! alpha6( X, empty_set ) }.
% 1.75/2.15 parent1[0]: (12314) {G0,W3,D2,L1,V0,M1} { alpha6( skol5, empty_set ) }.
% 1.75/2.15 substitution0:
% 1.75/2.15 X := skol5
% 1.75/2.15 end
% 1.75/2.15 substitution1:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 subsumption: (12081) {G5,W0,D0,L0,V0,M0} S(528);d(769);d(5422);q;r(95) {
% 1.75/2.15 }.
% 1.75/2.15 parent0: (12315) {G1,W0,D0,L0,V0,M0} { }.
% 1.75/2.15 substitution0:
% 1.75/2.15 end
% 1.75/2.15 permutation0:
% 1.75/2.15 end
% 1.75/2.15
% 1.75/2.15 Proof check complete!
% 1.75/2.15
% 1.75/2.15 Memory use:
% 1.75/2.15
% 1.75/2.15 space for terms: 138526
% 1.75/2.15 space for clauses: 496548
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 clauses generated: 58385
% 1.75/2.15 clauses kept: 12082
% 1.75/2.15 clauses selected: 1251
% 1.75/2.15 clauses deleted: 180
% 1.75/2.15 clauses inuse deleted: 80
% 1.75/2.15
% 1.75/2.15 subsentry: 161026
% 1.75/2.15 literals s-matched: 114991
% 1.75/2.15 literals matched: 105643
% 1.75/2.15 full subsumption: 10467
% 1.75/2.15
% 1.75/2.15 checksum: -1131409401
% 1.75/2.15
% 1.75/2.15
% 1.75/2.15 Bliksem ended
%------------------------------------------------------------------------------