%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SEU094+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Tue Jul 19 07:10:35 EDT 2022
% Result : Theorem 1.94s 2.38s
% Output : Refutation 1.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU094+1 : TPTP v8.1.0. Released v3.2.0.
% 0.12/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Sun Jun 19 22:10:59 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.75/1.14 *** allocated 10000 integers for termspace/termends
% 0.75/1.14 *** allocated 10000 integers for clauses
% 0.75/1.14 *** allocated 10000 integers for justifications
% 0.75/1.14 Bliksem 1.12
% 0.75/1.14
% 0.75/1.14
% 0.75/1.14 Automatic Strategy Selection
% 0.75/1.14
% 0.75/1.14
% 0.75/1.14 Clauses:
% 0.75/1.14
% 0.75/1.14 { ! in( X, Y ), ! in( Y, X ) }.
% 0.75/1.14 { ! ordinal( X ), ! element( Y, X ), epsilon_transitive( Y ) }.
% 0.75/1.14 { ! ordinal( X ), ! element( Y, X ), epsilon_connected( Y ) }.
% 0.75/1.14 { ! ordinal( X ), ! element( Y, X ), ordinal( Y ) }.
% 0.75/1.14 { ! empty( X ), finite( X ) }.
% 0.75/1.14 { ! empty( X ), function( X ) }.
% 0.75/1.14 { ! ordinal( X ), epsilon_transitive( X ) }.
% 0.75/1.14 { ! ordinal( X ), epsilon_connected( X ) }.
% 0.75/1.14 { ! empty( X ), relation( X ) }.
% 0.75/1.14 { ! empty( X ), ! ordinal( X ), alpha2( X ) }.
% 0.75/1.14 { ! empty( X ), ! ordinal( X ), natural( X ) }.
% 0.75/1.14 { ! alpha2( X ), epsilon_transitive( X ) }.
% 0.75/1.14 { ! alpha2( X ), epsilon_connected( X ) }.
% 0.75/1.14 { ! alpha2( X ), ordinal( X ) }.
% 0.75/1.14 { ! epsilon_transitive( X ), ! epsilon_connected( X ), ! ordinal( X ),
% 0.75/1.14 alpha2( X ) }.
% 0.75/1.14 { ! finite( X ), ! element( Y, powerset( X ) ), finite( Y ) }.
% 0.75/1.14 { ! relation( X ), ! empty( X ), ! function( X ), relation( X ) }.
% 0.75/1.14 { ! relation( X ), ! empty( X ), ! function( X ), function( X ) }.
% 0.75/1.14 { ! relation( X ), ! empty( X ), ! function( X ), one_to_one( X ) }.
% 0.75/1.14 { ! epsilon_transitive( X ), ! epsilon_connected( X ), ordinal( X ) }.
% 0.75/1.14 { ! empty( X ), epsilon_transitive( X ) }.
% 0.75/1.14 { ! empty( X ), epsilon_connected( X ) }.
% 0.75/1.14 { ! empty( X ), ordinal( X ) }.
% 0.75/1.14 { ! element( X, positive_rationals ), ! ordinal( X ), alpha3( X ) }.
% 0.75/1.14 { ! element( X, positive_rationals ), ! ordinal( X ), natural( X ) }.
% 0.75/1.14 { ! alpha3( X ), epsilon_transitive( X ) }.
% 0.75/1.14 { ! alpha3( X ), epsilon_connected( X ) }.
% 0.75/1.14 { ! alpha3( X ), ordinal( X ) }.
% 0.75/1.14 { ! epsilon_transitive( X ), ! epsilon_connected( X ), ! ordinal( X ),
% 0.75/1.14 alpha3( X ) }.
% 0.75/1.14 { element( skol1( X ), X ) }.
% 0.75/1.14 { empty( empty_set ) }.
% 0.75/1.14 { relation( empty_set ) }.
% 0.75/1.14 { relation_empty_yielding( empty_set ) }.
% 0.75/1.14 { ! empty( powerset( X ) ) }.
% 0.75/1.14 { empty( empty_set ) }.
% 0.75/1.14 { relation( empty_set ) }.
% 0.75/1.14 { relation_empty_yielding( empty_set ) }.
% 0.75/1.14 { function( empty_set ) }.
% 0.75/1.14 { one_to_one( empty_set ) }.
% 0.75/1.14 { empty( empty_set ) }.
% 0.75/1.14 { epsilon_transitive( empty_set ) }.
% 0.75/1.14 { epsilon_connected( empty_set ) }.
% 0.75/1.14 { ordinal( empty_set ) }.
% 0.75/1.14 { ! ordinal( X ), epsilon_transitive( union( X ) ) }.
% 0.75/1.14 { ! ordinal( X ), epsilon_connected( union( X ) ) }.
% 0.75/1.14 { ! ordinal( X ), ordinal( union( X ) ) }.
% 0.75/1.14 { empty( empty_set ) }.
% 0.75/1.14 { relation( empty_set ) }.
% 0.75/1.14 { ! empty( positive_rationals ) }.
% 0.75/1.14 { ! finite( X ), ! finite( skol2( Y ) ), finite( union( X ) ) }.
% 0.75/1.14 { ! finite( X ), in( skol2( X ), X ), finite( union( X ) ) }.
% 0.75/1.14 { ! empty( skol3 ) }.
% 0.75/1.14 { epsilon_transitive( skol3 ) }.
% 0.75/1.14 { epsilon_connected( skol3 ) }.
% 0.75/1.14 { ordinal( skol3 ) }.
% 0.75/1.14 { natural( skol3 ) }.
% 0.75/1.14 { ! empty( skol4 ) }.
% 0.75/1.14 { finite( skol4 ) }.
% 0.75/1.14 { relation( skol5 ) }.
% 0.75/1.14 { function( skol5 ) }.
% 0.75/1.14 { function_yielding( skol5 ) }.
% 0.75/1.14 { relation( skol6 ) }.
% 0.75/1.14 { function( skol6 ) }.
% 0.75/1.14 { epsilon_transitive( skol7 ) }.
% 0.75/1.14 { epsilon_connected( skol7 ) }.
% 0.75/1.14 { ordinal( skol7 ) }.
% 0.75/1.14 { epsilon_transitive( skol8 ) }.
% 0.75/1.14 { epsilon_connected( skol8 ) }.
% 0.75/1.14 { ordinal( skol8 ) }.
% 0.75/1.14 { being_limit_ordinal( skol8 ) }.
% 0.75/1.14 { empty( skol9 ) }.
% 0.75/1.14 { relation( skol9 ) }.
% 0.75/1.14 { empty( X ), ! empty( skol10( Y ) ) }.
% 0.75/1.14 { empty( X ), element( skol10( X ), powerset( X ) ) }.
% 0.75/1.14 { empty( skol11 ) }.
% 0.75/1.14 { element( skol12, positive_rationals ) }.
% 0.75/1.14 { ! empty( skol12 ) }.
% 0.75/1.14 { epsilon_transitive( skol12 ) }.
% 0.75/1.14 { epsilon_connected( skol12 ) }.
% 0.75/1.14 { ordinal( skol12 ) }.
% 0.75/1.14 { empty( skol13( Y ) ) }.
% 0.75/1.14 { relation( skol13( Y ) ) }.
% 0.75/1.14 { function( skol13( Y ) ) }.
% 0.75/1.14 { one_to_one( skol13( Y ) ) }.
% 0.75/1.14 { epsilon_transitive( skol13( Y ) ) }.
% 0.75/1.14 { epsilon_connected( skol13( Y ) ) }.
% 0.75/1.14 { ordinal( skol13( Y ) ) }.
% 0.75/1.14 { natural( skol13( Y ) ) }.
% 0.75/1.14 { finite( skol13( Y ) ) }.
% 0.75/1.14 { element( skol13( X ), powerset( X ) ) }.
% 0.75/1.14 { relation( skol14 ) }.
% 0.75/1.14 { empty( skol14 ) }.
% 0.75/1.14 { function( skol14 ) }.
% 0.75/1.14 { relation( skol15 ) }.
% 0.75/1.14 { function( skol15 ) }.
% 0.75/1.14 { one_to_one( skol15 ) }.
% 0.75/1.14 { empty( skol15 ) }.
% 0.75/1.14 { epsilon_transitive( skol15 ) }.
% 0.75/1.14 { epsilon_connected( skol15 ) }.
% 0.75/1.14 { ordinal( skol15 ) }.
% 0.75/1.14 { relation( skol16 ) }.
% 0.75/1.14 { function( skol16 ) }.
% 0.75/1.14 { transfinite_sequence( skol16 ) }.
% 0.75/1.14 { ordinal_yielding( skol16 ) }.
% 0.75/1.14 { ! empty( skol17 ) }.
% 0.75/1.14 { relation( skol17 ) }.
% 0.75/1.14 { empty( skol18( Y ) ) }.
% 0.75/1.14 { element( skol18( X ), powerset( X ) ) }.
% 1.62/2.06 { ! empty( skol19 ) }.
% 1.62/2.06 { element( skol20, positive_rationals ) }.
% 1.62/2.06 { empty( skol20 ) }.
% 1.62/2.06 { epsilon_transitive( skol20 ) }.
% 1.62/2.06 { epsilon_connected( skol20 ) }.
% 1.62/2.06 { ordinal( skol20 ) }.
% 1.62/2.06 { natural( skol20 ) }.
% 1.62/2.06 { empty( X ), ! empty( skol21( Y ) ) }.
% 1.62/2.06 { empty( X ), finite( skol21( Y ) ) }.
% 1.62/2.06 { empty( X ), element( skol21( X ), powerset( X ) ) }.
% 1.62/2.06 { relation( skol22 ) }.
% 1.62/2.06 { function( skol22 ) }.
% 1.62/2.06 { one_to_one( skol22 ) }.
% 1.62/2.06 { ! empty( skol23 ) }.
% 1.62/2.06 { epsilon_transitive( skol23 ) }.
% 1.62/2.06 { epsilon_connected( skol23 ) }.
% 1.62/2.06 { ordinal( skol23 ) }.
% 1.62/2.06 { relation( skol24 ) }.
% 1.62/2.06 { relation_empty_yielding( skol24 ) }.
% 1.62/2.06 { relation( skol25 ) }.
% 1.62/2.06 { relation_empty_yielding( skol25 ) }.
% 1.62/2.06 { function( skol25 ) }.
% 1.62/2.06 { relation( skol26 ) }.
% 1.62/2.06 { function( skol26 ) }.
% 1.62/2.06 { transfinite_sequence( skol26 ) }.
% 1.62/2.06 { relation( skol27 ) }.
% 1.62/2.06 { relation_non_empty( skol27 ) }.
% 1.62/2.06 { function( skol27 ) }.
% 1.62/2.06 { subset( X, X ) }.
% 1.62/2.06 { subset( X, powerset( union( X ) ) ) }.
% 1.62/2.06 { ! subset( X, Y ), ! finite( Y ), finite( X ) }.
% 1.62/2.06 { ! in( X, Y ), element( X, Y ) }.
% 1.62/2.06 { ! finite( X ), finite( powerset( X ) ) }.
% 1.62/2.06 { ! finite( powerset( X ) ), finite( X ) }.
% 1.62/2.06 { alpha4( skol28 ), finite( union( skol28 ) ) }.
% 1.62/2.06 { alpha4( skol28 ), ! finite( skol28 ), ! alpha1( skol28 ) }.
% 1.62/2.06 { ! alpha4( X ), finite( X ) }.
% 1.62/2.06 { ! alpha4( X ), alpha1( X ) }.
% 1.62/2.06 { ! alpha4( X ), ! finite( union( X ) ) }.
% 1.62/2.06 { ! finite( X ), ! alpha1( X ), finite( union( X ) ), alpha4( X ) }.
% 1.62/2.06 { ! alpha1( X ), ! in( Y, X ), finite( Y ) }.
% 1.62/2.06 { ! finite( skol29( Y ) ), alpha1( X ) }.
% 1.62/2.06 { in( skol29( X ), X ), alpha1( X ) }.
% 1.62/2.06 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 1.62/2.06 { ! element( X, powerset( Y ) ), subset( X, Y ) }.
% 1.62/2.06 { ! subset( X, Y ), element( X, powerset( Y ) ) }.
% 1.62/2.06 { ! in( X, Z ), ! element( Z, powerset( Y ) ), element( X, Y ) }.
% 1.62/2.06 { ! in( X, Y ), ! element( Y, powerset( Z ) ), ! empty( Z ) }.
% 1.62/2.06 { ! empty( X ), X = empty_set }.
% 1.62/2.06 { ! in( X, Y ), ! empty( Y ) }.
% 1.62/2.06 { ! empty( X ), X = Y, ! empty( Y ) }.
% 1.62/2.06 { ! in( X, Y ), subset( X, union( Y ) ) }.
% 1.62/2.06
% 1.62/2.06 percentage equality = 0.008439, percentage horn = 0.947368
% 1.62/2.06 This is a problem with some equality
% 1.62/2.06
% 1.62/2.06
% 1.62/2.06
% 1.62/2.06 Options Used:
% 1.62/2.06
% 1.62/2.06 useres = 1
% 1.62/2.06 useparamod = 1
% 1.62/2.06 useeqrefl = 1
% 1.62/2.06 useeqfact = 1
% 1.62/2.06 usefactor = 1
% 1.62/2.06 usesimpsplitting = 0
% 1.62/2.06 usesimpdemod = 5
% 1.62/2.06 usesimpres = 3
% 1.62/2.06
% 1.62/2.06 resimpinuse = 1000
% 1.62/2.06 resimpclauses = 20000
% 1.62/2.06 substype = eqrewr
% 1.62/2.06 backwardsubs = 1
% 1.62/2.06 selectoldest = 5
% 1.62/2.06
% 1.62/2.06 litorderings [0] = split
% 1.62/2.06 litorderings [1] = extend the termordering, first sorting on arguments
% 1.62/2.06
% 1.62/2.06 termordering = kbo
% 1.62/2.06
% 1.62/2.06 litapriori = 0
% 1.62/2.06 termapriori = 1
% 1.62/2.06 litaposteriori = 0
% 1.62/2.06 termaposteriori = 0
% 1.62/2.06 demodaposteriori = 0
% 1.62/2.06 ordereqreflfact = 0
% 1.62/2.06
% 1.62/2.06 litselect = negord
% 1.62/2.06
% 1.62/2.06 maxweight = 15
% 1.62/2.06 maxdepth = 30000
% 1.62/2.06 maxlength = 115
% 1.62/2.06 maxnrvars = 195
% 1.62/2.06 excuselevel = 1
% 1.62/2.06 increasemaxweight = 1
% 1.62/2.06
% 1.62/2.06 maxselected = 10000000
% 1.62/2.06 maxnrclauses = 10000000
% 1.62/2.06
% 1.62/2.06 showgenerated = 0
% 1.62/2.06 showkept = 0
% 1.62/2.06 showselected = 0
% 1.62/2.06 showdeleted = 0
% 1.62/2.06 showresimp = 1
% 1.62/2.06 showstatus = 2000
% 1.62/2.06
% 1.62/2.06 prologoutput = 0
% 1.62/2.06 nrgoals = 5000000
% 1.62/2.06 totalproof = 1
% 1.62/2.06
% 1.62/2.06 Symbols occurring in the translation:
% 1.62/2.06
% 1.62/2.06 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.62/2.06 . [1, 2] (w:1, o:66, a:1, s:1, b:0),
% 1.62/2.06 ! [4, 1] (w:0, o:33, a:1, s:1, b:0),
% 1.62/2.06 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.62/2.06 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.62/2.06 in [37, 2] (w:1, o:90, a:1, s:1, b:0),
% 1.62/2.06 ordinal [38, 1] (w:1, o:39, a:1, s:1, b:0),
% 1.62/2.06 element [39, 2] (w:1, o:91, a:1, s:1, b:0),
% 1.62/2.06 epsilon_transitive [40, 1] (w:1, o:40, a:1, s:1, b:0),
% 1.62/2.06 epsilon_connected [41, 1] (w:1, o:41, a:1, s:1, b:0),
% 1.62/2.06 empty [42, 1] (w:1, o:42, a:1, s:1, b:0),
% 1.62/2.06 finite [43, 1] (w:1, o:43, a:1, s:1, b:0),
% 1.62/2.06 function [44, 1] (w:1, o:44, a:1, s:1, b:0),
% 1.62/2.06 relation [45, 1] (w:1, o:45, a:1, s:1, b:0),
% 1.62/2.06 natural [46, 1] (w:1, o:38, a:1, s:1, b:0),
% 1.62/2.06 powerset [47, 1] (w:1, o:48, a:1, s:1, b:0),
% 1.62/2.06 one_to_one [48, 1] (w:1, o:46, a:1, s:1, b:0),
% 1.62/2.06 positive_rationals [49, 0] (w:1, o:8, a:1, s:1, b:0),
% 1.62/2.06 empty_set [50, 0] (w:1, o:9, a:1, s:1, b:0),
% 1.62/2.06 relation_empty_yielding [51, 1] (w:1, o:49, a:1, s:1, b:0),
% 1.94/2.38 union [52, 1] (w:1, o:58, a:1, s:1, b:0),
% 1.94/2.38 function_yielding [53, 1] (w:1, o:59, a:1, s:1, b:0),
% 1.94/2.38 being_limit_ordinal [54, 1] (w:1, o:64, a:1, s:1, b:0),
% 1.94/2.38 transfinite_sequence [55, 1] (w:1, o:57, a:1, s:1, b:0),
% 1.94/2.38 ordinal_yielding [56, 1] (w:1, o:47, a:1, s:1, b:0),
% 1.94/2.38 relation_non_empty [57, 1] (w:1, o:65, a:1, s:1, b:0),
% 1.94/2.38 subset [58, 2] (w:1, o:92, a:1, s:1, b:0),
% 1.94/2.38 alpha1 [60, 1] (w:1, o:60, a:1, s:1, b:1),
% 1.94/2.38 alpha2 [61, 1] (w:1, o:61, a:1, s:1, b:1),
% 1.94/2.38 alpha3 [62, 1] (w:1, o:62, a:1, s:1, b:1),
% 1.94/2.38 alpha4 [63, 1] (w:1, o:63, a:1, s:1, b:1),
% 1.94/2.38 skol1 [64, 1] (w:1, o:50, a:1, s:1, b:1),
% 1.94/2.38 skol2 [65, 1] (w:1, o:54, a:1, s:1, b:1),
% 1.94/2.38 skol3 [66, 0] (w:1, o:19, a:1, s:1, b:1),
% 1.94/2.38 skol4 [67, 0] (w:1, o:20, a:1, s:1, b:1),
% 1.94/2.38 skol5 [68, 0] (w:1, o:21, a:1, s:1, b:1),
% 1.94/2.38 skol6 [69, 0] (w:1, o:22, a:1, s:1, b:1),
% 1.94/2.38 skol7 [70, 0] (w:1, o:23, a:1, s:1, b:1),
% 1.94/2.38 skol8 [71, 0] (w:1, o:24, a:1, s:1, b:1),
% 1.94/2.38 skol9 [72, 0] (w:1, o:25, a:1, s:1, b:1),
% 1.94/2.38 skol10 [73, 1] (w:1, o:51, a:1, s:1, b:1),
% 1.94/2.38 skol11 [74, 0] (w:1, o:26, a:1, s:1, b:1),
% 1.94/2.38 skol12 [75, 0] (w:1, o:27, a:1, s:1, b:1),
% 1.94/2.38 skol13 [76, 1] (w:1, o:52, a:1, s:1, b:1),
% 1.94/2.38 skol14 [77, 0] (w:1, o:28, a:1, s:1, b:1),
% 1.94/2.38 skol15 [78, 0] (w:1, o:29, a:1, s:1, b:1),
% 1.94/2.38 skol16 [79, 0] (w:1, o:30, a:1, s:1, b:1),
% 1.94/2.38 skol17 [80, 0] (w:1, o:31, a:1, s:1, b:1),
% 1.94/2.38 skol18 [81, 1] (w:1, o:53, a:1, s:1, b:1),
% 1.94/2.38 skol19 [82, 0] (w:1, o:32, a:1, s:1, b:1),
% 1.94/2.38 skol20 [83, 0] (w:1, o:11, a:1, s:1, b:1),
% 1.94/2.38 skol21 [84, 1] (w:1, o:55, a:1, s:1, b:1),
% 1.94/2.38 skol22 [85, 0] (w:1, o:12, a:1, s:1, b:1),
% 1.94/2.38 skol23 [86, 0] (w:1, o:13, a:1, s:1, b:1),
% 1.94/2.38 skol24 [87, 0] (w:1, o:14, a:1, s:1, b:1),
% 1.94/2.38 skol25 [88, 0] (w:1, o:15, a:1, s:1, b:1),
% 1.94/2.38 skol26 [89, 0] (w:1, o:16, a:1, s:1, b:1),
% 1.94/2.38 skol27 [90, 0] (w:1, o:17, a:1, s:1, b:1),
% 1.94/2.38 skol28 [91, 0] (w:1, o:18, a:1, s:1, b:1),
% 1.94/2.38 skol29 [92, 1] (w:1, o:56, a:1, s:1, b:1).
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Starting Search:
% 1.94/2.38
% 1.94/2.38 *** allocated 15000 integers for clauses
% 1.94/2.38 *** allocated 22500 integers for clauses
% 1.94/2.38 *** allocated 33750 integers for clauses
% 1.94/2.38 *** allocated 50625 integers for clauses
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 75937 integers for clauses
% 1.94/2.38 *** allocated 15000 integers for termspace/termends
% 1.94/2.38 *** allocated 22500 integers for termspace/termends
% 1.94/2.38 *** allocated 113905 integers for clauses
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 6441
% 1.94/2.38 Kept: 2006
% 1.94/2.38 Inuse: 556
% 1.94/2.38 Deleted: 205
% 1.94/2.38 Deletedinuse: 122
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 33750 integers for termspace/termends
% 1.94/2.38 *** allocated 170857 integers for clauses
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 50625 integers for termspace/termends
% 1.94/2.38 *** allocated 256285 integers for clauses
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 12951
% 1.94/2.38 Kept: 4013
% 1.94/2.38 Inuse: 762
% 1.94/2.38 Deleted: 217
% 1.94/2.38 Deletedinuse: 122
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 75937 integers for termspace/termends
% 1.94/2.38 *** allocated 384427 integers for clauses
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 17190
% 1.94/2.38 Kept: 6014
% 1.94/2.38 Inuse: 908
% 1.94/2.38 Deleted: 259
% 1.94/2.38 Deletedinuse: 134
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 113905 integers for termspace/termends
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 23152
% 1.94/2.38 Kept: 8046
% 1.94/2.38 Inuse: 1121
% 1.94/2.38 Deleted: 278
% 1.94/2.38 Deletedinuse: 143
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 576640 integers for clauses
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 30520
% 1.94/2.38 Kept: 10145
% 1.94/2.38 Inuse: 1299
% 1.94/2.38 Deleted: 291
% 1.94/2.38 Deletedinuse: 144
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 170857 integers for termspace/termends
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 35005
% 1.94/2.38 Kept: 12305
% 1.94/2.38 Inuse: 1372
% 1.94/2.38 Deleted: 293
% 1.94/2.38 Deletedinuse: 144
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 864960 integers for clauses
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 38809
% 1.94/2.38 Kept: 14370
% 1.94/2.38 Inuse: 1438
% 1.94/2.38 Deleted: 302
% 1.94/2.38 Deletedinuse: 144
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 *** allocated 256285 integers for termspace/termends
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 43153
% 1.94/2.38 Kept: 16392
% 1.94/2.38 Inuse: 1500
% 1.94/2.38 Deleted: 319
% 1.94/2.38 Deletedinuse: 144
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Intermediate Status:
% 1.94/2.38 Generated: 47707
% 1.94/2.38 Kept: 18392
% 1.94/2.38 Inuse: 1616
% 1.94/2.38 Deleted: 337
% 1.94/2.38 Deletedinuse: 144
% 1.94/2.38
% 1.94/2.38 Resimplifying inuse:
% 1.94/2.38 Done
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Bliksems!, er is een bewijs:
% 1.94/2.38 % SZS status Theorem
% 1.94/2.38 % SZS output start Refutation
% 1.94/2.38
% 1.94/2.38 (31) {G0,W3,D3,L1,V1,M1} I { ! empty( powerset( X ) ) }.
% 1.94/2.38 (41) {G0,W8,D3,L3,V2,M3} I { ! finite( X ), ! finite( skol2( Y ) ), finite
% 1.94/2.38 ( union( X ) ) }.
% 1.94/2.38 (42) {G0,W9,D3,L3,V1,M3} I { ! finite( X ), in( skol2( X ), X ), finite(
% 1.94/2.38 union( X ) ) }.
% 1.94/2.38 (128) {G0,W3,D2,L1,V1,M1} I { subset( X, X ) }.
% 1.94/2.38 (129) {G0,W5,D4,L1,V1,M1} I { subset( X, powerset( union( X ) ) ) }.
% 1.94/2.38 (130) {G0,W7,D2,L3,V2,M3} I { ! subset( X, Y ), ! finite( Y ), finite( X )
% 1.94/2.38 }.
% 1.94/2.38 (132) {G0,W5,D3,L2,V1,M2} I { ! finite( X ), finite( powerset( X ) ) }.
% 1.94/2.38 (134) {G0,W5,D3,L2,V0,M2} I { alpha4( skol28 ), finite( union( skol28 ) )
% 1.94/2.38 }.
% 1.94/2.38 (135) {G0,W6,D2,L3,V0,M3} I { alpha4( skol28 ), ! finite( skol28 ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 (136) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), finite( X ) }.
% 1.94/2.38 (137) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), alpha1( X ) }.
% 1.94/2.38 (138) {G0,W5,D3,L2,V1,M2} I { ! alpha4( X ), ! finite( union( X ) ) }.
% 1.94/2.38 (140) {G0,W7,D2,L3,V2,M3} I { ! alpha1( X ), ! in( Y, X ), finite( Y ) }.
% 1.94/2.38 (141) {G0,W5,D3,L2,V2,M2} I { ! finite( skol29( Y ) ), alpha1( X ) }.
% 1.94/2.38 (142) {G0,W6,D3,L2,V1,M2} I { in( skol29( X ), X ), alpha1( X ) }.
% 1.94/2.38 (143) {G0,W8,D2,L3,V2,M3} I { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 1.94/2.38 (145) {G0,W7,D3,L2,V2,M2} I { ! subset( X, Y ), element( X, powerset( Y ) )
% 1.94/2.38 }.
% 1.94/2.38 (151) {G0,W7,D3,L2,V2,M2} I { ! in( X, Y ), subset( X, union( Y ) ) }.
% 1.94/2.38 (541) {G1,W6,D4,L2,V1,M2} R(130,129) { ! finite( powerset( union( X ) ) ),
% 1.94/2.38 finite( X ) }.
% 1.94/2.38 (681) {G1,W5,D3,L2,V0,M2} R(136,134) { finite( skol28 ), finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 (685) {G1,W6,D3,L2,V1,M2} R(136,42);r(138) { ! alpha4( X ), in( skol2( X )
% 1.94/2.38 , X ) }.
% 1.94/2.38 (686) {G1,W5,D3,L2,V2,M2} R(136,41);r(138) { ! alpha4( X ), ! finite( skol2
% 1.94/2.38 ( Y ) ) }.
% 1.94/2.38 (689) {G1,W5,D3,L2,V0,M2} R(137,134) { alpha1( skol28 ), finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 (817) {G1,W4,D3,L1,V1,M1} R(145,128) { element( X, powerset( X ) ) }.
% 1.94/2.38 (821) {G2,W4,D3,L1,V1,M1} R(817,143);r(31) { in( X, powerset( X ) ) }.
% 1.94/2.38 (848) {G3,W5,D3,L2,V1,M2} R(821,140) { ! alpha1( powerset( X ) ), finite( X
% 1.94/2.38 ) }.
% 1.94/2.38 (3935) {G4,W5,D3,L2,V2,M2} R(848,141) { finite( X ), ! finite( skol29( Y )
% 1.94/2.38 ) }.
% 1.94/2.38 (3978) {G5,W5,D3,L2,V2,M2} R(3935,686) { ! finite( skol29( X ) ), ! alpha4
% 1.94/2.38 ( Y ) }.
% 1.94/2.38 (4894) {G2,W2,D2,L1,V0,M1} R(681,132);r(541) { finite( skol28 ) }.
% 1.94/2.38 (4904) {G3,W4,D2,L2,V0,M2} R(4894,135) { alpha4( skol28 ), ! alpha1( skol28
% 1.94/2.38 ) }.
% 1.94/2.38 (4948) {G6,W5,D3,L2,V1,M2} R(4904,3978) { ! alpha1( skol28 ), ! finite(
% 1.94/2.38 skol29( X ) ) }.
% 1.94/2.38 (4951) {G4,W5,D3,L2,V1,M2} R(4904,686) { ! alpha1( skol28 ), ! finite(
% 1.94/2.38 skol2( X ) ) }.
% 1.94/2.38 (5092) {G7,W6,D3,L2,V2,M2} R(4948,141) { ! finite( skol29( X ) ), ! finite
% 1.94/2.38 ( skol29( Y ) ) }.
% 1.94/2.38 (5098) {G8,W3,D3,L1,V1,M1} F(5092) { ! finite( skol29( X ) ) }.
% 1.94/2.38 (5244) {G9,W6,D3,L2,V2,M2} R(5098,130) { ! subset( skol29( X ), Y ), !
% 1.94/2.38 finite( Y ) }.
% 1.94/2.38 (5389) {G5,W8,D3,L3,V2,M3} R(4951,140) { ! alpha1( skol28 ), ! alpha1( X )
% 1.94/2.38 , ! in( skol2( Y ), X ) }.
% 1.94/2.38 (5393) {G6,W6,D3,L2,V1,M2} F(5389) { ! alpha1( skol28 ), ! in( skol2( X ),
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 (19182) {G7,W2,D2,L1,V0,M1} R(685,4904);r(5393) { ! alpha1( skol28 ) }.
% 1.94/2.38 (19187) {G8,W3,D3,L1,V0,M1} R(19182,689) { finite( union( skol28 ) ) }.
% 1.94/2.38 (19188) {G8,W4,D3,L1,V0,M1} R(19182,142) { in( skol29( skol28 ), skol28 )
% 1.94/2.38 }.
% 1.94/2.38 (19200) {G10,W5,D3,L1,V1,M1} R(19187,5244) { ! subset( skol29( X ), union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 (19235) {G11,W0,D0,L0,V0,M0} R(19188,151);r(19200) { }.
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 % SZS output end Refutation
% 1.94/2.38 found a proof!
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Unprocessed initial clauses:
% 1.94/2.38
% 1.94/2.38 (19237) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 1.94/2.38 (19238) {G0,W7,D2,L3,V2,M3} { ! ordinal( X ), ! element( Y, X ),
% 1.94/2.38 epsilon_transitive( Y ) }.
% 1.94/2.38 (19239) {G0,W7,D2,L3,V2,M3} { ! ordinal( X ), ! element( Y, X ),
% 1.94/2.38 epsilon_connected( Y ) }.
% 1.94/2.38 (19240) {G0,W7,D2,L3,V2,M3} { ! ordinal( X ), ! element( Y, X ), ordinal(
% 1.94/2.38 Y ) }.
% 1.94/2.38 (19241) {G0,W4,D2,L2,V1,M2} { ! empty( X ), finite( X ) }.
% 1.94/2.38 (19242) {G0,W4,D2,L2,V1,M2} { ! empty( X ), function( X ) }.
% 1.94/2.38 (19243) {G0,W4,D2,L2,V1,M2} { ! ordinal( X ), epsilon_transitive( X ) }.
% 1.94/2.38 (19244) {G0,W4,D2,L2,V1,M2} { ! ordinal( X ), epsilon_connected( X ) }.
% 1.94/2.38 (19245) {G0,W4,D2,L2,V1,M2} { ! empty( X ), relation( X ) }.
% 1.94/2.38 (19246) {G0,W6,D2,L3,V1,M3} { ! empty( X ), ! ordinal( X ), alpha2( X )
% 1.94/2.38 }.
% 1.94/2.38 (19247) {G0,W6,D2,L3,V1,M3} { ! empty( X ), ! ordinal( X ), natural( X )
% 1.94/2.38 }.
% 1.94/2.38 (19248) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), epsilon_transitive( X ) }.
% 1.94/2.38 (19249) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), epsilon_connected( X ) }.
% 1.94/2.38 (19250) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), ordinal( X ) }.
% 1.94/2.38 (19251) {G0,W8,D2,L4,V1,M4} { ! epsilon_transitive( X ), !
% 1.94/2.38 epsilon_connected( X ), ! ordinal( X ), alpha2( X ) }.
% 1.94/2.38 (19252) {G0,W8,D3,L3,V2,M3} { ! finite( X ), ! element( Y, powerset( X ) )
% 1.94/2.38 , finite( Y ) }.
% 1.94/2.38 (19253) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 1.94/2.38 ), relation( X ) }.
% 1.94/2.38 (19254) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 1.94/2.38 ), function( X ) }.
% 1.94/2.38 (19255) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 1.94/2.38 ), one_to_one( X ) }.
% 1.94/2.38 (19256) {G0,W6,D2,L3,V1,M3} { ! epsilon_transitive( X ), !
% 1.94/2.38 epsilon_connected( X ), ordinal( X ) }.
% 1.94/2.38 (19257) {G0,W4,D2,L2,V1,M2} { ! empty( X ), epsilon_transitive( X ) }.
% 1.94/2.38 (19258) {G0,W4,D2,L2,V1,M2} { ! empty( X ), epsilon_connected( X ) }.
% 1.94/2.38 (19259) {G0,W4,D2,L2,V1,M2} { ! empty( X ), ordinal( X ) }.
% 1.94/2.38 (19260) {G0,W7,D2,L3,V1,M3} { ! element( X, positive_rationals ), !
% 1.94/2.38 ordinal( X ), alpha3( X ) }.
% 1.94/2.38 (19261) {G0,W7,D2,L3,V1,M3} { ! element( X, positive_rationals ), !
% 1.94/2.38 ordinal( X ), natural( X ) }.
% 1.94/2.38 (19262) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), epsilon_transitive( X ) }.
% 1.94/2.38 (19263) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), epsilon_connected( X ) }.
% 1.94/2.38 (19264) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), ordinal( X ) }.
% 1.94/2.38 (19265) {G0,W8,D2,L4,V1,M4} { ! epsilon_transitive( X ), !
% 1.94/2.38 epsilon_connected( X ), ! ordinal( X ), alpha3( X ) }.
% 1.94/2.38 (19266) {G0,W4,D3,L1,V1,M1} { element( skol1( X ), X ) }.
% 1.94/2.38 (19267) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 1.94/2.38 (19268) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 1.94/2.38 (19269) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( empty_set ) }.
% 1.94/2.38 (19270) {G0,W3,D3,L1,V1,M1} { ! empty( powerset( X ) ) }.
% 1.94/2.38 (19271) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 1.94/2.38 (19272) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 1.94/2.38 (19273) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( empty_set ) }.
% 1.94/2.38 (19274) {G0,W2,D2,L1,V0,M1} { function( empty_set ) }.
% 1.94/2.38 (19275) {G0,W2,D2,L1,V0,M1} { one_to_one( empty_set ) }.
% 1.94/2.38 (19276) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 1.94/2.38 (19277) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( empty_set ) }.
% 1.94/2.38 (19278) {G0,W2,D2,L1,V0,M1} { epsilon_connected( empty_set ) }.
% 1.94/2.38 (19279) {G0,W2,D2,L1,V0,M1} { ordinal( empty_set ) }.
% 1.94/2.38 (19280) {G0,W5,D3,L2,V1,M2} { ! ordinal( X ), epsilon_transitive( union( X
% 1.94/2.38 ) ) }.
% 1.94/2.38 (19281) {G0,W5,D3,L2,V1,M2} { ! ordinal( X ), epsilon_connected( union( X
% 1.94/2.38 ) ) }.
% 1.94/2.38 (19282) {G0,W5,D3,L2,V1,M2} { ! ordinal( X ), ordinal( union( X ) ) }.
% 1.94/2.38 (19283) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 1.94/2.38 (19284) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 1.94/2.38 (19285) {G0,W2,D2,L1,V0,M1} { ! empty( positive_rationals ) }.
% 1.94/2.38 (19286) {G0,W8,D3,L3,V2,M3} { ! finite( X ), ! finite( skol2( Y ) ),
% 1.94/2.38 finite( union( X ) ) }.
% 1.94/2.38 (19287) {G0,W9,D3,L3,V1,M3} { ! finite( X ), in( skol2( X ), X ), finite(
% 1.94/2.38 union( X ) ) }.
% 1.94/2.38 (19288) {G0,W2,D2,L1,V0,M1} { ! empty( skol3 ) }.
% 1.94/2.38 (19289) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol3 ) }.
% 1.94/2.38 (19290) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol3 ) }.
% 1.94/2.38 (19291) {G0,W2,D2,L1,V0,M1} { ordinal( skol3 ) }.
% 1.94/2.38 (19292) {G0,W2,D2,L1,V0,M1} { natural( skol3 ) }.
% 1.94/2.38 (19293) {G0,W2,D2,L1,V0,M1} { ! empty( skol4 ) }.
% 1.94/2.38 (19294) {G0,W2,D2,L1,V0,M1} { finite( skol4 ) }.
% 1.94/2.38 (19295) {G0,W2,D2,L1,V0,M1} { relation( skol5 ) }.
% 1.94/2.38 (19296) {G0,W2,D2,L1,V0,M1} { function( skol5 ) }.
% 1.94/2.38 (19297) {G0,W2,D2,L1,V0,M1} { function_yielding( skol5 ) }.
% 1.94/2.38 (19298) {G0,W2,D2,L1,V0,M1} { relation( skol6 ) }.
% 1.94/2.38 (19299) {G0,W2,D2,L1,V0,M1} { function( skol6 ) }.
% 1.94/2.38 (19300) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol7 ) }.
% 1.94/2.38 (19301) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol7 ) }.
% 1.94/2.38 (19302) {G0,W2,D2,L1,V0,M1} { ordinal( skol7 ) }.
% 1.94/2.38 (19303) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol8 ) }.
% 1.94/2.38 (19304) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol8 ) }.
% 1.94/2.38 (19305) {G0,W2,D2,L1,V0,M1} { ordinal( skol8 ) }.
% 1.94/2.38 (19306) {G0,W2,D2,L1,V0,M1} { being_limit_ordinal( skol8 ) }.
% 1.94/2.38 (19307) {G0,W2,D2,L1,V0,M1} { empty( skol9 ) }.
% 1.94/2.38 (19308) {G0,W2,D2,L1,V0,M1} { relation( skol9 ) }.
% 1.94/2.38 (19309) {G0,W5,D3,L2,V2,M2} { empty( X ), ! empty( skol10( Y ) ) }.
% 1.94/2.38 (19310) {G0,W7,D3,L2,V1,M2} { empty( X ), element( skol10( X ), powerset(
% 1.94/2.38 X ) ) }.
% 1.94/2.38 (19311) {G0,W2,D2,L1,V0,M1} { empty( skol11 ) }.
% 1.94/2.38 (19312) {G0,W3,D2,L1,V0,M1} { element( skol12, positive_rationals ) }.
% 1.94/2.38 (19313) {G0,W2,D2,L1,V0,M1} { ! empty( skol12 ) }.
% 1.94/2.38 (19314) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol12 ) }.
% 1.94/2.38 (19315) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol12 ) }.
% 1.94/2.38 (19316) {G0,W2,D2,L1,V0,M1} { ordinal( skol12 ) }.
% 1.94/2.38 (19317) {G0,W3,D3,L1,V1,M1} { empty( skol13( Y ) ) }.
% 1.94/2.38 (19318) {G0,W3,D3,L1,V1,M1} { relation( skol13( Y ) ) }.
% 1.94/2.38 (19319) {G0,W3,D3,L1,V1,M1} { function( skol13( Y ) ) }.
% 1.94/2.38 (19320) {G0,W3,D3,L1,V1,M1} { one_to_one( skol13( Y ) ) }.
% 1.94/2.38 (19321) {G0,W3,D3,L1,V1,M1} { epsilon_transitive( skol13( Y ) ) }.
% 1.94/2.38 (19322) {G0,W3,D3,L1,V1,M1} { epsilon_connected( skol13( Y ) ) }.
% 1.94/2.38 (19323) {G0,W3,D3,L1,V1,M1} { ordinal( skol13( Y ) ) }.
% 1.94/2.38 (19324) {G0,W3,D3,L1,V1,M1} { natural( skol13( Y ) ) }.
% 1.94/2.38 (19325) {G0,W3,D3,L1,V1,M1} { finite( skol13( Y ) ) }.
% 1.94/2.38 (19326) {G0,W5,D3,L1,V1,M1} { element( skol13( X ), powerset( X ) ) }.
% 1.94/2.38 (19327) {G0,W2,D2,L1,V0,M1} { relation( skol14 ) }.
% 1.94/2.38 (19328) {G0,W2,D2,L1,V0,M1} { empty( skol14 ) }.
% 1.94/2.38 (19329) {G0,W2,D2,L1,V0,M1} { function( skol14 ) }.
% 1.94/2.38 (19330) {G0,W2,D2,L1,V0,M1} { relation( skol15 ) }.
% 1.94/2.38 (19331) {G0,W2,D2,L1,V0,M1} { function( skol15 ) }.
% 1.94/2.38 (19332) {G0,W2,D2,L1,V0,M1} { one_to_one( skol15 ) }.
% 1.94/2.38 (19333) {G0,W2,D2,L1,V0,M1} { empty( skol15 ) }.
% 1.94/2.38 (19334) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol15 ) }.
% 1.94/2.38 (19335) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol15 ) }.
% 1.94/2.38 (19336) {G0,W2,D2,L1,V0,M1} { ordinal( skol15 ) }.
% 1.94/2.38 (19337) {G0,W2,D2,L1,V0,M1} { relation( skol16 ) }.
% 1.94/2.38 (19338) {G0,W2,D2,L1,V0,M1} { function( skol16 ) }.
% 1.94/2.38 (19339) {G0,W2,D2,L1,V0,M1} { transfinite_sequence( skol16 ) }.
% 1.94/2.38 (19340) {G0,W2,D2,L1,V0,M1} { ordinal_yielding( skol16 ) }.
% 1.94/2.38 (19341) {G0,W2,D2,L1,V0,M1} { ! empty( skol17 ) }.
% 1.94/2.38 (19342) {G0,W2,D2,L1,V0,M1} { relation( skol17 ) }.
% 1.94/2.38 (19343) {G0,W3,D3,L1,V1,M1} { empty( skol18( Y ) ) }.
% 1.94/2.38 (19344) {G0,W5,D3,L1,V1,M1} { element( skol18( X ), powerset( X ) ) }.
% 1.94/2.38 (19345) {G0,W2,D2,L1,V0,M1} { ! empty( skol19 ) }.
% 1.94/2.38 (19346) {G0,W3,D2,L1,V0,M1} { element( skol20, positive_rationals ) }.
% 1.94/2.38 (19347) {G0,W2,D2,L1,V0,M1} { empty( skol20 ) }.
% 1.94/2.38 (19348) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol20 ) }.
% 1.94/2.38 (19349) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol20 ) }.
% 1.94/2.38 (19350) {G0,W2,D2,L1,V0,M1} { ordinal( skol20 ) }.
% 1.94/2.38 (19351) {G0,W2,D2,L1,V0,M1} { natural( skol20 ) }.
% 1.94/2.38 (19352) {G0,W5,D3,L2,V2,M2} { empty( X ), ! empty( skol21( Y ) ) }.
% 1.94/2.38 (19353) {G0,W5,D3,L2,V2,M2} { empty( X ), finite( skol21( Y ) ) }.
% 1.94/2.38 (19354) {G0,W7,D3,L2,V1,M2} { empty( X ), element( skol21( X ), powerset(
% 1.94/2.38 X ) ) }.
% 1.94/2.38 (19355) {G0,W2,D2,L1,V0,M1} { relation( skol22 ) }.
% 1.94/2.38 (19356) {G0,W2,D2,L1,V0,M1} { function( skol22 ) }.
% 1.94/2.38 (19357) {G0,W2,D2,L1,V0,M1} { one_to_one( skol22 ) }.
% 1.94/2.38 (19358) {G0,W2,D2,L1,V0,M1} { ! empty( skol23 ) }.
% 1.94/2.38 (19359) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol23 ) }.
% 1.94/2.38 (19360) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol23 ) }.
% 1.94/2.38 (19361) {G0,W2,D2,L1,V0,M1} { ordinal( skol23 ) }.
% 1.94/2.38 (19362) {G0,W2,D2,L1,V0,M1} { relation( skol24 ) }.
% 1.94/2.38 (19363) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol24 ) }.
% 1.94/2.38 (19364) {G0,W2,D2,L1,V0,M1} { relation( skol25 ) }.
% 1.94/2.38 (19365) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol25 ) }.
% 1.94/2.38 (19366) {G0,W2,D2,L1,V0,M1} { function( skol25 ) }.
% 1.94/2.38 (19367) {G0,W2,D2,L1,V0,M1} { relation( skol26 ) }.
% 1.94/2.38 (19368) {G0,W2,D2,L1,V0,M1} { function( skol26 ) }.
% 1.94/2.38 (19369) {G0,W2,D2,L1,V0,M1} { transfinite_sequence( skol26 ) }.
% 1.94/2.38 (19370) {G0,W2,D2,L1,V0,M1} { relation( skol27 ) }.
% 1.94/2.38 (19371) {G0,W2,D2,L1,V0,M1} { relation_non_empty( skol27 ) }.
% 1.94/2.38 (19372) {G0,W2,D2,L1,V0,M1} { function( skol27 ) }.
% 1.94/2.38 (19373) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 1.94/2.38 (19374) {G0,W5,D4,L1,V1,M1} { subset( X, powerset( union( X ) ) ) }.
% 1.94/2.38 (19375) {G0,W7,D2,L3,V2,M3} { ! subset( X, Y ), ! finite( Y ), finite( X )
% 1.94/2.38 }.
% 1.94/2.38 (19376) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 1.94/2.38 (19377) {G0,W5,D3,L2,V1,M2} { ! finite( X ), finite( powerset( X ) ) }.
% 1.94/2.38 (19378) {G0,W5,D3,L2,V1,M2} { ! finite( powerset( X ) ), finite( X ) }.
% 1.94/2.38 (19379) {G0,W5,D3,L2,V0,M2} { alpha4( skol28 ), finite( union( skol28 ) )
% 1.94/2.38 }.
% 1.94/2.38 (19380) {G0,W6,D2,L3,V0,M3} { alpha4( skol28 ), ! finite( skol28 ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 (19381) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), finite( X ) }.
% 1.94/2.38 (19382) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), alpha1( X ) }.
% 1.94/2.38 (19383) {G0,W5,D3,L2,V1,M2} { ! alpha4( X ), ! finite( union( X ) ) }.
% 1.94/2.38 (19384) {G0,W9,D3,L4,V1,M4} { ! finite( X ), ! alpha1( X ), finite( union
% 1.94/2.38 ( X ) ), alpha4( X ) }.
% 1.94/2.38 (19385) {G0,W7,D2,L3,V2,M3} { ! alpha1( X ), ! in( Y, X ), finite( Y ) }.
% 1.94/2.38 (19386) {G0,W5,D3,L2,V2,M2} { ! finite( skol29( Y ) ), alpha1( X ) }.
% 1.94/2.38 (19387) {G0,W6,D3,L2,V1,M2} { in( skol29( X ), X ), alpha1( X ) }.
% 1.94/2.38 (19388) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y )
% 1.94/2.38 }.
% 1.94/2.38 (19389) {G0,W7,D3,L2,V2,M2} { ! element( X, powerset( Y ) ), subset( X, Y
% 1.94/2.38 ) }.
% 1.94/2.38 (19390) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X, powerset( Y )
% 1.94/2.38 ) }.
% 1.94/2.38 (19391) {G0,W10,D3,L3,V3,M3} { ! in( X, Z ), ! element( Z, powerset( Y ) )
% 1.94/2.38 , element( X, Y ) }.
% 1.94/2.38 (19392) {G0,W9,D3,L3,V3,M3} { ! in( X, Y ), ! element( Y, powerset( Z ) )
% 1.94/2.38 , ! empty( Z ) }.
% 1.94/2.38 (19393) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 1.94/2.38 (19394) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 1.94/2.38 (19395) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 1.94/2.38 (19396) {G0,W7,D3,L2,V2,M2} { ! in( X, Y ), subset( X, union( Y ) ) }.
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Total Proof:
% 1.94/2.38
% 1.94/2.38 subsumption: (31) {G0,W3,D3,L1,V1,M1} I { ! empty( powerset( X ) ) }.
% 1.94/2.38 parent0: (19270) {G0,W3,D3,L1,V1,M1} { ! empty( powerset( X ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (41) {G0,W8,D3,L3,V2,M3} I { ! finite( X ), ! finite( skol2( Y
% 1.94/2.38 ) ), finite( union( X ) ) }.
% 1.94/2.38 parent0: (19286) {G0,W8,D3,L3,V2,M3} { ! finite( X ), ! finite( skol2( Y )
% 1.94/2.38 ), finite( union( X ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 2 ==> 2
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (42) {G0,W9,D3,L3,V1,M3} I { ! finite( X ), in( skol2( X ), X
% 1.94/2.38 ), finite( union( X ) ) }.
% 1.94/2.38 parent0: (19287) {G0,W9,D3,L3,V1,M3} { ! finite( X ), in( skol2( X ), X )
% 1.94/2.38 , finite( union( X ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 2 ==> 2
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (128) {G0,W3,D2,L1,V1,M1} I { subset( X, X ) }.
% 1.94/2.38 parent0: (19373) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (129) {G0,W5,D4,L1,V1,M1} I { subset( X, powerset( union( X )
% 1.94/2.38 ) ) }.
% 1.94/2.38 parent0: (19374) {G0,W5,D4,L1,V1,M1} { subset( X, powerset( union( X ) ) )
% 1.94/2.38 }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (130) {G0,W7,D2,L3,V2,M3} I { ! subset( X, Y ), ! finite( Y )
% 1.94/2.38 , finite( X ) }.
% 1.94/2.38 parent0: (19375) {G0,W7,D2,L3,V2,M3} { ! subset( X, Y ), ! finite( Y ),
% 1.94/2.38 finite( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 2 ==> 2
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (132) {G0,W5,D3,L2,V1,M2} I { ! finite( X ), finite( powerset
% 1.94/2.38 ( X ) ) }.
% 1.94/2.38 parent0: (19377) {G0,W5,D3,L2,V1,M2} { ! finite( X ), finite( powerset( X
% 1.94/2.38 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (134) {G0,W5,D3,L2,V0,M2} I { alpha4( skol28 ), finite( union
% 1.94/2.38 ( skol28 ) ) }.
% 1.94/2.38 parent0: (19379) {G0,W5,D3,L2,V0,M2} { alpha4( skol28 ), finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (135) {G0,W6,D2,L3,V0,M3} I { alpha4( skol28 ), ! finite(
% 1.94/2.38 skol28 ), ! alpha1( skol28 ) }.
% 1.94/2.38 parent0: (19380) {G0,W6,D2,L3,V0,M3} { alpha4( skol28 ), ! finite( skol28
% 1.94/2.38 ), ! alpha1( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 2 ==> 2
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (136) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), finite( X ) }.
% 1.94/2.38 parent0: (19381) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), finite( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (137) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), alpha1( X ) }.
% 1.94/2.38 parent0: (19382) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), alpha1( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (138) {G0,W5,D3,L2,V1,M2} I { ! alpha4( X ), ! finite( union(
% 1.94/2.38 X ) ) }.
% 1.94/2.38 parent0: (19383) {G0,W5,D3,L2,V1,M2} { ! alpha4( X ), ! finite( union( X )
% 1.94/2.38 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (140) {G0,W7,D2,L3,V2,M3} I { ! alpha1( X ), ! in( Y, X ),
% 1.94/2.38 finite( Y ) }.
% 1.94/2.38 parent0: (19385) {G0,W7,D2,L3,V2,M3} { ! alpha1( X ), ! in( Y, X ), finite
% 1.94/2.38 ( Y ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 2 ==> 2
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (141) {G0,W5,D3,L2,V2,M2} I { ! finite( skol29( Y ) ), alpha1
% 1.94/2.38 ( X ) }.
% 1.94/2.38 parent0: (19386) {G0,W5,D3,L2,V2,M2} { ! finite( skol29( Y ) ), alpha1( X
% 1.94/2.38 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (142) {G0,W6,D3,L2,V1,M2} I { in( skol29( X ), X ), alpha1( X
% 1.94/2.38 ) }.
% 1.94/2.38 parent0: (19387) {G0,W6,D3,L2,V1,M2} { in( skol29( X ), X ), alpha1( X )
% 1.94/2.38 }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (143) {G0,W8,D2,L3,V2,M3} I { ! element( X, Y ), empty( Y ),
% 1.94/2.38 in( X, Y ) }.
% 1.94/2.38 parent0: (19388) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in(
% 1.94/2.38 X, Y ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 2 ==> 2
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (145) {G0,W7,D3,L2,V2,M2} I { ! subset( X, Y ), element( X,
% 1.94/2.38 powerset( Y ) ) }.
% 1.94/2.38 parent0: (19390) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X,
% 1.94/2.38 powerset( Y ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (151) {G0,W7,D3,L2,V2,M2} I { ! in( X, Y ), subset( X, union(
% 1.94/2.38 Y ) ) }.
% 1.94/2.38 parent0: (19396) {G0,W7,D3,L2,V2,M2} { ! in( X, Y ), subset( X, union( Y )
% 1.94/2.38 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19434) {G1,W6,D4,L2,V1,M2} { ! finite( powerset( union( X ) )
% 1.94/2.38 ), finite( X ) }.
% 1.94/2.38 parent0[0]: (130) {G0,W7,D2,L3,V2,M3} I { ! subset( X, Y ), ! finite( Y ),
% 1.94/2.38 finite( X ) }.
% 1.94/2.38 parent1[0]: (129) {G0,W5,D4,L1,V1,M1} I { subset( X, powerset( union( X ) )
% 1.94/2.38 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := powerset( union( X ) )
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (541) {G1,W6,D4,L2,V1,M2} R(130,129) { ! finite( powerset(
% 1.94/2.38 union( X ) ) ), finite( X ) }.
% 1.94/2.38 parent0: (19434) {G1,W6,D4,L2,V1,M2} { ! finite( powerset( union( X ) ) )
% 1.94/2.38 , finite( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19435) {G1,W5,D3,L2,V0,M2} { finite( skol28 ), finite( union
% 1.94/2.38 ( skol28 ) ) }.
% 1.94/2.38 parent0[0]: (136) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), finite( X ) }.
% 1.94/2.38 parent1[0]: (134) {G0,W5,D3,L2,V0,M2} I { alpha4( skol28 ), finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol28
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (681) {G1,W5,D3,L2,V0,M2} R(136,134) { finite( skol28 ),
% 1.94/2.38 finite( union( skol28 ) ) }.
% 1.94/2.38 parent0: (19435) {G1,W5,D3,L2,V0,M2} { finite( skol28 ), finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19436) {G1,W9,D3,L3,V1,M3} { in( skol2( X ), X ), finite(
% 1.94/2.38 union( X ) ), ! alpha4( X ) }.
% 1.94/2.38 parent0[0]: (42) {G0,W9,D3,L3,V1,M3} I { ! finite( X ), in( skol2( X ), X )
% 1.94/2.38 , finite( union( X ) ) }.
% 1.94/2.38 parent1[1]: (136) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), finite( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19437) {G1,W8,D3,L3,V1,M3} { ! alpha4( X ), in( skol2( X ), X
% 1.94/2.38 ), ! alpha4( X ) }.
% 1.94/2.38 parent0[1]: (138) {G0,W5,D3,L2,V1,M2} I { ! alpha4( X ), ! finite( union( X
% 1.94/2.38 ) ) }.
% 1.94/2.38 parent1[1]: (19436) {G1,W9,D3,L3,V1,M3} { in( skol2( X ), X ), finite(
% 1.94/2.38 union( X ) ), ! alpha4( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 factor: (19438) {G1,W6,D3,L2,V1,M2} { ! alpha4( X ), in( skol2( X ), X )
% 1.94/2.38 }.
% 1.94/2.38 parent0[0, 2]: (19437) {G1,W8,D3,L3,V1,M3} { ! alpha4( X ), in( skol2( X )
% 1.94/2.38 , X ), ! alpha4( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (685) {G1,W6,D3,L2,V1,M2} R(136,42);r(138) { ! alpha4( X ), in
% 1.94/2.38 ( skol2( X ), X ) }.
% 1.94/2.38 parent0: (19438) {G1,W6,D3,L2,V1,M2} { ! alpha4( X ), in( skol2( X ), X )
% 1.94/2.38 }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19439) {G1,W8,D3,L3,V2,M3} { ! finite( skol2( Y ) ), finite(
% 1.94/2.38 union( X ) ), ! alpha4( X ) }.
% 1.94/2.38 parent0[0]: (41) {G0,W8,D3,L3,V2,M3} I { ! finite( X ), ! finite( skol2( Y
% 1.94/2.38 ) ), finite( union( X ) ) }.
% 1.94/2.38 parent1[1]: (136) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), finite( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19441) {G1,W7,D3,L3,V2,M3} { ! alpha4( X ), ! finite( skol2(
% 1.94/2.38 Y ) ), ! alpha4( X ) }.
% 1.94/2.38 parent0[1]: (138) {G0,W5,D3,L2,V1,M2} I { ! alpha4( X ), ! finite( union( X
% 1.94/2.38 ) ) }.
% 1.94/2.38 parent1[1]: (19439) {G1,W8,D3,L3,V2,M3} { ! finite( skol2( Y ) ), finite(
% 1.94/2.38 union( X ) ), ! alpha4( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 factor: (19442) {G1,W5,D3,L2,V2,M2} { ! alpha4( X ), ! finite( skol2( Y )
% 1.94/2.38 ) }.
% 1.94/2.38 parent0[0, 2]: (19441) {G1,W7,D3,L3,V2,M3} { ! alpha4( X ), ! finite(
% 1.94/2.38 skol2( Y ) ), ! alpha4( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (686) {G1,W5,D3,L2,V2,M2} R(136,41);r(138) { ! alpha4( X ), !
% 1.94/2.38 finite( skol2( Y ) ) }.
% 1.94/2.38 parent0: (19442) {G1,W5,D3,L2,V2,M2} { ! alpha4( X ), ! finite( skol2( Y )
% 1.94/2.38 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19443) {G1,W5,D3,L2,V0,M2} { alpha1( skol28 ), finite( union
% 1.94/2.38 ( skol28 ) ) }.
% 1.94/2.38 parent0[0]: (137) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), alpha1( X ) }.
% 1.94/2.38 parent1[0]: (134) {G0,W5,D3,L2,V0,M2} I { alpha4( skol28 ), finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol28
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (689) {G1,W5,D3,L2,V0,M2} R(137,134) { alpha1( skol28 ),
% 1.94/2.38 finite( union( skol28 ) ) }.
% 1.94/2.38 parent0: (19443) {G1,W5,D3,L2,V0,M2} { alpha1( skol28 ), finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19444) {G1,W4,D3,L1,V1,M1} { element( X, powerset( X ) ) }.
% 1.94/2.38 parent0[0]: (145) {G0,W7,D3,L2,V2,M2} I { ! subset( X, Y ), element( X,
% 1.94/2.38 powerset( Y ) ) }.
% 1.94/2.38 parent1[0]: (128) {G0,W3,D2,L1,V1,M1} I { subset( X, X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (817) {G1,W4,D3,L1,V1,M1} R(145,128) { element( X, powerset( X
% 1.94/2.38 ) ) }.
% 1.94/2.38 parent0: (19444) {G1,W4,D3,L1,V1,M1} { element( X, powerset( X ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19445) {G1,W7,D3,L2,V1,M2} { empty( powerset( X ) ), in( X,
% 1.94/2.38 powerset( X ) ) }.
% 1.94/2.38 parent0[0]: (143) {G0,W8,D2,L3,V2,M3} I { ! element( X, Y ), empty( Y ), in
% 1.94/2.38 ( X, Y ) }.
% 1.94/2.38 parent1[0]: (817) {G1,W4,D3,L1,V1,M1} R(145,128) { element( X, powerset( X
% 1.94/2.38 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := powerset( X )
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19446) {G1,W4,D3,L1,V1,M1} { in( X, powerset( X ) ) }.
% 1.94/2.38 parent0[0]: (31) {G0,W3,D3,L1,V1,M1} I { ! empty( powerset( X ) ) }.
% 1.94/2.38 parent1[0]: (19445) {G1,W7,D3,L2,V1,M2} { empty( powerset( X ) ), in( X,
% 1.94/2.38 powerset( X ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (821) {G2,W4,D3,L1,V1,M1} R(817,143);r(31) { in( X, powerset(
% 1.94/2.38 X ) ) }.
% 1.94/2.38 parent0: (19446) {G1,W4,D3,L1,V1,M1} { in( X, powerset( X ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19447) {G1,W5,D3,L2,V1,M2} { ! alpha1( powerset( X ) ),
% 1.94/2.38 finite( X ) }.
% 1.94/2.38 parent0[1]: (140) {G0,W7,D2,L3,V2,M3} I { ! alpha1( X ), ! in( Y, X ),
% 1.94/2.38 finite( Y ) }.
% 1.94/2.38 parent1[0]: (821) {G2,W4,D3,L1,V1,M1} R(817,143);r(31) { in( X, powerset( X
% 1.94/2.38 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := powerset( X )
% 1.94/2.38 Y := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (848) {G3,W5,D3,L2,V1,M2} R(821,140) { ! alpha1( powerset( X )
% 1.94/2.38 ), finite( X ) }.
% 1.94/2.38 parent0: (19447) {G1,W5,D3,L2,V1,M2} { ! alpha1( powerset( X ) ), finite(
% 1.94/2.38 X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19448) {G1,W5,D3,L2,V2,M2} { finite( X ), ! finite( skol29( Y
% 1.94/2.38 ) ) }.
% 1.94/2.38 parent0[0]: (848) {G3,W5,D3,L2,V1,M2} R(821,140) { ! alpha1( powerset( X )
% 1.94/2.38 ), finite( X ) }.
% 1.94/2.38 parent1[1]: (141) {G0,W5,D3,L2,V2,M2} I { ! finite( skol29( Y ) ), alpha1(
% 1.94/2.38 X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := powerset( X )
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (3935) {G4,W5,D3,L2,V2,M2} R(848,141) { finite( X ), ! finite
% 1.94/2.38 ( skol29( Y ) ) }.
% 1.94/2.38 parent0: (19448) {G1,W5,D3,L2,V2,M2} { finite( X ), ! finite( skol29( Y )
% 1.94/2.38 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19449) {G2,W5,D3,L2,V2,M2} { ! alpha4( X ), ! finite( skol29
% 1.94/2.38 ( Z ) ) }.
% 1.94/2.38 parent0[1]: (686) {G1,W5,D3,L2,V2,M2} R(136,41);r(138) { ! alpha4( X ), !
% 1.94/2.38 finite( skol2( Y ) ) }.
% 1.94/2.38 parent1[0]: (3935) {G4,W5,D3,L2,V2,M2} R(848,141) { finite( X ), ! finite(
% 1.94/2.38 skol29( Y ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := skol2( Y )
% 1.94/2.38 Y := Z
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (3978) {G5,W5,D3,L2,V2,M2} R(3935,686) { ! finite( skol29( X )
% 1.94/2.38 ), ! alpha4( Y ) }.
% 1.94/2.38 parent0: (19449) {G2,W5,D3,L2,V2,M2} { ! alpha4( X ), ! finite( skol29( Z
% 1.94/2.38 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := Y
% 1.94/2.38 Y := Z
% 1.94/2.38 Z := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 1
% 1.94/2.38 1 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19451) {G1,W6,D4,L2,V0,M2} { finite( powerset( union( skol28
% 1.94/2.38 ) ) ), finite( skol28 ) }.
% 1.94/2.38 parent0[0]: (132) {G0,W5,D3,L2,V1,M2} I { ! finite( X ), finite( powerset(
% 1.94/2.38 X ) ) }.
% 1.94/2.38 parent1[1]: (681) {G1,W5,D3,L2,V0,M2} R(136,134) { finite( skol28 ), finite
% 1.94/2.38 ( union( skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := union( skol28 )
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19452) {G2,W4,D2,L2,V0,M2} { finite( skol28 ), finite( skol28
% 1.94/2.38 ) }.
% 1.94/2.38 parent0[0]: (541) {G1,W6,D4,L2,V1,M2} R(130,129) { ! finite( powerset(
% 1.94/2.38 union( X ) ) ), finite( X ) }.
% 1.94/2.38 parent1[0]: (19451) {G1,W6,D4,L2,V0,M2} { finite( powerset( union( skol28
% 1.94/2.38 ) ) ), finite( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol28
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 factor: (19453) {G2,W2,D2,L1,V0,M1} { finite( skol28 ) }.
% 1.94/2.38 parent0[0, 1]: (19452) {G2,W4,D2,L2,V0,M2} { finite( skol28 ), finite(
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (4894) {G2,W2,D2,L1,V0,M1} R(681,132);r(541) { finite( skol28
% 1.94/2.38 ) }.
% 1.94/2.38 parent0: (19453) {G2,W2,D2,L1,V0,M1} { finite( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19454) {G1,W4,D2,L2,V0,M2} { alpha4( skol28 ), ! alpha1(
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 parent0[1]: (135) {G0,W6,D2,L3,V0,M3} I { alpha4( skol28 ), ! finite(
% 1.94/2.38 skol28 ), ! alpha1( skol28 ) }.
% 1.94/2.38 parent1[0]: (4894) {G2,W2,D2,L1,V0,M1} R(681,132);r(541) { finite( skol28 )
% 1.94/2.38 }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (4904) {G3,W4,D2,L2,V0,M2} R(4894,135) { alpha4( skol28 ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 parent0: (19454) {G1,W4,D2,L2,V0,M2} { alpha4( skol28 ), ! alpha1( skol28
% 1.94/2.38 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19455) {G4,W5,D3,L2,V1,M2} { ! finite( skol29( X ) ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 parent0[1]: (3978) {G5,W5,D3,L2,V2,M2} R(3935,686) { ! finite( skol29( X )
% 1.94/2.38 ), ! alpha4( Y ) }.
% 1.94/2.38 parent1[0]: (4904) {G3,W4,D2,L2,V0,M2} R(4894,135) { alpha4( skol28 ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := skol28
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (4948) {G6,W5,D3,L2,V1,M2} R(4904,3978) { ! alpha1( skol28 ),
% 1.94/2.38 ! finite( skol29( X ) ) }.
% 1.94/2.38 parent0: (19455) {G4,W5,D3,L2,V1,M2} { ! finite( skol29( X ) ), ! alpha1(
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 1
% 1.94/2.38 1 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19456) {G2,W5,D3,L2,V1,M2} { ! finite( skol2( X ) ), ! alpha1
% 1.94/2.38 ( skol28 ) }.
% 1.94/2.38 parent0[0]: (686) {G1,W5,D3,L2,V2,M2} R(136,41);r(138) { ! alpha4( X ), !
% 1.94/2.38 finite( skol2( Y ) ) }.
% 1.94/2.38 parent1[0]: (4904) {G3,W4,D2,L2,V0,M2} R(4894,135) { alpha4( skol28 ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol28
% 1.94/2.38 Y := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (4951) {G4,W5,D3,L2,V1,M2} R(4904,686) { ! alpha1( skol28 ), !
% 1.94/2.38 finite( skol2( X ) ) }.
% 1.94/2.38 parent0: (19456) {G2,W5,D3,L2,V1,M2} { ! finite( skol2( X ) ), ! alpha1(
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 1
% 1.94/2.38 1 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19457) {G1,W6,D3,L2,V2,M2} { ! finite( skol29( X ) ), !
% 1.94/2.38 finite( skol29( Y ) ) }.
% 1.94/2.38 parent0[0]: (4948) {G6,W5,D3,L2,V1,M2} R(4904,3978) { ! alpha1( skol28 ), !
% 1.94/2.38 finite( skol29( X ) ) }.
% 1.94/2.38 parent1[1]: (141) {G0,W5,D3,L2,V2,M2} I { ! finite( skol29( Y ) ), alpha1(
% 1.94/2.38 X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := skol28
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (5092) {G7,W6,D3,L2,V2,M2} R(4948,141) { ! finite( skol29( X )
% 1.94/2.38 ), ! finite( skol29( Y ) ) }.
% 1.94/2.38 parent0: (19457) {G1,W6,D3,L2,V2,M2} { ! finite( skol29( X ) ), ! finite(
% 1.94/2.38 skol29( Y ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 factor: (19459) {G7,W3,D3,L1,V1,M1} { ! finite( skol29( X ) ) }.
% 1.94/2.38 parent0[0, 1]: (5092) {G7,W6,D3,L2,V2,M2} R(4948,141) { ! finite( skol29( X
% 1.94/2.38 ) ), ! finite( skol29( Y ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (5098) {G8,W3,D3,L1,V1,M1} F(5092) { ! finite( skol29( X ) )
% 1.94/2.38 }.
% 1.94/2.38 parent0: (19459) {G7,W3,D3,L1,V1,M1} { ! finite( skol29( X ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19460) {G1,W6,D3,L2,V2,M2} { ! subset( skol29( X ), Y ), !
% 1.94/2.38 finite( Y ) }.
% 1.94/2.38 parent0[0]: (5098) {G8,W3,D3,L1,V1,M1} F(5092) { ! finite( skol29( X ) )
% 1.94/2.38 }.
% 1.94/2.38 parent1[2]: (130) {G0,W7,D2,L3,V2,M3} I { ! subset( X, Y ), ! finite( Y ),
% 1.94/2.38 finite( X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := skol29( X )
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (5244) {G9,W6,D3,L2,V2,M2} R(5098,130) { ! subset( skol29( X )
% 1.94/2.38 , Y ), ! finite( Y ) }.
% 1.94/2.38 parent0: (19460) {G1,W6,D3,L2,V2,M2} { ! subset( skol29( X ), Y ), !
% 1.94/2.38 finite( Y ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := Y
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19461) {G1,W8,D3,L3,V2,M3} { ! alpha1( skol28 ), ! alpha1( Y
% 1.94/2.38 ), ! in( skol2( X ), Y ) }.
% 1.94/2.38 parent0[1]: (4951) {G4,W5,D3,L2,V1,M2} R(4904,686) { ! alpha1( skol28 ), !
% 1.94/2.38 finite( skol2( X ) ) }.
% 1.94/2.38 parent1[2]: (140) {G0,W7,D2,L3,V2,M3} I { ! alpha1( X ), ! in( Y, X ),
% 1.94/2.38 finite( Y ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := Y
% 1.94/2.38 Y := skol2( X )
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (5389) {G5,W8,D3,L3,V2,M3} R(4951,140) { ! alpha1( skol28 ), !
% 1.94/2.38 alpha1( X ), ! in( skol2( Y ), X ) }.
% 1.94/2.38 parent0: (19461) {G1,W8,D3,L3,V2,M3} { ! alpha1( skol28 ), ! alpha1( Y ),
% 1.94/2.38 ! in( skol2( X ), Y ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := Y
% 1.94/2.38 Y := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 2 ==> 2
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 factor: (19463) {G5,W6,D3,L2,V1,M2} { ! alpha1( skol28 ), ! in( skol2( X )
% 1.94/2.38 , skol28 ) }.
% 1.94/2.38 parent0[0, 1]: (5389) {G5,W8,D3,L3,V2,M3} R(4951,140) { ! alpha1( skol28 )
% 1.94/2.38 , ! alpha1( X ), ! in( skol2( Y ), X ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol28
% 1.94/2.38 Y := X
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (5393) {G6,W6,D3,L2,V1,M2} F(5389) { ! alpha1( skol28 ), ! in
% 1.94/2.38 ( skol2( X ), skol28 ) }.
% 1.94/2.38 parent0: (19463) {G5,W6,D3,L2,V1,M2} { ! alpha1( skol28 ), ! in( skol2( X
% 1.94/2.38 ), skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 1 ==> 1
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19464) {G2,W6,D3,L2,V0,M2} { in( skol2( skol28 ), skol28 ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 parent0[0]: (685) {G1,W6,D3,L2,V1,M2} R(136,42);r(138) { ! alpha4( X ), in
% 1.94/2.38 ( skol2( X ), X ) }.
% 1.94/2.38 parent1[0]: (4904) {G3,W4,D2,L2,V0,M2} R(4894,135) { alpha4( skol28 ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol28
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19465) {G3,W4,D2,L2,V0,M2} { ! alpha1( skol28 ), ! alpha1(
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 parent0[1]: (5393) {G6,W6,D3,L2,V1,M2} F(5389) { ! alpha1( skol28 ), ! in(
% 1.94/2.38 skol2( X ), skol28 ) }.
% 1.94/2.38 parent1[0]: (19464) {G2,W6,D3,L2,V0,M2} { in( skol2( skol28 ), skol28 ), !
% 1.94/2.38 alpha1( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol28
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 factor: (19466) {G3,W2,D2,L1,V0,M1} { ! alpha1( skol28 ) }.
% 1.94/2.38 parent0[0, 1]: (19465) {G3,W4,D2,L2,V0,M2} { ! alpha1( skol28 ), ! alpha1
% 1.94/2.38 ( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (19182) {G7,W2,D2,L1,V0,M1} R(685,4904);r(5393) { ! alpha1(
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 parent0: (19466) {G3,W2,D2,L1,V0,M1} { ! alpha1( skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19467) {G2,W3,D3,L1,V0,M1} { finite( union( skol28 ) ) }.
% 1.94/2.38 parent0[0]: (19182) {G7,W2,D2,L1,V0,M1} R(685,4904);r(5393) { ! alpha1(
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 parent1[0]: (689) {G1,W5,D3,L2,V0,M2} R(137,134) { alpha1( skol28 ), finite
% 1.94/2.38 ( union( skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (19187) {G8,W3,D3,L1,V0,M1} R(19182,689) { finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 parent0: (19467) {G2,W3,D3,L1,V0,M1} { finite( union( skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19468) {G1,W4,D3,L1,V0,M1} { in( skol29( skol28 ), skol28 )
% 1.94/2.38 }.
% 1.94/2.38 parent0[0]: (19182) {G7,W2,D2,L1,V0,M1} R(685,4904);r(5393) { ! alpha1(
% 1.94/2.38 skol28 ) }.
% 1.94/2.38 parent1[1]: (142) {G0,W6,D3,L2,V1,M2} I { in( skol29( X ), X ), alpha1( X )
% 1.94/2.38 }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 X := skol28
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (19188) {G8,W4,D3,L1,V0,M1} R(19182,142) { in( skol29( skol28
% 1.94/2.38 ), skol28 ) }.
% 1.94/2.38 parent0: (19468) {G1,W4,D3,L1,V0,M1} { in( skol29( skol28 ), skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19469) {G9,W5,D3,L1,V1,M1} { ! subset( skol29( X ), union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 parent0[1]: (5244) {G9,W6,D3,L2,V2,M2} R(5098,130) { ! subset( skol29( X )
% 1.94/2.38 , Y ), ! finite( Y ) }.
% 1.94/2.38 parent1[0]: (19187) {G8,W3,D3,L1,V0,M1} R(19182,689) { finite( union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 Y := union( skol28 )
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (19200) {G10,W5,D3,L1,V1,M1} R(19187,5244) { ! subset( skol29
% 1.94/2.38 ( X ), union( skol28 ) ) }.
% 1.94/2.38 parent0: (19469) {G9,W5,D3,L1,V1,M1} { ! subset( skol29( X ), union(
% 1.94/2.38 skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := X
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 0 ==> 0
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19470) {G1,W5,D3,L1,V0,M1} { subset( skol29( skol28 ), union
% 1.94/2.38 ( skol28 ) ) }.
% 1.94/2.38 parent0[0]: (151) {G0,W7,D3,L2,V2,M2} I { ! in( X, Y ), subset( X, union( Y
% 1.94/2.38 ) ) }.
% 1.94/2.38 parent1[0]: (19188) {G8,W4,D3,L1,V0,M1} R(19182,142) { in( skol29( skol28 )
% 1.94/2.38 , skol28 ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol29( skol28 )
% 1.94/2.38 Y := skol28
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 resolution: (19471) {G2,W0,D0,L0,V0,M0} { }.
% 1.94/2.38 parent0[0]: (19200) {G10,W5,D3,L1,V1,M1} R(19187,5244) { ! subset( skol29(
% 1.94/2.38 X ), union( skol28 ) ) }.
% 1.94/2.38 parent1[0]: (19470) {G1,W5,D3,L1,V0,M1} { subset( skol29( skol28 ), union
% 1.94/2.38 ( skol28 ) ) }.
% 1.94/2.38 substitution0:
% 1.94/2.38 X := skol28
% 1.94/2.38 end
% 1.94/2.38 substitution1:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 subsumption: (19235) {G11,W0,D0,L0,V0,M0} R(19188,151);r(19200) { }.
% 1.94/2.38 parent0: (19471) {G2,W0,D0,L0,V0,M0} { }.
% 1.94/2.38 substitution0:
% 1.94/2.38 end
% 1.94/2.38 permutation0:
% 1.94/2.38 end
% 1.94/2.38
% 1.94/2.38 Proof check complete!
% 1.94/2.38
% 1.94/2.38 Memory use:
% 1.94/2.38
% 1.94/2.38 space for terms: 210449
% 1.94/2.38 space for clauses: 810717
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 clauses generated: 49638
% 1.94/2.38 clauses kept: 19236
% 1.94/2.38 clauses selected: 1656
% 1.94/2.38 clauses deleted: 344
% 1.94/2.38 clauses inuse deleted: 145
% 1.94/2.38
% 1.94/2.38 subsentry: 185085
% 1.94/2.38 literals s-matched: 107476
% 1.94/2.38 literals matched: 98916
% 1.94/2.38 full subsumption: 14143
% 1.94/2.38
% 1.94/2.38 checksum: 208215316
% 1.94/2.38
% 1.94/2.38
% 1.94/2.38 Bliksem ended
%------------------------------------------------------------------------------