%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SEU308+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Tue Jul 19 07:12:20 EDT 2022
% Result : Theorem 19.72s 20.11s
% Output : Refutation 19.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SEU308+1 : TPTP v8.1.0. Released v3.3.0.
% 0.11/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n025.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % DateTime : Sun Jun 19 01:43:28 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.68/1.08 *** allocated 10000 integers for termspace/termends
% 0.68/1.08 *** allocated 10000 integers for clauses
% 0.68/1.08 *** allocated 10000 integers for justifications
% 0.68/1.08 Bliksem 1.12
% 0.68/1.08
% 0.68/1.08
% 0.68/1.08 Automatic Strategy Selection
% 0.68/1.08
% 0.68/1.08
% 0.68/1.08 Clauses:
% 0.68/1.08
% 0.68/1.08 { ! in( X, Y ), ! in( Y, X ) }.
% 0.68/1.08 { && }.
% 0.68/1.08 { ! v5_membered( X ), v4_membered( X ) }.
% 0.68/1.08 { ! v4_membered( X ), v3_membered( X ) }.
% 0.68/1.08 { ! v3_membered( X ), v2_membered( X ) }.
% 0.68/1.08 { ! v2_membered( X ), v1_membered( X ) }.
% 0.68/1.08 { ! empty( skol1 ) }.
% 0.68/1.08 { v1_membered( skol1 ) }.
% 0.68/1.08 { v2_membered( skol1 ) }.
% 0.68/1.08 { v3_membered( skol1 ) }.
% 0.68/1.08 { v4_membered( skol1 ) }.
% 0.68/1.08 { v5_membered( skol1 ) }.
% 0.68/1.08 { ! v1_membered( X ), ! element( Y, X ), v1_xcmplx_0( Y ) }.
% 0.68/1.08 { ! v2_membered( X ), ! element( Y, X ), v1_xcmplx_0( Y ) }.
% 0.68/1.08 { ! v2_membered( X ), ! element( Y, X ), v1_xreal_0( Y ) }.
% 0.68/1.08 { ! v3_membered( X ), ! element( Y, X ), v1_xcmplx_0( Y ) }.
% 0.68/1.08 { ! v3_membered( X ), ! element( Y, X ), v1_xreal_0( Y ) }.
% 0.68/1.08 { ! v3_membered( X ), ! element( Y, X ), v1_rat_1( Y ) }.
% 0.68/1.08 { ! v4_membered( X ), ! element( Y, X ), alpha1( Y ) }.
% 0.68/1.08 { ! v4_membered( X ), ! element( Y, X ), v1_rat_1( Y ) }.
% 0.68/1.08 { ! alpha1( X ), v1_xcmplx_0( X ) }.
% 0.68/1.08 { ! alpha1( X ), v1_xreal_0( X ) }.
% 0.68/1.08 { ! alpha1( X ), v1_int_1( X ) }.
% 0.68/1.08 { ! v1_xcmplx_0( X ), ! v1_xreal_0( X ), ! v1_int_1( X ), alpha1( X ) }.
% 0.68/1.08 { ! v5_membered( X ), ! element( Y, X ), alpha2( Y ) }.
% 0.68/1.08 { ! v5_membered( X ), ! element( Y, X ), v1_rat_1( Y ) }.
% 0.68/1.08 { ! alpha2( X ), alpha8( X ) }.
% 0.68/1.08 { ! alpha2( X ), v1_int_1( X ) }.
% 0.68/1.08 { ! alpha8( X ), ! v1_int_1( X ), alpha2( X ) }.
% 0.68/1.08 { ! alpha8( X ), v1_xcmplx_0( X ) }.
% 0.68/1.08 { ! alpha8( X ), natural( X ) }.
% 0.68/1.08 { ! alpha8( X ), v1_xreal_0( X ) }.
% 0.68/1.08 { ! v1_xcmplx_0( X ), ! natural( X ), ! v1_xreal_0( X ), alpha8( X ) }.
% 0.68/1.08 { empty( empty_set ) }.
% 0.68/1.08 { v1_membered( empty_set ) }.
% 0.68/1.08 { v2_membered( empty_set ) }.
% 0.68/1.08 { v3_membered( empty_set ) }.
% 0.68/1.08 { v4_membered( empty_set ) }.
% 0.68/1.08 { v5_membered( empty_set ) }.
% 0.68/1.08 { ! v1_membered( X ), ! element( Y, powerset( X ) ), v1_membered( Y ) }.
% 0.68/1.08 { ! v2_membered( X ), ! element( Y, powerset( X ) ), v1_membered( Y ) }.
% 0.68/1.08 { ! v2_membered( X ), ! element( Y, powerset( X ) ), v2_membered( Y ) }.
% 0.68/1.08 { ! v3_membered( X ), ! element( Y, powerset( X ) ), v1_membered( Y ) }.
% 0.68/1.08 { ! v3_membered( X ), ! element( Y, powerset( X ) ), v2_membered( Y ) }.
% 0.68/1.08 { ! v3_membered( X ), ! element( Y, powerset( X ) ), v3_membered( Y ) }.
% 0.68/1.08 { ! v4_membered( X ), ! element( Y, powerset( X ) ), alpha3( Y ) }.
% 0.68/1.08 { ! v4_membered( X ), ! element( Y, powerset( X ) ), v4_membered( Y ) }.
% 0.68/1.08 { ! alpha3( X ), v1_membered( X ) }.
% 0.68/1.08 { ! alpha3( X ), v2_membered( X ) }.
% 0.68/1.08 { ! alpha3( X ), v3_membered( X ) }.
% 0.68/1.08 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha3( X ) }
% 0.68/1.08 .
% 0.68/1.08 { ! v5_membered( X ), ! element( Y, powerset( X ) ), alpha4( Y ) }.
% 0.68/1.08 { ! v5_membered( X ), ! element( Y, powerset( X ) ), v5_membered( Y ) }.
% 0.68/1.08 { ! alpha4( X ), alpha9( X ) }.
% 0.68/1.08 { ! alpha4( X ), v4_membered( X ) }.
% 0.68/1.08 { ! alpha9( X ), ! v4_membered( X ), alpha4( X ) }.
% 0.68/1.08 { ! alpha9( X ), v1_membered( X ) }.
% 0.68/1.08 { ! alpha9( X ), v2_membered( X ) }.
% 0.68/1.08 { ! alpha9( X ), v3_membered( X ) }.
% 0.68/1.08 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha9( X ) }
% 0.68/1.08 .
% 0.68/1.08 { ! v1_membered( X ), v1_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! v2_membered( X ), v1_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! v2_membered( X ), v2_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! v3_membered( X ), v1_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! v3_membered( X ), v2_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! v3_membered( X ), v3_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! v4_membered( X ), alpha5( X, Y ) }.
% 0.68/1.08 { ! v4_membered( X ), v4_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! alpha5( X, Y ), v1_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! alpha5( X, Y ), v2_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! alpha5( X, Y ), v3_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! v1_membered( set_difference( X, Y ) ), ! v2_membered( set_difference( X
% 0.68/1.08 , Y ) ), ! v3_membered( set_difference( X, Y ) ), alpha5( X, Y ) }.
% 0.68/1.08 { ! v5_membered( X ), alpha6( X, Y ) }.
% 0.68/1.08 { ! v5_membered( X ), v5_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! alpha6( X, Y ), alpha10( X, Y ) }.
% 0.68/1.08 { ! alpha6( X, Y ), v4_membered( set_difference( X, Y ) ) }.
% 0.68/1.08 { ! alpha10( X, Y ), ! v4_membered( set_difference( X, Y ) ), alpha6( X, Y
% 2.13/2.59 ) }.
% 2.13/2.59 { ! alpha10( X, Y ), v1_membered( set_difference( X, Y ) ) }.
% 2.13/2.59 { ! alpha10( X, Y ), v2_membered( set_difference( X, Y ) ) }.
% 2.13/2.59 { ! alpha10( X, Y ), v3_membered( set_difference( X, Y ) ) }.
% 2.13/2.59 { ! v1_membered( set_difference( X, Y ) ), ! v2_membered( set_difference( X
% 2.13/2.59 , Y ) ), ! v3_membered( set_difference( X, Y ) ), alpha10( X, Y ) }.
% 2.13/2.59 { ! in( X, Y ), element( X, Y ) }.
% 2.13/2.59 { set_difference( X, empty_set ) = X }.
% 2.13/2.59 { set_difference( empty_set, X ) = empty_set }.
% 2.13/2.59 { ! in( X, Z ), ! element( Z, powerset( Y ) ), element( X, Y ) }.
% 2.13/2.59 { ! in( X, Y ), ! element( Y, powerset( Z ) ), ! empty( Z ) }.
% 2.13/2.59 { subset( X, X ) }.
% 2.13/2.59 { empty( X ), ! empty( skol2( Y ) ) }.
% 2.13/2.59 { empty( X ), element( skol2( X ), powerset( X ) ) }.
% 2.13/2.59 { empty( skol3( Y ) ) }.
% 2.13/2.59 { element( skol3( X ), powerset( X ) ) }.
% 2.13/2.59 { ! empty( X ), alpha7( X ) }.
% 2.13/2.59 { ! empty( X ), v5_membered( X ) }.
% 2.13/2.59 { ! alpha7( X ), alpha11( X ) }.
% 2.13/2.59 { ! alpha7( X ), v4_membered( X ) }.
% 2.13/2.59 { ! alpha11( X ), ! v4_membered( X ), alpha7( X ) }.
% 2.13/2.59 { ! alpha11( X ), v1_membered( X ) }.
% 2.13/2.59 { ! alpha11( X ), v2_membered( X ) }.
% 2.13/2.59 { ! alpha11( X ), v3_membered( X ) }.
% 2.13/2.59 { ! v1_membered( X ), ! v2_membered( X ), ! v3_membered( X ), alpha11( X )
% 2.13/2.59 }.
% 2.13/2.59 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 2.13/2.59 { ! empty( X ), X = empty_set }.
% 2.13/2.59 { ! in( X, Y ), ! empty( Y ) }.
% 2.13/2.59 { ! empty( X ), X = Y, ! empty( Y ) }.
% 2.13/2.59 { ! element( Y, powerset( X ) ), subset_complement( X, subset_complement( X
% 2.13/2.59 , Y ) ) = Y }.
% 2.13/2.59 { one_sorted_str( skol4 ) }.
% 2.13/2.59 { element( skol5( X ), X ) }.
% 2.13/2.59 { ! element( Y, powerset( X ) ), ! element( Z, powerset( X ) ),
% 2.13/2.59 subset_difference( X, Y, Z ) = set_difference( Y, Z ) }.
% 2.13/2.59 { && }.
% 2.13/2.59 { ! one_sorted_str( X ), element( cast_as_carrier_subset( X ), powerset(
% 2.13/2.59 the_carrier( X ) ) ) }.
% 2.13/2.59 { ! element( Y, powerset( X ) ), element( subset_complement( X, Y ),
% 2.13/2.59 powerset( X ) ) }.
% 2.13/2.59 { && }.
% 2.13/2.59 { ! element( Y, powerset( X ) ), ! element( Z, powerset( X ) ), element(
% 2.13/2.59 subset_difference( X, Y, Z ), powerset( X ) ) }.
% 2.13/2.59 { && }.
% 2.13/2.59 { && }.
% 2.13/2.59 { && }.
% 2.13/2.59 { ! empty( powerset( X ) ) }.
% 2.13/2.59 { ! element( X, powerset( Y ) ), subset( X, Y ) }.
% 2.13/2.59 { ! subset( X, Y ), element( X, powerset( Y ) ) }.
% 2.13/2.59 { ! one_sorted_str( X ), cast_as_carrier_subset( X ) = the_carrier( X ) }.
% 2.13/2.59 { one_sorted_str( skol6 ) }.
% 2.13/2.59 { element( skol7, powerset( the_carrier( skol6 ) ) ) }.
% 2.13/2.59 { ! subset_complement( the_carrier( skol6 ), skol7 ) = subset_difference(
% 2.13/2.59 the_carrier( skol6 ), cast_as_carrier_subset( skol6 ), skol7 ) }.
% 2.13/2.59 { ! element( Y, powerset( X ) ), subset_complement( X, Y ) = set_difference
% 2.13/2.59 ( X, Y ) }.
% 2.13/2.59
% 2.13/2.59 percentage equality = 0.034884, percentage horn = 0.983193
% 2.13/2.59 This is a problem with some equality
% 2.13/2.59
% 2.13/2.59
% 2.13/2.59
% 2.13/2.59 Options Used:
% 2.13/2.59
% 2.13/2.59 useres = 1
% 2.13/2.59 useparamod = 1
% 2.13/2.59 useeqrefl = 1
% 2.13/2.59 useeqfact = 1
% 2.13/2.59 usefactor = 1
% 2.13/2.59 usesimpsplitting = 0
% 2.13/2.59 usesimpdemod = 5
% 2.13/2.59 usesimpres = 3
% 2.13/2.59
% 2.13/2.59 resimpinuse = 1000
% 2.13/2.59 resimpclauses = 20000
% 2.13/2.59 substype = eqrewr
% 2.13/2.59 backwardsubs = 1
% 2.13/2.59 selectoldest = 5
% 2.13/2.59
% 2.13/2.59 litorderings [0] = split
% 2.13/2.59 litorderings [1] = extend the termordering, first sorting on arguments
% 2.13/2.59
% 2.13/2.59 termordering = kbo
% 2.13/2.59
% 2.13/2.59 litapriori = 0
% 2.13/2.59 termapriori = 1
% 2.13/2.59 litaposteriori = 0
% 2.13/2.59 termaposteriori = 0
% 2.13/2.59 demodaposteriori = 0
% 2.13/2.59 ordereqreflfact = 0
% 2.13/2.59
% 2.13/2.59 litselect = negord
% 2.13/2.59
% 2.13/2.59 maxweight = 15
% 2.13/2.59 maxdepth = 30000
% 2.13/2.59 maxlength = 115
% 2.13/2.59 maxnrvars = 195
% 2.13/2.59 excuselevel = 1
% 2.13/2.59 increasemaxweight = 1
% 2.13/2.59
% 2.13/2.59 maxselected = 10000000
% 2.13/2.59 maxnrclauses = 10000000
% 2.13/2.59
% 2.13/2.59 showgenerated = 0
% 2.13/2.59 showkept = 0
% 2.13/2.59 showselected = 0
% 2.13/2.59 showdeleted = 0
% 2.13/2.59 showresimp = 1
% 2.13/2.59 showstatus = 2000
% 2.13/2.59
% 2.13/2.59 prologoutput = 0
% 2.13/2.59 nrgoals = 5000000
% 2.13/2.59 totalproof = 1
% 2.13/2.59
% 2.13/2.59 Symbols occurring in the translation:
% 2.13/2.59
% 2.13/2.59 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.13/2.59 . [1, 2] (w:1, o:45, a:1, s:1, b:0),
% 2.13/2.59 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 2.13/2.59 ! [4, 1] (w:0, o:14, a:1, s:1, b:0),
% 2.13/2.59 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.13/2.59 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.13/2.59 in [37, 2] (w:1, o:69, a:1, s:1, b:0),
% 2.13/2.59 v5_membered [38, 1] (w:1, o:27, a:1, s:1, b:0),
% 2.13/2.59 v4_membered [39, 1] (w:1, o:26, a:1, s:1, b:0),
% 2.13/2.59 v3_membered [40, 1] (w:1, o:25, a:1, s:1, b:0),
% 2.13/2.59 v2_membered [41, 1] (w:1, o:24, a:1, s:1, b:0),
% 19.72/20.11 v1_membered [42, 1] (w:1, o:19, a:1, s:1, b:0),
% 19.72/20.11 empty [43, 1] (w:1, o:28, a:1, s:1, b:0),
% 19.72/20.11 element [44, 2] (w:1, o:70, a:1, s:1, b:0),
% 19.72/20.11 v1_xcmplx_0 [45, 1] (w:1, o:20, a:1, s:1, b:0),
% 19.72/20.11 v1_xreal_0 [46, 1] (w:1, o:21, a:1, s:1, b:0),
% 19.72/20.11 v1_rat_1 [47, 1] (w:1, o:22, a:1, s:1, b:0),
% 19.72/20.11 v1_int_1 [48, 1] (w:1, o:23, a:1, s:1, b:0),
% 19.72/20.11 natural [49, 1] (w:1, o:29, a:1, s:1, b:0),
% 19.72/20.11 empty_set [50, 0] (w:1, o:8, a:1, s:1, b:0),
% 19.72/20.11 powerset [51, 1] (w:1, o:31, a:1, s:1, b:0),
% 19.72/20.11 set_difference [52, 2] (w:1, o:71, a:1, s:1, b:0),
% 19.72/20.11 subset [54, 2] (w:1, o:72, a:1, s:1, b:0),
% 19.72/20.11 subset_complement [55, 2] (w:1, o:73, a:1, s:1, b:0),
% 19.72/20.11 one_sorted_str [56, 1] (w:1, o:30, a:1, s:1, b:0),
% 19.72/20.11 subset_difference [57, 3] (w:1, o:77, a:1, s:1, b:0),
% 19.72/20.11 cast_as_carrier_subset [58, 1] (w:1, o:32, a:1, s:1, b:0),
% 19.72/20.11 the_carrier [59, 1] (w:1, o:36, a:1, s:1, b:0),
% 19.72/20.11 alpha1 [60, 1] (w:1, o:37, a:1, s:1, b:1),
% 19.72/20.11 alpha2 [61, 1] (w:1, o:39, a:1, s:1, b:1),
% 19.72/20.11 alpha3 [62, 1] (w:1, o:40, a:1, s:1, b:1),
% 19.72/20.11 alpha4 [63, 1] (w:1, o:41, a:1, s:1, b:1),
% 19.72/20.11 alpha5 [64, 2] (w:1, o:74, a:1, s:1, b:1),
% 19.72/20.11 alpha6 [65, 2] (w:1, o:75, a:1, s:1, b:1),
% 19.72/20.11 alpha7 [66, 1] (w:1, o:42, a:1, s:1, b:1),
% 19.72/20.11 alpha8 [67, 1] (w:1, o:43, a:1, s:1, b:1),
% 19.72/20.11 alpha9 [68, 1] (w:1, o:44, a:1, s:1, b:1),
% 19.72/20.11 alpha10 [69, 2] (w:1, o:76, a:1, s:1, b:1),
% 19.72/20.11 alpha11 [70, 1] (w:1, o:38, a:1, s:1, b:1),
% 19.72/20.11 skol1 [71, 0] (w:1, o:10, a:1, s:1, b:1),
% 19.72/20.11 skol2 [72, 1] (w:1, o:33, a:1, s:1, b:1),
% 19.72/20.11 skol3 [73, 1] (w:1, o:34, a:1, s:1, b:1),
% 19.72/20.11 skol4 [74, 0] (w:1, o:11, a:1, s:1, b:1),
% 19.72/20.11 skol5 [75, 1] (w:1, o:35, a:1, s:1, b:1),
% 19.72/20.11 skol6 [76, 0] (w:1, o:12, a:1, s:1, b:1),
% 19.72/20.11 skol7 [77, 0] (w:1, o:13, a:1, s:1, b:1).
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Starting Search:
% 19.72/20.11
% 19.72/20.11 *** allocated 15000 integers for clauses
% 19.72/20.11 *** allocated 22500 integers for clauses
% 19.72/20.11 *** allocated 33750 integers for clauses
% 19.72/20.11 *** allocated 50625 integers for clauses
% 19.72/20.11 *** allocated 15000 integers for termspace/termends
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 75937 integers for clauses
% 19.72/20.11 *** allocated 22500 integers for termspace/termends
% 19.72/20.11 *** allocated 113905 integers for clauses
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 6487
% 19.72/20.11 Kept: 2026
% 19.72/20.11 Inuse: 517
% 19.72/20.11 Deleted: 47
% 19.72/20.11 Deletedinuse: 15
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 33750 integers for termspace/termends
% 19.72/20.11 *** allocated 170857 integers for clauses
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 50625 integers for termspace/termends
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 15582
% 19.72/20.11 Kept: 4028
% 19.72/20.11 Inuse: 759
% 19.72/20.11 Deleted: 74
% 19.72/20.11 Deletedinuse: 19
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 256285 integers for clauses
% 19.72/20.11 *** allocated 75937 integers for termspace/termends
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 26536
% 19.72/20.11 Kept: 6043
% 19.72/20.11 Inuse: 1005
% 19.72/20.11 Deleted: 100
% 19.72/20.11 Deletedinuse: 34
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 384427 integers for clauses
% 19.72/20.11 *** allocated 113905 integers for termspace/termends
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 36088
% 19.72/20.11 Kept: 8057
% 19.72/20.11 Inuse: 1212
% 19.72/20.11 Deleted: 114
% 19.72/20.11 Deletedinuse: 34
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 576640 integers for clauses
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 46939
% 19.72/20.11 Kept: 10063
% 19.72/20.11 Inuse: 1401
% 19.72/20.11 Deleted: 114
% 19.72/20.11 Deletedinuse: 34
% 19.72/20.11
% 19.72/20.11 *** allocated 170857 integers for termspace/termends
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 54640
% 19.72/20.11 Kept: 12065
% 19.72/20.11 Inuse: 1534
% 19.72/20.11 Deleted: 117
% 19.72/20.11 Deletedinuse: 34
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 64956
% 19.72/20.11 Kept: 14066
% 19.72/20.11 Inuse: 1625
% 19.72/20.11 Deleted: 117
% 19.72/20.11 Deletedinuse: 34
% 19.72/20.11
% 19.72/20.11 *** allocated 864960 integers for clauses
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 256285 integers for termspace/termends
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 82666
% 19.72/20.11 Kept: 16073
% 19.72/20.11 Inuse: 1817
% 19.72/20.11 Deleted: 120
% 19.72/20.11 Deletedinuse: 34
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 94743
% 19.72/20.11 Kept: 18140
% 19.72/20.11 Inuse: 1930
% 19.72/20.11 Deleted: 225
% 19.72/20.11 Deletedinuse: 120
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 106568
% 19.72/20.11 Kept: 20354
% 19.72/20.11 Inuse: 1990
% 19.72/20.11 Deleted: 239
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying clauses:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 1297440 integers for clauses
% 19.72/20.11 *** allocated 384427 integers for termspace/termends
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 115577
% 19.72/20.11 Kept: 22357
% 19.72/20.11 Inuse: 2054
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 125132
% 19.72/20.11 Kept: 24617
% 19.72/20.11 Inuse: 2149
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 133918
% 19.72/20.11 Kept: 26978
% 19.72/20.11 Inuse: 2199
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 139741
% 19.72/20.11 Kept: 29024
% 19.72/20.11 Inuse: 2254
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 150243
% 19.72/20.11 Kept: 31038
% 19.72/20.11 Inuse: 2302
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 576640 integers for termspace/termends
% 19.72/20.11 *** allocated 1946160 integers for clauses
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 161485
% 19.72/20.11 Kept: 33134
% 19.72/20.11 Inuse: 2334
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 171764
% 19.72/20.11 Kept: 35178
% 19.72/20.11 Inuse: 2404
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 183973
% 19.72/20.11 Kept: 37183
% 19.72/20.11 Inuse: 2467
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 200516
% 19.72/20.11 Kept: 39524
% 19.72/20.11 Inuse: 2524
% 19.72/20.11 Deleted: 2259
% 19.72/20.11 Deletedinuse: 132
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying clauses:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 211577
% 19.72/20.11 Kept: 41573
% 19.72/20.11 Inuse: 2563
% 19.72/20.11 Deleted: 3403
% 19.72/20.11 Deletedinuse: 140
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 224851
% 19.72/20.11 Kept: 43625
% 19.72/20.11 Inuse: 2663
% 19.72/20.11 Deleted: 3450
% 19.72/20.11 Deletedinuse: 186
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 241578
% 19.72/20.11 Kept: 46086
% 19.72/20.11 Inuse: 2709
% 19.72/20.11 Deleted: 3464
% 19.72/20.11 Deletedinuse: 195
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 864960 integers for termspace/termends
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 253445
% 19.72/20.11 Kept: 48106
% 19.72/20.11 Inuse: 2776
% 19.72/20.11 Deleted: 3464
% 19.72/20.11 Deletedinuse: 195
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 *** allocated 2919240 integers for clauses
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 263517
% 19.72/20.11 Kept: 50133
% 19.72/20.11 Inuse: 2820
% 19.72/20.11 Deleted: 3469
% 19.72/20.11 Deletedinuse: 195
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 281018
% 19.72/20.11 Kept: 52175
% 19.72/20.11 Inuse: 2874
% 19.72/20.11 Deleted: 3478
% 19.72/20.11 Deletedinuse: 195
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 293783
% 19.72/20.11 Kept: 54327
% 19.72/20.11 Inuse: 2909
% 19.72/20.11 Deleted: 3481
% 19.72/20.11 Deletedinuse: 195
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 304610
% 19.72/20.11 Kept: 56432
% 19.72/20.11 Inuse: 2939
% 19.72/20.11 Deleted: 3482
% 19.72/20.11 Deletedinuse: 195
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11 Resimplifying inuse:
% 19.72/20.11 Done
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Intermediate Status:
% 19.72/20.11 Generated: 315646
% 19.72/20.11 Kept: 58465
% 19.72/20.11 Inuse: 2997
% 19.72/20.11 Deleted: 3482
% 19.72/20.11 Deletedinuse: 195
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Bliksems!, er is een bewijs:
% 19.72/20.11 % SZS status Theorem
% 19.72/20.11 % SZS output start Refutation
% 19.72/20.11
% 19.72/20.11 (86) {G0,W3,D2,L1,V1,M1} I { subset( X, X ) }.
% 19.72/20.11 (107) {G0,W16,D3,L3,V3,M3} I { ! element( Y, powerset( X ) ), ! element( Z
% 19.72/20.11 , powerset( X ) ), subset_difference( X, Y, Z ) ==> set_difference( Y, Z
% 19.72/20.11 ) }.
% 19.72/20.11 (113) {G0,W7,D3,L2,V2,M2} I { ! subset( X, Y ), element( X, powerset( Y ) )
% 19.72/20.11 }.
% 19.72/20.11 (114) {G0,W7,D3,L2,V1,M2} I { ! one_sorted_str( X ), the_carrier( X ) ==>
% 19.72/20.11 cast_as_carrier_subset( X ) }.
% 19.72/20.11 (115) {G0,W2,D2,L1,V0,M1} I { one_sorted_str( skol6 ) }.
% 19.72/20.11 (116) {G0,W5,D4,L1,V0,M1} I { element( skol7, powerset( the_carrier( skol6
% 19.72/20.11 ) ) ) }.
% 19.72/20.11 (117) {G0,W11,D4,L1,V0,M1} I { ! subset_difference( the_carrier( skol6 ),
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_complement(
% 19.72/20.11 the_carrier( skol6 ), skol7 ) }.
% 19.72/20.11 (118) {G0,W11,D3,L2,V2,M2} I { ! element( Y, powerset( X ) ),
% 19.72/20.11 subset_complement( X, Y ) ==> set_difference( X, Y ) }.
% 19.72/20.11 (1097) {G1,W4,D3,L1,V1,M1} R(113,86) { element( X, powerset( X ) ) }.
% 19.72/20.11 (1099) {G2,W12,D3,L2,V2,M2} R(1097,107) { ! element( X, powerset( Y ) ),
% 19.72/20.11 subset_difference( Y, Y, X ) ==> set_difference( Y, X ) }.
% 19.72/20.11 (1118) {G1,W5,D3,L1,V0,M1} R(114,115) { the_carrier( skol6 ) ==>
% 19.72/20.11 cast_as_carrier_subset( skol6 ) }.
% 19.72/20.11 (1130) {G2,W5,D4,L1,V0,M1} S(116);d(1118) { element( skol7, powerset(
% 19.72/20.11 cast_as_carrier_subset( skol6 ) ) ) }.
% 19.72/20.11 (1144) {G2,W11,D4,L1,V0,M1} S(117);d(1118) { ! subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 ==> subset_complement( cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 (1957) {G3,W9,D4,L1,V0,M1} R(1130,118) { subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 (20357) {G4,W11,D4,L1,V0,M1} S(1144);d(1957) { ! subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 ==> set_difference( cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 (58495) {G5,W0,D0,L0,V0,M0} R(1099,1130);r(20357) { }.
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 % SZS output end Refutation
% 19.72/20.11 found a proof!
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Unprocessed initial clauses:
% 19.72/20.11
% 19.72/20.11 (58497) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 19.72/20.11 (58498) {G0,W1,D1,L1,V0,M1} { && }.
% 19.72/20.11 (58499) {G0,W4,D2,L2,V1,M2} { ! v5_membered( X ), v4_membered( X ) }.
% 19.72/20.11 (58500) {G0,W4,D2,L2,V1,M2} { ! v4_membered( X ), v3_membered( X ) }.
% 19.72/20.11 (58501) {G0,W4,D2,L2,V1,M2} { ! v3_membered( X ), v2_membered( X ) }.
% 19.72/20.11 (58502) {G0,W4,D2,L2,V1,M2} { ! v2_membered( X ), v1_membered( X ) }.
% 19.72/20.11 (58503) {G0,W2,D2,L1,V0,M1} { ! empty( skol1 ) }.
% 19.72/20.11 (58504) {G0,W2,D2,L1,V0,M1} { v1_membered( skol1 ) }.
% 19.72/20.11 (58505) {G0,W2,D2,L1,V0,M1} { v2_membered( skol1 ) }.
% 19.72/20.11 (58506) {G0,W2,D2,L1,V0,M1} { v3_membered( skol1 ) }.
% 19.72/20.11 (58507) {G0,W2,D2,L1,V0,M1} { v4_membered( skol1 ) }.
% 19.72/20.11 (58508) {G0,W2,D2,L1,V0,M1} { v5_membered( skol1 ) }.
% 19.72/20.11 (58509) {G0,W7,D2,L3,V2,M3} { ! v1_membered( X ), ! element( Y, X ),
% 19.72/20.11 v1_xcmplx_0( Y ) }.
% 19.72/20.11 (58510) {G0,W7,D2,L3,V2,M3} { ! v2_membered( X ), ! element( Y, X ),
% 19.72/20.11 v1_xcmplx_0( Y ) }.
% 19.72/20.11 (58511) {G0,W7,D2,L3,V2,M3} { ! v2_membered( X ), ! element( Y, X ),
% 19.72/20.11 v1_xreal_0( Y ) }.
% 19.72/20.11 (58512) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! element( Y, X ),
% 19.72/20.11 v1_xcmplx_0( Y ) }.
% 19.72/20.11 (58513) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! element( Y, X ),
% 19.72/20.11 v1_xreal_0( Y ) }.
% 19.72/20.11 (58514) {G0,W7,D2,L3,V2,M3} { ! v3_membered( X ), ! element( Y, X ),
% 19.72/20.11 v1_rat_1( Y ) }.
% 19.72/20.11 (58515) {G0,W7,D2,L3,V2,M3} { ! v4_membered( X ), ! element( Y, X ),
% 19.72/20.11 alpha1( Y ) }.
% 19.72/20.11 (58516) {G0,W7,D2,L3,V2,M3} { ! v4_membered( X ), ! element( Y, X ),
% 19.72/20.11 v1_rat_1( Y ) }.
% 19.72/20.11 (58517) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_xcmplx_0( X ) }.
% 19.72/20.11 (58518) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_xreal_0( X ) }.
% 19.72/20.11 (58519) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v1_int_1( X ) }.
% 19.72/20.11 (58520) {G0,W8,D2,L4,V1,M4} { ! v1_xcmplx_0( X ), ! v1_xreal_0( X ), !
% 19.72/20.11 v1_int_1( X ), alpha1( X ) }.
% 19.72/20.11 (58521) {G0,W7,D2,L3,V2,M3} { ! v5_membered( X ), ! element( Y, X ),
% 19.72/20.11 alpha2( Y ) }.
% 19.72/20.11 (58522) {G0,W7,D2,L3,V2,M3} { ! v5_membered( X ), ! element( Y, X ),
% 19.72/20.11 v1_rat_1( Y ) }.
% 19.72/20.11 (58523) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha8( X ) }.
% 19.72/20.11 (58524) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), v1_int_1( X ) }.
% 19.72/20.11 (58525) {G0,W6,D2,L3,V1,M3} { ! alpha8( X ), ! v1_int_1( X ), alpha2( X )
% 19.72/20.11 }.
% 19.72/20.11 (58526) {G0,W4,D2,L2,V1,M2} { ! alpha8( X ), v1_xcmplx_0( X ) }.
% 19.72/20.11 (58527) {G0,W4,D2,L2,V1,M2} { ! alpha8( X ), natural( X ) }.
% 19.72/20.11 (58528) {G0,W4,D2,L2,V1,M2} { ! alpha8( X ), v1_xreal_0( X ) }.
% 19.72/20.11 (58529) {G0,W8,D2,L4,V1,M4} { ! v1_xcmplx_0( X ), ! natural( X ), !
% 19.72/20.11 v1_xreal_0( X ), alpha8( X ) }.
% 19.72/20.11 (58530) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 19.72/20.11 (58531) {G0,W2,D2,L1,V0,M1} { v1_membered( empty_set ) }.
% 19.72/20.11 (58532) {G0,W2,D2,L1,V0,M1} { v2_membered( empty_set ) }.
% 19.72/20.11 (58533) {G0,W2,D2,L1,V0,M1} { v3_membered( empty_set ) }.
% 19.72/20.11 (58534) {G0,W2,D2,L1,V0,M1} { v4_membered( empty_set ) }.
% 19.72/20.11 (58535) {G0,W2,D2,L1,V0,M1} { v5_membered( empty_set ) }.
% 19.72/20.11 (58536) {G0,W8,D3,L3,V2,M3} { ! v1_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), v1_membered( Y ) }.
% 19.72/20.11 (58537) {G0,W8,D3,L3,V2,M3} { ! v2_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), v1_membered( Y ) }.
% 19.72/20.11 (58538) {G0,W8,D3,L3,V2,M3} { ! v2_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), v2_membered( Y ) }.
% 19.72/20.11 (58539) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), v1_membered( Y ) }.
% 19.72/20.11 (58540) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), v2_membered( Y ) }.
% 19.72/20.11 (58541) {G0,W8,D3,L3,V2,M3} { ! v3_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), v3_membered( Y ) }.
% 19.72/20.11 (58542) {G0,W8,D3,L3,V2,M3} { ! v4_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), alpha3( Y ) }.
% 19.72/20.11 (58543) {G0,W8,D3,L3,V2,M3} { ! v4_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), v4_membered( Y ) }.
% 19.72/20.11 (58544) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), v1_membered( X ) }.
% 19.72/20.11 (58545) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), v2_membered( X ) }.
% 19.72/20.11 (58546) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), v3_membered( X ) }.
% 19.72/20.11 (58547) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 19.72/20.11 v3_membered( X ), alpha3( X ) }.
% 19.72/20.11 (58548) {G0,W8,D3,L3,V2,M3} { ! v5_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), alpha4( Y ) }.
% 19.72/20.11 (58549) {G0,W8,D3,L3,V2,M3} { ! v5_membered( X ), ! element( Y, powerset(
% 19.72/20.11 X ) ), v5_membered( Y ) }.
% 19.72/20.11 (58550) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), alpha9( X ) }.
% 19.72/20.11 (58551) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v4_membered( X ) }.
% 19.72/20.11 (58552) {G0,W6,D2,L3,V1,M3} { ! alpha9( X ), ! v4_membered( X ), alpha4( X
% 19.72/20.11 ) }.
% 19.72/20.11 (58553) {G0,W4,D2,L2,V1,M2} { ! alpha9( X ), v1_membered( X ) }.
% 19.72/20.11 (58554) {G0,W4,D2,L2,V1,M2} { ! alpha9( X ), v2_membered( X ) }.
% 19.72/20.11 (58555) {G0,W4,D2,L2,V1,M2} { ! alpha9( X ), v3_membered( X ) }.
% 19.72/20.11 (58556) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 19.72/20.11 v3_membered( X ), alpha9( X ) }.
% 19.72/20.11 (58557) {G0,W6,D3,L2,V2,M2} { ! v1_membered( X ), v1_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58558) {G0,W6,D3,L2,V2,M2} { ! v2_membered( X ), v1_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58559) {G0,W6,D3,L2,V2,M2} { ! v2_membered( X ), v2_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58560) {G0,W6,D3,L2,V2,M2} { ! v3_membered( X ), v1_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58561) {G0,W6,D3,L2,V2,M2} { ! v3_membered( X ), v2_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58562) {G0,W6,D3,L2,V2,M2} { ! v3_membered( X ), v3_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58563) {G0,W5,D2,L2,V2,M2} { ! v4_membered( X ), alpha5( X, Y ) }.
% 19.72/20.11 (58564) {G0,W6,D3,L2,V2,M2} { ! v4_membered( X ), v4_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58565) {G0,W7,D3,L2,V2,M2} { ! alpha5( X, Y ), v1_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58566) {G0,W7,D3,L2,V2,M2} { ! alpha5( X, Y ), v2_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58567) {G0,W7,D3,L2,V2,M2} { ! alpha5( X, Y ), v3_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58568) {G0,W15,D3,L4,V2,M4} { ! v1_membered( set_difference( X, Y ) ), !
% 19.72/20.11 v2_membered( set_difference( X, Y ) ), ! v3_membered( set_difference( X,
% 19.72/20.11 Y ) ), alpha5( X, Y ) }.
% 19.72/20.11 (58569) {G0,W5,D2,L2,V2,M2} { ! v5_membered( X ), alpha6( X, Y ) }.
% 19.72/20.11 (58570) {G0,W6,D3,L2,V2,M2} { ! v5_membered( X ), v5_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58571) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), alpha10( X, Y ) }.
% 19.72/20.11 (58572) {G0,W7,D3,L2,V2,M2} { ! alpha6( X, Y ), v4_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58573) {G0,W10,D3,L3,V2,M3} { ! alpha10( X, Y ), ! v4_membered(
% 19.72/20.11 set_difference( X, Y ) ), alpha6( X, Y ) }.
% 19.72/20.11 (58574) {G0,W7,D3,L2,V2,M2} { ! alpha10( X, Y ), v1_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58575) {G0,W7,D3,L2,V2,M2} { ! alpha10( X, Y ), v2_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58576) {G0,W7,D3,L2,V2,M2} { ! alpha10( X, Y ), v3_membered(
% 19.72/20.11 set_difference( X, Y ) ) }.
% 19.72/20.11 (58577) {G0,W15,D3,L4,V2,M4} { ! v1_membered( set_difference( X, Y ) ), !
% 19.72/20.11 v2_membered( set_difference( X, Y ) ), ! v3_membered( set_difference( X,
% 19.72/20.11 Y ) ), alpha10( X, Y ) }.
% 19.72/20.11 (58578) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 19.72/20.11 (58579) {G0,W5,D3,L1,V1,M1} { set_difference( X, empty_set ) = X }.
% 19.72/20.11 (58580) {G0,W5,D3,L1,V1,M1} { set_difference( empty_set, X ) = empty_set
% 19.72/20.11 }.
% 19.72/20.11 (58581) {G0,W10,D3,L3,V3,M3} { ! in( X, Z ), ! element( Z, powerset( Y ) )
% 19.72/20.11 , element( X, Y ) }.
% 19.72/20.11 (58582) {G0,W9,D3,L3,V3,M3} { ! in( X, Y ), ! element( Y, powerset( Z ) )
% 19.72/20.11 , ! empty( Z ) }.
% 19.72/20.11 (58583) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 19.72/20.11 (58584) {G0,W5,D3,L2,V2,M2} { empty( X ), ! empty( skol2( Y ) ) }.
% 19.72/20.11 (58585) {G0,W7,D3,L2,V1,M2} { empty( X ), element( skol2( X ), powerset( X
% 19.72/20.11 ) ) }.
% 19.72/20.11 (58586) {G0,W3,D3,L1,V1,M1} { empty( skol3( Y ) ) }.
% 19.72/20.11 (58587) {G0,W5,D3,L1,V1,M1} { element( skol3( X ), powerset( X ) ) }.
% 19.72/20.11 (58588) {G0,W4,D2,L2,V1,M2} { ! empty( X ), alpha7( X ) }.
% 19.72/20.11 (58589) {G0,W4,D2,L2,V1,M2} { ! empty( X ), v5_membered( X ) }.
% 19.72/20.11 (58590) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), alpha11( X ) }.
% 19.72/20.11 (58591) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), v4_membered( X ) }.
% 19.72/20.11 (58592) {G0,W6,D2,L3,V1,M3} { ! alpha11( X ), ! v4_membered( X ), alpha7(
% 19.72/20.11 X ) }.
% 19.72/20.11 (58593) {G0,W4,D2,L2,V1,M2} { ! alpha11( X ), v1_membered( X ) }.
% 19.72/20.11 (58594) {G0,W4,D2,L2,V1,M2} { ! alpha11( X ), v2_membered( X ) }.
% 19.72/20.11 (58595) {G0,W4,D2,L2,V1,M2} { ! alpha11( X ), v3_membered( X ) }.
% 19.72/20.11 (58596) {G0,W8,D2,L4,V1,M4} { ! v1_membered( X ), ! v2_membered( X ), !
% 19.72/20.11 v3_membered( X ), alpha11( X ) }.
% 19.72/20.11 (58597) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y )
% 19.72/20.11 }.
% 19.72/20.11 (58598) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 19.72/20.11 (58599) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 19.72/20.11 (58600) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 19.72/20.11 (58601) {G0,W11,D4,L2,V2,M2} { ! element( Y, powerset( X ) ),
% 19.72/20.11 subset_complement( X, subset_complement( X, Y ) ) = Y }.
% 19.72/20.11 (58602) {G0,W2,D2,L1,V0,M1} { one_sorted_str( skol4 ) }.
% 19.72/20.11 (58603) {G0,W4,D3,L1,V1,M1} { element( skol5( X ), X ) }.
% 19.72/20.11 (58604) {G0,W16,D3,L3,V3,M3} { ! element( Y, powerset( X ) ), ! element( Z
% 19.72/20.11 , powerset( X ) ), subset_difference( X, Y, Z ) = set_difference( Y, Z )
% 19.72/20.11 }.
% 19.72/20.11 (58605) {G0,W1,D1,L1,V0,M1} { && }.
% 19.72/20.11 (58606) {G0,W8,D4,L2,V1,M2} { ! one_sorted_str( X ), element(
% 19.72/20.11 cast_as_carrier_subset( X ), powerset( the_carrier( X ) ) ) }.
% 19.72/20.11 (58607) {G0,W10,D3,L2,V2,M2} { ! element( Y, powerset( X ) ), element(
% 19.72/20.11 subset_complement( X, Y ), powerset( X ) ) }.
% 19.72/20.11 (58608) {G0,W1,D1,L1,V0,M1} { && }.
% 19.72/20.11 (58609) {G0,W15,D3,L3,V3,M3} { ! element( Y, powerset( X ) ), ! element( Z
% 19.72/20.11 , powerset( X ) ), element( subset_difference( X, Y, Z ), powerset( X ) )
% 19.72/20.11 }.
% 19.72/20.11 (58610) {G0,W1,D1,L1,V0,M1} { && }.
% 19.72/20.11 (58611) {G0,W1,D1,L1,V0,M1} { && }.
% 19.72/20.11 (58612) {G0,W1,D1,L1,V0,M1} { && }.
% 19.72/20.11 (58613) {G0,W3,D3,L1,V1,M1} { ! empty( powerset( X ) ) }.
% 19.72/20.11 (58614) {G0,W7,D3,L2,V2,M2} { ! element( X, powerset( Y ) ), subset( X, Y
% 19.72/20.11 ) }.
% 19.72/20.11 (58615) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X, powerset( Y )
% 19.72/20.11 ) }.
% 19.72/20.11 (58616) {G0,W7,D3,L2,V1,M2} { ! one_sorted_str( X ),
% 19.72/20.11 cast_as_carrier_subset( X ) = the_carrier( X ) }.
% 19.72/20.11 (58617) {G0,W2,D2,L1,V0,M1} { one_sorted_str( skol6 ) }.
% 19.72/20.11 (58618) {G0,W5,D4,L1,V0,M1} { element( skol7, powerset( the_carrier( skol6
% 19.72/20.11 ) ) ) }.
% 19.72/20.11 (58619) {G0,W11,D4,L1,V0,M1} { ! subset_complement( the_carrier( skol6 ),
% 19.72/20.11 skol7 ) = subset_difference( the_carrier( skol6 ), cast_as_carrier_subset
% 19.72/20.11 ( skol6 ), skol7 ) }.
% 19.72/20.11 (58620) {G0,W11,D3,L2,V2,M2} { ! element( Y, powerset( X ) ),
% 19.72/20.11 subset_complement( X, Y ) = set_difference( X, Y ) }.
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Total Proof:
% 19.72/20.11
% 19.72/20.11 subsumption: (86) {G0,W3,D2,L1,V1,M1} I { subset( X, X ) }.
% 19.72/20.11 parent0: (58583) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (107) {G0,W16,D3,L3,V3,M3} I { ! element( Y, powerset( X ) ),
% 19.72/20.11 ! element( Z, powerset( X ) ), subset_difference( X, Y, Z ) ==>
% 19.72/20.11 set_difference( Y, Z ) }.
% 19.72/20.11 parent0: (58604) {G0,W16,D3,L3,V3,M3} { ! element( Y, powerset( X ) ), !
% 19.72/20.11 element( Z, powerset( X ) ), subset_difference( X, Y, Z ) =
% 19.72/20.11 set_difference( Y, Z ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 Y := Y
% 19.72/20.11 Z := Z
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 1 ==> 1
% 19.72/20.11 2 ==> 2
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (113) {G0,W7,D3,L2,V2,M2} I { ! subset( X, Y ), element( X,
% 19.72/20.11 powerset( Y ) ) }.
% 19.72/20.11 parent0: (58615) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X,
% 19.72/20.11 powerset( Y ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 Y := Y
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 1 ==> 1
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58653) {G0,W7,D3,L2,V1,M2} { the_carrier( X ) =
% 19.72/20.11 cast_as_carrier_subset( X ), ! one_sorted_str( X ) }.
% 19.72/20.11 parent0[1]: (58616) {G0,W7,D3,L2,V1,M2} { ! one_sorted_str( X ),
% 19.72/20.11 cast_as_carrier_subset( X ) = the_carrier( X ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (114) {G0,W7,D3,L2,V1,M2} I { ! one_sorted_str( X ),
% 19.72/20.11 the_carrier( X ) ==> cast_as_carrier_subset( X ) }.
% 19.72/20.11 parent0: (58653) {G0,W7,D3,L2,V1,M2} { the_carrier( X ) =
% 19.72/20.11 cast_as_carrier_subset( X ), ! one_sorted_str( X ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 1
% 19.72/20.11 1 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (115) {G0,W2,D2,L1,V0,M1} I { one_sorted_str( skol6 ) }.
% 19.72/20.11 parent0: (58617) {G0,W2,D2,L1,V0,M1} { one_sorted_str( skol6 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (116) {G0,W5,D4,L1,V0,M1} I { element( skol7, powerset(
% 19.72/20.11 the_carrier( skol6 ) ) ) }.
% 19.72/20.11 parent0: (58618) {G0,W5,D4,L1,V0,M1} { element( skol7, powerset(
% 19.72/20.11 the_carrier( skol6 ) ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58687) {G0,W11,D4,L1,V0,M1} { ! subset_difference( the_carrier(
% 19.72/20.11 skol6 ), cast_as_carrier_subset( skol6 ), skol7 ) = subset_complement(
% 19.72/20.11 the_carrier( skol6 ), skol7 ) }.
% 19.72/20.11 parent0[0]: (58619) {G0,W11,D4,L1,V0,M1} { ! subset_complement(
% 19.72/20.11 the_carrier( skol6 ), skol7 ) = subset_difference( the_carrier( skol6 ),
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (117) {G0,W11,D4,L1,V0,M1} I { ! subset_difference(
% 19.72/20.11 the_carrier( skol6 ), cast_as_carrier_subset( skol6 ), skol7 ) ==>
% 19.72/20.11 subset_complement( the_carrier( skol6 ), skol7 ) }.
% 19.72/20.11 parent0: (58687) {G0,W11,D4,L1,V0,M1} { ! subset_difference( the_carrier(
% 19.72/20.11 skol6 ), cast_as_carrier_subset( skol6 ), skol7 ) = subset_complement(
% 19.72/20.11 the_carrier( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (118) {G0,W11,D3,L2,V2,M2} I { ! element( Y, powerset( X ) ),
% 19.72/20.11 subset_complement( X, Y ) ==> set_difference( X, Y ) }.
% 19.72/20.11 parent0: (58620) {G0,W11,D3,L2,V2,M2} { ! element( Y, powerset( X ) ),
% 19.72/20.11 subset_complement( X, Y ) = set_difference( X, Y ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 Y := Y
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 1 ==> 1
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 resolution: (58701) {G1,W4,D3,L1,V1,M1} { element( X, powerset( X ) ) }.
% 19.72/20.11 parent0[0]: (113) {G0,W7,D3,L2,V2,M2} I { ! subset( X, Y ), element( X,
% 19.72/20.11 powerset( Y ) ) }.
% 19.72/20.11 parent1[0]: (86) {G0,W3,D2,L1,V1,M1} I { subset( X, X ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 Y := X
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 X := X
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (1097) {G1,W4,D3,L1,V1,M1} R(113,86) { element( X, powerset( X
% 19.72/20.11 ) ) }.
% 19.72/20.11 parent0: (58701) {G1,W4,D3,L1,V1,M1} { element( X, powerset( X ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58702) {G0,W16,D3,L3,V3,M3} { set_difference( Y, Z ) ==>
% 19.72/20.11 subset_difference( X, Y, Z ), ! element( Y, powerset( X ) ), ! element( Z
% 19.72/20.11 , powerset( X ) ) }.
% 19.72/20.11 parent0[2]: (107) {G0,W16,D3,L3,V3,M3} I { ! element( Y, powerset( X ) ), !
% 19.72/20.11 element( Z, powerset( X ) ), subset_difference( X, Y, Z ) ==>
% 19.72/20.11 set_difference( Y, Z ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 Y := Y
% 19.72/20.11 Z := Z
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 resolution: (58703) {G1,W12,D3,L2,V2,M2} { set_difference( X, Y ) ==>
% 19.72/20.11 subset_difference( X, X, Y ), ! element( Y, powerset( X ) ) }.
% 19.72/20.11 parent0[1]: (58702) {G0,W16,D3,L3,V3,M3} { set_difference( Y, Z ) ==>
% 19.72/20.11 subset_difference( X, Y, Z ), ! element( Y, powerset( X ) ), ! element( Z
% 19.72/20.11 , powerset( X ) ) }.
% 19.72/20.11 parent1[0]: (1097) {G1,W4,D3,L1,V1,M1} R(113,86) { element( X, powerset( X
% 19.72/20.11 ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 Y := X
% 19.72/20.11 Z := Y
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 X := X
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58706) {G1,W12,D3,L2,V2,M2} { subset_difference( X, X, Y ) ==>
% 19.72/20.11 set_difference( X, Y ), ! element( Y, powerset( X ) ) }.
% 19.72/20.11 parent0[0]: (58703) {G1,W12,D3,L2,V2,M2} { set_difference( X, Y ) ==>
% 19.72/20.11 subset_difference( X, X, Y ), ! element( Y, powerset( X ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 Y := Y
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (1099) {G2,W12,D3,L2,V2,M2} R(1097,107) { ! element( X,
% 19.72/20.11 powerset( Y ) ), subset_difference( Y, Y, X ) ==> set_difference( Y, X )
% 19.72/20.11 }.
% 19.72/20.11 parent0: (58706) {G1,W12,D3,L2,V2,M2} { subset_difference( X, X, Y ) ==>
% 19.72/20.11 set_difference( X, Y ), ! element( Y, powerset( X ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := Y
% 19.72/20.11 Y := X
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 1
% 19.72/20.11 1 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58707) {G0,W7,D3,L2,V1,M2} { cast_as_carrier_subset( X ) ==>
% 19.72/20.11 the_carrier( X ), ! one_sorted_str( X ) }.
% 19.72/20.11 parent0[1]: (114) {G0,W7,D3,L2,V1,M2} I { ! one_sorted_str( X ),
% 19.72/20.11 the_carrier( X ) ==> cast_as_carrier_subset( X ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 resolution: (58708) {G1,W5,D3,L1,V0,M1} { cast_as_carrier_subset( skol6 )
% 19.72/20.11 ==> the_carrier( skol6 ) }.
% 19.72/20.11 parent0[1]: (58707) {G0,W7,D3,L2,V1,M2} { cast_as_carrier_subset( X ) ==>
% 19.72/20.11 the_carrier( X ), ! one_sorted_str( X ) }.
% 19.72/20.11 parent1[0]: (115) {G0,W2,D2,L1,V0,M1} I { one_sorted_str( skol6 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := skol6
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58709) {G1,W5,D3,L1,V0,M1} { the_carrier( skol6 ) ==>
% 19.72/20.11 cast_as_carrier_subset( skol6 ) }.
% 19.72/20.11 parent0[0]: (58708) {G1,W5,D3,L1,V0,M1} { cast_as_carrier_subset( skol6 )
% 19.72/20.11 ==> the_carrier( skol6 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (1118) {G1,W5,D3,L1,V0,M1} R(114,115) { the_carrier( skol6 )
% 19.72/20.11 ==> cast_as_carrier_subset( skol6 ) }.
% 19.72/20.11 parent0: (58709) {G1,W5,D3,L1,V0,M1} { the_carrier( skol6 ) ==>
% 19.72/20.11 cast_as_carrier_subset( skol6 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 paramod: (58711) {G1,W5,D4,L1,V0,M1} { element( skol7, powerset(
% 19.72/20.11 cast_as_carrier_subset( skol6 ) ) ) }.
% 19.72/20.11 parent0[0]: (1118) {G1,W5,D3,L1,V0,M1} R(114,115) { the_carrier( skol6 )
% 19.72/20.11 ==> cast_as_carrier_subset( skol6 ) }.
% 19.72/20.11 parent1[0; 3]: (116) {G0,W5,D4,L1,V0,M1} I { element( skol7, powerset(
% 19.72/20.11 the_carrier( skol6 ) ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (1130) {G2,W5,D4,L1,V0,M1} S(116);d(1118) { element( skol7,
% 19.72/20.11 powerset( cast_as_carrier_subset( skol6 ) ) ) }.
% 19.72/20.11 parent0: (58711) {G1,W5,D4,L1,V0,M1} { element( skol7, powerset(
% 19.72/20.11 cast_as_carrier_subset( skol6 ) ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 paramod: (58715) {G1,W11,D4,L1,V0,M1} { ! subset_difference( the_carrier(
% 19.72/20.11 skol6 ), cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent0[0]: (1118) {G1,W5,D3,L1,V0,M1} R(114,115) { the_carrier( skol6 )
% 19.72/20.11 ==> cast_as_carrier_subset( skol6 ) }.
% 19.72/20.11 parent1[0; 9]: (117) {G0,W11,D4,L1,V0,M1} I { ! subset_difference(
% 19.72/20.11 the_carrier( skol6 ), cast_as_carrier_subset( skol6 ), skol7 ) ==>
% 19.72/20.11 subset_complement( the_carrier( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 paramod: (58716) {G2,W11,D4,L1,V0,M1} { ! subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 ==> subset_complement( cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent0[0]: (1118) {G1,W5,D3,L1,V0,M1} R(114,115) { the_carrier( skol6 )
% 19.72/20.11 ==> cast_as_carrier_subset( skol6 ) }.
% 19.72/20.11 parent1[0; 3]: (58715) {G1,W11,D4,L1,V0,M1} { ! subset_difference(
% 19.72/20.11 the_carrier( skol6 ), cast_as_carrier_subset( skol6 ), skol7 ) ==>
% 19.72/20.11 subset_complement( cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (1144) {G2,W11,D4,L1,V0,M1} S(117);d(1118) { !
% 19.72/20.11 subset_difference( cast_as_carrier_subset( skol6 ),
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent0: (58716) {G2,W11,D4,L1,V0,M1} { ! subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 ==> subset_complement( cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58720) {G0,W11,D3,L2,V2,M2} { set_difference( X, Y ) ==>
% 19.72/20.11 subset_complement( X, Y ), ! element( Y, powerset( X ) ) }.
% 19.72/20.11 parent0[1]: (118) {G0,W11,D3,L2,V2,M2} I { ! element( Y, powerset( X ) ),
% 19.72/20.11 subset_complement( X, Y ) ==> set_difference( X, Y ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := X
% 19.72/20.11 Y := Y
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 resolution: (58721) {G1,W9,D4,L1,V0,M1} { set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent0[1]: (58720) {G0,W11,D3,L2,V2,M2} { set_difference( X, Y ) ==>
% 19.72/20.11 subset_complement( X, Y ), ! element( Y, powerset( X ) ) }.
% 19.72/20.11 parent1[0]: (1130) {G2,W5,D4,L1,V0,M1} S(116);d(1118) { element( skol7,
% 19.72/20.11 powerset( cast_as_carrier_subset( skol6 ) ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := cast_as_carrier_subset( skol6 )
% 19.72/20.11 Y := skol7
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58722) {G1,W9,D4,L1,V0,M1} { subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent0[0]: (58721) {G1,W9,D4,L1,V0,M1} { set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (1957) {G3,W9,D4,L1,V0,M1} R(1130,118) { subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent0: (58722) {G1,W9,D4,L1,V0,M1} { subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 paramod: (58725) {G3,W11,D4,L1,V0,M1} { ! subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 ==> set_difference( cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent0[0]: (1957) {G3,W9,D4,L1,V0,M1} R(1130,118) { subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent1[0; 8]: (1144) {G2,W11,D4,L1,V0,M1} S(117);d(1118) { !
% 19.72/20.11 subset_difference( cast_as_carrier_subset( skol6 ),
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_complement(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (20357) {G4,W11,D4,L1,V0,M1} S(1144);d(1957) { !
% 19.72/20.11 subset_difference( cast_as_carrier_subset( skol6 ),
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 parent0: (58725) {G3,W11,D4,L1,V0,M1} { ! subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 ==> set_difference( cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 0 ==> 0
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58727) {G2,W12,D3,L2,V2,M2} { set_difference( X, Y ) ==>
% 19.72/20.11 subset_difference( X, X, Y ), ! element( Y, powerset( X ) ) }.
% 19.72/20.11 parent0[1]: (1099) {G2,W12,D3,L2,V2,M2} R(1097,107) { ! element( X,
% 19.72/20.11 powerset( Y ) ), subset_difference( Y, Y, X ) ==> set_difference( Y, X )
% 19.72/20.11 }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := Y
% 19.72/20.11 Y := X
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 eqswap: (58728) {G4,W11,D4,L1,V0,M1} { ! set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 }.
% 19.72/20.11 parent0[0]: (20357) {G4,W11,D4,L1,V0,M1} S(1144);d(1957) { !
% 19.72/20.11 subset_difference( cast_as_carrier_subset( skol6 ),
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 resolution: (58729) {G3,W11,D4,L1,V0,M1} { set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 }.
% 19.72/20.11 parent0[1]: (58727) {G2,W12,D3,L2,V2,M2} { set_difference( X, Y ) ==>
% 19.72/20.11 subset_difference( X, X, Y ), ! element( Y, powerset( X ) ) }.
% 19.72/20.11 parent1[0]: (1130) {G2,W5,D4,L1,V0,M1} S(116);d(1118) { element( skol7,
% 19.72/20.11 powerset( cast_as_carrier_subset( skol6 ) ) ) }.
% 19.72/20.11 substitution0:
% 19.72/20.11 X := cast_as_carrier_subset( skol6 )
% 19.72/20.11 Y := skol7
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 resolution: (58730) {G4,W0,D0,L0,V0,M0} { }.
% 19.72/20.11 parent0[0]: (58728) {G4,W11,D4,L1,V0,M1} { ! set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 }.
% 19.72/20.11 parent1[0]: (58729) {G3,W11,D4,L1,V0,M1} { set_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), skol7 ) ==> subset_difference(
% 19.72/20.11 cast_as_carrier_subset( skol6 ), cast_as_carrier_subset( skol6 ), skol7 )
% 19.72/20.11 }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 substitution1:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 subsumption: (58495) {G5,W0,D0,L0,V0,M0} R(1099,1130);r(20357) { }.
% 19.72/20.11 parent0: (58730) {G4,W0,D0,L0,V0,M0} { }.
% 19.72/20.11 substitution0:
% 19.72/20.11 end
% 19.72/20.11 permutation0:
% 19.72/20.11 end
% 19.72/20.11
% 19.72/20.11 Proof check complete!
% 19.72/20.11
% 19.72/20.11 Memory use:
% 19.72/20.11
% 19.72/20.11 space for terms: 732218
% 19.72/20.11 space for clauses: 2305276
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 clauses generated: 315846
% 19.72/20.11 clauses kept: 58496
% 19.72/20.11 clauses selected: 2999
% 19.72/20.11 clauses deleted: 3482
% 19.72/20.11 clauses inuse deleted: 195
% 19.72/20.11
% 19.72/20.11 subsentry: 1930126
% 19.72/20.11 literals s-matched: 1239030
% 19.72/20.11 literals matched: 1101021
% 19.72/20.11 full subsumption: 115692
% 19.72/20.11
% 19.72/20.11 checksum: -1190623722
% 19.72/20.11
% 19.72/20.11
% 19.72/20.11 Bliksem ended
%------------------------------------------------------------------------------