%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : LAT313+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sun Jul 17 03:50:36 EDT 2022
% Result : Theorem 65.23s 65.59s
% Output : Refutation 65.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : LAT313+1 : TPTP v8.1.0. Released v3.4.0.
% 0.06/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n024.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.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Tue Jun 28 20:39:00 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.44/1.08 *** allocated 10000 integers for termspace/termends
% 0.44/1.08 *** allocated 10000 integers for clauses
% 0.44/1.08 *** allocated 10000 integers for justifications
% 0.44/1.08 Bliksem 1.12
% 0.44/1.08
% 0.44/1.08
% 0.44/1.08 Automatic Strategy Selection
% 0.44/1.08
% 0.44/1.08
% 0.44/1.08 Clauses:
% 0.44/1.08
% 0.44/1.08 { ! v3_struct_0( skol1 ) }.
% 0.44/1.08 { v10_lattices( skol1 ) }.
% 0.44/1.08 { l3_lattices( skol1 ) }.
% 0.44/1.08 { m2_filter_2( skol16, skol1 ) }.
% 0.44/1.08 { v14_lattices( skol1 ) }.
% 0.44/1.08 { r2_hidden( k6_lattices( skol1 ), skol16 ) }.
% 0.44/1.08 { ! r1_filter_2( u1_struct_0( skol1 ), skol16, k17_filter_2( skol1 ) ), !
% 0.44/1.08 skol16 = u1_struct_0( skol1 ) }.
% 0.44/1.08 { ! r2_hidden( X, Y ), ! r2_hidden( Y, X ) }.
% 0.44/1.08 { ! v1_xboole_0( X ), v1_funct_1( X ) }.
% 0.44/1.08 { ! l3_lattices( X ), v3_struct_0( X ), ! v10_lattices( X ), alpha1( X ) }
% 0.44/1.08 .
% 0.44/1.08 { ! l3_lattices( X ), v3_struct_0( X ), ! v10_lattices( X ), v9_lattices( X
% 0.44/1.08 ) }.
% 0.44/1.08 { ! alpha1( X ), alpha2( X ) }.
% 0.44/1.08 { ! alpha1( X ), v8_lattices( X ) }.
% 0.44/1.08 { ! alpha2( X ), ! v8_lattices( X ), alpha1( X ) }.
% 0.44/1.08 { ! alpha2( X ), alpha3( X ) }.
% 0.44/1.08 { ! alpha2( X ), v7_lattices( X ) }.
% 0.44/1.08 { ! alpha3( X ), ! v7_lattices( X ), alpha2( X ) }.
% 0.44/1.08 { ! alpha3( X ), alpha4( X ) }.
% 0.44/1.08 { ! alpha3( X ), v6_lattices( X ) }.
% 0.44/1.08 { ! alpha4( X ), ! v6_lattices( X ), alpha3( X ) }.
% 0.44/1.08 { ! alpha4( X ), ! v3_struct_0( X ) }.
% 0.44/1.08 { ! alpha4( X ), v4_lattices( X ) }.
% 0.44/1.08 { ! alpha4( X ), v5_lattices( X ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v4_lattices( X ), ! v5_lattices( X ), alpha4( X ) }.
% 0.44/1.08 { ! l3_lattices( X ), v3_struct_0( X ), ! v4_lattices( X ), ! v5_lattices(
% 0.44/1.08 X ), ! v6_lattices( X ), ! v7_lattices( X ), ! v8_lattices( X ), !
% 0.44/1.08 v9_lattices( X ), ! v3_struct_0( X ) }.
% 0.44/1.08 { ! l3_lattices( X ), v3_struct_0( X ), ! v4_lattices( X ), ! v5_lattices(
% 0.44/1.08 X ), ! v6_lattices( X ), ! v7_lattices( X ), ! v8_lattices( X ), !
% 0.44/1.08 v9_lattices( X ), v10_lattices( X ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), k17_filter_2(
% 0.44/1.08 X ) = u1_struct_0( X ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m2_filter_2(
% 0.44/1.08 k17_filter_2( X ), X ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), v1_xboole_0( Y
% 0.44/1.08 ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), m2_filter_2(
% 0.44/1.08 k19_filter_2( X, Y ), X ) }.
% 0.44/1.08 { && }.
% 0.44/1.08 { && }.
% 0.44/1.08 { v3_struct_0( X ), ! l2_lattices( X ), m1_subset_1( k6_lattices( X ),
% 0.44/1.08 u1_struct_0( X ) ) }.
% 0.44/1.08 { ! l1_lattices( X ), l1_struct_0( X ) }.
% 0.44/1.08 { && }.
% 0.44/1.08 { ! l2_lattices( X ), l1_struct_0( X ) }.
% 0.44/1.08 { ! l3_lattices( X ), l1_lattices( X ) }.
% 0.44/1.08 { ! l3_lattices( X ), l2_lattices( X ) }.
% 0.44/1.08 { && }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2
% 0.44/1.08 ( Y, X ), ! v1_xboole_0( Y ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2
% 0.44/1.08 ( Y, X ), m2_lattice4( Y, X ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_lattice4
% 0.44/1.08 ( Y, X ), m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.44/1.08 { && }.
% 0.44/1.08 { l1_lattices( skol2 ) }.
% 0.44/1.08 { l1_struct_0( skol3 ) }.
% 0.44/1.08 { l2_lattices( skol4 ) }.
% 0.44/1.08 { l3_lattices( skol5 ) }.
% 0.44/1.08 { m1_subset_1( skol6( X ), X ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m2_filter_2(
% 0.44/1.08 skol7( X ), X ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m2_lattice4(
% 0.44/1.08 skol8( X ), X ) }.
% 0.44/1.08 { v3_struct_0( X ), ! l1_struct_0( X ), ! v1_xboole_0( u1_struct_0( X ) ) }
% 0.44/1.08 .
% 0.44/1.08 { ! v1_xboole_0( k1_zfmisc_1( X ) ) }.
% 0.44/1.08 { v1_xboole_0( k1_xboole_0 ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! v1_xboole_0
% 0.44/1.08 ( skol9( Y ) ) }.
% 0.44/1.08 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), m2_lattice4(
% 0.44/1.08 skol9( X ), X ) }.
% 0.44/1.08 { v1_xboole_0( X ), ! v1_xboole_0( skol10( Y ) ) }.
% 0.44/1.08 { v1_xboole_0( X ), m1_subset_1( skol10( X ), k1_zfmisc_1( X ) ) }.
% 0.44/1.08 { v1_xboole_0( skol11 ) }.
% 0.44/1.08 { v1_xboole_0( skol12( Y ) ) }.
% 0.44/1.08 { m1_subset_1( skol12( X ), k1_zfmisc_1( X ) ) }.
% 0.44/1.08 { ! v1_xboole_0( skol13 ) }.
% 0.44/1.08 { l1_struct_0( skol14 ) }.
% 0.44/1.08 { ! v3_struct_0( skol14 ) }.
% 0.44/1.08 { v3_struct_0( X ), ! l1_struct_0( X ), ! v1_xboole_0( skol15( Y ) ) }.
% 0.44/1.08 { v3_struct_0( X ), ! l1_struct_0( X ), m1_subset_1( skol15( X ),
% 0.44/1.08 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 0.44/1.08 { v1_xboole_0( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z
% 0.44/1.08 , k1_zfmisc_1( X ) ), ! r1_filter_2( X, Y, Z ), Y = Z }.
% 0.44/1.08 { v1_xboole_0( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z
% 0.44/1.08 , k1_zfmisc_1( X ) ), ! Y = Z, r1_filter_2( X, Y, Z ) }.
% 3.76/4.14 { v1_xboole_0( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z
% 3.76/4.14 , k1_zfmisc_1( X ) ), r1_filter_2( X, Y, Y ) }.
% 3.76/4.14 { r1_tarski( X, X ) }.
% 3.76/4.14 { v1_xboole_0( X ), ! m1_subset_1( Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z
% 3.76/4.14 , k1_zfmisc_1( X ) ), ! r1_filter_2( X, Y, Z ), r1_filter_2( X, Z, Y ) }
% 3.76/4.14 .
% 3.76/4.14 { ! r2_hidden( X, Y ), m1_subset_1( X, Y ) }.
% 3.76/4.14 { ! m1_subset_1( X, Y ), v1_xboole_0( Y ), r2_hidden( X, Y ) }.
% 3.76/4.14 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), ! m2_filter_2
% 3.76/4.14 ( Y, X ), r1_filter_2( u1_struct_0( X ), k19_filter_2( X, Y ), Y ) }.
% 3.76/4.14 { ! m1_subset_1( X, k1_zfmisc_1( Y ) ), r1_tarski( X, Y ) }.
% 3.76/4.14 { ! r1_tarski( X, Y ), m1_subset_1( X, k1_zfmisc_1( Y ) ) }.
% 3.76/4.14 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), v1_xboole_0( Y
% 3.76/4.14 ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v14_lattices(
% 3.76/4.14 X ), ! r2_hidden( k6_lattices( X ), Y ), r1_filter_2( u1_struct_0( X ),
% 3.76/4.14 k19_filter_2( X, Y ), k17_filter_2( X ) ) }.
% 3.76/4.14 { v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ), v1_xboole_0( Y
% 3.76/4.14 ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), ! v14_lattices(
% 3.76/4.14 X ), ! r2_hidden( k6_lattices( X ), Y ), k19_filter_2( X, Y ) =
% 3.76/4.14 u1_struct_0( X ) }.
% 3.76/4.14 { ! r2_hidden( X, Z ), ! m1_subset_1( Z, k1_zfmisc_1( Y ) ), m1_subset_1( X
% 3.76/4.14 , Y ) }.
% 3.76/4.14 { ! r2_hidden( X, Y ), ! m1_subset_1( Y, k1_zfmisc_1( Z ) ), ! v1_xboole_0
% 3.76/4.14 ( Z ) }.
% 3.76/4.14 { ! v1_xboole_0( X ), X = k1_xboole_0 }.
% 3.76/4.14 { ! r2_hidden( X, Y ), ! v1_xboole_0( Y ) }.
% 3.76/4.14 { ! v1_xboole_0( X ), X = Y, ! v1_xboole_0( Y ) }.
% 3.76/4.14
% 3.76/4.14 percentage equality = 0.033981, percentage horn = 0.697368
% 3.76/4.14 This is a problem with some equality
% 3.76/4.14
% 3.76/4.14
% 3.76/4.14
% 3.76/4.14 Options Used:
% 3.76/4.14
% 3.76/4.14 useres = 1
% 3.76/4.14 useparamod = 1
% 3.76/4.14 useeqrefl = 1
% 3.76/4.14 useeqfact = 1
% 3.76/4.14 usefactor = 1
% 3.76/4.14 usesimpsplitting = 0
% 3.76/4.14 usesimpdemod = 5
% 3.76/4.14 usesimpres = 3
% 3.76/4.14
% 3.76/4.14 resimpinuse = 1000
% 3.76/4.14 resimpclauses = 20000
% 3.76/4.14 substype = eqrewr
% 3.76/4.14 backwardsubs = 1
% 3.76/4.14 selectoldest = 5
% 3.76/4.14
% 3.76/4.14 litorderings [0] = split
% 3.76/4.14 litorderings [1] = extend the termordering, first sorting on arguments
% 3.76/4.14
% 3.76/4.14 termordering = kbo
% 3.76/4.14
% 3.76/4.14 litapriori = 0
% 3.76/4.14 termapriori = 1
% 3.76/4.14 litaposteriori = 0
% 3.76/4.14 termaposteriori = 0
% 3.76/4.14 demodaposteriori = 0
% 3.76/4.14 ordereqreflfact = 0
% 3.76/4.14
% 3.76/4.14 litselect = negord
% 3.76/4.14
% 3.76/4.14 maxweight = 15
% 3.76/4.14 maxdepth = 30000
% 3.76/4.14 maxlength = 115
% 3.76/4.14 maxnrvars = 195
% 3.76/4.14 excuselevel = 1
% 3.76/4.14 increasemaxweight = 1
% 3.76/4.14
% 3.76/4.14 maxselected = 10000000
% 3.76/4.14 maxnrclauses = 10000000
% 3.76/4.14
% 3.76/4.14 showgenerated = 0
% 3.76/4.14 showkept = 0
% 3.76/4.14 showselected = 0
% 3.76/4.14 showdeleted = 0
% 3.76/4.14 showresimp = 1
% 3.76/4.14 showstatus = 2000
% 3.76/4.14
% 3.76/4.14 prologoutput = 0
% 3.76/4.14 nrgoals = 5000000
% 3.76/4.14 totalproof = 1
% 3.76/4.14
% 3.76/4.14 Symbols occurring in the translation:
% 3.76/4.14
% 3.76/4.14 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.76/4.14 . [1, 2] (w:1, o:54, a:1, s:1, b:0),
% 3.76/4.14 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 3.76/4.14 ! [4, 1] (w:0, o:19, a:1, s:1, b:0),
% 3.76/4.14 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.76/4.14 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.76/4.14 v3_struct_0 [36, 1] (w:1, o:25, a:1, s:1, b:0),
% 3.76/4.14 v10_lattices [37, 1] (w:1, o:26, a:1, s:1, b:0),
% 3.76/4.14 l3_lattices [38, 1] (w:1, o:33, a:1, s:1, b:0),
% 3.76/4.14 m2_filter_2 [40, 2] (w:1, o:79, a:1, s:1, b:0),
% 3.76/4.14 v14_lattices [41, 1] (w:1, o:34, a:1, s:1, b:0),
% 3.76/4.14 k6_lattices [42, 1] (w:1, o:27, a:1, s:1, b:0),
% 3.76/4.14 r2_hidden [43, 2] (w:1, o:81, a:1, s:1, b:0),
% 3.76/4.14 u1_struct_0 [44, 1] (w:1, o:24, a:1, s:1, b:0),
% 3.76/4.14 k17_filter_2 [45, 1] (w:1, o:28, a:1, s:1, b:0),
% 3.76/4.14 r1_filter_2 [46, 3] (w:1, o:84, a:1, s:1, b:0),
% 3.76/4.14 v1_xboole_0 [47, 1] (w:1, o:35, a:1, s:1, b:0),
% 3.76/4.14 v1_funct_1 [48, 1] (w:1, o:36, a:1, s:1, b:0),
% 3.76/4.14 v4_lattices [49, 1] (w:1, o:37, a:1, s:1, b:0),
% 3.76/4.14 v5_lattices [50, 1] (w:1, o:38, a:1, s:1, b:0),
% 3.76/4.14 v6_lattices [51, 1] (w:1, o:39, a:1, s:1, b:0),
% 3.76/4.14 v7_lattices [52, 1] (w:1, o:40, a:1, s:1, b:0),
% 3.76/4.14 v8_lattices [53, 1] (w:1, o:41, a:1, s:1, b:0),
% 3.76/4.14 v9_lattices [54, 1] (w:1, o:42, a:1, s:1, b:0),
% 3.76/4.14 k1_zfmisc_1 [55, 1] (w:1, o:29, a:1, s:1, b:0),
% 3.76/4.14 m1_subset_1 [56, 2] (w:1, o:78, a:1, s:1, b:0),
% 3.76/4.14 k19_filter_2 [57, 2] (w:1, o:82, a:1, s:1, b:0),
% 65.23/65.59 l2_lattices [58, 1] (w:1, o:32, a:1, s:1, b:0),
% 65.23/65.59 l1_lattices [59, 1] (w:1, o:30, a:1, s:1, b:0),
% 65.23/65.59 l1_struct_0 [60, 1] (w:1, o:31, a:1, s:1, b:0),
% 65.23/65.59 m2_lattice4 [61, 2] (w:1, o:83, a:1, s:1, b:0),
% 65.23/65.59 k1_xboole_0 [62, 0] (w:1, o:8, a:1, s:1, b:0),
% 65.23/65.59 r1_tarski [64, 2] (w:1, o:80, a:1, s:1, b:0),
% 65.23/65.59 alpha1 [65, 1] (w:1, o:43, a:1, s:1, b:1),
% 65.23/65.59 alpha2 [66, 1] (w:1, o:44, a:1, s:1, b:1),
% 65.23/65.59 alpha3 [67, 1] (w:1, o:45, a:1, s:1, b:1),
% 65.23/65.59 alpha4 [68, 1] (w:1, o:46, a:1, s:1, b:1),
% 65.23/65.59 skol1 [69, 0] (w:1, o:10, a:1, s:1, b:1),
% 65.23/65.59 skol2 [70, 0] (w:1, o:15, a:1, s:1, b:1),
% 65.23/65.59 skol3 [71, 0] (w:1, o:16, a:1, s:1, b:1),
% 65.23/65.59 skol4 [72, 0] (w:1, o:17, a:1, s:1, b:1),
% 65.23/65.59 skol5 [73, 0] (w:1, o:18, a:1, s:1, b:1),
% 65.23/65.59 skol6 [74, 1] (w:1, o:47, a:1, s:1, b:1),
% 65.23/65.59 skol7 [75, 1] (w:1, o:48, a:1, s:1, b:1),
% 65.23/65.59 skol8 [76, 1] (w:1, o:49, a:1, s:1, b:1),
% 65.23/65.59 skol9 [77, 1] (w:1, o:50, a:1, s:1, b:1),
% 65.23/65.59 skol10 [78, 1] (w:1, o:51, a:1, s:1, b:1),
% 65.23/65.59 skol11 [79, 0] (w:1, o:11, a:1, s:1, b:1),
% 65.23/65.59 skol12 [80, 1] (w:1, o:52, a:1, s:1, b:1),
% 65.23/65.59 skol13 [81, 0] (w:1, o:12, a:1, s:1, b:1),
% 65.23/65.59 skol14 [82, 0] (w:1, o:13, a:1, s:1, b:1),
% 65.23/65.59 skol15 [83, 1] (w:1, o:53, a:1, s:1, b:1),
% 65.23/65.59 skol16 [84, 0] (w:1, o:14, a:1, s:1, b:1).
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Starting Search:
% 65.23/65.59
% 65.23/65.59 *** allocated 15000 integers for clauses
% 65.23/65.59 *** allocated 22500 integers for clauses
% 65.23/65.59 *** allocated 33750 integers for clauses
% 65.23/65.59 *** allocated 15000 integers for termspace/termends
% 65.23/65.59 *** allocated 50625 integers for clauses
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 22500 integers for termspace/termends
% 65.23/65.59 *** allocated 75937 integers for clauses
% 65.23/65.59 *** allocated 33750 integers for termspace/termends
% 65.23/65.59 *** allocated 113905 integers for clauses
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 6646
% 65.23/65.59 Kept: 2001
% 65.23/65.59 Inuse: 304
% 65.23/65.59 Deleted: 21
% 65.23/65.59 Deletedinuse: 9
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 50625 integers for termspace/termends
% 65.23/65.59 *** allocated 170857 integers for clauses
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 17549
% 65.23/65.59 Kept: 4004
% 65.23/65.59 Inuse: 527
% 65.23/65.59 Deleted: 67
% 65.23/65.59 Deletedinuse: 19
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 256285 integers for clauses
% 65.23/65.59 *** allocated 75937 integers for termspace/termends
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 29665
% 65.23/65.59 Kept: 6014
% 65.23/65.59 Inuse: 731
% 65.23/65.59 Deleted: 98
% 65.23/65.59 Deletedinuse: 22
% 65.23/65.59
% 65.23/65.59 *** allocated 384427 integers for clauses
% 65.23/65.59 *** allocated 113905 integers for termspace/termends
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 41356
% 65.23/65.59 Kept: 8017
% 65.23/65.59 Inuse: 854
% 65.23/65.59 Deleted: 158
% 65.23/65.59 Deletedinuse: 28
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 170857 integers for termspace/termends
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 576640 integers for clauses
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 52364
% 65.23/65.59 Kept: 10018
% 65.23/65.59 Inuse: 974
% 65.23/65.59 Deleted: 167
% 65.23/65.59 Deletedinuse: 31
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 63126
% 65.23/65.59 Kept: 12280
% 65.23/65.59 Inuse: 1086
% 65.23/65.59 Deleted: 220
% 65.23/65.59 Deletedinuse: 31
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 256285 integers for termspace/termends
% 65.23/65.59 *** allocated 864960 integers for clauses
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 70964
% 65.23/65.59 Kept: 14290
% 65.23/65.59 Inuse: 1164
% 65.23/65.59 Deleted: 222
% 65.23/65.59 Deletedinuse: 32
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 81085
% 65.23/65.59 Kept: 16324
% 65.23/65.59 Inuse: 1272
% 65.23/65.59 Deleted: 246
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 93739
% 65.23/65.59 Kept: 18850
% 65.23/65.59 Inuse: 1311
% 65.23/65.59 Deleted: 273
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying clauses:
% 65.23/65.59 *** allocated 384427 integers for termspace/termends
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 104936
% 65.23/65.59 Kept: 20858
% 65.23/65.59 Inuse: 1344
% 65.23/65.59 Deleted: 2672
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 *** allocated 1297440 integers for clauses
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 111672
% 65.23/65.59 Kept: 22859
% 65.23/65.59 Inuse: 1397
% 65.23/65.59 Deleted: 2673
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 160989
% 65.23/65.59 Kept: 24880
% 65.23/65.59 Inuse: 1502
% 65.23/65.59 Deleted: 2673
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 186012
% 65.23/65.59 Kept: 27070
% 65.23/65.59 Inuse: 1517
% 65.23/65.59 Deleted: 2673
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 576640 integers for termspace/termends
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 238953
% 65.23/65.59 Kept: 31416
% 65.23/65.59 Inuse: 1542
% 65.23/65.59 Deleted: 2673
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 1946160 integers for clauses
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 285057
% 65.23/65.59 Kept: 36119
% 65.23/65.59 Inuse: 1572
% 65.23/65.59 Deleted: 2673
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 321168
% 65.23/65.59 Kept: 38668
% 65.23/65.59 Inuse: 1585
% 65.23/65.59 Deleted: 2673
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 363232
% 65.23/65.59 Kept: 40847
% 65.23/65.59 Inuse: 1689
% 65.23/65.59 Deleted: 2677
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying clauses:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 864960 integers for termspace/termends
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 378144
% 65.23/65.59 Kept: 42853
% 65.23/65.59 Inuse: 1730
% 65.23/65.59 Deleted: 3890
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 396332
% 65.23/65.59 Kept: 44908
% 65.23/65.59 Inuse: 1761
% 65.23/65.59 Deleted: 3890
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 414696
% 65.23/65.59 Kept: 46983
% 65.23/65.59 Inuse: 1807
% 65.23/65.59 Deleted: 3890
% 65.23/65.59 Deletedinuse: 56
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 *** allocated 2919240 integers for clauses
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 437756
% 65.23/65.59 Kept: 49011
% 65.23/65.59 Inuse: 1857
% 65.23/65.59 Deleted: 3894
% 65.23/65.59 Deletedinuse: 60
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 460739
% 65.23/65.59 Kept: 51030
% 65.23/65.59 Inuse: 1898
% 65.23/65.59 Deleted: 3894
% 65.23/65.59 Deletedinuse: 60
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 487567
% 65.23/65.59 Kept: 53051
% 65.23/65.59 Inuse: 1955
% 65.23/65.59 Deleted: 3894
% 65.23/65.59 Deletedinuse: 60
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 509413
% 65.23/65.59 Kept: 55059
% 65.23/65.59 Inuse: 1996
% 65.23/65.59 Deleted: 3894
% 65.23/65.59 Deletedinuse: 60
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 535206
% 65.23/65.59 Kept: 57154
% 65.23/65.59 Inuse: 2045
% 65.23/65.59 Deleted: 3900
% 65.23/65.59 Deletedinuse: 60
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59
% 65.23/65.59 Intermediate Status:
% 65.23/65.59 Generated: 551216
% 65.23/65.59 Kept: 59176
% 65.23/65.59 Inuse: 2076
% 65.23/65.59 Deleted: 3900
% 65.23/65.59 Deletedinuse: 60
% 65.23/65.59
% 65.23/65.59 Resimplifying inuse:
% 65.23/65.59 Done
% 65.23/65.59
% 65.23/65.59 Resimplifying clauses:
% 65.23/65.59
% 65.23/65.59 Bliksems!, er is een bewijs:
% 65.23/65.59 % SZS status Theorem
% 65.23/65.59 % SZS output start Refutation
% 65.23/65.59
% 65.23/65.59 (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.59 (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 65.23/65.59 (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 65.23/65.59 (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol16, skol1 ) }.
% 65.23/65.59 (4) {G0,W2,D2,L1,V0,M1} I { v14_lattices( skol1 ) }.
% 65.23/65.59 (5) {G0,W4,D3,L1,V0,M1} I { r2_hidden( k6_lattices( skol1 ), skol16 ) }.
% 65.23/65.59 (6) {G0,W10,D3,L2,V0,M2} I { ! r1_filter_2( u1_struct_0( skol1 ), skol16,
% 65.23/65.59 k17_filter_2( skol1 ) ), ! u1_struct_0( skol1 ) ==> skol16 }.
% 65.23/65.59 (9) {G0,W8,D2,L4,V1,M4} I { ! l3_lattices( X ), v3_struct_0( X ), !
% 65.23/65.59 v10_lattices( X ), alpha1( X ) }.
% 65.23/65.59 (11) {G0,W4,D2,L2,V1,M2} I { ! alpha1( X ), alpha2( X ) }.
% 65.23/65.59 (14) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha3( X ) }.
% 65.23/65.59 (17) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha4( X ) }.
% 65.23/65.59 (20) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), ! v3_struct_0( X ) }.
% 65.23/65.59 (25) {G0,W11,D3,L4,V1,M4} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.59 l3_lattices( X ), k17_filter_2( X ) ==> u1_struct_0( X ) }.
% 65.23/65.59 (29) {G0,W9,D3,L3,V1,M3} I { v3_struct_0( X ), ! l2_lattices( X ),
% 65.23/65.59 m1_subset_1( k6_lattices( X ), u1_struct_0( X ) ) }.
% 65.23/65.59 (31) {G0,W4,D2,L2,V1,M2} I { ! l2_lattices( X ), l1_struct_0( X ) }.
% 65.23/65.59 (33) {G0,W4,D2,L2,V1,M2} I { ! l3_lattices( X ), l2_lattices( X ) }.
% 65.23/65.59 (35) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.59 l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 65.23/65.59 (36) {G0,W14,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.59 l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y, k1_zfmisc_1(
% 65.23/65.59 u1_struct_0( X ) ) ) }.
% 65.23/65.59 (41) {G0,W4,D3,L1,V1,M1} I { m1_subset_1( skol6( X ), X ) }.
% 65.23/65.59 (44) {G0,W7,D3,L3,V1,M3} I { v3_struct_0( X ), ! l1_struct_0( X ), !
% 65.23/65.59 v1_xboole_0( u1_struct_0( X ) ) }.
% 65.23/65.59 (46) {G0,W2,D2,L1,V0,M1} I { v1_xboole_0( k1_xboole_0 ) }.
% 65.23/65.59 (52) {G0,W3,D3,L1,V1,M1} I { v1_xboole_0( skol12( Y ) ) }.
% 65.23/65.59 (53) {G0,W5,D3,L1,V1,M1} I { m1_subset_1( skol12( X ), k1_zfmisc_1( X ) )
% 65.23/65.59 }.
% 65.23/65.59 (59) {G0,W17,D3,L5,V3,M5} I { v1_xboole_0( X ), ! m1_subset_1( Y,
% 65.23/65.59 k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! r1_filter_2(
% 65.23/65.59 X, Y, Z ), Y = Z }.
% 65.23/65.59 (60) {G0,W17,D3,L5,V3,M5} I { v1_xboole_0( X ), ! m1_subset_1( Y,
% 65.23/65.59 k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! Y = Z,
% 65.23/65.59 r1_filter_2( X, Y, Z ) }.
% 65.23/65.59 (62) {G0,W3,D2,L1,V1,M1} I { r1_tarski( X, X ) }.
% 65.23/65.59 (65) {G0,W8,D2,L3,V2,M3} I { ! m1_subset_1( X, Y ), v1_xboole_0( Y ),
% 65.23/65.59 r2_hidden( X, Y ) }.
% 65.23/65.59 (66) {G0,W16,D3,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.59 l3_lattices( X ), ! m2_filter_2( Y, X ), r1_filter_2( u1_struct_0( X ),
% 65.23/65.59 k19_filter_2( X, Y ), Y ) }.
% 65.23/65.59 (68) {G0,W7,D3,L2,V2,M2} I { ! r1_tarski( X, Y ), m1_subset_1( X,
% 65.23/65.59 k1_zfmisc_1( Y ) ) }.
% 65.23/65.59 (70) {G0,W25,D4,L8,V2,M8} I { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.59 l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y, k1_zfmisc_1(
% 65.23/65.59 u1_struct_0( X ) ) ), ! v14_lattices( X ), ! r2_hidden( k6_lattices( X )
% 65.23/65.59 , Y ), k19_filter_2( X, Y ) ==> u1_struct_0( X ) }.
% 65.23/65.59 (72) {G0,W9,D3,L3,V3,M3} I { ! r2_hidden( X, Y ), ! m1_subset_1( Y,
% 65.23/65.59 k1_zfmisc_1( Z ) ), ! v1_xboole_0( Z ) }.
% 65.23/65.59 (73) {G0,W5,D2,L2,V1,M2} I { ! v1_xboole_0( X ), X = k1_xboole_0 }.
% 65.23/65.59 (74) {G0,W5,D2,L2,V2,M2} I { ! r2_hidden( X, Y ), ! v1_xboole_0( Y ) }.
% 65.23/65.60 (78) {G1,W2,D2,L1,V0,M1} R(33,2) { l2_lattices( skol1 ) }.
% 65.23/65.60 (83) {G2,W2,D2,L1,V0,M1} R(31,78) { l1_struct_0( skol1 ) }.
% 65.23/65.60 (91) {G1,W4,D2,L2,V0,M2} R(9,2);r(0) { ! v10_lattices( skol1 ), alpha1(
% 65.23/65.60 skol1 ) }.
% 65.23/65.60 (109) {G1,W4,D2,L2,V1,M2} R(14,11) { alpha3( X ), ! alpha1( X ) }.
% 65.23/65.60 (118) {G2,W4,D2,L2,V1,M2} R(109,17) { ! alpha1( X ), alpha4( X ) }.
% 65.23/65.60 (132) {G2,W2,D2,L1,V0,M1} S(91);r(1) { alpha1( skol1 ) }.
% 65.23/65.60 (134) {G3,W2,D2,L1,V0,M1} R(132,118) { alpha4( skol1 ) }.
% 65.23/65.60 (153) {G1,W7,D3,L2,V0,M2} R(25,2);r(0) { ! v10_lattices( skol1 ),
% 65.23/65.60 k17_filter_2( skol1 ) ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 (158) {G1,W2,D2,L1,V0,M1} R(74,5) { ! v1_xboole_0( skol16 ) }.
% 65.23/65.60 (170) {G1,W4,D3,L1,V1,M1} R(73,52) { skol12( X ) ==> k1_xboole_0 }.
% 65.23/65.60 (232) {G2,W5,D3,L1,V0,M1} R(29,78);r(0) { m1_subset_1( k6_lattices( skol1 )
% 65.23/65.60 , u1_struct_0( skol1 ) ) }.
% 65.23/65.60 (267) {G1,W7,D2,L3,V0,M3} R(35,3);r(0) { ! v10_lattices( skol1 ), !
% 65.23/65.60 l3_lattices( skol1 ), m2_lattice4( skol16, skol1 ) }.
% 65.23/65.60 (291) {G1,W14,D4,L5,V2,M5} R(36,20) { ! v10_lattices( X ), ! l3_lattices( X
% 65.23/65.60 ), ! m2_lattice4( Y, X ), m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X )
% 65.23/65.60 ) ), ! alpha4( X ) }.
% 65.23/65.60 (378) {G3,W3,D3,L1,V0,M1} R(44,83);r(0) { ! v1_xboole_0( u1_struct_0( skol1
% 65.23/65.60 ) ) }.
% 65.23/65.60 (385) {G2,W4,D3,L1,V1,M1} S(53);d(170) { m1_subset_1( k1_xboole_0,
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 (531) {G1,W18,D3,L5,V3,M5} R(59,73) { ! m1_subset_1( X, k1_zfmisc_1( Y ) )
% 65.23/65.60 , ! m1_subset_1( Z, k1_zfmisc_1( Y ) ), ! r1_filter_2( Y, X, Z ), X = Z,
% 65.23/65.60 Y = k1_xboole_0 }.
% 65.23/65.60 (988) {G4,W5,D3,L1,V0,M1} R(65,232);r(378) { r2_hidden( k6_lattices( skol1
% 65.23/65.60 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 (1028) {G1,W6,D3,L2,V1,M2} R(65,41) { v1_xboole_0( X ), r2_hidden( skol6( X
% 65.23/65.60 ), X ) }.
% 65.23/65.60 (1111) {G1,W11,D3,L3,V0,M3} R(66,3);r(0) { ! v10_lattices( skol1 ), !
% 65.23/65.60 l3_lattices( skol1 ), r1_filter_2( u1_struct_0( skol1 ), k19_filter_2(
% 65.23/65.60 skol1, skol16 ), skol16 ) }.
% 65.23/65.60 (1183) {G1,W4,D3,L1,V1,M1} R(68,62) { m1_subset_1( X, k1_zfmisc_1( X ) )
% 65.23/65.60 }.
% 65.23/65.60 (1190) {G2,W13,D3,L4,V2,M4} R(1183,60) { v1_xboole_0( X ), ! m1_subset_1( Y
% 65.23/65.60 , k1_zfmisc_1( X ) ), ! Y = X, r1_filter_2( X, Y, X ) }.
% 65.23/65.60 (1194) {G3,W6,D2,L2,V1,M2} Q(1190);r(1183) { v1_xboole_0( X ), r1_filter_2
% 65.23/65.60 ( X, X, X ) }.
% 65.23/65.60 (1235) {G1,W19,D4,L6,V0,M6} R(70,5);r(0) { ! v10_lattices( skol1 ), !
% 65.23/65.60 l3_lattices( skol1 ), v1_xboole_0( skol16 ), ! m1_subset_1( skol16,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! v14_lattices( skol1 ),
% 65.23/65.60 k19_filter_2( skol1, skol16 ) ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 (1348) {G1,W7,D3,L2,V2,M2} R(72,46) { ! r2_hidden( X, Y ), ! m1_subset_1( Y
% 65.23/65.60 , k1_zfmisc_1( k1_xboole_0 ) ) }.
% 65.23/65.60 (1565) {G5,W7,D3,L2,V1,M2} R(988,72) { ! m1_subset_1( u1_struct_0( skol1 )
% 65.23/65.60 , k1_zfmisc_1( X ) ), ! v1_xboole_0( X ) }.
% 65.23/65.60 (1654) {G4,W4,D2,L1,V0,M1} R(1194,158) { r1_filter_2( skol16, skol16,
% 65.23/65.60 skol16 ) }.
% 65.23/65.60 (2763) {G2,W5,D3,L1,V0,M1} S(153);r(1) { k17_filter_2( skol1 ) ==>
% 65.23/65.60 u1_struct_0( skol1 ) }.
% 65.23/65.60 (2767) {G3,W10,D3,L2,V0,M2} P(2763,6) { ! r1_filter_2( u1_struct_0( skol1 )
% 65.23/65.60 , skol16, u1_struct_0( skol1 ) ), ! u1_struct_0( skol1 ) ==> skol16 }.
% 65.23/65.60 (3566) {G4,W6,D4,L1,V0,M1} R(1028,378) { r2_hidden( skol6( u1_struct_0(
% 65.23/65.60 skol1 ) ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 (5323) {G2,W3,D2,L1,V0,M1} S(267);r(1);r(2) { m2_lattice4( skol16, skol1 )
% 65.23/65.60 }.
% 65.23/65.60 (6417) {G3,W9,D4,L3,V0,M3} R(291,5323);r(1) { ! l3_lattices( skol1 ),
% 65.23/65.60 m1_subset_1( skol16, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! alpha4(
% 65.23/65.60 skol1 ) }.
% 65.23/65.60 (8364) {G5,W5,D3,L1,V0,M1} R(1348,3566) { ! m1_subset_1( u1_struct_0( skol1
% 65.23/65.60 ), k1_zfmisc_1( k1_xboole_0 ) ) }.
% 65.23/65.60 (8411) {G6,W15,D3,L4,V2,M4} P(59,8364);r(385) { ! m1_subset_1( u1_struct_0
% 65.23/65.60 ( skol1 ), k1_zfmisc_1( X ) ), v1_xboole_0( Y ), ! m1_subset_1( X,
% 65.23/65.60 k1_zfmisc_1( Y ) ), ! r1_filter_2( Y, k1_xboole_0, X ) }.
% 65.23/65.60 (8415) {G7,W9,D3,L2,V0,M2} F(8411);r(1183) { v1_xboole_0( u1_struct_0(
% 65.23/65.60 skol1 ) ), ! r1_filter_2( u1_struct_0( skol1 ), k1_xboole_0, u1_struct_0
% 65.23/65.60 ( skol1 ) ) }.
% 65.23/65.60 (20561) {G8,W6,D3,L1,V0,M1} S(8415);r(378) { ! r1_filter_2( u1_struct_0(
% 65.23/65.60 skol1 ), k1_xboole_0, u1_struct_0( skol1 ) ) }.
% 65.23/65.60 (20638) {G4,W5,D4,L1,V0,M1} S(6417);r(2);r(134) { m1_subset_1( skol16,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( skol1 ) ) ) }.
% 65.23/65.60 (20764) {G5,W6,D3,L1,V0,M1} S(1235);r(1);r(2);r(158);r(20638);r(4) {
% 65.23/65.60 k19_filter_2( skol1, skol16 ) ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 (20767) {G6,W8,D3,L2,V0,M2} S(1111);d(20764);r(1) { ! l3_lattices( skol1 )
% 65.23/65.60 , r1_filter_2( u1_struct_0( skol1 ), u1_struct_0( skol1 ), skol16 ) }.
% 65.23/65.60 (23565) {G9,W15,D4,L3,V0,M3} R(20561,60);r(1565) { ! m1_subset_1(
% 65.23/65.60 k1_xboole_0, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! m1_subset_1(
% 65.23/65.60 u1_struct_0( skol1 ), k1_zfmisc_1( u1_struct_0( skol1 ) ) ), !
% 65.23/65.60 u1_struct_0( skol1 ) ==> k1_xboole_0 }.
% 65.23/65.60 (40916) {G10,W4,D3,L1,V0,M1} S(23565);r(385);r(1183) { ! u1_struct_0( skol1
% 65.23/65.60 ) ==> k1_xboole_0 }.
% 65.23/65.60 (40985) {G7,W6,D3,L1,V0,M1} S(20767);r(2) { r1_filter_2( u1_struct_0( skol1
% 65.23/65.60 ), u1_struct_0( skol1 ), skol16 ) }.
% 65.23/65.60 (44581) {G8,W13,D4,L3,V0,M3} R(40985,531);r(1183) { ! m1_subset_1( skol16,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( skol1 ) ) ), u1_struct_0( skol1 ) ==> skol16,
% 65.23/65.60 u1_struct_0( skol1 ) ==> k1_xboole_0 }.
% 65.23/65.60 (61113) {G11,W4,D3,L1,V0,M1} S(44581);r(20638);r(40916) { u1_struct_0(
% 65.23/65.60 skol1 ) ==> skol16 }.
% 65.23/65.60 (61357) {G12,W0,D0,L0,V0,M0} S(2767);d(61113);d(61113);q;r(1654) { }.
% 65.23/65.60
% 65.23/65.60
% 65.23/65.60 % SZS output end Refutation
% 65.23/65.60 found a proof!
% 65.23/65.60
% 65.23/65.60
% 65.23/65.60 Unprocessed initial clauses:
% 65.23/65.60
% 65.23/65.60 (61359) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 (61360) {G0,W2,D2,L1,V0,M1} { v10_lattices( skol1 ) }.
% 65.23/65.60 (61361) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol1 ) }.
% 65.23/65.60 (61362) {G0,W3,D2,L1,V0,M1} { m2_filter_2( skol16, skol1 ) }.
% 65.23/65.60 (61363) {G0,W2,D2,L1,V0,M1} { v14_lattices( skol1 ) }.
% 65.23/65.60 (61364) {G0,W4,D3,L1,V0,M1} { r2_hidden( k6_lattices( skol1 ), skol16 )
% 65.23/65.60 }.
% 65.23/65.60 (61365) {G0,W10,D3,L2,V0,M2} { ! r1_filter_2( u1_struct_0( skol1 ), skol16
% 65.23/65.60 , k17_filter_2( skol1 ) ), ! skol16 = u1_struct_0( skol1 ) }.
% 65.23/65.60 (61366) {G0,W6,D2,L2,V2,M2} { ! r2_hidden( X, Y ), ! r2_hidden( Y, X ) }.
% 65.23/65.60 (61367) {G0,W4,D2,L2,V1,M2} { ! v1_xboole_0( X ), v1_funct_1( X ) }.
% 65.23/65.60 (61368) {G0,W8,D2,L4,V1,M4} { ! l3_lattices( X ), v3_struct_0( X ), !
% 65.23/65.60 v10_lattices( X ), alpha1( X ) }.
% 65.23/65.60 (61369) {G0,W8,D2,L4,V1,M4} { ! l3_lattices( X ), v3_struct_0( X ), !
% 65.23/65.60 v10_lattices( X ), v9_lattices( X ) }.
% 65.23/65.60 (61370) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), alpha2( X ) }.
% 65.23/65.60 (61371) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), v8_lattices( X ) }.
% 65.23/65.60 (61372) {G0,W6,D2,L3,V1,M3} { ! alpha2( X ), ! v8_lattices( X ), alpha1( X
% 65.23/65.60 ) }.
% 65.23/65.60 (61373) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha3( X ) }.
% 65.23/65.60 (61374) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), v7_lattices( X ) }.
% 65.23/65.60 (61375) {G0,W6,D2,L3,V1,M3} { ! alpha3( X ), ! v7_lattices( X ), alpha2( X
% 65.23/65.60 ) }.
% 65.23/65.60 (61376) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha4( X ) }.
% 65.23/65.60 (61377) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), v6_lattices( X ) }.
% 65.23/65.60 (61378) {G0,W6,D2,L3,V1,M3} { ! alpha4( X ), ! v6_lattices( X ), alpha3( X
% 65.23/65.60 ) }.
% 65.23/65.60 (61379) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), ! v3_struct_0( X ) }.
% 65.23/65.60 (61380) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v4_lattices( X ) }.
% 65.23/65.60 (61381) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), v5_lattices( X ) }.
% 65.23/65.60 (61382) {G0,W8,D2,L4,V1,M4} { v3_struct_0( X ), ! v4_lattices( X ), !
% 65.23/65.60 v5_lattices( X ), alpha4( X ) }.
% 65.23/65.60 (61383) {G0,W18,D2,L9,V1,M9} { ! l3_lattices( X ), v3_struct_0( X ), !
% 65.23/65.60 v4_lattices( X ), ! v5_lattices( X ), ! v6_lattices( X ), ! v7_lattices(
% 65.23/65.60 X ), ! v8_lattices( X ), ! v9_lattices( X ), ! v3_struct_0( X ) }.
% 65.23/65.60 (61384) {G0,W18,D2,L9,V1,M9} { ! l3_lattices( X ), v3_struct_0( X ), !
% 65.23/65.60 v4_lattices( X ), ! v5_lattices( X ), ! v6_lattices( X ), ! v7_lattices(
% 65.23/65.60 X ), ! v8_lattices( X ), ! v9_lattices( X ), v10_lattices( X ) }.
% 65.23/65.60 (61385) {G0,W11,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), k17_filter_2( X ) = u1_struct_0( X ) }.
% 65.23/65.60 (61386) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), m2_filter_2( k17_filter_2( X ), X ) }.
% 65.23/65.60 (61387) {G0,W18,D4,L6,V2,M6} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y, k1_zfmisc_1(
% 65.23/65.60 u1_struct_0( X ) ) ), m2_filter_2( k19_filter_2( X, Y ), X ) }.
% 65.23/65.60 (61388) {G0,W1,D1,L1,V0,M1} { && }.
% 65.23/65.60 (61389) {G0,W1,D1,L1,V0,M1} { && }.
% 65.23/65.60 (61390) {G0,W9,D3,L3,V1,M3} { v3_struct_0( X ), ! l2_lattices( X ),
% 65.23/65.60 m1_subset_1( k6_lattices( X ), u1_struct_0( X ) ) }.
% 65.23/65.60 (61391) {G0,W4,D2,L2,V1,M2} { ! l1_lattices( X ), l1_struct_0( X ) }.
% 65.23/65.60 (61392) {G0,W1,D1,L1,V0,M1} { && }.
% 65.23/65.60 (61393) {G0,W4,D2,L2,V1,M2} { ! l2_lattices( X ), l1_struct_0( X ) }.
% 65.23/65.60 (61394) {G0,W4,D2,L2,V1,M2} { ! l3_lattices( X ), l1_lattices( X ) }.
% 65.23/65.60 (61395) {G0,W4,D2,L2,V1,M2} { ! l3_lattices( X ), l2_lattices( X ) }.
% 65.23/65.60 (61396) {G0,W1,D1,L1,V0,M1} { && }.
% 65.23/65.60 (61397) {G0,W11,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), ! m2_filter_2( Y, X ), ! v1_xboole_0( Y ) }.
% 65.23/65.60 (61398) {G0,W12,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 65.23/65.60 (61399) {G0,W14,D4,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y, k1_zfmisc_1(
% 65.23/65.60 u1_struct_0( X ) ) ) }.
% 65.23/65.60 (61400) {G0,W1,D1,L1,V0,M1} { && }.
% 65.23/65.60 (61401) {G0,W2,D2,L1,V0,M1} { l1_lattices( skol2 ) }.
% 65.23/65.60 (61402) {G0,W2,D2,L1,V0,M1} { l1_struct_0( skol3 ) }.
% 65.23/65.60 (61403) {G0,W2,D2,L1,V0,M1} { l2_lattices( skol4 ) }.
% 65.23/65.60 (61404) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol5 ) }.
% 65.23/65.60 (61405) {G0,W4,D3,L1,V1,M1} { m1_subset_1( skol6( X ), X ) }.
% 65.23/65.60 (61406) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), m2_filter_2( skol7( X ), X ) }.
% 65.23/65.60 (61407) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), m2_lattice4( skol8( X ), X ) }.
% 65.23/65.60 (61408) {G0,W7,D3,L3,V1,M3} { v3_struct_0( X ), ! l1_struct_0( X ), !
% 65.23/65.60 v1_xboole_0( u1_struct_0( X ) ) }.
% 65.23/65.60 (61409) {G0,W3,D3,L1,V1,M1} { ! v1_xboole_0( k1_zfmisc_1( X ) ) }.
% 65.23/65.60 (61410) {G0,W2,D2,L1,V0,M1} { v1_xboole_0( k1_xboole_0 ) }.
% 65.23/65.60 (61411) {G0,W9,D3,L4,V2,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), ! v1_xboole_0( skol9( Y ) ) }.
% 65.23/65.60 (61412) {G0,W10,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), m2_lattice4( skol9( X ), X ) }.
% 65.23/65.60 (61413) {G0,W5,D3,L2,V2,M2} { v1_xboole_0( X ), ! v1_xboole_0( skol10( Y )
% 65.23/65.60 ) }.
% 65.23/65.60 (61414) {G0,W7,D3,L2,V1,M2} { v1_xboole_0( X ), m1_subset_1( skol10( X ),
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 (61415) {G0,W2,D2,L1,V0,M1} { v1_xboole_0( skol11 ) }.
% 65.23/65.60 (61416) {G0,W3,D3,L1,V1,M1} { v1_xboole_0( skol12( Y ) ) }.
% 65.23/65.60 (61417) {G0,W5,D3,L1,V1,M1} { m1_subset_1( skol12( X ), k1_zfmisc_1( X ) )
% 65.23/65.60 }.
% 65.23/65.60 (61418) {G0,W2,D2,L1,V0,M1} { ! v1_xboole_0( skol13 ) }.
% 65.23/65.60 (61419) {G0,W2,D2,L1,V0,M1} { l1_struct_0( skol14 ) }.
% 65.23/65.60 (61420) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol14 ) }.
% 65.23/65.60 (61421) {G0,W7,D3,L3,V2,M3} { v3_struct_0( X ), ! l1_struct_0( X ), !
% 65.23/65.60 v1_xboole_0( skol15( Y ) ) }.
% 65.23/65.60 (61422) {G0,W10,D4,L3,V1,M3} { v3_struct_0( X ), ! l1_struct_0( X ),
% 65.23/65.60 m1_subset_1( skol15( X ), k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 65.23/65.60 (61423) {G0,W17,D3,L5,V3,M5} { v1_xboole_0( X ), ! m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! r1_filter_2(
% 65.23/65.60 X, Y, Z ), Y = Z }.
% 65.23/65.60 (61424) {G0,W17,D3,L5,V3,M5} { v1_xboole_0( X ), ! m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! Y = Z,
% 65.23/65.60 r1_filter_2( X, Y, Z ) }.
% 65.23/65.60 (61425) {G0,W14,D3,L4,V3,M4} { v1_xboole_0( X ), ! m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), r1_filter_2( X
% 65.23/65.60 , Y, Y ) }.
% 65.23/65.60 (61426) {G0,W3,D2,L1,V1,M1} { r1_tarski( X, X ) }.
% 65.23/65.60 (61427) {G0,W18,D3,L5,V3,M5} { v1_xboole_0( X ), ! m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! r1_filter_2(
% 65.23/65.60 X, Y, Z ), r1_filter_2( X, Z, Y ) }.
% 65.23/65.60 (61428) {G0,W6,D2,L2,V2,M2} { ! r2_hidden( X, Y ), m1_subset_1( X, Y ) }.
% 65.23/65.60 (61429) {G0,W8,D2,L3,V2,M3} { ! m1_subset_1( X, Y ), v1_xboole_0( Y ),
% 65.23/65.60 r2_hidden( X, Y ) }.
% 65.23/65.60 (61430) {G0,W16,D3,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), ! m2_filter_2( Y, X ), r1_filter_2( u1_struct_0( X ),
% 65.23/65.60 k19_filter_2( X, Y ), Y ) }.
% 65.23/65.60 (61431) {G0,W7,D3,L2,V2,M2} { ! m1_subset_1( X, k1_zfmisc_1( Y ) ),
% 65.23/65.60 r1_tarski( X, Y ) }.
% 65.23/65.60 (61432) {G0,W7,D3,L2,V2,M2} { ! r1_tarski( X, Y ), m1_subset_1( X,
% 65.23/65.60 k1_zfmisc_1( Y ) ) }.
% 65.23/65.60 (61433) {G0,W27,D4,L8,V2,M8} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y, k1_zfmisc_1(
% 65.23/65.60 u1_struct_0( X ) ) ), ! v14_lattices( X ), ! r2_hidden( k6_lattices( X )
% 65.23/65.60 , Y ), r1_filter_2( u1_struct_0( X ), k19_filter_2( X, Y ), k17_filter_2
% 65.23/65.60 ( X ) ) }.
% 65.23/65.60 (61434) {G0,W25,D4,L8,V2,M8} { v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y, k1_zfmisc_1(
% 65.23/65.60 u1_struct_0( X ) ) ), ! v14_lattices( X ), ! r2_hidden( k6_lattices( X )
% 65.23/65.60 , Y ), k19_filter_2( X, Y ) = u1_struct_0( X ) }.
% 65.23/65.60 (61435) {G0,W10,D3,L3,V3,M3} { ! r2_hidden( X, Z ), ! m1_subset_1( Z,
% 65.23/65.60 k1_zfmisc_1( Y ) ), m1_subset_1( X, Y ) }.
% 65.23/65.60 (61436) {G0,W9,D3,L3,V3,M3} { ! r2_hidden( X, Y ), ! m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( Z ) ), ! v1_xboole_0( Z ) }.
% 65.23/65.60 (61437) {G0,W5,D2,L2,V1,M2} { ! v1_xboole_0( X ), X = k1_xboole_0 }.
% 65.23/65.60 (61438) {G0,W5,D2,L2,V2,M2} { ! r2_hidden( X, Y ), ! v1_xboole_0( Y ) }.
% 65.23/65.60 (61439) {G0,W7,D2,L3,V2,M3} { ! v1_xboole_0( X ), X = Y, ! v1_xboole_0( Y
% 65.23/65.60 ) }.
% 65.23/65.60
% 65.23/65.60
% 65.23/65.60 Total Proof:
% 65.23/65.60
% 65.23/65.60 subsumption: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 parent0: (61359) {G0,W2,D2,L1,V0,M1} { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 65.23/65.60 parent0: (61360) {G0,W2,D2,L1,V0,M1} { v10_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 65.23/65.60 parent0: (61361) {G0,W2,D2,L1,V0,M1} { l3_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol16, skol1 ) }.
% 65.23/65.60 parent0: (61362) {G0,W3,D2,L1,V0,M1} { m2_filter_2( skol16, skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (4) {G0,W2,D2,L1,V0,M1} I { v14_lattices( skol1 ) }.
% 65.23/65.60 parent0: (61363) {G0,W2,D2,L1,V0,M1} { v14_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (5) {G0,W4,D3,L1,V0,M1} I { r2_hidden( k6_lattices( skol1 ),
% 65.23/65.60 skol16 ) }.
% 65.23/65.60 parent0: (61364) {G0,W4,D3,L1,V0,M1} { r2_hidden( k6_lattices( skol1 ),
% 65.23/65.60 skol16 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61440) {G0,W10,D3,L2,V0,M2} { ! u1_struct_0( skol1 ) = skol16, !
% 65.23/65.60 r1_filter_2( u1_struct_0( skol1 ), skol16, k17_filter_2( skol1 ) ) }.
% 65.23/65.60 parent0[1]: (61365) {G0,W10,D3,L2,V0,M2} { ! r1_filter_2( u1_struct_0(
% 65.23/65.60 skol1 ), skol16, k17_filter_2( skol1 ) ), ! skol16 = u1_struct_0( skol1 )
% 65.23/65.60 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (6) {G0,W10,D3,L2,V0,M2} I { ! r1_filter_2( u1_struct_0( skol1
% 65.23/65.60 ), skol16, k17_filter_2( skol1 ) ), ! u1_struct_0( skol1 ) ==> skol16
% 65.23/65.60 }.
% 65.23/65.60 parent0: (61440) {G0,W10,D3,L2,V0,M2} { ! u1_struct_0( skol1 ) = skol16, !
% 65.23/65.60 r1_filter_2( u1_struct_0( skol1 ), skol16, k17_filter_2( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 1
% 65.23/65.60 1 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (9) {G0,W8,D2,L4,V1,M4} I { ! l3_lattices( X ), v3_struct_0( X
% 65.23/65.60 ), ! v10_lattices( X ), alpha1( X ) }.
% 65.23/65.60 parent0: (61368) {G0,W8,D2,L4,V1,M4} { ! l3_lattices( X ), v3_struct_0( X
% 65.23/65.60 ), ! v10_lattices( X ), alpha1( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 3 ==> 3
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (11) {G0,W4,D2,L2,V1,M2} I { ! alpha1( X ), alpha2( X ) }.
% 65.23/65.60 parent0: (61370) {G0,W4,D2,L2,V1,M2} { ! alpha1( X ), alpha2( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (14) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha3( X ) }.
% 65.23/65.60 parent0: (61373) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha3( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (17) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha4( X ) }.
% 65.23/65.60 parent0: (61376) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha4( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (20) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), ! v3_struct_0( X )
% 65.23/65.60 }.
% 65.23/65.60 parent0: (61379) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), ! v3_struct_0( X )
% 65.23/65.60 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (25) {G0,W11,D3,L4,V1,M4} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), k17_filter_2( X ) ==> u1_struct_0( X ) }.
% 65.23/65.60 parent0: (61385) {G0,W11,D3,L4,V1,M4} { v3_struct_0( X ), ! v10_lattices(
% 65.23/65.60 X ), ! l3_lattices( X ), k17_filter_2( X ) = u1_struct_0( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 3 ==> 3
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (29) {G0,W9,D3,L3,V1,M3} I { v3_struct_0( X ), ! l2_lattices(
% 65.23/65.60 X ), m1_subset_1( k6_lattices( X ), u1_struct_0( X ) ) }.
% 65.23/65.60 parent0: (61390) {G0,W9,D3,L3,V1,M3} { v3_struct_0( X ), ! l2_lattices( X
% 65.23/65.60 ), m1_subset_1( k6_lattices( X ), u1_struct_0( X ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (31) {G0,W4,D2,L2,V1,M2} I { ! l2_lattices( X ), l1_struct_0(
% 65.23/65.60 X ) }.
% 65.23/65.60 parent0: (61393) {G0,W4,D2,L2,V1,M2} { ! l2_lattices( X ), l1_struct_0( X
% 65.23/65.60 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (33) {G0,W4,D2,L2,V1,M2} I { ! l3_lattices( X ), l2_lattices(
% 65.23/65.60 X ) }.
% 65.23/65.60 parent0: (61395) {G0,W4,D2,L2,V1,M2} { ! l3_lattices( X ), l2_lattices( X
% 65.23/65.60 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (35) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 65.23/65.60 parent0: (61398) {G0,W12,D2,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices(
% 65.23/65.60 X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 3 ==> 3
% 65.23/65.60 4 ==> 4
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (36) {G0,W14,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 65.23/65.60 parent0: (61399) {G0,W14,D4,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices(
% 65.23/65.60 X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 3 ==> 3
% 65.23/65.60 4 ==> 4
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (41) {G0,W4,D3,L1,V1,M1} I { m1_subset_1( skol6( X ), X ) }.
% 65.23/65.60 parent0: (61405) {G0,W4,D3,L1,V1,M1} { m1_subset_1( skol6( X ), X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (44) {G0,W7,D3,L3,V1,M3} I { v3_struct_0( X ), ! l1_struct_0(
% 65.23/65.60 X ), ! v1_xboole_0( u1_struct_0( X ) ) }.
% 65.23/65.60 parent0: (61408) {G0,W7,D3,L3,V1,M3} { v3_struct_0( X ), ! l1_struct_0( X
% 65.23/65.60 ), ! v1_xboole_0( u1_struct_0( X ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (46) {G0,W2,D2,L1,V0,M1} I { v1_xboole_0( k1_xboole_0 ) }.
% 65.23/65.60 parent0: (61410) {G0,W2,D2,L1,V0,M1} { v1_xboole_0( k1_xboole_0 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (52) {G0,W3,D3,L1,V1,M1} I { v1_xboole_0( skol12( Y ) ) }.
% 65.23/65.60 parent0: (61416) {G0,W3,D3,L1,V1,M1} { v1_xboole_0( skol12( Y ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := Z
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (53) {G0,W5,D3,L1,V1,M1} I { m1_subset_1( skol12( X ),
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 parent0: (61417) {G0,W5,D3,L1,V1,M1} { m1_subset_1( skol12( X ),
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (59) {G0,W17,D3,L5,V3,M5} I { v1_xboole_0( X ), ! m1_subset_1
% 65.23/65.60 ( Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), !
% 65.23/65.60 r1_filter_2( X, Y, Z ), Y = Z }.
% 65.23/65.60 parent0: (61423) {G0,W17,D3,L5,V3,M5} { v1_xboole_0( X ), ! m1_subset_1( Y
% 65.23/65.60 , k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! r1_filter_2
% 65.23/65.60 ( X, Y, Z ), Y = Z }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 Z := Z
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 3 ==> 3
% 65.23/65.60 4 ==> 4
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (60) {G0,W17,D3,L5,V3,M5} I { v1_xboole_0( X ), ! m1_subset_1
% 65.23/65.60 ( Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! Y = Z,
% 65.23/65.60 r1_filter_2( X, Y, Z ) }.
% 65.23/65.60 parent0: (61424) {G0,W17,D3,L5,V3,M5} { v1_xboole_0( X ), ! m1_subset_1( Y
% 65.23/65.60 , k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! Y = Z,
% 65.23/65.60 r1_filter_2( X, Y, Z ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 Z := Z
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 3 ==> 3
% 65.23/65.60 4 ==> 4
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (62) {G0,W3,D2,L1,V1,M1} I { r1_tarski( X, X ) }.
% 65.23/65.60 parent0: (61426) {G0,W3,D2,L1,V1,M1} { r1_tarski( X, X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (65) {G0,W8,D2,L3,V2,M3} I { ! m1_subset_1( X, Y ),
% 65.23/65.60 v1_xboole_0( Y ), r2_hidden( X, Y ) }.
% 65.23/65.60 parent0: (61429) {G0,W8,D2,L3,V2,M3} { ! m1_subset_1( X, Y ), v1_xboole_0
% 65.23/65.60 ( Y ), r2_hidden( X, Y ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (66) {G0,W16,D3,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), r1_filter_2(
% 65.23/65.60 u1_struct_0( X ), k19_filter_2( X, Y ), Y ) }.
% 65.23/65.60 parent0: (61430) {G0,W16,D3,L5,V2,M5} { v3_struct_0( X ), ! v10_lattices(
% 65.23/65.60 X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), r1_filter_2( u1_struct_0
% 65.23/65.60 ( X ), k19_filter_2( X, Y ), Y ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 3 ==> 3
% 65.23/65.60 4 ==> 4
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (68) {G0,W7,D3,L2,V2,M2} I { ! r1_tarski( X, Y ), m1_subset_1
% 65.23/65.60 ( X, k1_zfmisc_1( Y ) ) }.
% 65.23/65.60 parent0: (61432) {G0,W7,D3,L2,V2,M2} { ! r1_tarski( X, Y ), m1_subset_1( X
% 65.23/65.60 , k1_zfmisc_1( Y ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (70) {G0,W25,D4,L8,V2,M8} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( X ) ) ), ! v14_lattices( X ), ! r2_hidden(
% 65.23/65.60 k6_lattices( X ), Y ), k19_filter_2( X, Y ) ==> u1_struct_0( X ) }.
% 65.23/65.60 parent0: (61434) {G0,W25,D4,L8,V2,M8} { v3_struct_0( X ), ! v10_lattices(
% 65.23/65.60 X ), ! l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y, k1_zfmisc_1
% 65.23/65.60 ( u1_struct_0( X ) ) ), ! v14_lattices( X ), ! r2_hidden( k6_lattices( X
% 65.23/65.60 ), Y ), k19_filter_2( X, Y ) = u1_struct_0( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 3 ==> 3
% 65.23/65.60 4 ==> 4
% 65.23/65.60 5 ==> 5
% 65.23/65.60 6 ==> 6
% 65.23/65.60 7 ==> 7
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (72) {G0,W9,D3,L3,V3,M3} I { ! r2_hidden( X, Y ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( Z ) ), ! v1_xboole_0( Z ) }.
% 65.23/65.60 parent0: (61436) {G0,W9,D3,L3,V3,M3} { ! r2_hidden( X, Y ), ! m1_subset_1
% 65.23/65.60 ( Y, k1_zfmisc_1( Z ) ), ! v1_xboole_0( Z ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 Z := Z
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (73) {G0,W5,D2,L2,V1,M2} I { ! v1_xboole_0( X ), X =
% 65.23/65.60 k1_xboole_0 }.
% 65.23/65.60 parent0: (61437) {G0,W5,D2,L2,V1,M2} { ! v1_xboole_0( X ), X = k1_xboole_0
% 65.23/65.60 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (74) {G0,W5,D2,L2,V2,M2} I { ! r2_hidden( X, Y ), !
% 65.23/65.60 v1_xboole_0( Y ) }.
% 65.23/65.60 parent0: (61438) {G0,W5,D2,L2,V2,M2} { ! r2_hidden( X, Y ), ! v1_xboole_0
% 65.23/65.60 ( Y ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61573) {G1,W2,D2,L1,V0,M1} { l2_lattices( skol1 ) }.
% 65.23/65.60 parent0[0]: (33) {G0,W4,D2,L2,V1,M2} I { ! l3_lattices( X ), l2_lattices( X
% 65.23/65.60 ) }.
% 65.23/65.60 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (78) {G1,W2,D2,L1,V0,M1} R(33,2) { l2_lattices( skol1 ) }.
% 65.23/65.60 parent0: (61573) {G1,W2,D2,L1,V0,M1} { l2_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61574) {G1,W2,D2,L1,V0,M1} { l1_struct_0( skol1 ) }.
% 65.23/65.60 parent0[0]: (31) {G0,W4,D2,L2,V1,M2} I { ! l2_lattices( X ), l1_struct_0( X
% 65.23/65.60 ) }.
% 65.23/65.60 parent1[0]: (78) {G1,W2,D2,L1,V0,M1} R(33,2) { l2_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (83) {G2,W2,D2,L1,V0,M1} R(31,78) { l1_struct_0( skol1 ) }.
% 65.23/65.60 parent0: (61574) {G1,W2,D2,L1,V0,M1} { l1_struct_0( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61575) {G1,W6,D2,L3,V0,M3} { v3_struct_0( skol1 ), !
% 65.23/65.60 v10_lattices( skol1 ), alpha1( skol1 ) }.
% 65.23/65.60 parent0[0]: (9) {G0,W8,D2,L4,V1,M4} I { ! l3_lattices( X ), v3_struct_0( X
% 65.23/65.60 ), ! v10_lattices( X ), alpha1( X ) }.
% 65.23/65.60 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61576) {G1,W4,D2,L2,V0,M2} { ! v10_lattices( skol1 ), alpha1
% 65.23/65.60 ( skol1 ) }.
% 65.23/65.60 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 parent1[0]: (61575) {G1,W6,D2,L3,V0,M3} { v3_struct_0( skol1 ), !
% 65.23/65.60 v10_lattices( skol1 ), alpha1( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (91) {G1,W4,D2,L2,V0,M2} R(9,2);r(0) { ! v10_lattices( skol1 )
% 65.23/65.60 , alpha1( skol1 ) }.
% 65.23/65.60 parent0: (61576) {G1,W4,D2,L2,V0,M2} { ! v10_lattices( skol1 ), alpha1(
% 65.23/65.60 skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61577) {G1,W4,D2,L2,V1,M2} { alpha3( X ), ! alpha1( X ) }.
% 65.23/65.60 parent0[0]: (14) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha3( X ) }.
% 65.23/65.60 parent1[1]: (11) {G0,W4,D2,L2,V1,M2} I { ! alpha1( X ), alpha2( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (109) {G1,W4,D2,L2,V1,M2} R(14,11) { alpha3( X ), ! alpha1( X
% 65.23/65.60 ) }.
% 65.23/65.60 parent0: (61577) {G1,W4,D2,L2,V1,M2} { alpha3( X ), ! alpha1( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61578) {G1,W4,D2,L2,V1,M2} { alpha4( X ), ! alpha1( X ) }.
% 65.23/65.60 parent0[0]: (17) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha4( X ) }.
% 65.23/65.60 parent1[0]: (109) {G1,W4,D2,L2,V1,M2} R(14,11) { alpha3( X ), ! alpha1( X )
% 65.23/65.60 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (118) {G2,W4,D2,L2,V1,M2} R(109,17) { ! alpha1( X ), alpha4( X
% 65.23/65.60 ) }.
% 65.23/65.60 parent0: (61578) {G1,W4,D2,L2,V1,M2} { alpha4( X ), ! alpha1( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 1
% 65.23/65.60 1 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61579) {G1,W2,D2,L1,V0,M1} { alpha1( skol1 ) }.
% 65.23/65.60 parent0[0]: (91) {G1,W4,D2,L2,V0,M2} R(9,2);r(0) { ! v10_lattices( skol1 )
% 65.23/65.60 , alpha1( skol1 ) }.
% 65.23/65.60 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (132) {G2,W2,D2,L1,V0,M1} S(91);r(1) { alpha1( skol1 ) }.
% 65.23/65.60 parent0: (61579) {G1,W2,D2,L1,V0,M1} { alpha1( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61580) {G3,W2,D2,L1,V0,M1} { alpha4( skol1 ) }.
% 65.23/65.60 parent0[0]: (118) {G2,W4,D2,L2,V1,M2} R(109,17) { ! alpha1( X ), alpha4( X
% 65.23/65.60 ) }.
% 65.23/65.60 parent1[0]: (132) {G2,W2,D2,L1,V0,M1} S(91);r(1) { alpha1( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (134) {G3,W2,D2,L1,V0,M1} R(132,118) { alpha4( skol1 ) }.
% 65.23/65.60 parent0: (61580) {G3,W2,D2,L1,V0,M1} { alpha4( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61581) {G0,W11,D3,L4,V1,M4} { u1_struct_0( X ) ==> k17_filter_2(
% 65.23/65.60 X ), v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ) }.
% 65.23/65.60 parent0[3]: (25) {G0,W11,D3,L4,V1,M4} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), k17_filter_2( X ) ==> u1_struct_0( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61582) {G1,W9,D3,L3,V0,M3} { u1_struct_0( skol1 ) ==>
% 65.23/65.60 k17_filter_2( skol1 ), v3_struct_0( skol1 ), ! v10_lattices( skol1 ) }.
% 65.23/65.60 parent0[3]: (61581) {G0,W11,D3,L4,V1,M4} { u1_struct_0( X ) ==>
% 65.23/65.60 k17_filter_2( X ), v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices(
% 65.23/65.60 X ) }.
% 65.23/65.60 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61583) {G1,W7,D3,L2,V0,M2} { u1_struct_0( skol1 ) ==>
% 65.23/65.60 k17_filter_2( skol1 ), ! v10_lattices( skol1 ) }.
% 65.23/65.60 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 parent1[1]: (61582) {G1,W9,D3,L3,V0,M3} { u1_struct_0( skol1 ) ==>
% 65.23/65.60 k17_filter_2( skol1 ), v3_struct_0( skol1 ), ! v10_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61584) {G1,W7,D3,L2,V0,M2} { k17_filter_2( skol1 ) ==>
% 65.23/65.60 u1_struct_0( skol1 ), ! v10_lattices( skol1 ) }.
% 65.23/65.60 parent0[0]: (61583) {G1,W7,D3,L2,V0,M2} { u1_struct_0( skol1 ) ==>
% 65.23/65.60 k17_filter_2( skol1 ), ! v10_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (153) {G1,W7,D3,L2,V0,M2} R(25,2);r(0) { ! v10_lattices( skol1
% 65.23/65.60 ), k17_filter_2( skol1 ) ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 parent0: (61584) {G1,W7,D3,L2,V0,M2} { k17_filter_2( skol1 ) ==>
% 65.23/65.60 u1_struct_0( skol1 ), ! v10_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 1
% 65.23/65.60 1 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61585) {G1,W2,D2,L1,V0,M1} { ! v1_xboole_0( skol16 ) }.
% 65.23/65.60 parent0[0]: (74) {G0,W5,D2,L2,V2,M2} I { ! r2_hidden( X, Y ), ! v1_xboole_0
% 65.23/65.60 ( Y ) }.
% 65.23/65.60 parent1[0]: (5) {G0,W4,D3,L1,V0,M1} I { r2_hidden( k6_lattices( skol1 ),
% 65.23/65.60 skol16 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := k6_lattices( skol1 )
% 65.23/65.60 Y := skol16
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (158) {G1,W2,D2,L1,V0,M1} R(74,5) { ! v1_xboole_0( skol16 )
% 65.23/65.60 }.
% 65.23/65.60 parent0: (61585) {G1,W2,D2,L1,V0,M1} { ! v1_xboole_0( skol16 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61586) {G0,W5,D2,L2,V1,M2} { k1_xboole_0 = X, ! v1_xboole_0( X )
% 65.23/65.60 }.
% 65.23/65.60 parent0[1]: (73) {G0,W5,D2,L2,V1,M2} I { ! v1_xboole_0( X ), X =
% 65.23/65.60 k1_xboole_0 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61587) {G1,W4,D3,L1,V1,M1} { k1_xboole_0 = skol12( X ) }.
% 65.23/65.60 parent0[1]: (61586) {G0,W5,D2,L2,V1,M2} { k1_xboole_0 = X, ! v1_xboole_0(
% 65.23/65.60 X ) }.
% 65.23/65.60 parent1[0]: (52) {G0,W3,D3,L1,V1,M1} I { v1_xboole_0( skol12( Y ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol12( X )
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := Y
% 65.23/65.60 Y := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61588) {G1,W4,D3,L1,V1,M1} { skol12( X ) = k1_xboole_0 }.
% 65.23/65.60 parent0[0]: (61587) {G1,W4,D3,L1,V1,M1} { k1_xboole_0 = skol12( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (170) {G1,W4,D3,L1,V1,M1} R(73,52) { skol12( X ) ==>
% 65.23/65.60 k1_xboole_0 }.
% 65.23/65.60 parent0: (61588) {G1,W4,D3,L1,V1,M1} { skol12( X ) = k1_xboole_0 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61589) {G1,W7,D3,L2,V0,M2} { v3_struct_0( skol1 ),
% 65.23/65.60 m1_subset_1( k6_lattices( skol1 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0[1]: (29) {G0,W9,D3,L3,V1,M3} I { v3_struct_0( X ), ! l2_lattices( X
% 65.23/65.60 ), m1_subset_1( k6_lattices( X ), u1_struct_0( X ) ) }.
% 65.23/65.60 parent1[0]: (78) {G1,W2,D2,L1,V0,M1} R(33,2) { l2_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61590) {G1,W5,D3,L1,V0,M1} { m1_subset_1( k6_lattices( skol1
% 65.23/65.60 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 parent1[0]: (61589) {G1,W7,D3,L2,V0,M2} { v3_struct_0( skol1 ),
% 65.23/65.60 m1_subset_1( k6_lattices( skol1 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (232) {G2,W5,D3,L1,V0,M1} R(29,78);r(0) { m1_subset_1(
% 65.23/65.60 k6_lattices( skol1 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0: (61590) {G1,W5,D3,L1,V0,M1} { m1_subset_1( k6_lattices( skol1 ),
% 65.23/65.60 u1_struct_0( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61591) {G1,W9,D2,L4,V0,M4} { v3_struct_0( skol1 ), !
% 65.23/65.60 v10_lattices( skol1 ), ! l3_lattices( skol1 ), m2_lattice4( skol16, skol1
% 65.23/65.60 ) }.
% 65.23/65.60 parent0[3]: (35) {G0,W12,D2,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), m2_lattice4( Y, X ) }.
% 65.23/65.60 parent1[0]: (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol16, skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 Y := skol16
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61592) {G1,W7,D2,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 65.23/65.60 l3_lattices( skol1 ), m2_lattice4( skol16, skol1 ) }.
% 65.23/65.60 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 parent1[0]: (61591) {G1,W9,D2,L4,V0,M4} { v3_struct_0( skol1 ), !
% 65.23/65.60 v10_lattices( skol1 ), ! l3_lattices( skol1 ), m2_lattice4( skol16, skol1
% 65.23/65.60 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (267) {G1,W7,D2,L3,V0,M3} R(35,3);r(0) { ! v10_lattices( skol1
% 65.23/65.60 ), ! l3_lattices( skol1 ), m2_lattice4( skol16, skol1 ) }.
% 65.23/65.60 parent0: (61592) {G1,W7,D2,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 65.23/65.60 l3_lattices( skol1 ), m2_lattice4( skol16, skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61593) {G1,W14,D4,L5,V2,M5} { ! alpha4( X ), ! v10_lattices(
% 65.23/65.60 X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 65.23/65.60 parent0[1]: (20) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), ! v3_struct_0( X )
% 65.23/65.60 }.
% 65.23/65.60 parent1[0]: (36) {G0,W14,D4,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( X ) ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (291) {G1,W14,D4,L5,V2,M5} R(36,20) { ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y, k1_zfmisc_1(
% 65.23/65.60 u1_struct_0( X ) ) ), ! alpha4( X ) }.
% 65.23/65.60 parent0: (61593) {G1,W14,D4,L5,V2,M5} { ! alpha4( X ), ! v10_lattices( X )
% 65.23/65.60 , ! l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y, k1_zfmisc_1
% 65.23/65.60 ( u1_struct_0( X ) ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 4
% 65.23/65.60 1 ==> 0
% 65.23/65.60 2 ==> 1
% 65.23/65.60 3 ==> 2
% 65.23/65.60 4 ==> 3
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61594) {G1,W5,D3,L2,V0,M2} { v3_struct_0( skol1 ), !
% 65.23/65.60 v1_xboole_0( u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0[1]: (44) {G0,W7,D3,L3,V1,M3} I { v3_struct_0( X ), ! l1_struct_0( X
% 65.23/65.60 ), ! v1_xboole_0( u1_struct_0( X ) ) }.
% 65.23/65.60 parent1[0]: (83) {G2,W2,D2,L1,V0,M1} R(31,78) { l1_struct_0( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61595) {G1,W3,D3,L1,V0,M1} { ! v1_xboole_0( u1_struct_0(
% 65.23/65.60 skol1 ) ) }.
% 65.23/65.60 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 parent1[0]: (61594) {G1,W5,D3,L2,V0,M2} { v3_struct_0( skol1 ), !
% 65.23/65.60 v1_xboole_0( u1_struct_0( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (378) {G3,W3,D3,L1,V0,M1} R(44,83);r(0) { ! v1_xboole_0(
% 65.23/65.60 u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0: (61595) {G1,W3,D3,L1,V0,M1} { ! v1_xboole_0( u1_struct_0( skol1 )
% 65.23/65.60 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 paramod: (61597) {G1,W4,D3,L1,V1,M1} { m1_subset_1( k1_xboole_0,
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 parent0[0]: (170) {G1,W4,D3,L1,V1,M1} R(73,52) { skol12( X ) ==>
% 65.23/65.60 k1_xboole_0 }.
% 65.23/65.60 parent1[0; 1]: (53) {G0,W5,D3,L1,V1,M1} I { m1_subset_1( skol12( X ),
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (385) {G2,W4,D3,L1,V1,M1} S(53);d(170) { m1_subset_1(
% 65.23/65.60 k1_xboole_0, k1_zfmisc_1( X ) ) }.
% 65.23/65.60 parent0: (61597) {G1,W4,D3,L1,V1,M1} { m1_subset_1( k1_xboole_0,
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61598) {G0,W17,D3,L5,V3,M5} { Y = X, v1_xboole_0( Z ), !
% 65.23/65.60 m1_subset_1( X, k1_zfmisc_1( Z ) ), ! m1_subset_1( Y, k1_zfmisc_1( Z ) )
% 65.23/65.60 , ! r1_filter_2( Z, X, Y ) }.
% 65.23/65.60 parent0[4]: (59) {G0,W17,D3,L5,V3,M5} I { v1_xboole_0( X ), ! m1_subset_1(
% 65.23/65.60 Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), !
% 65.23/65.60 r1_filter_2( X, Y, Z ), Y = Z }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := Z
% 65.23/65.60 Y := X
% 65.23/65.60 Z := Y
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61599) {G0,W5,D2,L2,V1,M2} { k1_xboole_0 = X, ! v1_xboole_0( X )
% 65.23/65.60 }.
% 65.23/65.60 parent0[1]: (73) {G0,W5,D2,L2,V1,M2} I { ! v1_xboole_0( X ), X =
% 65.23/65.60 k1_xboole_0 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61600) {G1,W18,D3,L5,V3,M5} { k1_xboole_0 = X, Y = Z, !
% 65.23/65.60 m1_subset_1( Z, k1_zfmisc_1( X ) ), ! m1_subset_1( Y, k1_zfmisc_1( X ) )
% 65.23/65.60 , ! r1_filter_2( X, Z, Y ) }.
% 65.23/65.60 parent0[1]: (61599) {G0,W5,D2,L2,V1,M2} { k1_xboole_0 = X, ! v1_xboole_0(
% 65.23/65.60 X ) }.
% 65.23/65.60 parent1[1]: (61598) {G0,W17,D3,L5,V3,M5} { Y = X, v1_xboole_0( Z ), !
% 65.23/65.60 m1_subset_1( X, k1_zfmisc_1( Z ) ), ! m1_subset_1( Y, k1_zfmisc_1( Z ) )
% 65.23/65.60 , ! r1_filter_2( Z, X, Y ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := Z
% 65.23/65.60 Y := Y
% 65.23/65.60 Z := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61602) {G1,W18,D3,L5,V3,M5} { Y = X, k1_xboole_0 = Z, !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( Z ) ), ! m1_subset_1( X, k1_zfmisc_1( Z ) )
% 65.23/65.60 , ! r1_filter_2( Z, Y, X ) }.
% 65.23/65.60 parent0[1]: (61600) {G1,W18,D3,L5,V3,M5} { k1_xboole_0 = X, Y = Z, !
% 65.23/65.60 m1_subset_1( Z, k1_zfmisc_1( X ) ), ! m1_subset_1( Y, k1_zfmisc_1( X ) )
% 65.23/65.60 , ! r1_filter_2( X, Z, Y ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := Z
% 65.23/65.60 Y := X
% 65.23/65.60 Z := Y
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61603) {G1,W18,D3,L5,V3,M5} { X = k1_xboole_0, Y = Z, !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) )
% 65.23/65.60 , ! r1_filter_2( X, Y, Z ) }.
% 65.23/65.60 parent0[1]: (61602) {G1,W18,D3,L5,V3,M5} { Y = X, k1_xboole_0 = Z, !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( Z ) ), ! m1_subset_1( X, k1_zfmisc_1( Z ) )
% 65.23/65.60 , ! r1_filter_2( Z, Y, X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := Z
% 65.23/65.60 Y := Y
% 65.23/65.60 Z := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (531) {G1,W18,D3,L5,V3,M5} R(59,73) { ! m1_subset_1( X,
% 65.23/65.60 k1_zfmisc_1( Y ) ), ! m1_subset_1( Z, k1_zfmisc_1( Y ) ), ! r1_filter_2(
% 65.23/65.60 Y, X, Z ), X = Z, Y = k1_xboole_0 }.
% 65.23/65.60 parent0: (61603) {G1,W18,D3,L5,V3,M5} { X = k1_xboole_0, Y = Z, !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) )
% 65.23/65.60 , ! r1_filter_2( X, Y, Z ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := Y
% 65.23/65.60 Y := X
% 65.23/65.60 Z := Z
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 4
% 65.23/65.60 1 ==> 3
% 65.23/65.60 2 ==> 0
% 65.23/65.60 3 ==> 1
% 65.23/65.60 4 ==> 2
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61611) {G1,W8,D3,L2,V0,M2} { v1_xboole_0( u1_struct_0( skol1
% 65.23/65.60 ) ), r2_hidden( k6_lattices( skol1 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0[0]: (65) {G0,W8,D2,L3,V2,M3} I { ! m1_subset_1( X, Y ), v1_xboole_0
% 65.23/65.60 ( Y ), r2_hidden( X, Y ) }.
% 65.23/65.60 parent1[0]: (232) {G2,W5,D3,L1,V0,M1} R(29,78);r(0) { m1_subset_1(
% 65.23/65.60 k6_lattices( skol1 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := k6_lattices( skol1 )
% 65.23/65.60 Y := u1_struct_0( skol1 )
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61612) {G2,W5,D3,L1,V0,M1} { r2_hidden( k6_lattices( skol1 )
% 65.23/65.60 , u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0[0]: (378) {G3,W3,D3,L1,V0,M1} R(44,83);r(0) { ! v1_xboole_0(
% 65.23/65.60 u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent1[0]: (61611) {G1,W8,D3,L2,V0,M2} { v1_xboole_0( u1_struct_0( skol1
% 65.23/65.60 ) ), r2_hidden( k6_lattices( skol1 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (988) {G4,W5,D3,L1,V0,M1} R(65,232);r(378) { r2_hidden(
% 65.23/65.60 k6_lattices( skol1 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0: (61612) {G2,W5,D3,L1,V0,M1} { r2_hidden( k6_lattices( skol1 ),
% 65.23/65.60 u1_struct_0( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61613) {G1,W6,D3,L2,V1,M2} { v1_xboole_0( X ), r2_hidden(
% 65.23/65.60 skol6( X ), X ) }.
% 65.23/65.60 parent0[0]: (65) {G0,W8,D2,L3,V2,M3} I { ! m1_subset_1( X, Y ), v1_xboole_0
% 65.23/65.60 ( Y ), r2_hidden( X, Y ) }.
% 65.23/65.60 parent1[0]: (41) {G0,W4,D3,L1,V1,M1} I { m1_subset_1( skol6( X ), X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol6( X )
% 65.23/65.60 Y := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1028) {G1,W6,D3,L2,V1,M2} R(65,41) { v1_xboole_0( X ),
% 65.23/65.60 r2_hidden( skol6( X ), X ) }.
% 65.23/65.60 parent0: (61613) {G1,W6,D3,L2,V1,M2} { v1_xboole_0( X ), r2_hidden( skol6
% 65.23/65.60 ( X ), X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61614) {G1,W13,D3,L4,V0,M4} { v3_struct_0( skol1 ), !
% 65.23/65.60 v10_lattices( skol1 ), ! l3_lattices( skol1 ), r1_filter_2( u1_struct_0(
% 65.23/65.60 skol1 ), k19_filter_2( skol1, skol16 ), skol16 ) }.
% 65.23/65.60 parent0[3]: (66) {G0,W16,D3,L5,V2,M5} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), ! m2_filter_2( Y, X ), r1_filter_2(
% 65.23/65.60 u1_struct_0( X ), k19_filter_2( X, Y ), Y ) }.
% 65.23/65.60 parent1[0]: (3) {G0,W3,D2,L1,V0,M1} I { m2_filter_2( skol16, skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 Y := skol16
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61615) {G1,W11,D3,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 65.23/65.60 l3_lattices( skol1 ), r1_filter_2( u1_struct_0( skol1 ), k19_filter_2(
% 65.23/65.60 skol1, skol16 ), skol16 ) }.
% 65.23/65.60 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 parent1[0]: (61614) {G1,W13,D3,L4,V0,M4} { v3_struct_0( skol1 ), !
% 65.23/65.60 v10_lattices( skol1 ), ! l3_lattices( skol1 ), r1_filter_2( u1_struct_0(
% 65.23/65.60 skol1 ), k19_filter_2( skol1, skol16 ), skol16 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1111) {G1,W11,D3,L3,V0,M3} R(66,3);r(0) { ! v10_lattices(
% 65.23/65.60 skol1 ), ! l3_lattices( skol1 ), r1_filter_2( u1_struct_0( skol1 ),
% 65.23/65.60 k19_filter_2( skol1, skol16 ), skol16 ) }.
% 65.23/65.60 parent0: (61615) {G1,W11,D3,L3,V0,M3} { ! v10_lattices( skol1 ), !
% 65.23/65.60 l3_lattices( skol1 ), r1_filter_2( u1_struct_0( skol1 ), k19_filter_2(
% 65.23/65.60 skol1, skol16 ), skol16 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 2 ==> 2
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61616) {G1,W4,D3,L1,V1,M1} { m1_subset_1( X, k1_zfmisc_1( X )
% 65.23/65.60 ) }.
% 65.23/65.60 parent0[0]: (68) {G0,W7,D3,L2,V2,M2} I { ! r1_tarski( X, Y ), m1_subset_1(
% 65.23/65.60 X, k1_zfmisc_1( Y ) ) }.
% 65.23/65.60 parent1[0]: (62) {G0,W3,D2,L1,V1,M1} I { r1_tarski( X, X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1183) {G1,W4,D3,L1,V1,M1} R(68,62) { m1_subset_1( X,
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 parent0: (61616) {G1,W4,D3,L1,V1,M1} { m1_subset_1( X, k1_zfmisc_1( X ) )
% 65.23/65.60 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61617) {G0,W17,D3,L5,V3,M5} { ! Y = X, v1_xboole_0( Z ), !
% 65.23/65.60 m1_subset_1( X, k1_zfmisc_1( Z ) ), ! m1_subset_1( Y, k1_zfmisc_1( Z ) )
% 65.23/65.60 , r1_filter_2( Z, X, Y ) }.
% 65.23/65.60 parent0[3]: (60) {G0,W17,D3,L5,V3,M5} I { v1_xboole_0( X ), ! m1_subset_1(
% 65.23/65.60 Y, k1_zfmisc_1( X ) ), ! m1_subset_1( Z, k1_zfmisc_1( X ) ), ! Y = Z,
% 65.23/65.60 r1_filter_2( X, Y, Z ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := Z
% 65.23/65.60 Y := X
% 65.23/65.60 Z := Y
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61619) {G1,W13,D3,L4,V2,M4} { ! X = Y, v1_xboole_0( X ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( X ) ), r1_filter_2( X, Y, X ) }.
% 65.23/65.60 parent0[3]: (61617) {G0,W17,D3,L5,V3,M5} { ! Y = X, v1_xboole_0( Z ), !
% 65.23/65.60 m1_subset_1( X, k1_zfmisc_1( Z ) ), ! m1_subset_1( Y, k1_zfmisc_1( Z ) )
% 65.23/65.60 , r1_filter_2( Z, X, Y ) }.
% 65.23/65.60 parent1[0]: (1183) {G1,W4,D3,L1,V1,M1} R(68,62) { m1_subset_1( X,
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := Y
% 65.23/65.60 Y := X
% 65.23/65.60 Z := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61620) {G1,W13,D3,L4,V2,M4} { ! Y = X, v1_xboole_0( X ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( X ) ), r1_filter_2( X, Y, X ) }.
% 65.23/65.60 parent0[0]: (61619) {G1,W13,D3,L4,V2,M4} { ! X = Y, v1_xboole_0( X ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( X ) ), r1_filter_2( X, Y, X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1190) {G2,W13,D3,L4,V2,M4} R(1183,60) { v1_xboole_0( X ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( X ) ), ! Y = X, r1_filter_2( X, Y, X ) }.
% 65.23/65.60 parent0: (61620) {G1,W13,D3,L4,V2,M4} { ! Y = X, v1_xboole_0( X ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( X ) ), r1_filter_2( X, Y, X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 2
% 65.23/65.60 1 ==> 0
% 65.23/65.60 2 ==> 1
% 65.23/65.60 3 ==> 3
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61622) {G2,W13,D3,L4,V2,M4} { ! Y = X, v1_xboole_0( Y ), !
% 65.23/65.60 m1_subset_1( X, k1_zfmisc_1( Y ) ), r1_filter_2( Y, X, Y ) }.
% 65.23/65.60 parent0[2]: (1190) {G2,W13,D3,L4,V2,M4} R(1183,60) { v1_xboole_0( X ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( X ) ), ! Y = X, r1_filter_2( X, Y, X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := Y
% 65.23/65.60 Y := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqrefl: (61623) {G0,W10,D3,L3,V1,M3} { v1_xboole_0( X ), ! m1_subset_1( X
% 65.23/65.60 , k1_zfmisc_1( X ) ), r1_filter_2( X, X, X ) }.
% 65.23/65.60 parent0[0]: (61622) {G2,W13,D3,L4,V2,M4} { ! Y = X, v1_xboole_0( Y ), !
% 65.23/65.60 m1_subset_1( X, k1_zfmisc_1( Y ) ), r1_filter_2( Y, X, Y ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61624) {G1,W6,D2,L2,V1,M2} { v1_xboole_0( X ), r1_filter_2( X
% 65.23/65.60 , X, X ) }.
% 65.23/65.60 parent0[1]: (61623) {G0,W10,D3,L3,V1,M3} { v1_xboole_0( X ), ! m1_subset_1
% 65.23/65.60 ( X, k1_zfmisc_1( X ) ), r1_filter_2( X, X, X ) }.
% 65.23/65.60 parent1[0]: (1183) {G1,W4,D3,L1,V1,M1} R(68,62) { m1_subset_1( X,
% 65.23/65.60 k1_zfmisc_1( X ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1194) {G3,W6,D2,L2,V1,M2} Q(1190);r(1183) { v1_xboole_0( X )
% 65.23/65.60 , r1_filter_2( X, X, X ) }.
% 65.23/65.60 parent0: (61624) {G1,W6,D2,L2,V1,M2} { v1_xboole_0( X ), r1_filter_2( X, X
% 65.23/65.60 , X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61625) {G0,W25,D4,L8,V2,M8} { u1_struct_0( X ) ==> k19_filter_2(
% 65.23/65.60 X, Y ), v3_struct_0( X ), ! v10_lattices( X ), ! l3_lattices( X ),
% 65.23/65.60 v1_xboole_0( Y ), ! m1_subset_1( Y, k1_zfmisc_1( u1_struct_0( X ) ) ), !
% 65.23/65.60 v14_lattices( X ), ! r2_hidden( k6_lattices( X ), Y ) }.
% 65.23/65.60 parent0[7]: (70) {G0,W25,D4,L8,V2,M8} I { v3_struct_0( X ), ! v10_lattices
% 65.23/65.60 ( X ), ! l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y,
% 65.23/65.60 k1_zfmisc_1( u1_struct_0( X ) ) ), ! v14_lattices( X ), ! r2_hidden(
% 65.23/65.60 k6_lattices( X ), Y ), k19_filter_2( X, Y ) ==> u1_struct_0( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61626) {G1,W21,D4,L7,V0,M7} { u1_struct_0( skol1 ) ==>
% 65.23/65.60 k19_filter_2( skol1, skol16 ), v3_struct_0( skol1 ), ! v10_lattices(
% 65.23/65.60 skol1 ), ! l3_lattices( skol1 ), v1_xboole_0( skol16 ), ! m1_subset_1(
% 65.23/65.60 skol16, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! v14_lattices( skol1 )
% 65.23/65.60 }.
% 65.23/65.60 parent0[7]: (61625) {G0,W25,D4,L8,V2,M8} { u1_struct_0( X ) ==>
% 65.23/65.60 k19_filter_2( X, Y ), v3_struct_0( X ), ! v10_lattices( X ), !
% 65.23/65.60 l3_lattices( X ), v1_xboole_0( Y ), ! m1_subset_1( Y, k1_zfmisc_1(
% 65.23/65.60 u1_struct_0( X ) ) ), ! v14_lattices( X ), ! r2_hidden( k6_lattices( X )
% 65.23/65.60 , Y ) }.
% 65.23/65.60 parent1[0]: (5) {G0,W4,D3,L1,V0,M1} I { r2_hidden( k6_lattices( skol1 ),
% 65.23/65.60 skol16 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := skol1
% 65.23/65.60 Y := skol16
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61627) {G1,W19,D4,L6,V0,M6} { u1_struct_0( skol1 ) ==>
% 65.23/65.60 k19_filter_2( skol1, skol16 ), ! v10_lattices( skol1 ), ! l3_lattices(
% 65.23/65.60 skol1 ), v1_xboole_0( skol16 ), ! m1_subset_1( skol16, k1_zfmisc_1(
% 65.23/65.60 u1_struct_0( skol1 ) ) ), ! v14_lattices( skol1 ) }.
% 65.23/65.60 parent0[0]: (0) {G0,W2,D2,L1,V0,M1} I { ! v3_struct_0( skol1 ) }.
% 65.23/65.60 parent1[1]: (61626) {G1,W21,D4,L7,V0,M7} { u1_struct_0( skol1 ) ==>
% 65.23/65.60 k19_filter_2( skol1, skol16 ), v3_struct_0( skol1 ), ! v10_lattices(
% 65.23/65.60 skol1 ), ! l3_lattices( skol1 ), v1_xboole_0( skol16 ), ! m1_subset_1(
% 65.23/65.60 skol16, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! v14_lattices( skol1 )
% 65.23/65.60 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61628) {G1,W19,D4,L6,V0,M6} { k19_filter_2( skol1, skol16 ) ==>
% 65.23/65.60 u1_struct_0( skol1 ), ! v10_lattices( skol1 ), ! l3_lattices( skol1 ),
% 65.23/65.60 v1_xboole_0( skol16 ), ! m1_subset_1( skol16, k1_zfmisc_1( u1_struct_0(
% 65.23/65.60 skol1 ) ) ), ! v14_lattices( skol1 ) }.
% 65.23/65.60 parent0[0]: (61627) {G1,W19,D4,L6,V0,M6} { u1_struct_0( skol1 ) ==>
% 65.23/65.60 k19_filter_2( skol1, skol16 ), ! v10_lattices( skol1 ), ! l3_lattices(
% 65.23/65.60 skol1 ), v1_xboole_0( skol16 ), ! m1_subset_1( skol16, k1_zfmisc_1(
% 65.23/65.60 u1_struct_0( skol1 ) ) ), ! v14_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1235) {G1,W19,D4,L6,V0,M6} R(70,5);r(0) { ! v10_lattices(
% 65.23/65.60 skol1 ), ! l3_lattices( skol1 ), v1_xboole_0( skol16 ), ! m1_subset_1(
% 65.23/65.60 skol16, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! v14_lattices( skol1 ),
% 65.23/65.60 k19_filter_2( skol1, skol16 ) ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 parent0: (61628) {G1,W19,D4,L6,V0,M6} { k19_filter_2( skol1, skol16 ) ==>
% 65.23/65.60 u1_struct_0( skol1 ), ! v10_lattices( skol1 ), ! l3_lattices( skol1 ),
% 65.23/65.60 v1_xboole_0( skol16 ), ! m1_subset_1( skol16, k1_zfmisc_1( u1_struct_0(
% 65.23/65.60 skol1 ) ) ), ! v14_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 5
% 65.23/65.60 1 ==> 0
% 65.23/65.60 2 ==> 1
% 65.23/65.60 3 ==> 2
% 65.23/65.60 4 ==> 3
% 65.23/65.60 5 ==> 4
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61629) {G1,W7,D3,L2,V2,M2} { ! r2_hidden( X, Y ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( k1_xboole_0 ) ) }.
% 65.23/65.60 parent0[2]: (72) {G0,W9,D3,L3,V3,M3} I { ! r2_hidden( X, Y ), ! m1_subset_1
% 65.23/65.60 ( Y, k1_zfmisc_1( Z ) ), ! v1_xboole_0( Z ) }.
% 65.23/65.60 parent1[0]: (46) {G0,W2,D2,L1,V0,M1} I { v1_xboole_0( k1_xboole_0 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 Z := k1_xboole_0
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1348) {G1,W7,D3,L2,V2,M2} R(72,46) { ! r2_hidden( X, Y ), !
% 65.23/65.60 m1_subset_1( Y, k1_zfmisc_1( k1_xboole_0 ) ) }.
% 65.23/65.60 parent0: (61629) {G1,W7,D3,L2,V2,M2} { ! r2_hidden( X, Y ), ! m1_subset_1
% 65.23/65.60 ( Y, k1_zfmisc_1( k1_xboole_0 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 Y := Y
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61630) {G1,W7,D3,L2,V1,M2} { ! m1_subset_1( u1_struct_0(
% 65.23/65.60 skol1 ), k1_zfmisc_1( X ) ), ! v1_xboole_0( X ) }.
% 65.23/65.60 parent0[0]: (72) {G0,W9,D3,L3,V3,M3} I { ! r2_hidden( X, Y ), ! m1_subset_1
% 65.23/65.60 ( Y, k1_zfmisc_1( Z ) ), ! v1_xboole_0( Z ) }.
% 65.23/65.60 parent1[0]: (988) {G4,W5,D3,L1,V0,M1} R(65,232);r(378) { r2_hidden(
% 65.23/65.60 k6_lattices( skol1 ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := k6_lattices( skol1 )
% 65.23/65.60 Y := u1_struct_0( skol1 )
% 65.23/65.60 Z := X
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1565) {G5,W7,D3,L2,V1,M2} R(988,72) { ! m1_subset_1(
% 65.23/65.60 u1_struct_0( skol1 ), k1_zfmisc_1( X ) ), ! v1_xboole_0( X ) }.
% 65.23/65.60 parent0: (61630) {G1,W7,D3,L2,V1,M2} { ! m1_subset_1( u1_struct_0( skol1 )
% 65.23/65.60 , k1_zfmisc_1( X ) ), ! v1_xboole_0( X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 X := X
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 1 ==> 1
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61631) {G2,W4,D2,L1,V0,M1} { r1_filter_2( skol16, skol16,
% 65.23/65.60 skol16 ) }.
% 65.23/65.60 parent0[0]: (158) {G1,W2,D2,L1,V0,M1} R(74,5) { ! v1_xboole_0( skol16 ) }.
% 65.23/65.60 parent1[0]: (1194) {G3,W6,D2,L2,V1,M2} Q(1190);r(1183) { v1_xboole_0( X ),
% 65.23/65.60 r1_filter_2( X, X, X ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 X := skol16
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (1654) {G4,W4,D2,L1,V0,M1} R(1194,158) { r1_filter_2( skol16,
% 65.23/65.60 skol16, skol16 ) }.
% 65.23/65.60 parent0: (61631) {G2,W4,D2,L1,V0,M1} { r1_filter_2( skol16, skol16, skol16
% 65.23/65.60 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61633) {G1,W5,D3,L1,V0,M1} { k17_filter_2( skol1 ) ==>
% 65.23/65.60 u1_struct_0( skol1 ) }.
% 65.23/65.60 parent0[0]: (153) {G1,W7,D3,L2,V0,M2} R(25,2);r(0) { ! v10_lattices( skol1
% 65.23/65.60 ), k17_filter_2( skol1 ) ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (2763) {G2,W5,D3,L1,V0,M1} S(153);r(1) { k17_filter_2( skol1 )
% 65.23/65.60 ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 parent0: (61633) {G1,W5,D3,L1,V0,M1} { k17_filter_2( skol1 ) ==>
% 65.23/65.60 u1_struct_0( skol1 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61636) {G0,W10,D3,L2,V0,M2} { ! skol16 ==> u1_struct_0( skol1 ),
% 65.23/65.60 ! r1_filter_2( u1_struct_0( skol1 ), skol16, k17_filter_2( skol1 ) ) }.
% 65.23/65.60 parent0[1]: (6) {G0,W10,D3,L2,V0,M2} I { ! r1_filter_2( u1_struct_0( skol1
% 65.23/65.60 ), skol16, k17_filter_2( skol1 ) ), ! u1_struct_0( skol1 ) ==> skol16
% 65.23/65.60 }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 paramod: (61637) {G1,W10,D3,L2,V0,M2} { ! r1_filter_2( u1_struct_0( skol1
% 65.23/65.60 ), skol16, u1_struct_0( skol1 ) ), ! skol16 ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 parent0[0]: (2763) {G2,W5,D3,L1,V0,M1} S(153);r(1) { k17_filter_2( skol1 )
% 65.23/65.60 ==> u1_struct_0( skol1 ) }.
% 65.23/65.60 parent1[1; 5]: (61636) {G0,W10,D3,L2,V0,M2} { ! skol16 ==> u1_struct_0(
% 65.23/65.60 skol1 ), ! r1_filter_2( u1_struct_0( skol1 ), skol16, k17_filter_2( skol1
% 65.23/65.60 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 substitution1:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 eqswap: (61638) {G1,W10,D3,L2,V0,M2} { ! u1_struct_0( skol1 ) ==> skol16,
% 65.23/65.60 ! r1_filter_2( u1_struct_0( skol1 ), skol16, u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0[1]: (61637) {G1,W10,D3,L2,V0,M2} { ! r1_filter_2( u1_struct_0(
% 65.23/65.60 skol1 ), skol16, u1_struct_0( skol1 ) ), ! skol16 ==> u1_struct_0( skol1
% 65.23/65.60 ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 subsumption: (2767) {G3,W10,D3,L2,V0,M2} P(2763,6) { ! r1_filter_2(
% 65.23/65.60 u1_struct_0( skol1 ), skol16, u1_struct_0( skol1 ) ), ! u1_struct_0(
% 65.23/65.60 skol1 ) ==> skol16 }.
% 65.23/65.60 parent0: (61638) {G1,W10,D3,L2,V0,M2} { ! u1_struct_0( skol1 ) ==> skol16
% 65.23/65.60 , ! r1_filter_2( u1_struct_0( skol1 ), skol16, u1_struct_0( skol1 ) ) }.
% 65.23/65.60 substitution0:
% 65.23/65.60 end
% 65.23/65.60 permutation0:
% 65.23/65.60 0 ==> 1
% 65.23/65.60 1 ==> 0
% 65.23/65.60 end
% 65.23/65.60
% 65.23/65.60 resolution: (61639) {G2,W6,D4,L1,V0,M1} { r2_hidden( skol6( u1_struct_0(
% 65.23/65.60 skol1 ) ), u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent0[0]: (378) {G3,W3,D3,L1,V0,M1} R(44,83);r(0) { ! v1_xboole_0(
% 65.23/65.60 u1_struct_0( skol1 ) ) }.
% 65.23/65.60 parent1[0]: (1028) {G1,W6,D3,L2,V1,M2} R(65,41) { v1_xboole_0( X ),
% 149.79/150.21 r2_hidden( skol6( X ), X ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 end
% 149.79/150.21 substitution1:
% 149.79/150.21 X := u1_struct_0( skol1 )
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 subsumption: (3566) {G4,W6,D4,L1,V0,M1} R(1028,378) { r2_hidden( skol6(
% 149.79/150.21 u1_struct_0( skol1 ) ), u1_struct_0( skol1 ) ) }.
% 149.79/150.21 parent0: (61639) {G2,W6,D4,L1,V0,M1} { r2_hidden( skol6( u1_struct_0(
% 149.79/150.21 skol1 ) ), u1_struct_0( skol1 ) ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 end
% 149.79/150.21 permutation0:
% 149.79/150.21 0 ==> 0
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 resolution: (61640) {G1,W5,D2,L2,V0,M2} { ! l3_lattices( skol1 ),
% 149.79/150.21 m2_lattice4( skol16, skol1 ) }.
% 149.79/150.21 parent0[0]: (267) {G1,W7,D2,L3,V0,M3} R(35,3);r(0) { ! v10_lattices( skol1
% 149.79/150.21 ), ! l3_lattices( skol1 ), m2_lattice4( skol16, skol1 ) }.
% 149.79/150.21 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 end
% 149.79/150.21 substitution1:
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 resolution: (61641) {G1,W3,D2,L1,V0,M1} { m2_lattice4( skol16, skol1 ) }.
% 149.79/150.21 parent0[0]: (61640) {G1,W5,D2,L2,V0,M2} { ! l3_lattices( skol1 ),
% 149.79/150.21 m2_lattice4( skol16, skol1 ) }.
% 149.79/150.21 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { l3_lattices( skol1 ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 end
% 149.79/150.21 substitution1:
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 subsumption: (5323) {G2,W3,D2,L1,V0,M1} S(267);r(1);r(2) { m2_lattice4(
% 149.79/150.21 skol16, skol1 ) }.
% 149.79/150.21 parent0: (61641) {G1,W3,D2,L1,V0,M1} { m2_lattice4( skol16, skol1 ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 end
% 149.79/150.21 permutation0:
% 149.79/150.21 0 ==> 0
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 resolution: (61642) {G2,W11,D4,L4,V0,M4} { ! v10_lattices( skol1 ), !
% 149.79/150.21 l3_lattices( skol1 ), m1_subset_1( skol16, k1_zfmisc_1( u1_struct_0(
% 149.79/150.21 skol1 ) ) ), ! alpha4( skol1 ) }.
% 149.79/150.21 parent0[2]: (291) {G1,W14,D4,L5,V2,M5} R(36,20) { ! v10_lattices( X ), !
% 149.79/150.21 l3_lattices( X ), ! m2_lattice4( Y, X ), m1_subset_1( Y, k1_zfmisc_1(
% 149.79/150.21 u1_struct_0( X ) ) ), ! alpha4( X ) }.
% 149.79/150.21 parent1[0]: (5323) {G2,W3,D2,L1,V0,M1} S(267);r(1);r(2) { m2_lattice4(
% 149.79/150.21 skol16, skol1 ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 X := skol1
% 149.79/150.21 Y := skol16
% 149.79/150.21 end
% 149.79/150.21 substitution1:
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 resolution: (61643) {G1,W9,D4,L3,V0,M3} { ! l3_lattices( skol1 ),
% 149.79/150.21 m1_subset_1( skol16, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! alpha4(
% 149.79/150.21 skol1 ) }.
% 149.79/150.21 parent0[0]: (61642) {G2,W11,D4,L4,V0,M4} { ! v10_lattices( skol1 ), !
% 149.79/150.21 l3_lattices( skol1 ), m1_subset_1( skol16, k1_zfmisc_1( u1_struct_0(
% 149.79/150.21 skol1 ) ) ), ! alpha4( skol1 ) }.
% 149.79/150.21 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { v10_lattices( skol1 ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 end
% 149.79/150.21 substitution1:
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 subsumption: (6417) {G3,W9,D4,L3,V0,M3} R(291,5323);r(1) { ! l3_lattices(
% 149.79/150.21 skol1 ), m1_subset_1( skol16, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), !
% 149.79/150.21 alpha4( skol1 ) }.
% 149.79/150.21 parent0: (61643) {G1,W9,D4,L3,V0,M3} { ! l3_lattices( skol1 ), m1_subset_1
% 149.79/150.21 ( skol16, k1_zfmisc_1( u1_struct_0( skol1 ) ) ), ! alpha4( skol1 ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 end
% 149.79/150.21 permutation0:
% 149.79/150.21 0 ==> 0
% 149.79/150.21 1 ==> 1
% 149.79/150.21 2 ==> 2
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 resolution: (61644) {G2,W5,D3,L1,V0,M1} { ! m1_subset_1( u1_struct_0(
% 149.79/150.21 skol1 ), k1_zfmisc_1( k1_xboole_0 ) ) }.
% 149.79/150.21 parent0[0]: (1348) {G1,W7,D3,L2,V2,M2} R(72,46) { ! r2_hidden( X, Y ), !
% 149.79/150.21 m1_subset_1( Y, k1_zfmisc_1( k1_xboole_0 ) ) }.
% 149.79/150.21 parent1[0]: (3566) {G4,W6,D4,L1,V0,M1} R(1028,378) { r2_hidden( skol6(
% 149.79/150.21 u1_struct_0( skol1 ) ), u1_struct_0( skol1 ) ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 X := skol6( u1_struct_0( skol1 ) )
% 149.79/150.21 Y := u1_struct_0( skol1 )
% 149.79/150.21 end
% 149.79/150.21 substitution1:
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 subsumption: (8364) {G5,W5,D3,L1,V0,M1} R(1348,3566) { ! m1_subset_1(
% 149.79/150.21 u1_struct_0( skol1 ), k1_zfmisc_1( k1_xboole_0 ) ) }.
% 149.79/150.21 parent0: (61644) {G2,W5,D3,L1,V0,M1} { ! m1_subset_1( u1_struct_0( skol1 )
% 149.79/150.21 , k1_zfmisc_1( k1_xboole_0 ) ) }.
% 149.79/150.21 substitution0:
% 149.79/150.21 end
% 149.79/150.21 permutation0:
% 149.79/150.21 0 ==> 0
% 149.79/150.21 end
% 149.79/150.21
% 149.79/150.21 *** allocated 1297440 integers for termspace/termends
% 149.79/150.21 *** allocated 15000 integers for justifications
% 149.79/150.21 *** allocated 22500 integers for justifications
% 149.79/150.21 *** allocated 33750 integers for justifications
% 149.79/150.21 *** allocated 50625 integers for justifications
% 149.79/150.21 *** allocated 75937 integers for justifications
% 149.79/150.21 *** allocated 113905 integers for justifications
% 149.79/150.21 *** allocated 170857 integers for justifications
% 149.79/150.21 *** allocated 256285 integers for justifications
% 149.79/150.21 *** allocated 1946160 integers for termspace/termends
% 149.79/150.21 *** allocated 384427 integers for justifications
% 149.79/150.21 *** allocated 576640 integers for justifications
% 149.79/150.21 *** allocated 4378860 integers for clauses
% 149.79/150.21 *** allocated 2919240 integers for termspace/termends
% 149.79/150.21 *** allocated 864960 integers for justificaCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------