%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM412+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Mon Jul 18 06:22:01 EDT 2022
% Result : Theorem 3.00s 3.42s
% Output : Refutation 3.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM412+1 : TPTP v8.1.0. Released v3.2.0.
% 0.07/0.12 % Command : bliksem %s
% 0.11/0.33 % Computer : n025.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % DateTime : Wed Jul 6 19:17:43 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.40/1.02 *** allocated 10000 integers for termspace/termends
% 0.40/1.02 *** allocated 10000 integers for clauses
% 0.40/1.02 *** allocated 10000 integers for justifications
% 0.40/1.02 Bliksem 1.12
% 0.40/1.02
% 0.40/1.02
% 0.40/1.02 Automatic Strategy Selection
% 0.40/1.02
% 0.40/1.02
% 0.40/1.02 Clauses:
% 0.40/1.02
% 0.40/1.02 { ! in( X, Y ), ! in( Y, X ) }.
% 0.40/1.02 { ! empty( X ), function( X ) }.
% 0.40/1.02 { ! ordinal( X ), epsilon_transitive( X ) }.
% 0.40/1.02 { ! ordinal( X ), epsilon_connected( X ) }.
% 0.40/1.02 { ! empty( X ), relation( X ) }.
% 0.40/1.02 { ! relation( X ), ! empty( X ), ! function( X ), relation( X ) }.
% 0.40/1.02 { ! relation( X ), ! empty( X ), ! function( X ), function( X ) }.
% 0.40/1.02 { ! relation( X ), ! empty( X ), ! function( X ), one_to_one( X ) }.
% 0.40/1.02 { ! epsilon_transitive( X ), ! epsilon_connected( X ), ordinal( X ) }.
% 0.40/1.02 { ! empty( X ), epsilon_transitive( X ) }.
% 0.40/1.02 { ! empty( X ), epsilon_connected( X ) }.
% 0.40/1.02 { ! empty( X ), ordinal( X ) }.
% 0.40/1.02 { ! relation( X ), ! function( X ), ! transfinite_sequence( X ), !
% 0.40/1.02 transfinite_sequence_of( X, Y ), subset( relation_rng( X ), Y ) }.
% 0.40/1.02 { ! relation( X ), ! function( X ), ! transfinite_sequence( X ), ! subset(
% 0.40/1.02 relation_rng( X ), Y ), transfinite_sequence_of( X, Y ) }.
% 0.40/1.02 { ! relation( X ), ! function( X ), ! transfinite_sequence( X ), ! ordinal
% 0.40/1.02 ( Y ), transfinite_sequence_of( tseq_dom_restriction( X, Y ),
% 0.40/1.02 relation_rng( X ) ) }.
% 0.40/1.02 { ! relation( X ), relation( relation_dom_restriction( X, Y ) ) }.
% 0.40/1.02 { ! transfinite_sequence_of( X, Y ), relation( X ) }.
% 0.40/1.02 { ! transfinite_sequence_of( X, Y ), function( X ) }.
% 0.40/1.02 { ! transfinite_sequence_of( X, Y ), transfinite_sequence( X ) }.
% 0.40/1.02 { transfinite_sequence_of( skol1( X ), X ) }.
% 0.40/1.02 { element( skol2( X ), X ) }.
% 0.40/1.02 { empty( empty_set ) }.
% 0.40/1.02 { relation( empty_set ) }.
% 0.40/1.02 { relation_empty_yielding( empty_set ) }.
% 0.40/1.02 { ! relation( X ), ! relation_empty_yielding( X ), relation(
% 0.40/1.02 relation_dom_restriction( X, Y ) ) }.
% 0.40/1.02 { ! relation( X ), ! relation_empty_yielding( X ), relation_empty_yielding
% 0.40/1.02 ( relation_dom_restriction( X, Y ) ) }.
% 0.40/1.02 { empty( empty_set ) }.
% 0.40/1.02 { relation( empty_set ) }.
% 0.40/1.02 { relation_empty_yielding( empty_set ) }.
% 0.40/1.02 { function( empty_set ) }.
% 0.40/1.02 { one_to_one( empty_set ) }.
% 0.40/1.02 { empty( empty_set ) }.
% 0.40/1.02 { epsilon_transitive( empty_set ) }.
% 0.40/1.02 { epsilon_connected( empty_set ) }.
% 0.40/1.02 { ordinal( empty_set ) }.
% 0.40/1.02 { ! relation( X ), ! function( X ), relation( relation_dom_restriction( X,
% 0.40/1.02 Y ) ) }.
% 0.40/1.02 { ! relation( X ), ! function( X ), function( relation_dom_restriction( X,
% 0.40/1.02 Y ) ) }.
% 0.40/1.02 { empty( empty_set ) }.
% 0.40/1.02 { relation( empty_set ) }.
% 0.40/1.02 { ! relation( X ), ! relation_non_empty( X ), ! function( X ),
% 0.40/1.02 with_non_empty_elements( relation_rng( X ) ) }.
% 0.40/1.02 { empty( X ), ! relation( X ), ! empty( relation_rng( X ) ) }.
% 0.40/1.02 { ! empty( X ), empty( relation_rng( X ) ) }.
% 0.40/1.02 { ! empty( X ), relation( relation_rng( X ) ) }.
% 0.40/1.02 { relation( skol3 ) }.
% 0.40/1.02 { function( skol3 ) }.
% 0.40/1.02 { epsilon_transitive( skol4 ) }.
% 0.40/1.02 { epsilon_connected( skol4 ) }.
% 0.40/1.02 { ordinal( skol4 ) }.
% 0.40/1.02 { empty( skol5 ) }.
% 0.40/1.02 { relation( skol5 ) }.
% 0.40/1.02 { empty( skol6 ) }.
% 0.40/1.02 { relation( skol7 ) }.
% 0.40/1.02 { empty( skol7 ) }.
% 0.40/1.02 { function( skol7 ) }.
% 0.40/1.02 { relation( skol8 ) }.
% 0.40/1.02 { function( skol8 ) }.
% 0.40/1.02 { one_to_one( skol8 ) }.
% 0.40/1.02 { empty( skol8 ) }.
% 0.40/1.02 { epsilon_transitive( skol8 ) }.
% 0.40/1.02 { epsilon_connected( skol8 ) }.
% 0.40/1.02 { ordinal( skol8 ) }.
% 0.40/1.02 { ! empty( skol9 ) }.
% 0.40/1.02 { relation( skol9 ) }.
% 0.40/1.02 { ! empty( skol10 ) }.
% 0.40/1.02 { relation( skol11 ) }.
% 0.40/1.02 { function( skol11 ) }.
% 0.40/1.02 { one_to_one( skol11 ) }.
% 0.40/1.02 { ! empty( skol12 ) }.
% 0.40/1.02 { epsilon_transitive( skol12 ) }.
% 0.40/1.02 { epsilon_connected( skol12 ) }.
% 0.40/1.02 { ordinal( skol12 ) }.
% 0.40/1.02 { relation( skol13 ) }.
% 0.40/1.02 { relation_empty_yielding( skol13 ) }.
% 0.40/1.02 { relation( skol14 ) }.
% 0.40/1.02 { relation_empty_yielding( skol14 ) }.
% 0.40/1.02 { function( skol14 ) }.
% 0.40/1.02 { relation( skol15 ) }.
% 0.40/1.02 { function( skol15 ) }.
% 0.40/1.02 { transfinite_sequence( skol15 ) }.
% 0.40/1.02 { relation( skol16 ) }.
% 0.40/1.02 { relation_non_empty( skol16 ) }.
% 0.40/1.02 { function( skol16 ) }.
% 0.40/1.02 { ! relation( X ), ! function( X ), ! transfinite_sequence( X ), ! ordinal
% 0.40/1.02 ( Y ), tseq_dom_restriction( X, Y ) = relation_dom_restriction( X, Y ) }
% 0.40/1.02 .
% 0.40/1.02 { subset( X, X ) }.
% 0.40/1.02 { ! in( X, Y ), element( X, Y ) }.
% 0.40/1.02 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 0.40/1.02 { ! element( X, powerset( Y ) ), subset( X, Y ) }.
% 0.40/1.02 { ! subset( X, Y ), element( X, powerset( Y ) ) }.
% 0.40/1.02 { ! subset( X, Y ), ! transfinite_sequence_of( Z, X ),
% 0.40/1.02 transfinite_sequence_of( Z, Y ) }.
% 0.40/1.02 { transfinite_sequence_of( skol18, skol17 ) }.
% 3.00/3.42 { ordinal( skol19 ) }.
% 3.00/3.42 { ! transfinite_sequence_of( tseq_dom_restriction( skol18, skol19 ), skol17
% 3.00/3.42 ) }.
% 3.00/3.42 { ! in( X, Z ), ! element( Z, powerset( Y ) ), element( X, Y ) }.
% 3.00/3.42 { ! in( X, Y ), ! element( Y, powerset( Z ) ), ! empty( Z ) }.
% 3.00/3.42 { ! empty( X ), X = empty_set }.
% 3.00/3.42 { ! in( X, Y ), ! empty( Y ) }.
% 3.00/3.42 { ! empty( X ), X = Y, ! empty( Y ) }.
% 3.00/3.42
% 3.00/3.42 percentage equality = 0.020548, percentage horn = 0.988506
% 3.00/3.42 This is a problem with some equality
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42 Options Used:
% 3.00/3.42
% 3.00/3.42 useres = 1
% 3.00/3.42 useparamod = 1
% 3.00/3.42 useeqrefl = 1
% 3.00/3.42 useeqfact = 1
% 3.00/3.42 usefactor = 1
% 3.00/3.42 usesimpsplitting = 0
% 3.00/3.42 usesimpdemod = 5
% 3.00/3.42 usesimpres = 3
% 3.00/3.42
% 3.00/3.42 resimpinuse = 1000
% 3.00/3.42 resimpclauses = 20000
% 3.00/3.42 substype = eqrewr
% 3.00/3.42 backwardsubs = 1
% 3.00/3.42 selectoldest = 5
% 3.00/3.42
% 3.00/3.42 litorderings [0] = split
% 3.00/3.42 litorderings [1] = extend the termordering, first sorting on arguments
% 3.00/3.42
% 3.00/3.42 termordering = kbo
% 3.00/3.42
% 3.00/3.42 litapriori = 0
% 3.00/3.42 termapriori = 1
% 3.00/3.42 litaposteriori = 0
% 3.00/3.42 termaposteriori = 0
% 3.00/3.42 demodaposteriori = 0
% 3.00/3.42 ordereqreflfact = 0
% 3.00/3.42
% 3.00/3.42 litselect = negord
% 3.00/3.42
% 3.00/3.42 maxweight = 15
% 3.00/3.42 maxdepth = 30000
% 3.00/3.42 maxlength = 115
% 3.00/3.42 maxnrvars = 195
% 3.00/3.42 excuselevel = 1
% 3.00/3.42 increasemaxweight = 1
% 3.00/3.42
% 3.00/3.42 maxselected = 10000000
% 3.00/3.42 maxnrclauses = 10000000
% 3.00/3.42
% 3.00/3.42 showgenerated = 0
% 3.00/3.42 showkept = 0
% 3.00/3.42 showselected = 0
% 3.00/3.42 showdeleted = 0
% 3.00/3.42 showresimp = 1
% 3.00/3.42 showstatus = 2000
% 3.00/3.42
% 3.00/3.42 prologoutput = 0
% 3.00/3.42 nrgoals = 5000000
% 3.00/3.42 totalproof = 1
% 3.00/3.42
% 3.00/3.42 Symbols occurring in the translation:
% 3.00/3.42
% 3.00/3.42 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.00/3.42 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 3.00/3.42 ! [4, 1] (w:0, o:27, a:1, s:1, b:0),
% 3.00/3.42 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.00/3.42 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.00/3.42 in [37, 2] (w:1, o:71, a:1, s:1, b:0),
% 3.00/3.42 empty [38, 1] (w:1, o:32, a:1, s:1, b:0),
% 3.00/3.42 function [39, 1] (w:1, o:35, a:1, s:1, b:0),
% 3.00/3.42 ordinal [40, 1] (w:1, o:36, a:1, s:1, b:0),
% 3.00/3.42 epsilon_transitive [41, 1] (w:1, o:33, a:1, s:1, b:0),
% 3.00/3.42 epsilon_connected [42, 1] (w:1, o:34, a:1, s:1, b:0),
% 3.00/3.42 relation [43, 1] (w:1, o:37, a:1, s:1, b:0),
% 3.00/3.42 one_to_one [44, 1] (w:1, o:38, a:1, s:1, b:0),
% 3.00/3.42 transfinite_sequence [45, 1] (w:1, o:41, a:1, s:1, b:0),
% 3.00/3.42 transfinite_sequence_of [46, 2] (w:1, o:74, a:1, s:1, b:0),
% 3.00/3.42 relation_rng [47, 1] (w:1, o:42, a:1, s:1, b:0),
% 3.00/3.42 subset [48, 2] (w:1, o:73, a:1, s:1, b:0),
% 3.00/3.42 tseq_dom_restriction [49, 2] (w:1, o:75, a:1, s:1, b:0),
% 3.00/3.42 relation_dom_restriction [50, 2] (w:1, o:72, a:1, s:1, b:0),
% 3.00/3.42 element [51, 2] (w:1, o:76, a:1, s:1, b:0),
% 3.00/3.42 empty_set [52, 0] (w:1, o:8, a:1, s:1, b:0),
% 3.00/3.42 relation_empty_yielding [53, 1] (w:1, o:43, a:1, s:1, b:0),
% 3.00/3.42 relation_non_empty [54, 1] (w:1, o:44, a:1, s:1, b:0),
% 3.00/3.42 with_non_empty_elements [55, 1] (w:1, o:45, a:1, s:1, b:0),
% 3.00/3.42 powerset [56, 1] (w:1, o:46, a:1, s:1, b:0),
% 3.00/3.42 skol1 [58, 1] (w:1, o:39, a:1, s:1, b:1),
% 3.00/3.42 skol2 [59, 1] (w:1, o:40, a:1, s:1, b:1),
% 3.00/3.42 skol3 [60, 0] (w:1, o:10, a:1, s:1, b:1),
% 3.00/3.42 skol4 [61, 0] (w:1, o:11, a:1, s:1, b:1),
% 3.00/3.42 skol5 [62, 0] (w:1, o:12, a:1, s:1, b:1),
% 3.00/3.42 skol6 [63, 0] (w:1, o:13, a:1, s:1, b:1),
% 3.00/3.42 skol7 [64, 0] (w:1, o:14, a:1, s:1, b:1),
% 3.00/3.42 skol8 [65, 0] (w:1, o:15, a:1, s:1, b:1),
% 3.00/3.42 skol9 [66, 0] (w:1, o:16, a:1, s:1, b:1),
% 3.00/3.42 skol10 [67, 0] (w:1, o:17, a:1, s:1, b:1),
% 3.00/3.42 skol11 [68, 0] (w:1, o:18, a:1, s:1, b:1),
% 3.00/3.42 skol12 [69, 0] (w:1, o:19, a:1, s:1, b:1),
% 3.00/3.42 skol13 [70, 0] (w:1, o:20, a:1, s:1, b:1),
% 3.00/3.42 skol14 [71, 0] (w:1, o:21, a:1, s:1, b:1),
% 3.00/3.42 skol15 [72, 0] (w:1, o:22, a:1, s:1, b:1),
% 3.00/3.42 skol16 [73, 0] (w:1, o:23, a:1, s:1, b:1),
% 3.00/3.42 skol17 [74, 0] (w:1, o:24, a:1, s:1, b:1),
% 3.00/3.42 skol18 [75, 0] (w:1, o:25, a:1, s:1, b:1),
% 3.00/3.42 skol19 [76, 0] (w:1, o:26, a:1, s:1, b:1).
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42 Starting Search:
% 3.00/3.42
% 3.00/3.42 *** allocated 15000 integers for clauses
% 3.00/3.42 *** allocated 22500 integers for clauses
% 3.00/3.42 *** allocated 33750 integers for clauses
% 3.00/3.42 *** allocated 50625 integers for clauses
% 3.00/3.42 *** allocated 15000 integers for termspace/termends
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 75937 integers for clauses
% 3.00/3.42 *** allocated 22500 integers for termspace/termends
% 3.00/3.42 *** allocated 113905 integers for clauses
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 7193
% 3.00/3.42 Kept: 2000
% 3.00/3.42 Inuse: 398
% 3.00/3.42 Deleted: 205
% 3.00/3.42 Deletedinuse: 85
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 33750 integers for termspace/termends
% 3.00/3.42 *** allocated 170857 integers for clauses
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 50625 integers for termspace/termends
% 3.00/3.42 *** allocated 256285 integers for clauses
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 16411
% 3.00/3.42 Kept: 4124
% 3.00/3.42 Inuse: 597
% 3.00/3.42 Deleted: 323
% 3.00/3.42 Deletedinuse: 109
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 75937 integers for termspace/termends
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 384427 integers for clauses
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 25730
% 3.00/3.42 Kept: 6314
% 3.00/3.42 Inuse: 729
% 3.00/3.42 Deleted: 382
% 3.00/3.42 Deletedinuse: 123
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 113905 integers for termspace/termends
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 37434
% 3.00/3.42 Kept: 8320
% 3.00/3.42 Inuse: 829
% 3.00/3.42 Deleted: 433
% 3.00/3.42 Deletedinuse: 157
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 576640 integers for clauses
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 170857 integers for termspace/termends
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 44752
% 3.00/3.42 Kept: 10424
% 3.00/3.42 Inuse: 916
% 3.00/3.42 Deleted: 462
% 3.00/3.42 Deletedinuse: 162
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 52061
% 3.00/3.42 Kept: 12500
% 3.00/3.42 Inuse: 990
% 3.00/3.42 Deleted: 512
% 3.00/3.42 Deletedinuse: 171
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 864960 integers for clauses
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 *** allocated 256285 integers for termspace/termends
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 58516
% 3.00/3.42 Kept: 14541
% 3.00/3.42 Inuse: 1060
% 3.00/3.42 Deleted: 599
% 3.00/3.42 Deletedinuse: 234
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 64751
% 3.00/3.42 Kept: 16559
% 3.00/3.42 Inuse: 1126
% 3.00/3.42 Deleted: 631
% 3.00/3.42 Deletedinuse: 236
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42 Intermediate Status:
% 3.00/3.42 Generated: 75049
% 3.00/3.42 Kept: 18589
% 3.00/3.42 Inuse: 1197
% 3.00/3.42 Deleted: 745
% 3.00/3.42 Deletedinuse: 336
% 3.00/3.42
% 3.00/3.42 Resimplifying inuse:
% 3.00/3.42 Done
% 3.00/3.42
% 3.00/3.42 Resimplifying clauses:
% 3.00/3.42 *** allocated 384427 integers for termspace/termends
% 3.00/3.42
% 3.00/3.42 Bliksems!, er is een bewijs:
% 3.00/3.42 % SZS status Theorem
% 3.00/3.42 % SZS output start Refutation
% 3.00/3.42
% 3.00/3.42 (10) {G0,W13,D3,L5,V2,M5} I { ! relation( X ), ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! transfinite_sequence_of( X, Y ), subset(
% 3.00/3.42 relation_rng( X ), Y ) }.
% 3.00/3.42 (12) {G0,W14,D3,L5,V2,M5} I { ! relation( X ), ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! ordinal( Y ), transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( X, Y ), relation_rng( X ) ) }.
% 3.00/3.42 (14) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y ), relation( X
% 3.00/3.42 ) }.
% 3.00/3.42 (15) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y ), function( X
% 3.00/3.42 ) }.
% 3.00/3.42 (16) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y ),
% 3.00/3.42 transfinite_sequence( X ) }.
% 3.00/3.42 (72) {G0,W15,D3,L5,V2,M5} I { ! relation( X ), ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! ordinal( Y ), tseq_dom_restriction( X, Y )
% 3.00/3.42 ==> relation_dom_restriction( X, Y ) }.
% 3.00/3.42 (78) {G0,W9,D2,L3,V3,M3} I { ! subset( X, Y ), ! transfinite_sequence_of( Z
% 3.00/3.42 , X ), transfinite_sequence_of( Z, Y ) }.
% 3.00/3.42 (79) {G0,W3,D2,L1,V0,M1} I { transfinite_sequence_of( skol18, skol17 ) }.
% 3.00/3.42 (80) {G0,W2,D2,L1,V0,M1} I { ordinal( skol19 ) }.
% 3.00/3.42 (81) {G0,W5,D3,L1,V0,M1} I { ! transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( skol18, skol19 ), skol17 ) }.
% 3.00/3.42 (131) {G1,W14,D3,L5,V2,M5} S(12);d(72) { ! relation( X ), ! function( X ),
% 3.00/3.42 ! transfinite_sequence( X ), ! ordinal( Y ), transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ) }.
% 3.00/3.42 (152) {G1,W14,D3,L5,V3,M5} R(14,10) { ! transfinite_sequence_of( X, Y ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! transfinite_sequence_of( X
% 3.00/3.42 , Z ), subset( relation_rng( X ), Z ) }.
% 3.00/3.42 (153) {G2,W11,D3,L4,V2,M4} F(152) { ! transfinite_sequence_of( X, Y ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), subset( relation_rng( X ), Y
% 3.00/3.42 ) }.
% 3.00/3.42 (155) {G1,W2,D2,L1,V0,M1} R(79,14) { relation( skol18 ) }.
% 3.00/3.42 (157) {G1,W2,D2,L1,V0,M1} R(15,79) { function( skol18 ) }.
% 3.00/3.42 (167) {G1,W2,D2,L1,V0,M1} R(16,79) { transfinite_sequence( skol18 ) }.
% 3.00/3.42 (1030) {G2,W10,D3,L3,V1,M3} R(131,167);r(155) { ! function( skol18 ), !
% 3.00/3.42 ordinal( X ), transfinite_sequence_of( relation_dom_restriction( skol18,
% 3.00/3.42 X ), relation_rng( skol18 ) ) }.
% 3.00/3.42 (1247) {G3,W6,D3,L2,V0,M2} R(153,79);r(157) { ! transfinite_sequence(
% 3.00/3.42 skol18 ), subset( relation_rng( skol18 ), skol17 ) }.
% 3.00/3.42 (1687) {G4,W4,D3,L1,V0,M1} S(1247);r(167) { subset( relation_rng( skol18 )
% 3.00/3.42 , skol17 ) }.
% 3.00/3.42 (1688) {G5,W7,D3,L2,V1,M2} R(1687,78) { ! transfinite_sequence_of( X,
% 3.00/3.42 relation_rng( skol18 ) ), transfinite_sequence_of( X, skol17 ) }.
% 3.00/3.42 (6823) {G6,W6,D3,L1,V0,M1} R(1688,81) { ! transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( skol18, skol19 ), relation_rng( skol18 ) ) }.
% 3.00/3.42 (6864) {G7,W8,D2,L4,V0,M4} P(72,6823);r(1030) { ! relation( skol18 ), !
% 3.00/3.42 function( skol18 ), ! transfinite_sequence( skol18 ), ! ordinal( skol19 )
% 3.00/3.42 }.
% 3.00/3.42 (20312) {G8,W0,D0,L0,V0,M0} S(6864);r(155);r(157);r(167);r(80) { }.
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42 % SZS output end Refutation
% 3.00/3.42 found a proof!
% 3.00/3.42
% 3.00/3.42 *** allocated 1297440 integers for clauses
% 3.00/3.42
% 3.00/3.42 Unprocessed initial clauses:
% 3.00/3.42
% 3.00/3.42 (20314) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 3.00/3.42 (20315) {G0,W4,D2,L2,V1,M2} { ! empty( X ), function( X ) }.
% 3.00/3.42 (20316) {G0,W4,D2,L2,V1,M2} { ! ordinal( X ), epsilon_transitive( X ) }.
% 3.00/3.42 (20317) {G0,W4,D2,L2,V1,M2} { ! ordinal( X ), epsilon_connected( X ) }.
% 3.00/3.42 (20318) {G0,W4,D2,L2,V1,M2} { ! empty( X ), relation( X ) }.
% 3.00/3.42 (20319) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 3.00/3.42 ), relation( X ) }.
% 3.00/3.42 (20320) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 3.00/3.42 ), function( X ) }.
% 3.00/3.42 (20321) {G0,W8,D2,L4,V1,M4} { ! relation( X ), ! empty( X ), ! function( X
% 3.00/3.42 ), one_to_one( X ) }.
% 3.00/3.42 (20322) {G0,W6,D2,L3,V1,M3} { ! epsilon_transitive( X ), !
% 3.00/3.42 epsilon_connected( X ), ordinal( X ) }.
% 3.00/3.42 (20323) {G0,W4,D2,L2,V1,M2} { ! empty( X ), epsilon_transitive( X ) }.
% 3.00/3.42 (20324) {G0,W4,D2,L2,V1,M2} { ! empty( X ), epsilon_connected( X ) }.
% 3.00/3.42 (20325) {G0,W4,D2,L2,V1,M2} { ! empty( X ), ordinal( X ) }.
% 3.00/3.42 (20326) {G0,W13,D3,L5,V2,M5} { ! relation( X ), ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! transfinite_sequence_of( X, Y ), subset(
% 3.00/3.42 relation_rng( X ), Y ) }.
% 3.00/3.42 (20327) {G0,W13,D3,L5,V2,M5} { ! relation( X ), ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! subset( relation_rng( X ), Y ),
% 3.00/3.42 transfinite_sequence_of( X, Y ) }.
% 3.00/3.42 (20328) {G0,W14,D3,L5,V2,M5} { ! relation( X ), ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! ordinal( Y ), transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( X, Y ), relation_rng( X ) ) }.
% 3.00/3.42 (20329) {G0,W6,D3,L2,V2,M2} { ! relation( X ), relation(
% 3.00/3.42 relation_dom_restriction( X, Y ) ) }.
% 3.00/3.42 (20330) {G0,W5,D2,L2,V2,M2} { ! transfinite_sequence_of( X, Y ), relation
% 3.00/3.42 ( X ) }.
% 3.00/3.42 (20331) {G0,W5,D2,L2,V2,M2} { ! transfinite_sequence_of( X, Y ), function
% 3.00/3.42 ( X ) }.
% 3.00/3.42 (20332) {G0,W5,D2,L2,V2,M2} { ! transfinite_sequence_of( X, Y ),
% 3.00/3.42 transfinite_sequence( X ) }.
% 3.00/3.42 (20333) {G0,W4,D3,L1,V1,M1} { transfinite_sequence_of( skol1( X ), X ) }.
% 3.00/3.42 (20334) {G0,W4,D3,L1,V1,M1} { element( skol2( X ), X ) }.
% 3.00/3.42 (20335) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 3.00/3.42 (20336) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 3.00/3.42 (20337) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( empty_set ) }.
% 3.00/3.42 (20338) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! relation_empty_yielding(
% 3.00/3.42 X ), relation( relation_dom_restriction( X, Y ) ) }.
% 3.00/3.42 (20339) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! relation_empty_yielding(
% 3.00/3.42 X ), relation_empty_yielding( relation_dom_restriction( X, Y ) ) }.
% 3.00/3.42 (20340) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 3.00/3.42 (20341) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 3.00/3.42 (20342) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( empty_set ) }.
% 3.00/3.42 (20343) {G0,W2,D2,L1,V0,M1} { function( empty_set ) }.
% 3.00/3.42 (20344) {G0,W2,D2,L1,V0,M1} { one_to_one( empty_set ) }.
% 3.00/3.42 (20345) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 3.00/3.42 (20346) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( empty_set ) }.
% 3.00/3.42 (20347) {G0,W2,D2,L1,V0,M1} { epsilon_connected( empty_set ) }.
% 3.00/3.42 (20348) {G0,W2,D2,L1,V0,M1} { ordinal( empty_set ) }.
% 3.00/3.42 (20349) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! function( X ), relation(
% 3.00/3.42 relation_dom_restriction( X, Y ) ) }.
% 3.00/3.42 (20350) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! function( X ), function(
% 3.00/3.42 relation_dom_restriction( X, Y ) ) }.
% 3.00/3.42 (20351) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 3.00/3.42 (20352) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 3.00/3.42 (20353) {G0,W9,D3,L4,V1,M4} { ! relation( X ), ! relation_non_empty( X ),
% 3.00/3.42 ! function( X ), with_non_empty_elements( relation_rng( X ) ) }.
% 3.00/3.42 (20354) {G0,W7,D3,L3,V1,M3} { empty( X ), ! relation( X ), ! empty(
% 3.00/3.42 relation_rng( X ) ) }.
% 3.00/3.42 (20355) {G0,W5,D3,L2,V1,M2} { ! empty( X ), empty( relation_rng( X ) ) }.
% 3.00/3.42 (20356) {G0,W5,D3,L2,V1,M2} { ! empty( X ), relation( relation_rng( X ) )
% 3.00/3.42 }.
% 3.00/3.42 (20357) {G0,W2,D2,L1,V0,M1} { relation( skol3 ) }.
% 3.00/3.42 (20358) {G0,W2,D2,L1,V0,M1} { function( skol3 ) }.
% 3.00/3.42 (20359) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol4 ) }.
% 3.00/3.42 (20360) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol4 ) }.
% 3.00/3.42 (20361) {G0,W2,D2,L1,V0,M1} { ordinal( skol4 ) }.
% 3.00/3.42 (20362) {G0,W2,D2,L1,V0,M1} { empty( skol5 ) }.
% 3.00/3.42 (20363) {G0,W2,D2,L1,V0,M1} { relation( skol5 ) }.
% 3.00/3.42 (20364) {G0,W2,D2,L1,V0,M1} { empty( skol6 ) }.
% 3.00/3.42 (20365) {G0,W2,D2,L1,V0,M1} { relation( skol7 ) }.
% 3.00/3.42 (20366) {G0,W2,D2,L1,V0,M1} { empty( skol7 ) }.
% 3.00/3.42 (20367) {G0,W2,D2,L1,V0,M1} { function( skol7 ) }.
% 3.00/3.42 (20368) {G0,W2,D2,L1,V0,M1} { relation( skol8 ) }.
% 3.00/3.42 (20369) {G0,W2,D2,L1,V0,M1} { function( skol8 ) }.
% 3.00/3.42 (20370) {G0,W2,D2,L1,V0,M1} { one_to_one( skol8 ) }.
% 3.00/3.42 (20371) {G0,W2,D2,L1,V0,M1} { empty( skol8 ) }.
% 3.00/3.42 (20372) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol8 ) }.
% 3.00/3.42 (20373) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol8 ) }.
% 3.00/3.42 (20374) {G0,W2,D2,L1,V0,M1} { ordinal( skol8 ) }.
% 3.00/3.42 (20375) {G0,W2,D2,L1,V0,M1} { ! empty( skol9 ) }.
% 3.00/3.42 (20376) {G0,W2,D2,L1,V0,M1} { relation( skol9 ) }.
% 3.00/3.42 (20377) {G0,W2,D2,L1,V0,M1} { ! empty( skol10 ) }.
% 3.00/3.42 (20378) {G0,W2,D2,L1,V0,M1} { relation( skol11 ) }.
% 3.00/3.42 (20379) {G0,W2,D2,L1,V0,M1} { function( skol11 ) }.
% 3.00/3.42 (20380) {G0,W2,D2,L1,V0,M1} { one_to_one( skol11 ) }.
% 3.00/3.42 (20381) {G0,W2,D2,L1,V0,M1} { ! empty( skol12 ) }.
% 3.00/3.42 (20382) {G0,W2,D2,L1,V0,M1} { epsilon_transitive( skol12 ) }.
% 3.00/3.42 (20383) {G0,W2,D2,L1,V0,M1} { epsilon_connected( skol12 ) }.
% 3.00/3.42 (20384) {G0,W2,D2,L1,V0,M1} { ordinal( skol12 ) }.
% 3.00/3.42 (20385) {G0,W2,D2,L1,V0,M1} { relation( skol13 ) }.
% 3.00/3.42 (20386) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol13 ) }.
% 3.00/3.42 (20387) {G0,W2,D2,L1,V0,M1} { relation( skol14 ) }.
% 3.00/3.42 (20388) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol14 ) }.
% 3.00/3.42 (20389) {G0,W2,D2,L1,V0,M1} { function( skol14 ) }.
% 3.00/3.42 (20390) {G0,W2,D2,L1,V0,M1} { relation( skol15 ) }.
% 3.00/3.42 (20391) {G0,W2,D2,L1,V0,M1} { function( skol15 ) }.
% 3.00/3.42 (20392) {G0,W2,D2,L1,V0,M1} { transfinite_sequence( skol15 ) }.
% 3.00/3.42 (20393) {G0,W2,D2,L1,V0,M1} { relation( skol16 ) }.
% 3.00/3.42 (20394) {G0,W2,D2,L1,V0,M1} { relation_non_empty( skol16 ) }.
% 3.00/3.42 (20395) {G0,W2,D2,L1,V0,M1} { function( skol16 ) }.
% 3.00/3.42 (20396) {G0,W15,D3,L5,V2,M5} { ! relation( X ), ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! ordinal( Y ), tseq_dom_restriction( X, Y ) =
% 3.00/3.42 relation_dom_restriction( X, Y ) }.
% 3.00/3.42 (20397) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 3.00/3.42 (20398) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 3.00/3.42 (20399) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y )
% 3.00/3.42 }.
% 3.00/3.42 (20400) {G0,W7,D3,L2,V2,M2} { ! element( X, powerset( Y ) ), subset( X, Y
% 3.00/3.42 ) }.
% 3.00/3.42 (20401) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X, powerset( Y )
% 3.00/3.42 ) }.
% 3.00/3.42 (20402) {G0,W9,D2,L3,V3,M3} { ! subset( X, Y ), ! transfinite_sequence_of
% 3.00/3.42 ( Z, X ), transfinite_sequence_of( Z, Y ) }.
% 3.00/3.42 (20403) {G0,W3,D2,L1,V0,M1} { transfinite_sequence_of( skol18, skol17 )
% 3.00/3.42 }.
% 3.00/3.42 (20404) {G0,W2,D2,L1,V0,M1} { ordinal( skol19 ) }.
% 3.00/3.42 (20405) {G0,W5,D3,L1,V0,M1} { ! transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( skol18, skol19 ), skol17 ) }.
% 3.00/3.42 (20406) {G0,W10,D3,L3,V3,M3} { ! in( X, Z ), ! element( Z, powerset( Y ) )
% 3.00/3.42 , element( X, Y ) }.
% 3.00/3.42 (20407) {G0,W9,D3,L3,V3,M3} { ! in( X, Y ), ! element( Y, powerset( Z ) )
% 3.00/3.42 , ! empty( Z ) }.
% 3.00/3.42 (20408) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 3.00/3.42 (20409) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 3.00/3.42 (20410) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 3.00/3.42
% 3.00/3.42
% 3.00/3.42 Total Proof:
% 3.00/3.42
% 3.00/3.42 subsumption: (10) {G0,W13,D3,L5,V2,M5} I { ! relation( X ), ! function( X )
% 3.00/3.42 , ! transfinite_sequence( X ), ! transfinite_sequence_of( X, Y ), subset
% 3.00/3.42 ( relation_rng( X ), Y ) }.
% 3.00/3.42 parent0: (20326) {G0,W13,D3,L5,V2,M5} { ! relation( X ), ! function( X ),
% 3.00/3.42 ! transfinite_sequence( X ), ! transfinite_sequence_of( X, Y ), subset(
% 3.00/3.42 relation_rng( X ), Y ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 2 ==> 2
% 3.00/3.42 3 ==> 3
% 3.00/3.42 4 ==> 4
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (12) {G0,W14,D3,L5,V2,M5} I { ! relation( X ), ! function( X )
% 3.00/3.42 , ! transfinite_sequence( X ), ! ordinal( Y ), transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( X, Y ), relation_rng( X ) ) }.
% 3.00/3.42 parent0: (20328) {G0,W14,D3,L5,V2,M5} { ! relation( X ), ! function( X ),
% 3.00/3.42 ! transfinite_sequence( X ), ! ordinal( Y ), transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( X, Y ), relation_rng( X ) ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 2 ==> 2
% 3.00/3.42 3 ==> 3
% 3.00/3.42 4 ==> 4
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (14) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y )
% 3.00/3.42 , relation( X ) }.
% 3.00/3.42 parent0: (20330) {G0,W5,D2,L2,V2,M2} { ! transfinite_sequence_of( X, Y ),
% 3.00/3.42 relation( X ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (15) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y )
% 3.00/3.42 , function( X ) }.
% 3.00/3.42 parent0: (20331) {G0,W5,D2,L2,V2,M2} { ! transfinite_sequence_of( X, Y ),
% 3.00/3.42 function( X ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (16) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y )
% 3.00/3.42 , transfinite_sequence( X ) }.
% 3.00/3.42 parent0: (20332) {G0,W5,D2,L2,V2,M2} { ! transfinite_sequence_of( X, Y ),
% 3.00/3.42 transfinite_sequence( X ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (72) {G0,W15,D3,L5,V2,M5} I { ! relation( X ), ! function( X )
% 3.00/3.42 , ! transfinite_sequence( X ), ! ordinal( Y ), tseq_dom_restriction( X, Y
% 3.00/3.42 ) ==> relation_dom_restriction( X, Y ) }.
% 3.00/3.42 parent0: (20396) {G0,W15,D3,L5,V2,M5} { ! relation( X ), ! function( X ),
% 3.00/3.42 ! transfinite_sequence( X ), ! ordinal( Y ), tseq_dom_restriction( X, Y )
% 3.00/3.42 = relation_dom_restriction( X, Y ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 2 ==> 2
% 3.00/3.42 3 ==> 3
% 3.00/3.42 4 ==> 4
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (78) {G0,W9,D2,L3,V3,M3} I { ! subset( X, Y ), !
% 3.00/3.42 transfinite_sequence_of( Z, X ), transfinite_sequence_of( Z, Y ) }.
% 3.00/3.42 parent0: (20402) {G0,W9,D2,L3,V3,M3} { ! subset( X, Y ), !
% 3.00/3.42 transfinite_sequence_of( Z, X ), transfinite_sequence_of( Z, Y ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 Z := Z
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 2 ==> 2
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (79) {G0,W3,D2,L1,V0,M1} I { transfinite_sequence_of( skol18,
% 3.00/3.42 skol17 ) }.
% 3.00/3.42 parent0: (20403) {G0,W3,D2,L1,V0,M1} { transfinite_sequence_of( skol18,
% 3.00/3.42 skol17 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (80) {G0,W2,D2,L1,V0,M1} I { ordinal( skol19 ) }.
% 3.00/3.42 parent0: (20404) {G0,W2,D2,L1,V0,M1} { ordinal( skol19 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (81) {G0,W5,D3,L1,V0,M1} I { ! transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( skol18, skol19 ), skol17 ) }.
% 3.00/3.42 parent0: (20405) {G0,W5,D3,L1,V0,M1} { ! transfinite_sequence_of(
% 3.00/3.42 tseq_dom_restriction( skol18, skol19 ), skol17 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 paramod: (20427) {G1,W22,D3,L9,V2,M9} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ), ! relation(
% 3.00/3.42 X ), ! function( X ), ! transfinite_sequence( X ), ! ordinal( Y ) }.
% 3.00/3.42 parent0[4]: (72) {G0,W15,D3,L5,V2,M5} I { ! relation( X ), ! function( X )
% 3.00/3.42 , ! transfinite_sequence( X ), ! ordinal( Y ), tseq_dom_restriction( X, Y
% 3.00/3.42 ) ==> relation_dom_restriction( X, Y ) }.
% 3.00/3.42 parent1[4; 1]: (12) {G0,W14,D3,L5,V2,M5} I { ! relation( X ), ! function( X
% 3.00/3.42 ), ! transfinite_sequence( X ), ! ordinal( Y ), transfinite_sequence_of
% 3.00/3.42 ( tseq_dom_restriction( X, Y ), relation_rng( X ) ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 substitution1:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 factor: (20428) {G1,W20,D3,L8,V2,M8} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ), ! function(
% 3.00/3.42 X ), ! transfinite_sequence( X ), ! ordinal( Y ) }.
% 3.00/3.42 parent0[1, 5]: (20427) {G1,W22,D3,L9,V2,M9} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ), ! relation(
% 3.00/3.42 X ), ! function( X ), ! transfinite_sequence( X ), ! ordinal( Y ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 factor: (20429) {G1,W18,D3,L7,V2,M7} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ), !
% 3.00/3.42 transfinite_sequence( X ), ! ordinal( Y ) }.
% 3.00/3.42 parent0[2, 5]: (20428) {G1,W20,D3,L8,V2,M8} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ), ! function(
% 3.00/3.42 X ), ! transfinite_sequence( X ), ! ordinal( Y ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 factor: (20430) {G1,W16,D3,L6,V2,M6} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ), ! ordinal( Y
% 3.00/3.42 ) }.
% 3.00/3.42 parent0[3, 5]: (20429) {G1,W18,D3,L7,V2,M7} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ), !
% 3.00/3.42 transfinite_sequence( X ), ! ordinal( Y ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 factor: (20431) {G1,W14,D3,L5,V2,M5} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ) }.
% 3.00/3.42 parent0[4, 5]: (20430) {G1,W16,D3,L6,V2,M6} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ), ! ordinal( Y
% 3.00/3.42 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (131) {G1,W14,D3,L5,V2,M5} S(12);d(72) { ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ),
% 3.00/3.42 transfinite_sequence_of( relation_dom_restriction( X, Y ), relation_rng(
% 3.00/3.42 X ) ) }.
% 3.00/3.42 parent0: (20431) {G1,W14,D3,L5,V2,M5} { transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( X, Y ), relation_rng( X ) ), ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 4
% 3.00/3.42 1 ==> 0
% 3.00/3.42 2 ==> 1
% 3.00/3.42 3 ==> 2
% 3.00/3.42 4 ==> 3
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 resolution: (20432) {G1,W14,D3,L5,V3,M5} { ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! transfinite_sequence_of( X, Y ), subset(
% 3.00/3.42 relation_rng( X ), Y ), ! transfinite_sequence_of( X, Z ) }.
% 3.00/3.42 parent0[0]: (10) {G0,W13,D3,L5,V2,M5} I { ! relation( X ), ! function( X )
% 3.00/3.42 , ! transfinite_sequence( X ), ! transfinite_sequence_of( X, Y ), subset
% 3.00/3.42 ( relation_rng( X ), Y ) }.
% 3.00/3.42 parent1[1]: (14) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y )
% 3.00/3.42 , relation( X ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 substitution1:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Z
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (152) {G1,W14,D3,L5,V3,M5} R(14,10) { !
% 3.00/3.42 transfinite_sequence_of( X, Y ), ! function( X ), ! transfinite_sequence
% 3.00/3.42 ( X ), ! transfinite_sequence_of( X, Z ), subset( relation_rng( X ), Z )
% 3.00/3.42 }.
% 3.00/3.42 parent0: (20432) {G1,W14,D3,L5,V3,M5} { ! function( X ), !
% 3.00/3.42 transfinite_sequence( X ), ! transfinite_sequence_of( X, Y ), subset(
% 3.00/3.42 relation_rng( X ), Y ), ! transfinite_sequence_of( X, Z ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Z
% 3.00/3.42 Z := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 1
% 3.00/3.42 1 ==> 2
% 3.00/3.42 2 ==> 3
% 3.00/3.42 3 ==> 4
% 3.00/3.42 4 ==> 0
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 factor: (20434) {G1,W11,D3,L4,V2,M4} { ! transfinite_sequence_of( X, Y ),
% 3.00/3.42 ! function( X ), ! transfinite_sequence( X ), subset( relation_rng( X ),
% 3.00/3.42 Y ) }.
% 3.00/3.42 parent0[0, 3]: (152) {G1,W14,D3,L5,V3,M5} R(14,10) { !
% 3.00/3.42 transfinite_sequence_of( X, Y ), ! function( X ), ! transfinite_sequence
% 3.00/3.42 ( X ), ! transfinite_sequence_of( X, Z ), subset( relation_rng( X ), Z )
% 3.00/3.42 }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 Z := Y
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (153) {G2,W11,D3,L4,V2,M4} F(152) { ! transfinite_sequence_of
% 3.00/3.42 ( X, Y ), ! function( X ), ! transfinite_sequence( X ), subset(
% 3.00/3.42 relation_rng( X ), Y ) }.
% 3.00/3.42 parent0: (20434) {G1,W11,D3,L4,V2,M4} { ! transfinite_sequence_of( X, Y )
% 3.00/3.42 , ! function( X ), ! transfinite_sequence( X ), subset( relation_rng( X )
% 3.00/3.42 , Y ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 Y := Y
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 2 ==> 2
% 3.00/3.42 3 ==> 3
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 resolution: (20435) {G1,W2,D2,L1,V0,M1} { relation( skol18 ) }.
% 3.00/3.42 parent0[0]: (14) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y )
% 3.00/3.42 , relation( X ) }.
% 3.00/3.42 parent1[0]: (79) {G0,W3,D2,L1,V0,M1} I { transfinite_sequence_of( skol18,
% 3.00/3.42 skol17 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := skol18
% 3.00/3.42 Y := skol17
% 3.00/3.42 end
% 3.00/3.42 substitution1:
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (155) {G1,W2,D2,L1,V0,M1} R(79,14) { relation( skol18 ) }.
% 3.00/3.42 parent0: (20435) {G1,W2,D2,L1,V0,M1} { relation( skol18 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 resolution: (20436) {G1,W2,D2,L1,V0,M1} { function( skol18 ) }.
% 3.00/3.42 parent0[0]: (15) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y )
% 3.00/3.42 , function( X ) }.
% 3.00/3.42 parent1[0]: (79) {G0,W3,D2,L1,V0,M1} I { transfinite_sequence_of( skol18,
% 3.00/3.42 skol17 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := skol18
% 3.00/3.42 Y := skol17
% 3.00/3.42 end
% 3.00/3.42 substitution1:
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (157) {G1,W2,D2,L1,V0,M1} R(15,79) { function( skol18 ) }.
% 3.00/3.42 parent0: (20436) {G1,W2,D2,L1,V0,M1} { function( skol18 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 resolution: (20437) {G1,W2,D2,L1,V0,M1} { transfinite_sequence( skol18 )
% 3.00/3.42 }.
% 3.00/3.42 parent0[0]: (16) {G0,W5,D2,L2,V2,M2} I { ! transfinite_sequence_of( X, Y )
% 3.00/3.42 , transfinite_sequence( X ) }.
% 3.00/3.42 parent1[0]: (79) {G0,W3,D2,L1,V0,M1} I { transfinite_sequence_of( skol18,
% 3.00/3.42 skol17 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := skol18
% 3.00/3.42 Y := skol17
% 3.00/3.42 end
% 3.00/3.42 substitution1:
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (167) {G1,W2,D2,L1,V0,M1} R(16,79) { transfinite_sequence(
% 3.00/3.42 skol18 ) }.
% 3.00/3.42 parent0: (20437) {G1,W2,D2,L1,V0,M1} { transfinite_sequence( skol18 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 resolution: (20438) {G2,W12,D3,L4,V1,M4} { ! relation( skol18 ), !
% 3.00/3.42 function( skol18 ), ! ordinal( X ), transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( skol18, X ), relation_rng( skol18 ) ) }.
% 3.00/3.42 parent0[2]: (131) {G1,W14,D3,L5,V2,M5} S(12);d(72) { ! relation( X ), !
% 3.00/3.42 function( X ), ! transfinite_sequence( X ), ! ordinal( Y ),
% 3.00/3.42 transfinite_sequence_of( relation_dom_restriction( X, Y ), relation_rng(
% 3.00/3.42 X ) ) }.
% 3.00/3.42 parent1[0]: (167) {G1,W2,D2,L1,V0,M1} R(16,79) { transfinite_sequence(
% 3.00/3.42 skol18 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := skol18
% 3.00/3.42 Y := X
% 3.00/3.42 end
% 3.00/3.42 substitution1:
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 resolution: (20439) {G2,W10,D3,L3,V1,M3} { ! function( skol18 ), ! ordinal
% 3.00/3.42 ( X ), transfinite_sequence_of( relation_dom_restriction( skol18, X ),
% 3.00/3.42 relation_rng( skol18 ) ) }.
% 3.00/3.42 parent0[0]: (20438) {G2,W12,D3,L4,V1,M4} { ! relation( skol18 ), !
% 3.00/3.42 function( skol18 ), ! ordinal( X ), transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( skol18, X ), relation_rng( skol18 ) ) }.
% 3.00/3.42 parent1[0]: (155) {G1,W2,D2,L1,V0,M1} R(79,14) { relation( skol18 ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 end
% 3.00/3.42 substitution1:
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 subsumption: (1030) {G2,W10,D3,L3,V1,M3} R(131,167);r(155) { ! function(
% 3.00/3.42 skol18 ), ! ordinal( X ), transfinite_sequence_of(
% 3.00/3.42 relation_dom_restriction( skol18, X ), relation_rng( skol18 ) ) }.
% 3.00/3.42 parent0: (20439) {G2,W10,D3,L3,V1,M3} { ! function( skol18 ), ! ordinal( X
% 3.00/3.42 ), transfinite_sequence_of( relation_dom_restriction( skol18, X ),
% 3.00/3.42 relation_rng( skol18 ) ) }.
% 3.00/3.42 substitution0:
% 3.00/3.42 X := X
% 3.00/3.42 end
% 3.00/3.42 permutation0:
% 3.00/3.42 0 ==> 0
% 3.00/3.42 1 ==> 1
% 3.00/3.42 2 ==> 2
% 3.00/3.42 end
% 3.00/3.42
% 3.00/3.42 resolution: (20440) {G1,W8,D3,L3,V0,M3} { ! function( skol18 ), !
% 3.00/3.42 transfinite_sequence( skol18 ), subset( relation_rng( skol18 ), skol17 )
% 3.00/3.42 }.
% 3.00/3.42 parent0[0]: (153) {G2,W11,D3,L4,V2,M4} F(152) { ! transfinite_sequence_of(
% 3.00/3.42 X, Y ), ! function( X ), ! transfinite_sequence( X ), subset(
% 3.00/3.43 relation_rng( X ), Y ) }.
% 3.00/3.43 parent1[0]: (79) {G0,W3,D2,L1,V0,M1} I { transfinite_sequence_of( skol18,
% 3.00/3.43 skol17 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 X := skol18
% 3.00/3.43 Y := skol17
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20441) {G2,W6,D3,L2,V0,M2} { ! transfinite_sequence( skol18 )
% 3.00/3.43 , subset( relation_rng( skol18 ), skol17 ) }.
% 3.00/3.43 parent0[0]: (20440) {G1,W8,D3,L3,V0,M3} { ! function( skol18 ), !
% 3.00/3.43 transfinite_sequence( skol18 ), subset( relation_rng( skol18 ), skol17 )
% 3.00/3.43 }.
% 3.00/3.43 parent1[0]: (157) {G1,W2,D2,L1,V0,M1} R(15,79) { function( skol18 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 subsumption: (1247) {G3,W6,D3,L2,V0,M2} R(153,79);r(157) { !
% 3.00/3.43 transfinite_sequence( skol18 ), subset( relation_rng( skol18 ), skol17 )
% 3.00/3.43 }.
% 3.00/3.43 parent0: (20441) {G2,W6,D3,L2,V0,M2} { ! transfinite_sequence( skol18 ),
% 3.00/3.43 subset( relation_rng( skol18 ), skol17 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 permutation0:
% 3.00/3.43 0 ==> 0
% 3.00/3.43 1 ==> 1
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20442) {G2,W4,D3,L1,V0,M1} { subset( relation_rng( skol18 ),
% 3.00/3.43 skol17 ) }.
% 3.00/3.43 parent0[0]: (1247) {G3,W6,D3,L2,V0,M2} R(153,79);r(157) { !
% 3.00/3.43 transfinite_sequence( skol18 ), subset( relation_rng( skol18 ), skol17 )
% 3.00/3.43 }.
% 3.00/3.43 parent1[0]: (167) {G1,W2,D2,L1,V0,M1} R(16,79) { transfinite_sequence(
% 3.00/3.43 skol18 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 subsumption: (1687) {G4,W4,D3,L1,V0,M1} S(1247);r(167) { subset(
% 3.00/3.43 relation_rng( skol18 ), skol17 ) }.
% 3.00/3.43 parent0: (20442) {G2,W4,D3,L1,V0,M1} { subset( relation_rng( skol18 ),
% 3.00/3.43 skol17 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 permutation0:
% 3.00/3.43 0 ==> 0
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20443) {G1,W7,D3,L2,V1,M2} { ! transfinite_sequence_of( X,
% 3.00/3.43 relation_rng( skol18 ) ), transfinite_sequence_of( X, skol17 ) }.
% 3.00/3.43 parent0[0]: (78) {G0,W9,D2,L3,V3,M3} I { ! subset( X, Y ), !
% 3.00/3.43 transfinite_sequence_of( Z, X ), transfinite_sequence_of( Z, Y ) }.
% 3.00/3.43 parent1[0]: (1687) {G4,W4,D3,L1,V0,M1} S(1247);r(167) { subset(
% 3.00/3.43 relation_rng( skol18 ), skol17 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 X := relation_rng( skol18 )
% 3.00/3.43 Y := skol17
% 3.00/3.43 Z := X
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 subsumption: (1688) {G5,W7,D3,L2,V1,M2} R(1687,78) { !
% 3.00/3.43 transfinite_sequence_of( X, relation_rng( skol18 ) ),
% 3.00/3.43 transfinite_sequence_of( X, skol17 ) }.
% 3.00/3.43 parent0: (20443) {G1,W7,D3,L2,V1,M2} { ! transfinite_sequence_of( X,
% 3.00/3.43 relation_rng( skol18 ) ), transfinite_sequence_of( X, skol17 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 X := X
% 3.00/3.43 end
% 3.00/3.43 permutation0:
% 3.00/3.43 0 ==> 0
% 3.00/3.43 1 ==> 1
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20444) {G1,W6,D3,L1,V0,M1} { ! transfinite_sequence_of(
% 3.00/3.43 tseq_dom_restriction( skol18, skol19 ), relation_rng( skol18 ) ) }.
% 3.00/3.43 parent0[0]: (81) {G0,W5,D3,L1,V0,M1} I { ! transfinite_sequence_of(
% 3.00/3.43 tseq_dom_restriction( skol18, skol19 ), skol17 ) }.
% 3.00/3.43 parent1[1]: (1688) {G5,W7,D3,L2,V1,M2} R(1687,78) { !
% 3.00/3.43 transfinite_sequence_of( X, relation_rng( skol18 ) ),
% 3.00/3.43 transfinite_sequence_of( X, skol17 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 X := tseq_dom_restriction( skol18, skol19 )
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 subsumption: (6823) {G6,W6,D3,L1,V0,M1} R(1688,81) { !
% 3.00/3.43 transfinite_sequence_of( tseq_dom_restriction( skol18, skol19 ),
% 3.00/3.43 relation_rng( skol18 ) ) }.
% 3.00/3.43 parent0: (20444) {G1,W6,D3,L1,V0,M1} { ! transfinite_sequence_of(
% 3.00/3.43 tseq_dom_restriction( skol18, skol19 ), relation_rng( skol18 ) ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 permutation0:
% 3.00/3.43 0 ==> 0
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 paramod: (20446) {G1,W14,D3,L5,V0,M5} { ! transfinite_sequence_of(
% 3.00/3.43 relation_dom_restriction( skol18, skol19 ), relation_rng( skol18 ) ), !
% 3.00/3.43 relation( skol18 ), ! function( skol18 ), ! transfinite_sequence( skol18
% 3.00/3.43 ), ! ordinal( skol19 ) }.
% 3.00/3.43 parent0[4]: (72) {G0,W15,D3,L5,V2,M5} I { ! relation( X ), ! function( X )
% 3.00/3.43 , ! transfinite_sequence( X ), ! ordinal( Y ), tseq_dom_restriction( X, Y
% 3.00/3.43 ) ==> relation_dom_restriction( X, Y ) }.
% 3.00/3.43 parent1[0; 2]: (6823) {G6,W6,D3,L1,V0,M1} R(1688,81) { !
% 3.00/3.43 transfinite_sequence_of( tseq_dom_restriction( skol18, skol19 ),
% 3.00/3.43 relation_rng( skol18 ) ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 X := skol18
% 3.00/3.43 Y := skol19
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20447) {G2,W12,D2,L6,V0,M6} { ! relation( skol18 ), !
% 3.00/3.43 function( skol18 ), ! transfinite_sequence( skol18 ), ! ordinal( skol19 )
% 3.00/3.43 , ! function( skol18 ), ! ordinal( skol19 ) }.
% 3.00/3.43 parent0[0]: (20446) {G1,W14,D3,L5,V0,M5} { ! transfinite_sequence_of(
% 3.00/3.43 relation_dom_restriction( skol18, skol19 ), relation_rng( skol18 ) ), !
% 3.00/3.43 relation( skol18 ), ! function( skol18 ), ! transfinite_sequence( skol18
% 3.00/3.43 ), ! ordinal( skol19 ) }.
% 3.00/3.43 parent1[2]: (1030) {G2,W10,D3,L3,V1,M3} R(131,167);r(155) { ! function(
% 3.00/3.43 skol18 ), ! ordinal( X ), transfinite_sequence_of(
% 3.00/3.43 relation_dom_restriction( skol18, X ), relation_rng( skol18 ) ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 X := skol19
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 factor: (20448) {G2,W10,D2,L5,V0,M5} { ! relation( skol18 ), ! function(
% 3.00/3.43 skol18 ), ! transfinite_sequence( skol18 ), ! ordinal( skol19 ), !
% 3.00/3.43 ordinal( skol19 ) }.
% 3.00/3.43 parent0[1, 4]: (20447) {G2,W12,D2,L6,V0,M6} { ! relation( skol18 ), !
% 3.00/3.43 function( skol18 ), ! transfinite_sequence( skol18 ), ! ordinal( skol19 )
% 3.00/3.43 , ! function( skol18 ), ! ordinal( skol19 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 factor: (20449) {G2,W8,D2,L4,V0,M4} { ! relation( skol18 ), ! function(
% 3.00/3.43 skol18 ), ! transfinite_sequence( skol18 ), ! ordinal( skol19 ) }.
% 3.00/3.43 parent0[3, 4]: (20448) {G2,W10,D2,L5,V0,M5} { ! relation( skol18 ), !
% 3.00/3.43 function( skol18 ), ! transfinite_sequence( skol18 ), ! ordinal( skol19 )
% 3.00/3.43 , ! ordinal( skol19 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 subsumption: (6864) {G7,W8,D2,L4,V0,M4} P(72,6823);r(1030) { ! relation(
% 3.00/3.43 skol18 ), ! function( skol18 ), ! transfinite_sequence( skol18 ), !
% 3.00/3.43 ordinal( skol19 ) }.
% 3.00/3.43 parent0: (20449) {G2,W8,D2,L4,V0,M4} { ! relation( skol18 ), ! function(
% 3.00/3.43 skol18 ), ! transfinite_sequence( skol18 ), ! ordinal( skol19 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 permutation0:
% 3.00/3.43 0 ==> 0
% 3.00/3.43 1 ==> 1
% 3.00/3.43 2 ==> 2
% 3.00/3.43 3 ==> 3
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20450) {G2,W6,D2,L3,V0,M3} { ! function( skol18 ), !
% 3.00/3.43 transfinite_sequence( skol18 ), ! ordinal( skol19 ) }.
% 3.00/3.43 parent0[0]: (6864) {G7,W8,D2,L4,V0,M4} P(72,6823);r(1030) { ! relation(
% 3.00/3.43 skol18 ), ! function( skol18 ), ! transfinite_sequence( skol18 ), !
% 3.00/3.43 ordinal( skol19 ) }.
% 3.00/3.43 parent1[0]: (155) {G1,W2,D2,L1,V0,M1} R(79,14) { relation( skol18 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20451) {G2,W4,D2,L2,V0,M2} { ! transfinite_sequence( skol18 )
% 3.00/3.43 , ! ordinal( skol19 ) }.
% 3.00/3.43 parent0[0]: (20450) {G2,W6,D2,L3,V0,M3} { ! function( skol18 ), !
% 3.00/3.43 transfinite_sequence( skol18 ), ! ordinal( skol19 ) }.
% 3.00/3.43 parent1[0]: (157) {G1,W2,D2,L1,V0,M1} R(15,79) { function( skol18 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20452) {G2,W2,D2,L1,V0,M1} { ! ordinal( skol19 ) }.
% 3.00/3.43 parent0[0]: (20451) {G2,W4,D2,L2,V0,M2} { ! transfinite_sequence( skol18 )
% 3.00/3.43 , ! ordinal( skol19 ) }.
% 3.00/3.43 parent1[0]: (167) {G1,W2,D2,L1,V0,M1} R(16,79) { transfinite_sequence(
% 3.00/3.43 skol18 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 resolution: (20453) {G1,W0,D0,L0,V0,M0} { }.
% 3.00/3.43 parent0[0]: (20452) {G2,W2,D2,L1,V0,M1} { ! ordinal( skol19 ) }.
% 3.00/3.43 parent1[0]: (80) {G0,W2,D2,L1,V0,M1} I { ordinal( skol19 ) }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 substitution1:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 subsumption: (20312) {G8,W0,D0,L0,V0,M0} S(6864);r(155);r(157);r(167);r(80)
% 3.00/3.43 { }.
% 3.00/3.43 parent0: (20453) {G1,W0,D0,L0,V0,M0} { }.
% 3.00/3.43 substitution0:
% 3.00/3.43 end
% 3.00/3.43 permutation0:
% 3.00/3.43 end
% 3.00/3.43
% 3.00/3.43 Proof check complete!
% 3.00/3.43
% 3.00/3.43 Memory use:
% 3.00/3.43
% 3.00/3.43 space for terms: 258605
% 3.00/3.43 space for clauses: 864134
% 3.00/3.43
% 3.00/3.43
% 3.00/3.43 clauses generated: 82305
% 3.00/3.43 clauses kept: 20313
% 3.00/3.43 clauses selected: 1244
% 3.00/3.43 clauses deleted: 4997
% 3.00/3.43 clauses inuse deleted: 336
% 3.00/3.43
% 3.00/3.43 subsentry: 365986
% 3.00/3.43 literals s-matched: 253641
% 3.00/3.43 literals matched: 219942
% 3.00/3.43 full subsumption: 43129
% 3.00/3.43
% 3.00/3.43 checksum: -2106470495
% 3.00/3.43
% 3.00/3.43
% 3.00/3.43 Bliksem ended
%------------------------------------------------------------------------------