%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SEU020+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n014.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:18 EDT 2022
% Result : Theorem 4.58s 4.96s
% Output : Refutation 4.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU020+1 : TPTP v8.1.0. Released v3.2.0.
% 0.11/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n014.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % DateTime : Mon Jun 20 10:59:02 EDT 2022
% 0.13/0.33 % CPUTime :
% 3.63/3.99 *** allocated 10000 integers for termspace/termends
% 3.63/3.99 *** allocated 10000 integers for clauses
% 3.63/3.99 *** allocated 10000 integers for justifications
% 3.63/3.99 Bliksem 1.12
% 3.63/3.99
% 3.63/3.99
% 3.63/3.99 Automatic Strategy Selection
% 3.63/3.99
% 3.63/3.99
% 3.63/3.99 Clauses:
% 3.63/3.99
% 3.63/3.99 { ! in( X, Y ), ! in( Y, X ) }.
% 3.63/3.99 { ! empty( X ), function( X ) }.
% 3.63/3.99 { ! empty( X ), relation( X ) }.
% 3.63/3.99 { ! relation( X ), ! relation( Y ), relation( relation_composition( X, Y )
% 3.63/3.99 ) }.
% 3.63/3.99 { relation( identity_relation( X ) ) }.
% 3.63/3.99 { element( skol1( X ), X ) }.
% 3.63/3.99 { ! empty( X ), ! relation( Y ), empty( relation_composition( Y, X ) ) }.
% 3.63/3.99 { ! empty( X ), ! relation( Y ), relation( relation_composition( Y, X ) ) }
% 3.63/3.99 .
% 3.63/3.99 { empty( empty_set ) }.
% 3.63/3.99 { relation( empty_set ) }.
% 3.63/3.99 { relation_empty_yielding( empty_set ) }.
% 3.63/3.99 { ! relation( X ), ! function( X ), ! relation( Y ), ! function( Y ),
% 3.63/3.99 relation( relation_composition( X, Y ) ) }.
% 3.63/3.99 { ! relation( X ), ! function( X ), ! relation( Y ), ! function( Y ),
% 3.63/3.99 function( relation_composition( X, Y ) ) }.
% 3.63/3.99 { ! empty( powerset( X ) ) }.
% 3.63/3.99 { empty( empty_set ) }.
% 3.63/3.99 { relation( identity_relation( X ) ) }.
% 3.63/3.99 { function( identity_relation( X ) ) }.
% 3.63/3.99 { empty( empty_set ) }.
% 3.63/3.99 { relation( empty_set ) }.
% 3.63/3.99 { empty( X ), ! relation( X ), ! empty( relation_dom( X ) ) }.
% 3.63/3.99 { empty( X ), ! relation( X ), ! empty( relation_rng( X ) ) }.
% 3.63/3.99 { ! empty( X ), empty( relation_dom( X ) ) }.
% 3.63/3.99 { ! empty( X ), relation( relation_dom( X ) ) }.
% 3.63/3.99 { ! empty( X ), empty( relation_rng( X ) ) }.
% 3.63/3.99 { ! empty( X ), relation( relation_rng( X ) ) }.
% 3.63/3.99 { ! empty( X ), ! relation( Y ), empty( relation_composition( X, Y ) ) }.
% 3.63/3.99 { ! empty( X ), ! relation( Y ), relation( relation_composition( X, Y ) ) }
% 3.63/3.99 .
% 3.63/3.99 { relation( skol2 ) }.
% 3.63/3.99 { function( skol2 ) }.
% 3.63/3.99 { empty( skol3 ) }.
% 3.63/3.99 { relation( skol3 ) }.
% 3.63/3.99 { empty( X ), ! empty( skol4( Y ) ) }.
% 3.63/3.99 { empty( X ), element( skol4( X ), powerset( X ) ) }.
% 3.63/3.99 { empty( skol5 ) }.
% 3.63/3.99 { ! empty( skol6 ) }.
% 3.63/3.99 { relation( skol6 ) }.
% 3.63/3.99 { empty( skol7( Y ) ) }.
% 3.63/3.99 { element( skol7( X ), powerset( X ) ) }.
% 3.63/3.99 { ! empty( skol8 ) }.
% 3.63/3.99 { relation( skol9 ) }.
% 3.63/3.99 { relation_empty_yielding( skol9 ) }.
% 3.63/3.99 { subset( X, X ) }.
% 3.63/3.99 { ! in( X, Y ), element( X, Y ) }.
% 3.63/3.99 { ! relation( X ), ! function( X ), ! relation( Y ), ! function( Y ), !
% 3.63/3.99 relation_dom( relation_composition( Y, X ) ) = relation_dom( Y ), subset
% 3.63/3.99 ( relation_rng( Y ), relation_dom( X ) ) }.
% 3.63/3.99 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 3.63/3.99 { ! element( X, powerset( Y ) ), subset( X, Y ) }.
% 3.63/3.99 { ! subset( X, Y ), element( X, powerset( Y ) ) }.
% 3.63/3.99 { ! relation( X ), ! function( X ), ! relation( Y ), ! function( Y ), !
% 3.63/3.99 one_to_one( relation_composition( Y, X ) ), ! subset( relation_rng( Y ),
% 3.63/3.99 relation_dom( X ) ), one_to_one( Y ) }.
% 3.63/3.99 { ! in( X, Z ), ! element( Z, powerset( Y ) ), element( X, Y ) }.
% 3.63/3.99 { one_to_one( identity_relation( X ) ) }.
% 3.63/3.99 { relation( skol10 ) }.
% 3.63/3.99 { function( skol10 ) }.
% 3.63/3.99 { relation( skol11 ) }.
% 3.63/3.99 { function( skol11 ) }.
% 3.63/3.99 { relation_composition( skol10, skol11 ) = identity_relation( relation_dom
% 3.63/3.99 ( skol10 ) ) }.
% 3.63/3.99 { ! one_to_one( skol10 ) }.
% 3.63/3.99 { ! in( X, Y ), ! element( Y, powerset( Z ) ), ! empty( Z ) }.
% 3.63/3.99 { ! empty( X ), X = empty_set }.
% 3.63/3.99 { relation_dom( identity_relation( X ) ) = X }.
% 3.63/3.99 { relation_rng( identity_relation( X ) ) = X }.
% 3.63/3.99 { ! in( X, Y ), ! empty( Y ) }.
% 3.63/3.99 { ! empty( X ), X = Y, ! empty( Y ) }.
% 3.63/3.99
% 3.63/3.99 percentage equality = 0.055556, percentage horn = 0.964912
% 3.63/3.99 This is a problem with some equality
% 3.63/3.99
% 3.63/3.99
% 3.63/3.99
% 3.63/3.99 Options Used:
% 3.63/3.99
% 3.63/3.99 useres = 1
% 3.63/3.99 useparamod = 1
% 3.63/3.99 useeqrefl = 1
% 3.63/3.99 useeqfact = 1
% 3.63/3.99 usefactor = 1
% 3.63/3.99 usesimpsplitting = 0
% 3.63/3.99 usesimpdemod = 5
% 3.63/3.99 usesimpres = 3
% 3.63/3.99
% 3.63/3.99 resimpinuse = 1000
% 3.63/3.99 resimpclauses = 20000
% 3.63/3.99 substype = eqrewr
% 3.63/3.99 backwardsubs = 1
% 3.63/3.99 selectoldest = 5
% 3.63/3.99
% 3.63/3.99 litorderings [0] = split
% 3.63/3.99 litorderings [1] = extend the termordering, first sorting on arguments
% 3.63/3.99
% 3.63/3.99 termordering = kbo
% 3.63/3.99
% 3.63/3.99 litapriori = 0
% 3.63/3.99 termapriori = 1
% 3.63/3.99 litaposteriori = 0
% 3.63/3.99 termaposteriori = 0
% 3.63/3.99 demodaposteriori = 0
% 3.63/3.99 ordereqreflfact = 0
% 3.63/3.99
% 3.63/3.99 litselect = negord
% 3.63/3.99
% 3.63/3.99 maxweight = 15
% 3.63/3.99 maxdepth = 30000
% 3.63/3.99 maxlength = 115
% 3.63/3.99 maxnrvars = 195
% 3.63/3.99 excuselevel = 1
% 3.63/3.99 increasemaxweight = 1
% 3.63/3.99
% 3.63/3.99 maxselected = 10000000
% 3.63/3.99 maxnrclauses = 10000000
% 3.63/3.99
% 3.63/3.99 showgenerated = 0
% 3.63/3.99 showkept = 0
% 4.58/4.96 showselected = 0
% 4.58/4.96 showdeleted = 0
% 4.58/4.96 showresimp = 1
% 4.58/4.96 showstatus = 2000
% 4.58/4.96
% 4.58/4.96 prologoutput = 0
% 4.58/4.96 nrgoals = 5000000
% 4.58/4.96 totalproof = 1
% 4.58/4.96
% 4.58/4.96 Symbols occurring in the translation:
% 4.58/4.96
% 4.58/4.96 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 4.58/4.96 . [1, 2] (w:1, o:35, a:1, s:1, b:0),
% 4.58/4.96 ! [4, 1] (w:0, o:18, a:1, s:1, b:0),
% 4.58/4.96 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 4.58/4.96 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 4.58/4.96 in [37, 2] (w:1, o:59, a:1, s:1, b:0),
% 4.58/4.96 empty [38, 1] (w:1, o:23, a:1, s:1, b:0),
% 4.58/4.96 function [39, 1] (w:1, o:24, a:1, s:1, b:0),
% 4.58/4.96 relation [40, 1] (w:1, o:25, a:1, s:1, b:0),
% 4.58/4.96 relation_composition [41, 2] (w:1, o:60, a:1, s:1, b:0),
% 4.58/4.96 identity_relation [42, 1] (w:1, o:26, a:1, s:1, b:0),
% 4.58/4.96 element [43, 2] (w:1, o:61, a:1, s:1, b:0),
% 4.58/4.96 empty_set [44, 0] (w:1, o:8, a:1, s:1, b:0),
% 4.58/4.96 relation_empty_yielding [45, 1] (w:1, o:28, a:1, s:1, b:0),
% 4.58/4.96 powerset [46, 1] (w:1, o:30, a:1, s:1, b:0),
% 4.58/4.96 relation_dom [47, 1] (w:1, o:27, a:1, s:1, b:0),
% 4.58/4.96 relation_rng [48, 1] (w:1, o:31, a:1, s:1, b:0),
% 4.58/4.96 subset [49, 2] (w:1, o:62, a:1, s:1, b:0),
% 4.58/4.96 one_to_one [50, 1] (w:1, o:29, a:1, s:1, b:0),
% 4.58/4.96 skol1 [52, 1] (w:1, o:32, a:1, s:1, b:1),
% 4.58/4.96 skol2 [53, 0] (w:1, o:12, a:1, s:1, b:1),
% 4.58/4.96 skol3 [54, 0] (w:1, o:13, a:1, s:1, b:1),
% 4.58/4.96 skol4 [55, 1] (w:1, o:33, a:1, s:1, b:1),
% 4.58/4.96 skol5 [56, 0] (w:1, o:14, a:1, s:1, b:1),
% 4.58/4.96 skol6 [57, 0] (w:1, o:15, a:1, s:1, b:1),
% 4.58/4.96 skol7 [58, 1] (w:1, o:34, a:1, s:1, b:1),
% 4.58/4.96 skol8 [59, 0] (w:1, o:16, a:1, s:1, b:1),
% 4.58/4.96 skol9 [60, 0] (w:1, o:17, a:1, s:1, b:1),
% 4.58/4.96 skol10 [61, 0] (w:1, o:10, a:1, s:1, b:1),
% 4.58/4.96 skol11 [62, 0] (w:1, o:11, a:1, s:1, b:1).
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Starting Search:
% 4.58/4.96
% 4.58/4.96 *** allocated 15000 integers for clauses
% 4.58/4.96 *** allocated 22500 integers for clauses
% 4.58/4.96 *** allocated 33750 integers for clauses
% 4.58/4.96 *** allocated 50625 integers for clauses
% 4.58/4.96 *** allocated 15000 integers for termspace/termends
% 4.58/4.96 *** allocated 75937 integers for clauses
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 22500 integers for termspace/termends
% 4.58/4.96 *** allocated 113905 integers for clauses
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 4619
% 4.58/4.96 Kept: 2006
% 4.58/4.96 Inuse: 198
% 4.58/4.96 Deleted: 62
% 4.58/4.96 Deletedinuse: 27
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 33750 integers for termspace/termends
% 4.58/4.96 *** allocated 170857 integers for clauses
% 4.58/4.96 *** allocated 50625 integers for termspace/termends
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 256285 integers for clauses
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 9163
% 4.58/4.96 Kept: 4030
% 4.58/4.96 Inuse: 269
% 4.58/4.96 Deleted: 65
% 4.58/4.96 Deletedinuse: 29
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 75937 integers for termspace/termends
% 4.58/4.96 *** allocated 384427 integers for clauses
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 14264
% 4.58/4.96 Kept: 6036
% 4.58/4.96 Inuse: 357
% 4.58/4.96 Deleted: 246
% 4.58/4.96 Deletedinuse: 53
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 113905 integers for termspace/termends
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 576640 integers for clauses
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 22440
% 4.58/4.96 Kept: 8049
% 4.58/4.96 Inuse: 445
% 4.58/4.96 Deleted: 299
% 4.58/4.96 Deletedinuse: 75
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 170857 integers for termspace/termends
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 31351
% 4.58/4.96 Kept: 10057
% 4.58/4.96 Inuse: 508
% 4.58/4.96 Deleted: 382
% 4.58/4.96 Deletedinuse: 79
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 864960 integers for clauses
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 41167
% 4.58/4.96 Kept: 12059
% 4.58/4.96 Inuse: 611
% 4.58/4.96 Deleted: 661
% 4.58/4.96 Deletedinuse: 125
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 56209
% 4.58/4.96 Kept: 14060
% 4.58/4.96 Inuse: 701
% 4.58/4.96 Deleted: 694
% 4.58/4.96 Deletedinuse: 125
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 256285 integers for termspace/termends
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 64472
% 4.58/4.96 Kept: 16077
% 4.58/4.96 Inuse: 776
% 4.58/4.96 Deleted: 714
% 4.58/4.96 Deletedinuse: 129
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 *** allocated 1297440 integers for clauses
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Intermediate Status:
% 4.58/4.96 Generated: 74413
% 4.58/4.96 Kept: 18177
% 4.58/4.96 Inuse: 817
% 4.58/4.96 Deleted: 728
% 4.58/4.96 Deletedinuse: 129
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 Resimplifying inuse:
% 4.58/4.96 Done
% 4.58/4.96
% 4.58/4.96 Resimplifying clauses:
% 4.58/4.96
% 4.58/4.96 Bliksems!, er is een bewijs:
% 4.58/4.96 % SZS status Theorem
% 4.58/4.96 % SZS output start Refutation
% 4.58/4.96
% 4.58/4.96 (38) {G0,W20,D4,L6,V2,M6} I { ! relation( X ), ! function( X ), ! relation
% 4.58/4.96 ( Y ), ! function( Y ), ! relation_dom( relation_composition( Y, X ) )
% 4.58/4.96 ==> relation_dom( Y ), subset( relation_rng( Y ), relation_dom( X ) ) }.
% 4.58/4.96 (42) {G0,W19,D3,L7,V2,M7} I { ! relation( X ), ! function( X ), ! relation
% 4.58/4.96 ( Y ), ! function( Y ), ! one_to_one( relation_composition( Y, X ) ), !
% 4.58/4.96 subset( relation_rng( Y ), relation_dom( X ) ), one_to_one( Y ) }.
% 4.58/4.96 (44) {G0,W3,D3,L1,V1,M1} I { one_to_one( identity_relation( X ) ) }.
% 4.58/4.96 (45) {G0,W2,D2,L1,V0,M1} I { relation( skol10 ) }.
% 4.58/4.96 (46) {G0,W2,D2,L1,V0,M1} I { function( skol10 ) }.
% 4.58/4.96 (47) {G0,W2,D2,L1,V0,M1} I { relation( skol11 ) }.
% 4.58/4.96 (48) {G0,W2,D2,L1,V0,M1} I { function( skol11 ) }.
% 4.58/4.96 (49) {G0,W7,D4,L1,V0,M1} I { relation_composition( skol10, skol11 ) ==>
% 4.58/4.96 identity_relation( relation_dom( skol10 ) ) }.
% 4.58/4.96 (50) {G0,W2,D2,L1,V0,M1} I { ! one_to_one( skol10 ) }.
% 4.58/4.96 (53) {G0,W5,D4,L1,V1,M1} I { relation_dom( identity_relation( X ) ) ==> X
% 4.58/4.96 }.
% 4.58/4.96 (358) {G1,W16,D4,L4,V1,M4} R(38,45);r(46) { ! relation( X ), ! function( X
% 4.58/4.96 ), ! relation_dom( relation_composition( skol10, X ) ) ==> relation_dom
% 4.58/4.96 ( skol10 ), subset( relation_rng( skol10 ), relation_dom( X ) ) }.
% 4.58/4.96 (13889) {G2,W5,D3,L1,V0,M1} R(358,47);d(49);d(53);q;r(48) { subset(
% 4.58/4.96 relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 (13892) {G3,W12,D4,L5,V0,M5} R(13889,42);d(49);r(47) { ! function( skol11 )
% 4.58/4.96 , ! relation( skol10 ), ! function( skol10 ), one_to_one( skol10 ), !
% 4.58/4.96 one_to_one( identity_relation( relation_dom( skol10 ) ) ) }.
% 4.58/4.96 (20020) {G4,W0,D0,L0,V0,M0} S(13892);r(48);r(45);r(46);r(50);r(44) { }.
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 % SZS output end Refutation
% 4.58/4.96 found a proof!
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Unprocessed initial clauses:
% 4.58/4.96
% 4.58/4.96 (20022) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 4.58/4.96 (20023) {G0,W4,D2,L2,V1,M2} { ! empty( X ), function( X ) }.
% 4.58/4.96 (20024) {G0,W4,D2,L2,V1,M2} { ! empty( X ), relation( X ) }.
% 4.58/4.96 (20025) {G0,W8,D3,L3,V2,M3} { ! relation( X ), ! relation( Y ), relation(
% 4.58/4.96 relation_composition( X, Y ) ) }.
% 4.58/4.96 (20026) {G0,W3,D3,L1,V1,M1} { relation( identity_relation( X ) ) }.
% 4.58/4.96 (20027) {G0,W4,D3,L1,V1,M1} { element( skol1( X ), X ) }.
% 4.58/4.96 (20028) {G0,W8,D3,L3,V2,M3} { ! empty( X ), ! relation( Y ), empty(
% 4.58/4.96 relation_composition( Y, X ) ) }.
% 4.58/4.96 (20029) {G0,W8,D3,L3,V2,M3} { ! empty( X ), ! relation( Y ), relation(
% 4.58/4.96 relation_composition( Y, X ) ) }.
% 4.58/4.96 (20030) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 4.58/4.96 (20031) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 4.58/4.96 (20032) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( empty_set ) }.
% 4.58/4.96 (20033) {G0,W12,D3,L5,V2,M5} { ! relation( X ), ! function( X ), !
% 4.58/4.96 relation( Y ), ! function( Y ), relation( relation_composition( X, Y ) )
% 4.58/4.96 }.
% 4.58/4.96 (20034) {G0,W12,D3,L5,V2,M5} { ! relation( X ), ! function( X ), !
% 4.58/4.96 relation( Y ), ! function( Y ), function( relation_composition( X, Y ) )
% 4.58/4.96 }.
% 4.58/4.96 (20035) {G0,W3,D3,L1,V1,M1} { ! empty( powerset( X ) ) }.
% 4.58/4.96 (20036) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 4.58/4.96 (20037) {G0,W3,D3,L1,V1,M1} { relation( identity_relation( X ) ) }.
% 4.58/4.96 (20038) {G0,W3,D3,L1,V1,M1} { function( identity_relation( X ) ) }.
% 4.58/4.96 (20039) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 4.58/4.96 (20040) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 4.58/4.96 (20041) {G0,W7,D3,L3,V1,M3} { empty( X ), ! relation( X ), ! empty(
% 4.58/4.96 relation_dom( X ) ) }.
% 4.58/4.96 (20042) {G0,W7,D3,L3,V1,M3} { empty( X ), ! relation( X ), ! empty(
% 4.58/4.96 relation_rng( X ) ) }.
% 4.58/4.96 (20043) {G0,W5,D3,L2,V1,M2} { ! empty( X ), empty( relation_dom( X ) ) }.
% 4.58/4.96 (20044) {G0,W5,D3,L2,V1,M2} { ! empty( X ), relation( relation_dom( X ) )
% 4.58/4.96 }.
% 4.58/4.96 (20045) {G0,W5,D3,L2,V1,M2} { ! empty( X ), empty( relation_rng( X ) ) }.
% 4.58/4.96 (20046) {G0,W5,D3,L2,V1,M2} { ! empty( X ), relation( relation_rng( X ) )
% 4.58/4.96 }.
% 4.58/4.96 (20047) {G0,W8,D3,L3,V2,M3} { ! empty( X ), ! relation( Y ), empty(
% 4.58/4.96 relation_composition( X, Y ) ) }.
% 4.58/4.96 (20048) {G0,W8,D3,L3,V2,M3} { ! empty( X ), ! relation( Y ), relation(
% 4.58/4.96 relation_composition( X, Y ) ) }.
% 4.58/4.96 (20049) {G0,W2,D2,L1,V0,M1} { relation( skol2 ) }.
% 4.58/4.96 (20050) {G0,W2,D2,L1,V0,M1} { function( skol2 ) }.
% 4.58/4.96 (20051) {G0,W2,D2,L1,V0,M1} { empty( skol3 ) }.
% 4.58/4.96 (20052) {G0,W2,D2,L1,V0,M1} { relation( skol3 ) }.
% 4.58/4.96 (20053) {G0,W5,D3,L2,V2,M2} { empty( X ), ! empty( skol4( Y ) ) }.
% 4.58/4.96 (20054) {G0,W7,D3,L2,V1,M2} { empty( X ), element( skol4( X ), powerset( X
% 4.58/4.96 ) ) }.
% 4.58/4.96 (20055) {G0,W2,D2,L1,V0,M1} { empty( skol5 ) }.
% 4.58/4.96 (20056) {G0,W2,D2,L1,V0,M1} { ! empty( skol6 ) }.
% 4.58/4.96 (20057) {G0,W2,D2,L1,V0,M1} { relation( skol6 ) }.
% 4.58/4.96 (20058) {G0,W3,D3,L1,V1,M1} { empty( skol7( Y ) ) }.
% 4.58/4.96 (20059) {G0,W5,D3,L1,V1,M1} { element( skol7( X ), powerset( X ) ) }.
% 4.58/4.96 (20060) {G0,W2,D2,L1,V0,M1} { ! empty( skol8 ) }.
% 4.58/4.96 (20061) {G0,W2,D2,L1,V0,M1} { relation( skol9 ) }.
% 4.58/4.96 (20062) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol9 ) }.
% 4.58/4.96 (20063) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 4.58/4.96 (20064) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 4.58/4.96 (20065) {G0,W20,D4,L6,V2,M6} { ! relation( X ), ! function( X ), !
% 4.58/4.96 relation( Y ), ! function( Y ), ! relation_dom( relation_composition( Y,
% 4.58/4.96 X ) ) = relation_dom( Y ), subset( relation_rng( Y ), relation_dom( X ) )
% 4.58/4.96 }.
% 4.58/4.96 (20066) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y )
% 4.58/4.96 }.
% 4.58/4.96 (20067) {G0,W7,D3,L2,V2,M2} { ! element( X, powerset( Y ) ), subset( X, Y
% 4.58/4.96 ) }.
% 4.58/4.96 (20068) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X, powerset( Y )
% 4.58/4.96 ) }.
% 4.58/4.96 (20069) {G0,W19,D3,L7,V2,M7} { ! relation( X ), ! function( X ), !
% 4.58/4.96 relation( Y ), ! function( Y ), ! one_to_one( relation_composition( Y, X
% 4.58/4.96 ) ), ! subset( relation_rng( Y ), relation_dom( X ) ), one_to_one( Y )
% 4.58/4.96 }.
% 4.58/4.96 (20070) {G0,W10,D3,L3,V3,M3} { ! in( X, Z ), ! element( Z, powerset( Y ) )
% 4.58/4.96 , element( X, Y ) }.
% 4.58/4.96 (20071) {G0,W3,D3,L1,V1,M1} { one_to_one( identity_relation( X ) ) }.
% 4.58/4.96 (20072) {G0,W2,D2,L1,V0,M1} { relation( skol10 ) }.
% 4.58/4.96 (20073) {G0,W2,D2,L1,V0,M1} { function( skol10 ) }.
% 4.58/4.96 (20074) {G0,W2,D2,L1,V0,M1} { relation( skol11 ) }.
% 4.58/4.96 (20075) {G0,W2,D2,L1,V0,M1} { function( skol11 ) }.
% 4.58/4.96 (20076) {G0,W7,D4,L1,V0,M1} { relation_composition( skol10, skol11 ) =
% 4.58/4.96 identity_relation( relation_dom( skol10 ) ) }.
% 4.58/4.96 (20077) {G0,W2,D2,L1,V0,M1} { ! one_to_one( skol10 ) }.
% 4.58/4.96 (20078) {G0,W9,D3,L3,V3,M3} { ! in( X, Y ), ! element( Y, powerset( Z ) )
% 4.58/4.96 , ! empty( Z ) }.
% 4.58/4.96 (20079) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 4.58/4.96 (20080) {G0,W5,D4,L1,V1,M1} { relation_dom( identity_relation( X ) ) = X
% 4.58/4.96 }.
% 4.58/4.96 (20081) {G0,W5,D4,L1,V1,M1} { relation_rng( identity_relation( X ) ) = X
% 4.58/4.96 }.
% 4.58/4.96 (20082) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 4.58/4.96 (20083) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Total Proof:
% 4.58/4.96
% 4.58/4.96 subsumption: (38) {G0,W20,D4,L6,V2,M6} I { ! relation( X ), ! function( X )
% 4.58/4.96 , ! relation( Y ), ! function( Y ), ! relation_dom( relation_composition
% 4.58/4.96 ( Y, X ) ) ==> relation_dom( Y ), subset( relation_rng( Y ), relation_dom
% 4.58/4.96 ( X ) ) }.
% 4.58/4.96 parent0: (20065) {G0,W20,D4,L6,V2,M6} { ! relation( X ), ! function( X ),
% 4.58/4.96 ! relation( Y ), ! function( Y ), ! relation_dom( relation_composition( Y
% 4.58/4.96 , X ) ) = relation_dom( Y ), subset( relation_rng( Y ), relation_dom( X )
% 4.58/4.96 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := X
% 4.58/4.96 Y := Y
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 1 ==> 1
% 4.58/4.96 2 ==> 2
% 4.58/4.96 3 ==> 3
% 4.58/4.96 4 ==> 4
% 4.58/4.96 5 ==> 5
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (42) {G0,W19,D3,L7,V2,M7} I { ! relation( X ), ! function( X )
% 4.58/4.96 , ! relation( Y ), ! function( Y ), ! one_to_one( relation_composition( Y
% 4.58/4.96 , X ) ), ! subset( relation_rng( Y ), relation_dom( X ) ), one_to_one( Y
% 4.58/4.96 ) }.
% 4.58/4.96 parent0: (20069) {G0,W19,D3,L7,V2,M7} { ! relation( X ), ! function( X ),
% 4.58/4.96 ! relation( Y ), ! function( Y ), ! one_to_one( relation_composition( Y,
% 4.58/4.96 X ) ), ! subset( relation_rng( Y ), relation_dom( X ) ), one_to_one( Y )
% 4.58/4.96 }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := X
% 4.58/4.96 Y := Y
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 1 ==> 1
% 4.58/4.96 2 ==> 2
% 4.58/4.96 3 ==> 3
% 4.58/4.96 4 ==> 4
% 4.58/4.96 5 ==> 5
% 4.58/4.96 6 ==> 6
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (44) {G0,W3,D3,L1,V1,M1} I { one_to_one( identity_relation( X
% 4.58/4.96 ) ) }.
% 4.58/4.96 parent0: (20071) {G0,W3,D3,L1,V1,M1} { one_to_one( identity_relation( X )
% 4.58/4.96 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := X
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (45) {G0,W2,D2,L1,V0,M1} I { relation( skol10 ) }.
% 4.58/4.96 parent0: (20072) {G0,W2,D2,L1,V0,M1} { relation( skol10 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (46) {G0,W2,D2,L1,V0,M1} I { function( skol10 ) }.
% 4.58/4.96 parent0: (20073) {G0,W2,D2,L1,V0,M1} { function( skol10 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (47) {G0,W2,D2,L1,V0,M1} I { relation( skol11 ) }.
% 4.58/4.96 parent0: (20074) {G0,W2,D2,L1,V0,M1} { relation( skol11 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (48) {G0,W2,D2,L1,V0,M1} I { function( skol11 ) }.
% 4.58/4.96 parent0: (20075) {G0,W2,D2,L1,V0,M1} { function( skol11 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (49) {G0,W7,D4,L1,V0,M1} I { relation_composition( skol10,
% 4.58/4.96 skol11 ) ==> identity_relation( relation_dom( skol10 ) ) }.
% 4.58/4.96 parent0: (20076) {G0,W7,D4,L1,V0,M1} { relation_composition( skol10,
% 4.58/4.96 skol11 ) = identity_relation( relation_dom( skol10 ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (50) {G0,W2,D2,L1,V0,M1} I { ! one_to_one( skol10 ) }.
% 4.58/4.96 parent0: (20077) {G0,W2,D2,L1,V0,M1} { ! one_to_one( skol10 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (53) {G0,W5,D4,L1,V1,M1} I { relation_dom( identity_relation(
% 4.58/4.96 X ) ) ==> X }.
% 4.58/4.96 parent0: (20080) {G0,W5,D4,L1,V1,M1} { relation_dom( identity_relation( X
% 4.58/4.96 ) ) = X }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := X
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 eqswap: (20217) {G0,W20,D4,L6,V2,M6} { ! relation_dom( X ) ==>
% 4.58/4.96 relation_dom( relation_composition( X, Y ) ), ! relation( Y ), ! function
% 4.58/4.96 ( Y ), ! relation( X ), ! function( X ), subset( relation_rng( X ),
% 4.58/4.96 relation_dom( Y ) ) }.
% 4.58/4.96 parent0[4]: (38) {G0,W20,D4,L6,V2,M6} I { ! relation( X ), ! function( X )
% 4.58/4.96 , ! relation( Y ), ! function( Y ), ! relation_dom( relation_composition
% 4.58/4.96 ( Y, X ) ) ==> relation_dom( Y ), subset( relation_rng( Y ), relation_dom
% 4.58/4.96 ( X ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := Y
% 4.58/4.96 Y := X
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20219) {G1,W18,D4,L5,V1,M5} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( relation_composition( skol10, X ) ), ! relation( X ), !
% 4.58/4.96 function( X ), ! function( skol10 ), subset( relation_rng( skol10 ),
% 4.58/4.96 relation_dom( X ) ) }.
% 4.58/4.96 parent0[3]: (20217) {G0,W20,D4,L6,V2,M6} { ! relation_dom( X ) ==>
% 4.58/4.96 relation_dom( relation_composition( X, Y ) ), ! relation( Y ), ! function
% 4.58/4.96 ( Y ), ! relation( X ), ! function( X ), subset( relation_rng( X ),
% 4.58/4.96 relation_dom( Y ) ) }.
% 4.58/4.96 parent1[0]: (45) {G0,W2,D2,L1,V0,M1} I { relation( skol10 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := skol10
% 4.58/4.96 Y := X
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20225) {G1,W16,D4,L4,V1,M4} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( relation_composition( skol10, X ) ), ! relation( X ), !
% 4.58/4.96 function( X ), subset( relation_rng( skol10 ), relation_dom( X ) ) }.
% 4.58/4.96 parent0[3]: (20219) {G1,W18,D4,L5,V1,M5} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( relation_composition( skol10, X ) ), ! relation( X ), !
% 4.58/4.96 function( X ), ! function( skol10 ), subset( relation_rng( skol10 ),
% 4.58/4.96 relation_dom( X ) ) }.
% 4.58/4.96 parent1[0]: (46) {G0,W2,D2,L1,V0,M1} I { function( skol10 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := X
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 eqswap: (20226) {G1,W16,D4,L4,V1,M4} { ! relation_dom(
% 4.58/4.96 relation_composition( skol10, X ) ) ==> relation_dom( skol10 ), !
% 4.58/4.96 relation( X ), ! function( X ), subset( relation_rng( skol10 ),
% 4.58/4.96 relation_dom( X ) ) }.
% 4.58/4.96 parent0[0]: (20225) {G1,W16,D4,L4,V1,M4} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( relation_composition( skol10, X ) ), ! relation( X ), !
% 4.58/4.96 function( X ), subset( relation_rng( skol10 ), relation_dom( X ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := X
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (358) {G1,W16,D4,L4,V1,M4} R(38,45);r(46) { ! relation( X ), !
% 4.58/4.96 function( X ), ! relation_dom( relation_composition( skol10, X ) ) ==>
% 4.58/4.96 relation_dom( skol10 ), subset( relation_rng( skol10 ), relation_dom( X )
% 4.58/4.96 ) }.
% 4.58/4.96 parent0: (20226) {G1,W16,D4,L4,V1,M4} { ! relation_dom(
% 4.58/4.96 relation_composition( skol10, X ) ) ==> relation_dom( skol10 ), !
% 4.58/4.96 relation( X ), ! function( X ), subset( relation_rng( skol10 ),
% 4.58/4.96 relation_dom( X ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := X
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 2
% 4.58/4.96 1 ==> 0
% 4.58/4.96 2 ==> 1
% 4.58/4.96 3 ==> 3
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 eqswap: (20227) {G1,W16,D4,L4,V1,M4} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( relation_composition( skol10, X ) ), ! relation( X ), !
% 4.58/4.96 function( X ), subset( relation_rng( skol10 ), relation_dom( X ) ) }.
% 4.58/4.96 parent0[2]: (358) {G1,W16,D4,L4,V1,M4} R(38,45);r(46) { ! relation( X ), !
% 4.58/4.96 function( X ), ! relation_dom( relation_composition( skol10, X ) ) ==>
% 4.58/4.96 relation_dom( skol10 ), subset( relation_rng( skol10 ), relation_dom( X )
% 4.58/4.96 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := X
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20230) {G1,W14,D4,L3,V0,M3} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( relation_composition( skol10, skol11 ) ), ! function(
% 4.58/4.96 skol11 ), subset( relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 parent0[1]: (20227) {G1,W16,D4,L4,V1,M4} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( relation_composition( skol10, X ) ), ! relation( X ), !
% 4.58/4.96 function( X ), subset( relation_rng( skol10 ), relation_dom( X ) ) }.
% 4.58/4.96 parent1[0]: (47) {G0,W2,D2,L1,V0,M1} I { relation( skol11 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := skol11
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 paramod: (20231) {G1,W14,D5,L3,V0,M3} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( identity_relation( relation_dom( skol10 ) ) ), ! function(
% 4.58/4.96 skol11 ), subset( relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 parent0[0]: (49) {G0,W7,D4,L1,V0,M1} I { relation_composition( skol10,
% 4.58/4.96 skol11 ) ==> identity_relation( relation_dom( skol10 ) ) }.
% 4.58/4.96 parent1[0; 5]: (20230) {G1,W14,D4,L3,V0,M3} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( relation_composition( skol10, skol11 ) ), ! function(
% 4.58/4.96 skol11 ), subset( relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 paramod: (20232) {G1,W12,D3,L3,V0,M3} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( skol10 ), ! function( skol11 ), subset( relation_rng(
% 4.58/4.96 skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 parent0[0]: (53) {G0,W5,D4,L1,V1,M1} I { relation_dom( identity_relation( X
% 4.58/4.96 ) ) ==> X }.
% 4.58/4.96 parent1[0; 4]: (20231) {G1,W14,D5,L3,V0,M3} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( identity_relation( relation_dom( skol10 ) ) ), ! function
% 4.58/4.96 ( skol11 ), subset( relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := relation_dom( skol10 )
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 eqrefl: (20233) {G0,W7,D3,L2,V0,M2} { ! function( skol11 ), subset(
% 4.58/4.96 relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 parent0[0]: (20232) {G1,W12,D3,L3,V0,M3} { ! relation_dom( skol10 ) ==>
% 4.58/4.96 relation_dom( skol10 ), ! function( skol11 ), subset( relation_rng(
% 4.58/4.96 skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20234) {G1,W5,D3,L1,V0,M1} { subset( relation_rng( skol10 ),
% 4.58/4.96 relation_dom( skol11 ) ) }.
% 4.58/4.96 parent0[0]: (20233) {G0,W7,D3,L2,V0,M2} { ! function( skol11 ), subset(
% 4.58/4.96 relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 parent1[0]: (48) {G0,W2,D2,L1,V0,M1} I { function( skol11 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (13889) {G2,W5,D3,L1,V0,M1} R(358,47);d(49);d(53);q;r(48) {
% 4.58/4.96 subset( relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 parent0: (20234) {G1,W5,D3,L1,V0,M1} { subset( relation_rng( skol10 ),
% 4.58/4.96 relation_dom( skol11 ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 0
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20236) {G1,W14,D3,L6,V0,M6} { ! relation( skol11 ), !
% 4.58/4.96 function( skol11 ), ! relation( skol10 ), ! function( skol10 ), !
% 4.58/4.96 one_to_one( relation_composition( skol10, skol11 ) ), one_to_one( skol10
% 4.58/4.96 ) }.
% 4.58/4.96 parent0[5]: (42) {G0,W19,D3,L7,V2,M7} I { ! relation( X ), ! function( X )
% 4.58/4.96 , ! relation( Y ), ! function( Y ), ! one_to_one( relation_composition( Y
% 4.58/4.96 , X ) ), ! subset( relation_rng( Y ), relation_dom( X ) ), one_to_one( Y
% 4.58/4.96 ) }.
% 4.58/4.96 parent1[0]: (13889) {G2,W5,D3,L1,V0,M1} R(358,47);d(49);d(53);q;r(48) {
% 4.58/4.96 subset( relation_rng( skol10 ), relation_dom( skol11 ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 X := skol11
% 4.58/4.96 Y := skol10
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 paramod: (20237) {G1,W14,D4,L6,V0,M6} { ! one_to_one( identity_relation(
% 4.58/4.96 relation_dom( skol10 ) ) ), ! relation( skol11 ), ! function( skol11 ), !
% 4.58/4.96 relation( skol10 ), ! function( skol10 ), one_to_one( skol10 ) }.
% 4.58/4.96 parent0[0]: (49) {G0,W7,D4,L1,V0,M1} I { relation_composition( skol10,
% 4.58/4.96 skol11 ) ==> identity_relation( relation_dom( skol10 ) ) }.
% 4.58/4.96 parent1[4; 2]: (20236) {G1,W14,D3,L6,V0,M6} { ! relation( skol11 ), !
% 4.58/4.96 function( skol11 ), ! relation( skol10 ), ! function( skol10 ), !
% 4.58/4.96 one_to_one( relation_composition( skol10, skol11 ) ), one_to_one( skol10
% 4.58/4.96 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20238) {G1,W12,D4,L5,V0,M5} { ! one_to_one( identity_relation
% 4.58/4.96 ( relation_dom( skol10 ) ) ), ! function( skol11 ), ! relation( skol10 )
% 4.58/4.96 , ! function( skol10 ), one_to_one( skol10 ) }.
% 4.58/4.96 parent0[1]: (20237) {G1,W14,D4,L6,V0,M6} { ! one_to_one( identity_relation
% 4.58/4.96 ( relation_dom( skol10 ) ) ), ! relation( skol11 ), ! function( skol11 )
% 4.58/4.96 , ! relation( skol10 ), ! function( skol10 ), one_to_one( skol10 ) }.
% 4.58/4.96 parent1[0]: (47) {G0,W2,D2,L1,V0,M1} I { relation( skol11 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (13892) {G3,W12,D4,L5,V0,M5} R(13889,42);d(49);r(47) { !
% 4.58/4.96 function( skol11 ), ! relation( skol10 ), ! function( skol10 ),
% 4.58/4.96 one_to_one( skol10 ), ! one_to_one( identity_relation( relation_dom(
% 4.58/4.96 skol10 ) ) ) }.
% 4.58/4.96 parent0: (20238) {G1,W12,D4,L5,V0,M5} { ! one_to_one( identity_relation(
% 4.58/4.96 relation_dom( skol10 ) ) ), ! function( skol11 ), ! relation( skol10 ), !
% 4.58/4.96 function( skol10 ), one_to_one( skol10 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 0 ==> 4
% 4.58/4.96 1 ==> 0
% 4.58/4.96 2 ==> 1
% 4.58/4.96 3 ==> 2
% 4.58/4.96 4 ==> 3
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20239) {G1,W10,D4,L4,V0,M4} { ! relation( skol10 ), !
% 4.58/4.96 function( skol10 ), one_to_one( skol10 ), ! one_to_one( identity_relation
% 4.58/4.96 ( relation_dom( skol10 ) ) ) }.
% 4.58/4.96 parent0[0]: (13892) {G3,W12,D4,L5,V0,M5} R(13889,42);d(49);r(47) { !
% 4.58/4.96 function( skol11 ), ! relation( skol10 ), ! function( skol10 ),
% 4.58/4.96 one_to_one( skol10 ), ! one_to_one( identity_relation( relation_dom(
% 4.58/4.96 skol10 ) ) ) }.
% 4.58/4.96 parent1[0]: (48) {G0,W2,D2,L1,V0,M1} I { function( skol11 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20240) {G1,W8,D4,L3,V0,M3} { ! function( skol10 ), one_to_one
% 4.58/4.96 ( skol10 ), ! one_to_one( identity_relation( relation_dom( skol10 ) ) )
% 4.58/4.96 }.
% 4.58/4.96 parent0[0]: (20239) {G1,W10,D4,L4,V0,M4} { ! relation( skol10 ), !
% 4.58/4.96 function( skol10 ), one_to_one( skol10 ), ! one_to_one( identity_relation
% 4.58/4.96 ( relation_dom( skol10 ) ) ) }.
% 4.58/4.96 parent1[0]: (45) {G0,W2,D2,L1,V0,M1} I { relation( skol10 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20241) {G1,W6,D4,L2,V0,M2} { one_to_one( skol10 ), !
% 4.58/4.96 one_to_one( identity_relation( relation_dom( skol10 ) ) ) }.
% 4.58/4.96 parent0[0]: (20240) {G1,W8,D4,L3,V0,M3} { ! function( skol10 ), one_to_one
% 4.58/4.96 ( skol10 ), ! one_to_one( identity_relation( relation_dom( skol10 ) ) )
% 4.58/4.96 }.
% 4.58/4.96 parent1[0]: (46) {G0,W2,D2,L1,V0,M1} I { function( skol10 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20242) {G1,W4,D4,L1,V0,M1} { ! one_to_one( identity_relation
% 4.58/4.96 ( relation_dom( skol10 ) ) ) }.
% 4.58/4.96 parent0[0]: (50) {G0,W2,D2,L1,V0,M1} I { ! one_to_one( skol10 ) }.
% 4.58/4.96 parent1[0]: (20241) {G1,W6,D4,L2,V0,M2} { one_to_one( skol10 ), !
% 4.58/4.96 one_to_one( identity_relation( relation_dom( skol10 ) ) ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 resolution: (20243) {G1,W0,D0,L0,V0,M0} { }.
% 4.58/4.96 parent0[0]: (20242) {G1,W4,D4,L1,V0,M1} { ! one_to_one( identity_relation
% 4.58/4.96 ( relation_dom( skol10 ) ) ) }.
% 4.58/4.96 parent1[0]: (44) {G0,W3,D3,L1,V1,M1} I { one_to_one( identity_relation( X )
% 4.58/4.96 ) }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 substitution1:
% 4.58/4.96 X := relation_dom( skol10 )
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 subsumption: (20020) {G4,W0,D0,L0,V0,M0} S(13892);r(48);r(45);r(46);r(50);r
% 4.58/4.96 (44) { }.
% 4.58/4.96 parent0: (20243) {G1,W0,D0,L0,V0,M0} { }.
% 4.58/4.96 substitution0:
% 4.58/4.96 end
% 4.58/4.96 permutation0:
% 4.58/4.96 end
% 4.58/4.96
% 4.58/4.96 Proof check complete!
% 4.58/4.96
% 4.58/4.96 Memory use:
% 4.58/4.96
% 4.58/4.96 space for terms: 239389
% 4.58/4.96 space for clauses: 1018907
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 clauses generated: 82677
% 4.58/4.96 clauses kept: 20021
% 4.58/4.96 clauses selected: 857
% 4.58/4.96 clauses deleted: 1424
% 4.58/4.96 clauses inuse deleted: 129
% 4.58/4.96
% 4.58/4.96 subsentry: 163161
% 4.58/4.96 literals s-matched: 85621
% 4.58/4.96 literals matched: 83628
% 4.58/4.96 full subsumption: 14126
% 4.58/4.96
% 4.58/4.96 checksum: -136592735
% 4.58/4.96
% 4.58/4.96
% 4.58/4.96 Bliksem ended
%------------------------------------------------------------------------------