%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SET994+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n015.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 22:53:49 EDT 2022
% Result : Theorem 0.72s 1.15s
% Output : Refutation 0.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SET994+1 : TPTP v8.1.0. Released v3.2.0.
% 0.10/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Sat Jul 9 23:38:52 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.72/1.15 *** allocated 10000 integers for termspace/termends
% 0.72/1.15 *** allocated 10000 integers for clauses
% 0.72/1.15 *** allocated 10000 integers for justifications
% 0.72/1.15 Bliksem 1.12
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 Automatic Strategy Selection
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 Clauses:
% 0.72/1.15
% 0.72/1.15 { ! in( X, Y ), ! in( Y, X ) }.
% 0.72/1.15 { ! empty( X ), function( X ) }.
% 0.72/1.15 { ! empty( X ), relation( X ) }.
% 0.72/1.15 { element( skol1( X ), X ) }.
% 0.72/1.15 { empty( empty_set ) }.
% 0.72/1.15 { relation( empty_set ) }.
% 0.72/1.15 { relation_empty_yielding( empty_set ) }.
% 0.72/1.15 { ! empty( powerset( X ) ) }.
% 0.72/1.15 { empty( empty_set ) }.
% 0.72/1.15 { empty( empty_set ) }.
% 0.72/1.15 { relation( empty_set ) }.
% 0.72/1.15 { empty( X ), ! relation( X ), ! empty( relation_dom( X ) ) }.
% 0.72/1.15 { ! empty( X ), empty( relation_dom( X ) ) }.
% 0.72/1.15 { ! empty( X ), relation( relation_dom( X ) ) }.
% 0.72/1.15 { relation( skol2 ) }.
% 0.72/1.15 { function( skol2 ) }.
% 0.72/1.15 { empty( skol3 ) }.
% 0.72/1.15 { relation( skol3 ) }.
% 0.72/1.15 { empty( X ), ! empty( skol4( Y ) ) }.
% 0.72/1.15 { empty( X ), element( skol4( X ), powerset( X ) ) }.
% 0.72/1.15 { empty( skol5 ) }.
% 0.72/1.15 { ! empty( skol6 ) }.
% 0.72/1.15 { relation( skol6 ) }.
% 0.72/1.15 { empty( skol7( Y ) ) }.
% 0.72/1.15 { element( skol7( X ), powerset( X ) ) }.
% 0.72/1.15 { ! empty( skol8 ) }.
% 0.72/1.15 { relation( skol9 ) }.
% 0.72/1.15 { relation_empty_yielding( skol9 ) }.
% 0.72/1.15 { subset( X, X ) }.
% 0.72/1.15 { relation( skol10( Y ) ) }.
% 0.72/1.15 { function( skol10( Y ) ) }.
% 0.72/1.15 { relation_dom( skol10( X ) ) = X }.
% 0.72/1.15 { ! in( Y, X ), apply( skol10( X ), Y ) = n0 }.
% 0.72/1.15 { relation( skol11( Y ) ) }.
% 0.72/1.15 { function( skol11( Y ) ) }.
% 0.72/1.15 { relation_dom( skol11( X ) ) = X }.
% 0.72/1.15 { ! in( Y, X ), apply( skol11( X ), Y ) = n1 }.
% 0.72/1.15 { empty( n0 ) }.
% 0.72/1.15 { ! empty( n1 ) }.
% 0.72/1.15 { ! relation( X ), ! function( X ), ! relation( Y ), ! function( Y ), !
% 0.72/1.15 relation_dom( X ) = skol12, ! relation_dom( Y ) = skol12, X = Y }.
% 0.72/1.15 { ! skol12 = empty_set }.
% 0.72/1.15 { ! in( X, Y ), element( X, Y ) }.
% 0.72/1.15 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 0.72/1.15 { ! element( X, powerset( Y ) ), subset( X, Y ) }.
% 0.72/1.15 { ! subset( X, Y ), element( X, powerset( Y ) ) }.
% 0.72/1.15 { ! in( X, Z ), ! element( Z, powerset( Y ) ), element( X, Y ) }.
% 0.72/1.15 { ! in( X, Y ), ! element( Y, powerset( Z ) ), ! empty( Z ) }.
% 0.72/1.15 { ! empty( X ), X = empty_set }.
% 0.72/1.15 { ! in( X, Y ), ! empty( Y ) }.
% 0.72/1.15 { ! empty( X ), X = Y, ! empty( Y ) }.
% 0.72/1.15
% 0.72/1.15 percentage equality = 0.129870, percentage horn = 0.957447
% 0.72/1.15 This is a problem with some equality
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 Options Used:
% 0.72/1.15
% 0.72/1.15 useres = 1
% 0.72/1.15 useparamod = 1
% 0.72/1.15 useeqrefl = 1
% 0.72/1.15 useeqfact = 1
% 0.72/1.15 usefactor = 1
% 0.72/1.15 usesimpsplitting = 0
% 0.72/1.15 usesimpdemod = 5
% 0.72/1.15 usesimpres = 3
% 0.72/1.15
% 0.72/1.15 resimpinuse = 1000
% 0.72/1.15 resimpclauses = 20000
% 0.72/1.15 substype = eqrewr
% 0.72/1.15 backwardsubs = 1
% 0.72/1.15 selectoldest = 5
% 0.72/1.15
% 0.72/1.15 litorderings [0] = split
% 0.72/1.15 litorderings [1] = extend the termordering, first sorting on arguments
% 0.72/1.15
% 0.72/1.15 termordering = kbo
% 0.72/1.15
% 0.72/1.15 litapriori = 0
% 0.72/1.15 termapriori = 1
% 0.72/1.15 litaposteriori = 0
% 0.72/1.15 termaposteriori = 0
% 0.72/1.15 demodaposteriori = 0
% 0.72/1.15 ordereqreflfact = 0
% 0.72/1.15
% 0.72/1.15 litselect = negord
% 0.72/1.15
% 0.72/1.15 maxweight = 15
% 0.72/1.15 maxdepth = 30000
% 0.72/1.15 maxlength = 115
% 0.72/1.15 maxnrvars = 195
% 0.72/1.15 excuselevel = 1
% 0.72/1.15 increasemaxweight = 1
% 0.72/1.15
% 0.72/1.15 maxselected = 10000000
% 0.72/1.15 maxnrclauses = 10000000
% 0.72/1.15
% 0.72/1.15 showgenerated = 0
% 0.72/1.15 showkept = 0
% 0.72/1.15 showselected = 0
% 0.72/1.15 showdeleted = 0
% 0.72/1.15 showresimp = 1
% 0.72/1.15 showstatus = 2000
% 0.72/1.15
% 0.72/1.15 prologoutput = 0
% 0.72/1.15 nrgoals = 5000000
% 0.72/1.15 totalproof = 1
% 0.72/1.15
% 0.72/1.15 Symbols occurring in the translation:
% 0.72/1.15
% 0.72/1.15 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.72/1.15 . [1, 2] (w:1, o:35, a:1, s:1, b:0),
% 0.72/1.15 ! [4, 1] (w:0, o:19, a:1, s:1, b:0),
% 0.72/1.15 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.15 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.15 in [37, 2] (w:1, o:59, a:1, s:1, b:0),
% 0.72/1.15 empty [38, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.72/1.15 function [39, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.72/1.15 relation [40, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.72/1.15 element [41, 2] (w:1, o:60, a:1, s:1, b:0),
% 0.72/1.15 empty_set [42, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.72/1.15 relation_empty_yielding [43, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.72/1.15 powerset [44, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.72/1.15 relation_dom [45, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.72/1.15 subset [46, 2] (w:1, o:61, a:1, s:1, b:0),
% 0.72/1.15 apply [48, 2] (w:1, o:62, a:1, s:1, b:0),
% 0.72/1.15 n0 [49, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.72/1.15 n1 [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.72/1.15 skol1 [51, 1] (w:1, o:30, a:1, s:1, b:1),
% 0.72/1.15 skol2 [52, 0] (w:1, o:13, a:1, s:1, b:1),
% 0.72/1.15 skol3 [53, 0] (w:1, o:14, a:1, s:1, b:1),
% 0.72/1.15 skol4 [54, 1] (w:1, o:31, a:1, s:1, b:1),
% 0.72/1.15 skol5 [55, 0] (w:1, o:15, a:1, s:1, b:1),
% 0.72/1.15 skol6 [56, 0] (w:1, o:16, a:1, s:1, b:1),
% 0.72/1.15 skol7 [57, 1] (w:1, o:32, a:1, s:1, b:1),
% 0.72/1.15 skol8 [58, 0] (w:1, o:17, a:1, s:1, b:1),
% 0.72/1.15 skol9 [59, 0] (w:1, o:18, a:1, s:1, b:1),
% 0.72/1.15 skol10 [60, 1] (w:1, o:33, a:1, s:1, b:1),
% 0.72/1.15 skol11 [61, 1] (w:1, o:34, a:1, s:1, b:1),
% 0.72/1.15 skol12 [62, 0] (w:1, o:12, a:1, s:1, b:1).
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 Starting Search:
% 0.72/1.15
% 0.72/1.15 *** allocated 15000 integers for clauses
% 0.72/1.15 *** allocated 22500 integers for clauses
% 0.72/1.15 *** allocated 33750 integers for clauses
% 0.72/1.15 *** allocated 50625 integers for clauses
% 0.72/1.15 *** allocated 75937 integers for clauses
% 0.72/1.15 Resimplifying inuse:
% 0.72/1.15 Done
% 0.72/1.15
% 0.72/1.15 *** allocated 15000 integers for termspace/termends
% 0.72/1.15
% 0.72/1.15 Bliksems!, er is een bewijs:
% 0.72/1.15 % SZS status Theorem
% 0.72/1.15 % SZS output start Refutation
% 0.72/1.15
% 0.72/1.15 (3) {G0,W4,D3,L1,V1,M1} I { element( skol1( X ), X ) }.
% 0.72/1.15 (4) {G0,W2,D2,L1,V0,M1} I { empty( empty_set ) }.
% 0.72/1.15 (26) {G0,W3,D3,L1,V1,M1} I { relation( skol10( Y ) ) }.
% 0.72/1.15 (27) {G0,W3,D3,L1,V1,M1} I { function( skol10( Y ) ) }.
% 0.72/1.15 (28) {G0,W5,D4,L1,V1,M1} I { relation_dom( skol10( X ) ) ==> X }.
% 0.72/1.15 (29) {G0,W9,D4,L2,V2,M2} I { ! in( Y, X ), apply( skol10( X ), Y ) ==> n0
% 0.72/1.15 }.
% 0.72/1.15 (30) {G0,W3,D3,L1,V1,M1} I { relation( skol11( Y ) ) }.
% 0.72/1.15 (31) {G0,W3,D3,L1,V1,M1} I { function( skol11( Y ) ) }.
% 0.72/1.15 (32) {G0,W5,D4,L1,V1,M1} I { relation_dom( skol11( X ) ) ==> X }.
% 0.72/1.15 (33) {G0,W9,D4,L2,V2,M2} I { ! in( Y, X ), apply( skol11( X ), Y ) ==> n1
% 0.72/1.15 }.
% 0.72/1.15 (34) {G0,W2,D2,L1,V0,M1} I { empty( n0 ) }.
% 0.72/1.15 (35) {G0,W2,D2,L1,V0,M1} I { ! empty( n1 ) }.
% 0.72/1.15 (36) {G0,W19,D3,L7,V2,M7} I { ! relation( X ), ! function( X ), ! relation
% 0.72/1.15 ( Y ), ! function( Y ), ! relation_dom( X ) ==> skol12, ! relation_dom( Y
% 0.72/1.15 ) ==> skol12, X = Y }.
% 0.72/1.15 (37) {G0,W3,D2,L1,V0,M1} I { ! skol12 ==> empty_set }.
% 0.72/1.15 (39) {G0,W8,D2,L3,V2,M3} I { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 0.72/1.15 (44) {G0,W5,D2,L2,V1,M2} I { ! empty( X ), X = empty_set }.
% 0.72/1.15 (145) {G1,W15,D3,L5,V2,M5} R(36,26);d(28);r(27) { ! relation( Y ), !
% 0.72/1.15 function( Y ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y, ! X =
% 0.72/1.15 skol12 }.
% 0.72/1.15 (196) {G1,W3,D2,L1,V0,M1} R(44,34) { n0 ==> empty_set }.
% 0.72/1.15 (202) {G1,W2,D2,L1,V0,M1} P(44,37);q { ! empty( skol12 ) }.
% 0.72/1.15 (207) {G2,W6,D2,L2,V1,M2} R(39,202) { ! element( X, skol12 ), in( X, skol12
% 0.72/1.15 ) }.
% 0.72/1.15 (1000) {G3,W4,D3,L1,V0,M1} R(207,3) { in( skol1( skol12 ), skol12 ) }.
% 0.72/1.15 (1002) {G2,W9,D4,L2,V2,M2} S(29);d(196) { ! in( Y, X ), apply( skol10( X )
% 0.72/1.15 , Y ) ==> empty_set }.
% 0.72/1.15 (1061) {G2,W11,D3,L3,V2,M3} R(145,30);d(32);r(31) { skol10( Y ) = skol11( X
% 0.72/1.15 ), ! Y = skol12, ! X = skol12 }.
% 0.72/1.15 (1136) {G3,W8,D3,L2,V1,M2} Q(1061) { skol10( X ) = skol11( skol12 ), ! X =
% 0.72/1.15 skol12 }.
% 0.72/1.15 (1137) {G4,W5,D3,L1,V0,M1} Q(1136) { skol11( skol12 ) ==> skol10( skol12 )
% 0.72/1.15 }.
% 0.72/1.15 (1145) {G5,W6,D2,L2,V1,M2} P(1137,33);d(1002) { ! in( X, skol12 ), n1 ==>
% 0.72/1.15 empty_set }.
% 0.72/1.15 (1154) {G6,W3,D2,L1,V1,M1} P(1145,35);r(4) { ! in( X, skol12 ) }.
% 0.72/1.15 (1155) {G7,W0,D0,L0,V0,M0} R(1154,1000) { }.
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 % SZS output end Refutation
% 0.72/1.15 found a proof!
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 Unprocessed initial clauses:
% 0.72/1.15
% 0.72/1.15 (1157) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 0.72/1.15 (1158) {G0,W4,D2,L2,V1,M2} { ! empty( X ), function( X ) }.
% 0.72/1.15 (1159) {G0,W4,D2,L2,V1,M2} { ! empty( X ), relation( X ) }.
% 0.72/1.15 (1160) {G0,W4,D3,L1,V1,M1} { element( skol1( X ), X ) }.
% 0.72/1.15 (1161) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.72/1.15 (1162) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 0.72/1.15 (1163) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( empty_set ) }.
% 0.72/1.15 (1164) {G0,W3,D3,L1,V1,M1} { ! empty( powerset( X ) ) }.
% 0.72/1.15 (1165) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.72/1.15 (1166) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.72/1.15 (1167) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 0.72/1.15 (1168) {G0,W7,D3,L3,V1,M3} { empty( X ), ! relation( X ), ! empty(
% 0.72/1.15 relation_dom( X ) ) }.
% 0.72/1.15 (1169) {G0,W5,D3,L2,V1,M2} { ! empty( X ), empty( relation_dom( X ) ) }.
% 0.72/1.15 (1170) {G0,W5,D3,L2,V1,M2} { ! empty( X ), relation( relation_dom( X ) )
% 0.72/1.15 }.
% 0.72/1.15 (1171) {G0,W2,D2,L1,V0,M1} { relation( skol2 ) }.
% 0.72/1.15 (1172) {G0,W2,D2,L1,V0,M1} { function( skol2 ) }.
% 0.72/1.15 (1173) {G0,W2,D2,L1,V0,M1} { empty( skol3 ) }.
% 0.72/1.15 (1174) {G0,W2,D2,L1,V0,M1} { relation( skol3 ) }.
% 0.72/1.15 (1175) {G0,W5,D3,L2,V2,M2} { empty( X ), ! empty( skol4( Y ) ) }.
% 0.72/1.15 (1176) {G0,W7,D3,L2,V1,M2} { empty( X ), element( skol4( X ), powerset( X
% 0.72/1.15 ) ) }.
% 0.72/1.15 (1177) {G0,W2,D2,L1,V0,M1} { empty( skol5 ) }.
% 0.72/1.15 (1178) {G0,W2,D2,L1,V0,M1} { ! empty( skol6 ) }.
% 0.72/1.15 (1179) {G0,W2,D2,L1,V0,M1} { relation( skol6 ) }.
% 0.72/1.15 (1180) {G0,W3,D3,L1,V1,M1} { empty( skol7( Y ) ) }.
% 0.72/1.15 (1181) {G0,W5,D3,L1,V1,M1} { element( skol7( X ), powerset( X ) ) }.
% 0.72/1.15 (1182) {G0,W2,D2,L1,V0,M1} { ! empty( skol8 ) }.
% 0.72/1.15 (1183) {G0,W2,D2,L1,V0,M1} { relation( skol9 ) }.
% 0.72/1.15 (1184) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol9 ) }.
% 0.72/1.15 (1185) {G0,W3,D2,L1,V1,M1} { subset( X, X ) }.
% 0.72/1.15 (1186) {G0,W3,D3,L1,V1,M1} { relation( skol10( Y ) ) }.
% 0.72/1.15 (1187) {G0,W3,D3,L1,V1,M1} { function( skol10( Y ) ) }.
% 0.72/1.15 (1188) {G0,W5,D4,L1,V1,M1} { relation_dom( skol10( X ) ) = X }.
% 0.72/1.15 (1189) {G0,W9,D4,L2,V2,M2} { ! in( Y, X ), apply( skol10( X ), Y ) = n0
% 0.72/1.15 }.
% 0.72/1.15 (1190) {G0,W3,D3,L1,V1,M1} { relation( skol11( Y ) ) }.
% 0.72/1.15 (1191) {G0,W3,D3,L1,V1,M1} { function( skol11( Y ) ) }.
% 0.72/1.15 (1192) {G0,W5,D4,L1,V1,M1} { relation_dom( skol11( X ) ) = X }.
% 0.72/1.15 (1193) {G0,W9,D4,L2,V2,M2} { ! in( Y, X ), apply( skol11( X ), Y ) = n1
% 0.72/1.15 }.
% 0.72/1.15 (1194) {G0,W2,D2,L1,V0,M1} { empty( n0 ) }.
% 0.72/1.15 (1195) {G0,W2,D2,L1,V0,M1} { ! empty( n1 ) }.
% 0.72/1.15 (1196) {G0,W19,D3,L7,V2,M7} { ! relation( X ), ! function( X ), ! relation
% 0.72/1.15 ( Y ), ! function( Y ), ! relation_dom( X ) = skol12, ! relation_dom( Y )
% 0.72/1.15 = skol12, X = Y }.
% 0.72/1.15 (1197) {G0,W3,D2,L1,V0,M1} { ! skol12 = empty_set }.
% 0.72/1.15 (1198) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 0.72/1.15 (1199) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 0.72/1.15 (1200) {G0,W7,D3,L2,V2,M2} { ! element( X, powerset( Y ) ), subset( X, Y )
% 0.72/1.15 }.
% 0.72/1.15 (1201) {G0,W7,D3,L2,V2,M2} { ! subset( X, Y ), element( X, powerset( Y ) )
% 0.72/1.15 }.
% 0.72/1.15 (1202) {G0,W10,D3,L3,V3,M3} { ! in( X, Z ), ! element( Z, powerset( Y ) )
% 0.72/1.15 , element( X, Y ) }.
% 0.72/1.15 (1203) {G0,W9,D3,L3,V3,M3} { ! in( X, Y ), ! element( Y, powerset( Z ) ),
% 0.72/1.15 ! empty( Z ) }.
% 0.72/1.15 (1204) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 0.72/1.15 (1205) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 0.72/1.15 (1206) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 Total Proof:
% 0.72/1.15
% 0.72/1.15 subsumption: (3) {G0,W4,D3,L1,V1,M1} I { element( skol1( X ), X ) }.
% 0.72/1.15 parent0: (1160) {G0,W4,D3,L1,V1,M1} { element( skol1( X ), X ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (4) {G0,W2,D2,L1,V0,M1} I { empty( empty_set ) }.
% 0.72/1.15 parent0: (1161) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (26) {G0,W3,D3,L1,V1,M1} I { relation( skol10( Y ) ) }.
% 0.72/1.15 parent0: (1186) {G0,W3,D3,L1,V1,M1} { relation( skol10( Y ) ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := Z
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (27) {G0,W3,D3,L1,V1,M1} I { function( skol10( Y ) ) }.
% 0.72/1.15 parent0: (1187) {G0,W3,D3,L1,V1,M1} { function( skol10( Y ) ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := Z
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (28) {G0,W5,D4,L1,V1,M1} I { relation_dom( skol10( X ) ) ==> X
% 0.72/1.15 }.
% 0.72/1.15 parent0: (1188) {G0,W5,D4,L1,V1,M1} { relation_dom( skol10( X ) ) = X }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (29) {G0,W9,D4,L2,V2,M2} I { ! in( Y, X ), apply( skol10( X )
% 0.72/1.15 , Y ) ==> n0 }.
% 0.72/1.15 parent0: (1189) {G0,W9,D4,L2,V2,M2} { ! in( Y, X ), apply( skol10( X ), Y
% 0.72/1.15 ) = n0 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 1 ==> 1
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (30) {G0,W3,D3,L1,V1,M1} I { relation( skol11( Y ) ) }.
% 0.72/1.15 parent0: (1190) {G0,W3,D3,L1,V1,M1} { relation( skol11( Y ) ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := Z
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (31) {G0,W3,D3,L1,V1,M1} I { function( skol11( Y ) ) }.
% 0.72/1.15 parent0: (1191) {G0,W3,D3,L1,V1,M1} { function( skol11( Y ) ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := Z
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (32) {G0,W5,D4,L1,V1,M1} I { relation_dom( skol11( X ) ) ==> X
% 0.72/1.15 }.
% 0.72/1.15 parent0: (1192) {G0,W5,D4,L1,V1,M1} { relation_dom( skol11( X ) ) = X }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (33) {G0,W9,D4,L2,V2,M2} I { ! in( Y, X ), apply( skol11( X )
% 0.72/1.15 , Y ) ==> n1 }.
% 0.72/1.15 parent0: (1193) {G0,W9,D4,L2,V2,M2} { ! in( Y, X ), apply( skol11( X ), Y
% 0.72/1.15 ) = n1 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 1 ==> 1
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (34) {G0,W2,D2,L1,V0,M1} I { empty( n0 ) }.
% 0.72/1.15 parent0: (1194) {G0,W2,D2,L1,V0,M1} { empty( n0 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (35) {G0,W2,D2,L1,V0,M1} I { ! empty( n1 ) }.
% 0.72/1.15 parent0: (1195) {G0,W2,D2,L1,V0,M1} { ! empty( n1 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (36) {G0,W19,D3,L7,V2,M7} I { ! relation( X ), ! function( X )
% 0.72/1.15 , ! relation( Y ), ! function( Y ), ! relation_dom( X ) ==> skol12, !
% 0.72/1.15 relation_dom( Y ) ==> skol12, X = Y }.
% 0.72/1.15 parent0: (1196) {G0,W19,D3,L7,V2,M7} { ! relation( X ), ! function( X ), !
% 0.72/1.15 relation( Y ), ! function( Y ), ! relation_dom( X ) = skol12, !
% 0.72/1.15 relation_dom( Y ) = skol12, X = Y }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 1 ==> 1
% 0.72/1.15 2 ==> 2
% 0.72/1.15 3 ==> 3
% 0.72/1.15 4 ==> 4
% 0.72/1.15 5 ==> 5
% 0.72/1.15 6 ==> 6
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (37) {G0,W3,D2,L1,V0,M1} I { ! skol12 ==> empty_set }.
% 0.72/1.15 parent0: (1197) {G0,W3,D2,L1,V0,M1} { ! skol12 = empty_set }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (39) {G0,W8,D2,L3,V2,M3} I { ! element( X, Y ), empty( Y ), in
% 0.72/1.15 ( X, Y ) }.
% 0.72/1.15 parent0: (1199) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X
% 0.72/1.15 , Y ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 1 ==> 1
% 0.72/1.15 2 ==> 2
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (44) {G0,W5,D2,L2,V1,M2} I { ! empty( X ), X = empty_set }.
% 0.72/1.15 parent0: (1204) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 1 ==> 1
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1305) {G0,W19,D3,L7,V2,M7} { ! skol12 ==> relation_dom( X ), !
% 0.72/1.15 relation( X ), ! function( X ), ! relation( Y ), ! function( Y ), !
% 0.72/1.15 relation_dom( Y ) ==> skol12, X = Y }.
% 0.72/1.15 parent0[4]: (36) {G0,W19,D3,L7,V2,M7} I { ! relation( X ), ! function( X )
% 0.72/1.15 , ! relation( Y ), ! function( Y ), ! relation_dom( X ) ==> skol12, !
% 0.72/1.15 relation_dom( Y ) ==> skol12, X = Y }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1309) {G1,W20,D4,L6,V2,M6} { ! skol12 ==> relation_dom(
% 0.72/1.15 skol10( X ) ), ! function( skol10( X ) ), ! relation( Y ), ! function( Y
% 0.72/1.15 ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y }.
% 0.72/1.15 parent0[1]: (1305) {G0,W19,D3,L7,V2,M7} { ! skol12 ==> relation_dom( X ),
% 0.72/1.15 ! relation( X ), ! function( X ), ! relation( Y ), ! function( Y ), !
% 0.72/1.15 relation_dom( Y ) ==> skol12, X = Y }.
% 0.72/1.15 parent1[0]: (26) {G0,W3,D3,L1,V1,M1} I { relation( skol10( Y ) ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := skol10( X )
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := Z
% 0.72/1.15 Y := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 paramod: (1312) {G1,W18,D3,L6,V2,M6} { ! skol12 ==> X, ! function( skol10
% 0.72/1.15 ( X ) ), ! relation( Y ), ! function( Y ), ! relation_dom( Y ) ==> skol12
% 0.72/1.15 , skol10( X ) = Y }.
% 0.72/1.15 parent0[0]: (28) {G0,W5,D4,L1,V1,M1} I { relation_dom( skol10( X ) ) ==> X
% 0.72/1.15 }.
% 0.72/1.15 parent1[0; 3]: (1309) {G1,W20,D4,L6,V2,M6} { ! skol12 ==> relation_dom(
% 0.72/1.15 skol10( X ) ), ! function( skol10( X ) ), ! relation( Y ), ! function( Y
% 0.72/1.15 ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1318) {G1,W15,D3,L5,V2,M5} { ! skol12 ==> X, ! relation( Y )
% 0.72/1.15 , ! function( Y ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y }.
% 0.72/1.15 parent0[1]: (1312) {G1,W18,D3,L6,V2,M6} { ! skol12 ==> X, ! function(
% 0.72/1.15 skol10( X ) ), ! relation( Y ), ! function( Y ), ! relation_dom( Y ) ==>
% 0.72/1.15 skol12, skol10( X ) = Y }.
% 0.72/1.15 parent1[0]: (27) {G0,W3,D3,L1,V1,M1} I { function( skol10( Y ) ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := Z
% 0.72/1.15 Y := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1319) {G1,W15,D3,L5,V2,M5} { ! X ==> skol12, ! relation( Y ), !
% 0.72/1.15 function( Y ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y }.
% 0.72/1.15 parent0[0]: (1318) {G1,W15,D3,L5,V2,M5} { ! skol12 ==> X, ! relation( Y )
% 0.72/1.15 , ! function( Y ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (145) {G1,W15,D3,L5,V2,M5} R(36,26);d(28);r(27) { ! relation(
% 0.72/1.15 Y ), ! function( Y ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y, !
% 0.72/1.15 X = skol12 }.
% 0.72/1.15 parent0: (1319) {G1,W15,D3,L5,V2,M5} { ! X ==> skol12, ! relation( Y ), !
% 0.72/1.15 function( Y ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 4
% 0.72/1.15 1 ==> 0
% 0.72/1.15 2 ==> 1
% 0.72/1.15 3 ==> 2
% 0.72/1.15 4 ==> 3
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1330) {G0,W5,D2,L2,V1,M2} { empty_set = X, ! empty( X ) }.
% 0.72/1.15 parent0[1]: (44) {G0,W5,D2,L2,V1,M2} I { ! empty( X ), X = empty_set }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1331) {G1,W3,D2,L1,V0,M1} { empty_set = n0 }.
% 0.72/1.15 parent0[1]: (1330) {G0,W5,D2,L2,V1,M2} { empty_set = X, ! empty( X ) }.
% 0.72/1.15 parent1[0]: (34) {G0,W2,D2,L1,V0,M1} I { empty( n0 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := n0
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1332) {G1,W3,D2,L1,V0,M1} { n0 = empty_set }.
% 0.72/1.15 parent0[0]: (1331) {G1,W3,D2,L1,V0,M1} { empty_set = n0 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (196) {G1,W3,D2,L1,V0,M1} R(44,34) { n0 ==> empty_set }.
% 0.72/1.15 parent0: (1332) {G1,W3,D2,L1,V0,M1} { n0 = empty_set }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1334) {G0,W3,D2,L1,V0,M1} { ! empty_set ==> skol12 }.
% 0.72/1.15 parent0[0]: (37) {G0,W3,D2,L1,V0,M1} I { ! skol12 ==> empty_set }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 paramod: (1338) {G1,W5,D2,L2,V0,M2} { ! empty_set ==> empty_set, ! empty(
% 0.72/1.15 skol12 ) }.
% 0.72/1.15 parent0[1]: (44) {G0,W5,D2,L2,V1,M2} I { ! empty( X ), X = empty_set }.
% 0.72/1.15 parent1[0; 3]: (1334) {G0,W3,D2,L1,V0,M1} { ! empty_set ==> skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := skol12
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqrefl: (1349) {G0,W2,D2,L1,V0,M1} { ! empty( skol12 ) }.
% 0.72/1.15 parent0[0]: (1338) {G1,W5,D2,L2,V0,M2} { ! empty_set ==> empty_set, !
% 0.72/1.15 empty( skol12 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (202) {G1,W2,D2,L1,V0,M1} P(44,37);q { ! empty( skol12 ) }.
% 0.72/1.15 parent0: (1349) {G0,W2,D2,L1,V0,M1} { ! empty( skol12 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1350) {G1,W6,D2,L2,V1,M2} { ! element( X, skol12 ), in( X,
% 0.72/1.15 skol12 ) }.
% 0.72/1.15 parent0[0]: (202) {G1,W2,D2,L1,V0,M1} P(44,37);q { ! empty( skol12 ) }.
% 0.72/1.15 parent1[1]: (39) {G0,W8,D2,L3,V2,M3} I { ! element( X, Y ), empty( Y ), in
% 0.72/1.15 ( X, Y ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := X
% 0.72/1.15 Y := skol12
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (207) {G2,W6,D2,L2,V1,M2} R(39,202) { ! element( X, skol12 ),
% 0.72/1.15 in( X, skol12 ) }.
% 0.72/1.15 parent0: (1350) {G1,W6,D2,L2,V1,M2} { ! element( X, skol12 ), in( X,
% 0.72/1.15 skol12 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 1 ==> 1
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1351) {G1,W4,D3,L1,V0,M1} { in( skol1( skol12 ), skol12 ) }.
% 0.72/1.15 parent0[0]: (207) {G2,W6,D2,L2,V1,M2} R(39,202) { ! element( X, skol12 ),
% 0.72/1.15 in( X, skol12 ) }.
% 0.72/1.15 parent1[0]: (3) {G0,W4,D3,L1,V1,M1} I { element( skol1( X ), X ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := skol1( skol12 )
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := skol12
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (1000) {G3,W4,D3,L1,V0,M1} R(207,3) { in( skol1( skol12 ),
% 0.72/1.15 skol12 ) }.
% 0.72/1.15 parent0: (1351) {G1,W4,D3,L1,V0,M1} { in( skol1( skol12 ), skol12 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 paramod: (1354) {G1,W9,D4,L2,V2,M2} { apply( skol10( X ), Y ) ==>
% 0.72/1.15 empty_set, ! in( Y, X ) }.
% 0.72/1.15 parent0[0]: (196) {G1,W3,D2,L1,V0,M1} R(44,34) { n0 ==> empty_set }.
% 0.72/1.15 parent1[1; 5]: (29) {G0,W9,D4,L2,V2,M2} I { ! in( Y, X ), apply( skol10( X
% 0.72/1.15 ), Y ) ==> n0 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (1002) {G2,W9,D4,L2,V2,M2} S(29);d(196) { ! in( Y, X ), apply
% 0.72/1.15 ( skol10( X ), Y ) ==> empty_set }.
% 0.72/1.15 parent0: (1354) {G1,W9,D4,L2,V2,M2} { apply( skol10( X ), Y ) ==>
% 0.72/1.15 empty_set, ! in( Y, X ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 1
% 0.72/1.15 1 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1356) {G1,W15,D3,L5,V2,M5} { ! skol12 ==> relation_dom( X ), !
% 0.72/1.15 relation( X ), ! function( X ), skol10( Y ) = X, ! Y = skol12 }.
% 0.72/1.15 parent0[2]: (145) {G1,W15,D3,L5,V2,M5} R(36,26);d(28);r(27) { ! relation( Y
% 0.72/1.15 ), ! function( Y ), ! relation_dom( Y ) ==> skol12, skol10( X ) = Y, ! X
% 0.72/1.15 = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := Y
% 0.72/1.15 Y := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1364) {G1,W16,D4,L4,V2,M4} { ! skol12 ==> relation_dom(
% 0.72/1.15 skol11( X ) ), ! function( skol11( X ) ), skol10( Y ) = skol11( X ), ! Y
% 0.72/1.15 = skol12 }.
% 0.72/1.15 parent0[1]: (1356) {G1,W15,D3,L5,V2,M5} { ! skol12 ==> relation_dom( X ),
% 0.72/1.15 ! relation( X ), ! function( X ), skol10( Y ) = X, ! Y = skol12 }.
% 0.72/1.15 parent1[0]: (30) {G0,W3,D3,L1,V1,M1} I { relation( skol11( Y ) ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := skol11( X )
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := Z
% 0.72/1.15 Y := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 paramod: (1365) {G1,W14,D3,L4,V2,M4} { ! skol12 ==> X, ! function( skol11
% 0.72/1.15 ( X ) ), skol10( Y ) = skol11( X ), ! Y = skol12 }.
% 0.72/1.15 parent0[0]: (32) {G0,W5,D4,L1,V1,M1} I { relation_dom( skol11( X ) ) ==> X
% 0.72/1.15 }.
% 0.72/1.15 parent1[0; 3]: (1364) {G1,W16,D4,L4,V2,M4} { ! skol12 ==> relation_dom(
% 0.72/1.15 skol11( X ) ), ! function( skol11( X ) ), skol10( Y ) = skol11( X ), ! Y
% 0.72/1.15 = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1369) {G1,W11,D3,L3,V2,M3} { ! skol12 ==> X, skol10( Y ) =
% 0.72/1.15 skol11( X ), ! Y = skol12 }.
% 0.72/1.15 parent0[1]: (1365) {G1,W14,D3,L4,V2,M4} { ! skol12 ==> X, ! function(
% 0.72/1.15 skol11( X ) ), skol10( Y ) = skol11( X ), ! Y = skol12 }.
% 0.72/1.15 parent1[0]: (31) {G0,W3,D3,L1,V1,M1} I { function( skol11( Y ) ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := Z
% 0.72/1.15 Y := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1370) {G1,W11,D3,L3,V2,M3} { ! X ==> skol12, skol10( Y ) = skol11
% 0.72/1.15 ( X ), ! Y = skol12 }.
% 0.72/1.15 parent0[0]: (1369) {G1,W11,D3,L3,V2,M3} { ! skol12 ==> X, skol10( Y ) =
% 0.72/1.15 skol11( X ), ! Y = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (1061) {G2,W11,D3,L3,V2,M3} R(145,30);d(32);r(31) { skol10( Y
% 0.72/1.15 ) = skol11( X ), ! Y = skol12, ! X = skol12 }.
% 0.72/1.15 parent0: (1370) {G1,W11,D3,L3,V2,M3} { ! X ==> skol12, skol10( Y ) =
% 0.72/1.15 skol11( X ), ! Y = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 2
% 0.72/1.15 1 ==> 0
% 0.72/1.15 2 ==> 1
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1382) {G2,W11,D3,L3,V2,M3} { skol11( Y ) = skol10( X ), ! X =
% 0.72/1.15 skol12, ! Y = skol12 }.
% 0.72/1.15 parent0[0]: (1061) {G2,W11,D3,L3,V2,M3} R(145,30);d(32);r(31) { skol10( Y )
% 0.72/1.15 = skol11( X ), ! Y = skol12, ! X = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := Y
% 0.72/1.15 Y := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqrefl: (1390) {G0,W8,D3,L2,V1,M2} { skol11( skol12 ) = skol10( X ), ! X =
% 0.72/1.15 skol12 }.
% 0.72/1.15 parent0[2]: (1382) {G2,W11,D3,L3,V2,M3} { skol11( Y ) = skol10( X ), ! X =
% 0.72/1.15 skol12, ! Y = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := skol12
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1391) {G0,W8,D3,L2,V1,M2} { skol10( X ) = skol11( skol12 ), ! X =
% 0.72/1.15 skol12 }.
% 0.72/1.15 parent0[0]: (1390) {G0,W8,D3,L2,V1,M2} { skol11( skol12 ) = skol10( X ), !
% 0.72/1.15 X = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (1136) {G3,W8,D3,L2,V1,M2} Q(1061) { skol10( X ) = skol11(
% 0.72/1.15 skol12 ), ! X = skol12 }.
% 0.72/1.15 parent0: (1391) {G0,W8,D3,L2,V1,M2} { skol10( X ) = skol11( skol12 ), ! X
% 0.72/1.15 = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 1 ==> 1
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1397) {G3,W8,D3,L2,V1,M2} { skol11( skol12 ) = skol10( X ), ! X =
% 0.72/1.15 skol12 }.
% 0.72/1.15 parent0[0]: (1136) {G3,W8,D3,L2,V1,M2} Q(1061) { skol10( X ) = skol11(
% 0.72/1.15 skol12 ), ! X = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqrefl: (1400) {G0,W5,D3,L1,V0,M1} { skol11( skol12 ) = skol10( skol12 )
% 0.72/1.15 }.
% 0.72/1.15 parent0[1]: (1397) {G3,W8,D3,L2,V1,M2} { skol11( skol12 ) = skol10( X ), !
% 0.72/1.15 X = skol12 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := skol12
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (1137) {G4,W5,D3,L1,V0,M1} Q(1136) { skol11( skol12 ) ==>
% 0.72/1.15 skol10( skol12 ) }.
% 0.72/1.15 parent0: (1400) {G0,W5,D3,L1,V0,M1} { skol11( skol12 ) = skol10( skol12 )
% 0.72/1.15 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 eqswap: (1403) {G0,W9,D4,L2,V2,M2} { n1 ==> apply( skol11( X ), Y ), ! in
% 0.72/1.15 ( Y, X ) }.
% 0.72/1.15 parent0[1]: (33) {G0,W9,D4,L2,V2,M2} I { ! in( Y, X ), apply( skol11( X ),
% 0.72/1.15 Y ) ==> n1 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 Y := Y
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 paramod: (1405) {G1,W9,D4,L2,V1,M2} { n1 ==> apply( skol10( skol12 ), X )
% 0.72/1.15 , ! in( X, skol12 ) }.
% 0.72/1.15 parent0[0]: (1137) {G4,W5,D3,L1,V0,M1} Q(1136) { skol11( skol12 ) ==>
% 0.72/1.15 skol10( skol12 ) }.
% 0.72/1.15 parent1[0; 3]: (1403) {G0,W9,D4,L2,V2,M2} { n1 ==> apply( skol11( X ), Y )
% 0.72/1.15 , ! in( Y, X ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := skol12
% 0.72/1.15 Y := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 paramod: (1406) {G2,W9,D2,L3,V1,M3} { n1 ==> empty_set, ! in( X, skol12 )
% 0.72/1.15 , ! in( X, skol12 ) }.
% 0.72/1.15 parent0[1]: (1002) {G2,W9,D4,L2,V2,M2} S(29);d(196) { ! in( Y, X ), apply(
% 0.72/1.15 skol10( X ), Y ) ==> empty_set }.
% 0.72/1.15 parent1[0; 2]: (1405) {G1,W9,D4,L2,V1,M2} { n1 ==> apply( skol10( skol12 )
% 0.72/1.15 , X ), ! in( X, skol12 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := skol12
% 0.72/1.15 Y := X
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 factor: (1409) {G2,W6,D2,L2,V1,M2} { n1 ==> empty_set, ! in( X, skol12 )
% 0.72/1.15 }.
% 0.72/1.15 parent0[1, 2]: (1406) {G2,W9,D2,L3,V1,M3} { n1 ==> empty_set, ! in( X,
% 0.72/1.15 skol12 ), ! in( X, skol12 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (1145) {G5,W6,D2,L2,V1,M2} P(1137,33);d(1002) { ! in( X,
% 0.72/1.15 skol12 ), n1 ==> empty_set }.
% 0.72/1.15 parent0: (1409) {G2,W6,D2,L2,V1,M2} { n1 ==> empty_set, ! in( X, skol12 )
% 0.72/1.15 }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 1
% 0.72/1.15 1 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 paramod: (1411) {G1,W5,D2,L2,V1,M2} { ! empty( empty_set ), ! in( X,
% 0.72/1.15 skol12 ) }.
% 0.72/1.15 parent0[1]: (1145) {G5,W6,D2,L2,V1,M2} P(1137,33);d(1002) { ! in( X, skol12
% 0.72/1.15 ), n1 ==> empty_set }.
% 0.72/1.15 parent1[0; 2]: (35) {G0,W2,D2,L1,V0,M1} I { ! empty( n1 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1412) {G1,W3,D2,L1,V1,M1} { ! in( X, skol12 ) }.
% 0.72/1.15 parent0[0]: (1411) {G1,W5,D2,L2,V1,M2} { ! empty( empty_set ), ! in( X,
% 0.72/1.15 skol12 ) }.
% 0.72/1.15 parent1[0]: (4) {G0,W2,D2,L1,V0,M1} I { empty( empty_set ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (1154) {G6,W3,D2,L1,V1,M1} P(1145,35);r(4) { ! in( X, skol12 )
% 0.72/1.15 }.
% 0.72/1.15 parent0: (1412) {G1,W3,D2,L1,V1,M1} { ! in( X, skol12 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := X
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 0 ==> 0
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 resolution: (1413) {G4,W0,D0,L0,V0,M0} { }.
% 0.72/1.15 parent0[0]: (1154) {G6,W3,D2,L1,V1,M1} P(1145,35);r(4) { ! in( X, skol12 )
% 0.72/1.15 }.
% 0.72/1.15 parent1[0]: (1000) {G3,W4,D3,L1,V0,M1} R(207,3) { in( skol1( skol12 ),
% 0.72/1.15 skol12 ) }.
% 0.72/1.15 substitution0:
% 0.72/1.15 X := skol1( skol12 )
% 0.72/1.15 end
% 0.72/1.15 substitution1:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 subsumption: (1155) {G7,W0,D0,L0,V0,M0} R(1154,1000) { }.
% 0.72/1.15 parent0: (1413) {G4,W0,D0,L0,V0,M0} { }.
% 0.72/1.15 substitution0:
% 0.72/1.15 end
% 0.72/1.15 permutation0:
% 0.72/1.15 end
% 0.72/1.15
% 0.72/1.15 Proof check complete!
% 0.72/1.15
% 0.72/1.15 Memory use:
% 0.72/1.15
% 0.72/1.15 space for terms: 11798
% 0.72/1.15 space for clauses: 60850
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 clauses generated: 5597
% 0.72/1.15 clauses kept: 1156
% 0.72/1.15 clauses selected: 278
% 0.72/1.15 clauses deleted: 102
% 0.72/1.15 clauses inuse deleted: 60
% 0.72/1.15
% 0.72/1.15 subsentry: 7118
% 0.72/1.15 literals s-matched: 5287
% 0.72/1.15 literals matched: 5264
% 0.72/1.15 full subsumption: 661
% 0.72/1.15
% 0.72/1.15 checksum: -316585264
% 0.72/1.15
% 0.72/1.15
% 0.72/1.15 Bliksem ended
%------------------------------------------------------------------------------