%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SET977+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n018.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:44 EDT 2022
% Result : Theorem 1.80s 2.18s
% Output : Refutation 1.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET977+1 : TPTP v8.1.0. Released v3.2.0.
% 0.03/0.13 % Command : bliksem %s
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Sat Jul 9 22:43:42 EDT 2022
% 0.12/0.34 % CPUTime :
% 1.80/2.18 *** allocated 10000 integers for termspace/termends
% 1.80/2.18 *** allocated 10000 integers for clauses
% 1.80/2.18 *** allocated 10000 integers for justifications
% 1.80/2.18 Bliksem 1.12
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 Automatic Strategy Selection
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 Clauses:
% 1.80/2.18
% 1.80/2.18 { ! in( X, Y ), ! in( Y, X ) }.
% 1.80/2.18 { unordered_pair( X, Y ) = unordered_pair( Y, X ) }.
% 1.80/2.18 { ! X = empty_set, ! in( Y, X ) }.
% 1.80/2.18 { in( skol1( X ), X ), X = empty_set }.
% 1.80/2.18 { ordered_pair( X, Y ) = unordered_pair( unordered_pair( X, Y ), singleton
% 1.80/2.18 ( X ) ) }.
% 1.80/2.18 { empty( empty_set ) }.
% 1.80/2.18 { ! empty( ordered_pair( X, Y ) ) }.
% 1.80/2.18 { empty( skol2 ) }.
% 1.80/2.18 { ! empty( skol3 ) }.
% 1.80/2.18 { ! in( ordered_pair( X, Y ), cartesian_product2( singleton( Z ), T ) ), X
% 1.80/2.18 = Z }.
% 1.80/2.18 { ! in( ordered_pair( X, Y ), cartesian_product2( singleton( Z ), T ) ), in
% 1.80/2.18 ( Y, T ) }.
% 1.80/2.18 { ! X = Z, ! in( Y, T ), in( ordered_pair( X, Y ), cartesian_product2(
% 1.80/2.18 singleton( Z ), T ) ) }.
% 1.80/2.18 { ! in( ordered_pair( X, Y ), cartesian_product2( Z, singleton( T ) ) ), in
% 1.80/2.18 ( X, Z ) }.
% 1.80/2.18 { ! in( ordered_pair( X, Y ), cartesian_product2( Z, singleton( T ) ) ), Y
% 1.80/2.18 = T }.
% 1.80/2.18 { ! in( X, Z ), ! Y = T, in( ordered_pair( X, Y ), cartesian_product2( Z,
% 1.80/2.18 singleton( T ) ) ) }.
% 1.80/2.18 { ! skol4 = empty_set }.
% 1.80/2.18 { cartesian_product2( singleton( skol5 ), skol4 ) = empty_set,
% 1.80/2.18 cartesian_product2( skol4, singleton( skol5 ) ) = empty_set }.
% 1.80/2.18
% 1.80/2.18 percentage equality = 0.379310, percentage horn = 0.882353
% 1.80/2.18 This is a problem with some equality
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 Options Used:
% 1.80/2.18
% 1.80/2.18 useres = 1
% 1.80/2.18 useparamod = 1
% 1.80/2.18 useeqrefl = 1
% 1.80/2.18 useeqfact = 1
% 1.80/2.18 usefactor = 1
% 1.80/2.18 usesimpsplitting = 0
% 1.80/2.18 usesimpdemod = 5
% 1.80/2.18 usesimpres = 3
% 1.80/2.18
% 1.80/2.18 resimpinuse = 1000
% 1.80/2.18 resimpclauses = 20000
% 1.80/2.18 substype = eqrewr
% 1.80/2.18 backwardsubs = 1
% 1.80/2.18 selectoldest = 5
% 1.80/2.18
% 1.80/2.18 litorderings [0] = split
% 1.80/2.18 litorderings [1] = extend the termordering, first sorting on arguments
% 1.80/2.18
% 1.80/2.18 termordering = kbo
% 1.80/2.18
% 1.80/2.18 litapriori = 0
% 1.80/2.18 termapriori = 1
% 1.80/2.18 litaposteriori = 0
% 1.80/2.18 termaposteriori = 0
% 1.80/2.18 demodaposteriori = 0
% 1.80/2.18 ordereqreflfact = 0
% 1.80/2.18
% 1.80/2.18 litselect = negord
% 1.80/2.18
% 1.80/2.18 maxweight = 15
% 1.80/2.18 maxdepth = 30000
% 1.80/2.18 maxlength = 115
% 1.80/2.18 maxnrvars = 195
% 1.80/2.18 excuselevel = 1
% 1.80/2.18 increasemaxweight = 1
% 1.80/2.18
% 1.80/2.18 maxselected = 10000000
% 1.80/2.18 maxnrclauses = 10000000
% 1.80/2.18
% 1.80/2.18 showgenerated = 0
% 1.80/2.18 showkept = 0
% 1.80/2.18 showselected = 0
% 1.80/2.18 showdeleted = 0
% 1.80/2.18 showresimp = 1
% 1.80/2.18 showstatus = 2000
% 1.80/2.18
% 1.80/2.18 prologoutput = 0
% 1.80/2.18 nrgoals = 5000000
% 1.80/2.18 totalproof = 1
% 1.80/2.18
% 1.80/2.18 Symbols occurring in the translation:
% 1.80/2.18
% 1.80/2.18 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.80/2.18 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 1.80/2.18 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 1.80/2.18 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.80/2.18 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.80/2.18 in [37, 2] (w:1, o:47, a:1, s:1, b:0),
% 1.80/2.18 unordered_pair [38, 2] (w:1, o:48, a:1, s:1, b:0),
% 1.80/2.18 empty_set [39, 0] (w:1, o:8, a:1, s:1, b:0),
% 1.80/2.18 ordered_pair [40, 2] (w:1, o:49, a:1, s:1, b:0),
% 1.80/2.18 singleton [41, 1] (w:1, o:20, a:1, s:1, b:0),
% 1.80/2.18 empty [42, 1] (w:1, o:21, a:1, s:1, b:0),
% 1.80/2.18 cartesian_product2 [45, 2] (w:1, o:50, a:1, s:1, b:0),
% 1.80/2.18 skol1 [46, 1] (w:1, o:22, a:1, s:1, b:1),
% 1.80/2.18 skol2 [47, 0] (w:1, o:11, a:1, s:1, b:1),
% 1.80/2.18 skol3 [48, 0] (w:1, o:12, a:1, s:1, b:1),
% 1.80/2.18 skol4 [49, 0] (w:1, o:13, a:1, s:1, b:1),
% 1.80/2.18 skol5 [50, 0] (w:1, o:14, a:1, s:1, b:1).
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 Starting Search:
% 1.80/2.18
% 1.80/2.18 *** allocated 15000 integers for clauses
% 1.80/2.18 *** allocated 22500 integers for clauses
% 1.80/2.18 *** allocated 33750 integers for clauses
% 1.80/2.18 *** allocated 15000 integers for termspace/termends
% 1.80/2.18 *** allocated 50625 integers for clauses
% 1.80/2.18 Resimplifying inuse:
% 1.80/2.18 Done
% 1.80/2.18
% 1.80/2.18 *** allocated 22500 integers for termspace/termends
% 1.80/2.18 *** allocated 75937 integers for clauses
% 1.80/2.18 *** allocated 33750 integers for termspace/termends
% 1.80/2.18 *** allocated 113905 integers for clauses
% 1.80/2.18
% 1.80/2.18 Intermediate Status:
% 1.80/2.18 Generated: 6519
% 1.80/2.18 Kept: 2008
% 1.80/2.18 Inuse: 128
% 1.80/2.18 Deleted: 1
% 1.80/2.18 Deletedinuse: 0
% 1.80/2.18
% 1.80/2.18 Resimplifying inuse:
% 1.80/2.18 Done
% 1.80/2.18
% 1.80/2.18 *** allocated 50625 integers for termspace/termends
% 1.80/2.18 *** allocated 170857 integers for clauses
% 1.80/2.18 Resimplifying inuse:
% 1.80/2.18 Done
% 1.80/2.18
% 1.80/2.18 *** allocated 75937 integers for termspace/termends
% 1.80/2.18 *** allocated 256285 integers for clauses
% 1.80/2.18
% 1.80/2.18 Intermediate Status:
% 1.80/2.18 Generated: 29004
% 1.80/2.18 Kept: 4014
% 1.80/2.18 Inuse: 252
% 1.80/2.18 Deleted: 10
% 1.80/2.18 Deletedinuse: 0
% 1.80/2.18
% 1.80/2.18 Resimplifying inuse:
% 1.80/2.18 Done
% 1.80/2.18
% 1.80/2.18 Resimplifying inuse:
% 1.80/2.18 Done
% 1.80/2.18
% 1.80/2.18 *** allocated 113905 integers for termspace/termends
% 1.80/2.18 *** allocated 384427 integers for clauses
% 1.80/2.18
% 1.80/2.18 Intermediate Status:
% 1.80/2.18 Generated: 62894
% 1.80/2.18 Kept: 6021
% 1.80/2.18 Inuse: 365
% 1.80/2.18 Deleted: 26
% 1.80/2.18 Deletedinuse: 3
% 1.80/2.18
% 1.80/2.18 Resimplifying inuse:
% 1.80/2.18 Done
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 Bliksems!, er is een bewijs:
% 1.80/2.18 % SZS status Theorem
% 1.80/2.18 % SZS output start Refutation
% 1.80/2.18
% 1.80/2.18 (2) {G0,W6,D2,L2,V2,M2} I { ! X = empty_set, ! in( Y, X ) }.
% 1.80/2.18 (3) {G0,W7,D3,L2,V1,M2} I { in( skol1( X ), X ), X = empty_set }.
% 1.80/2.18 (11) {G0,W14,D4,L3,V4,M3} I { ! X = Z, ! in( Y, T ), in( ordered_pair( X, Y
% 1.80/2.18 ), cartesian_product2( singleton( Z ), T ) ) }.
% 1.80/2.18 (14) {G0,W14,D4,L3,V4,M3} I { ! in( X, Z ), ! Y = T, in( ordered_pair( X, Y
% 1.80/2.18 ), cartesian_product2( Z, singleton( T ) ) ) }.
% 1.80/2.18 (15) {G0,W3,D2,L1,V0,M1} I { ! skol4 ==> empty_set }.
% 1.80/2.18 (16) {G0,W12,D4,L2,V0,M2} I { cartesian_product2( singleton( skol5 ), skol4
% 1.80/2.18 ) ==> empty_set, cartesian_product2( skol4, singleton( skol5 ) ) ==>
% 1.80/2.18 empty_set }.
% 1.80/2.18 (18) {G1,W3,D2,L1,V1,M1} Q(2) { ! in( X, empty_set ) }.
% 1.80/2.18 (19) {G1,W11,D4,L2,V3,M2} Q(11) { ! in( X, Y ), in( ordered_pair( Z, X ),
% 1.80/2.18 cartesian_product2( singleton( Z ), Y ) ) }.
% 1.80/2.18 (26) {G1,W10,D3,L3,V3,M3} P(3,2) { ! Y = X, ! in( Z, Y ), in( skol1( X ), X
% 1.80/2.18 ) }.
% 1.80/2.18 (28) {G1,W4,D3,L1,V0,M1} P(3,15);q { in( skol1( skol4 ), skol4 ) }.
% 1.80/2.18 (629) {G2,W12,D4,L2,V2,M2} R(14,28) { ! X = Y, in( ordered_pair( skol1(
% 1.80/2.18 skol4 ), X ), cartesian_product2( skol4, singleton( Y ) ) ) }.
% 1.80/2.18 (651) {G3,W9,D4,L1,V1,M1} Q(629) { in( ordered_pair( skol1( skol4 ), X ),
% 1.80/2.18 cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 (1228) {G2,W7,D3,L2,V1,M2} R(26,28) { ! skol4 = X, in( skol1( X ), X ) }.
% 1.80/2.18 (6971) {G4,W6,D4,L1,V0,M1} P(16,651);r(18) { cartesian_product2( singleton
% 1.80/2.18 ( skol5 ), skol4 ) ==> empty_set }.
% 1.80/2.18 (7028) {G5,W3,D2,L1,V1,M1} P(6971,19);r(18) { ! in( X, skol4 ) }.
% 1.80/2.18 (7078) {G6,W0,D0,L0,V0,M0} R(7028,1228);q { }.
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 % SZS output end Refutation
% 1.80/2.18 found a proof!
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 Unprocessed initial clauses:
% 1.80/2.18
% 1.80/2.18 (7080) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 1.80/2.18 (7081) {G0,W7,D3,L1,V2,M1} { unordered_pair( X, Y ) = unordered_pair( Y, X
% 1.80/2.18 ) }.
% 1.80/2.18 (7082) {G0,W6,D2,L2,V2,M2} { ! X = empty_set, ! in( Y, X ) }.
% 1.80/2.18 (7083) {G0,W7,D3,L2,V1,M2} { in( skol1( X ), X ), X = empty_set }.
% 1.80/2.18 (7084) {G0,W10,D4,L1,V2,M1} { ordered_pair( X, Y ) = unordered_pair(
% 1.80/2.18 unordered_pair( X, Y ), singleton( X ) ) }.
% 1.80/2.18 (7085) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 1.80/2.18 (7086) {G0,W4,D3,L1,V2,M1} { ! empty( ordered_pair( X, Y ) ) }.
% 1.80/2.18 (7087) {G0,W2,D2,L1,V0,M1} { empty( skol2 ) }.
% 1.80/2.18 (7088) {G0,W2,D2,L1,V0,M1} { ! empty( skol3 ) }.
% 1.80/2.18 (7089) {G0,W11,D4,L2,V4,M2} { ! in( ordered_pair( X, Y ),
% 1.80/2.18 cartesian_product2( singleton( Z ), T ) ), X = Z }.
% 1.80/2.18 (7090) {G0,W11,D4,L2,V4,M2} { ! in( ordered_pair( X, Y ),
% 1.80/2.18 cartesian_product2( singleton( Z ), T ) ), in( Y, T ) }.
% 1.80/2.18 (7091) {G0,W14,D4,L3,V4,M3} { ! X = Z, ! in( Y, T ), in( ordered_pair( X,
% 1.80/2.18 Y ), cartesian_product2( singleton( Z ), T ) ) }.
% 1.80/2.18 (7092) {G0,W11,D4,L2,V4,M2} { ! in( ordered_pair( X, Y ),
% 1.80/2.18 cartesian_product2( Z, singleton( T ) ) ), in( X, Z ) }.
% 1.80/2.18 (7093) {G0,W11,D4,L2,V4,M2} { ! in( ordered_pair( X, Y ),
% 1.80/2.18 cartesian_product2( Z, singleton( T ) ) ), Y = T }.
% 1.80/2.18 (7094) {G0,W14,D4,L3,V4,M3} { ! in( X, Z ), ! Y = T, in( ordered_pair( X,
% 1.80/2.18 Y ), cartesian_product2( Z, singleton( T ) ) ) }.
% 1.80/2.18 (7095) {G0,W3,D2,L1,V0,M1} { ! skol4 = empty_set }.
% 1.80/2.18 (7096) {G0,W12,D4,L2,V0,M2} { cartesian_product2( singleton( skol5 ),
% 1.80/2.18 skol4 ) = empty_set, cartesian_product2( skol4, singleton( skol5 ) ) =
% 1.80/2.18 empty_set }.
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 Total Proof:
% 1.80/2.18
% 1.80/2.18 subsumption: (2) {G0,W6,D2,L2,V2,M2} I { ! X = empty_set, ! in( Y, X ) }.
% 1.80/2.18 parent0: (7082) {G0,W6,D2,L2,V2,M2} { ! X = empty_set, ! in( Y, X ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Y
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 1
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (3) {G0,W7,D3,L2,V1,M2} I { in( skol1( X ), X ), X = empty_set
% 1.80/2.18 }.
% 1.80/2.18 parent0: (7083) {G0,W7,D3,L2,V1,M2} { in( skol1( X ), X ), X = empty_set
% 1.80/2.18 }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 1
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (11) {G0,W14,D4,L3,V4,M3} I { ! X = Z, ! in( Y, T ), in(
% 1.80/2.18 ordered_pair( X, Y ), cartesian_product2( singleton( Z ), T ) ) }.
% 1.80/2.18 parent0: (7091) {G0,W14,D4,L3,V4,M3} { ! X = Z, ! in( Y, T ), in(
% 1.80/2.18 ordered_pair( X, Y ), cartesian_product2( singleton( Z ), T ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Y
% 1.80/2.18 Z := Z
% 1.80/2.18 T := T
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 1
% 1.80/2.18 2 ==> 2
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (14) {G0,W14,D4,L3,V4,M3} I { ! in( X, Z ), ! Y = T, in(
% 1.80/2.18 ordered_pair( X, Y ), cartesian_product2( Z, singleton( T ) ) ) }.
% 1.80/2.18 parent0: (7094) {G0,W14,D4,L3,V4,M3} { ! in( X, Z ), ! Y = T, in(
% 1.80/2.18 ordered_pair( X, Y ), cartesian_product2( Z, singleton( T ) ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Y
% 1.80/2.18 Z := Z
% 1.80/2.18 T := T
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 1
% 1.80/2.18 2 ==> 2
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (15) {G0,W3,D2,L1,V0,M1} I { ! skol4 ==> empty_set }.
% 1.80/2.18 parent0: (7095) {G0,W3,D2,L1,V0,M1} { ! skol4 = empty_set }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (16) {G0,W12,D4,L2,V0,M2} I { cartesian_product2( singleton(
% 1.80/2.18 skol5 ), skol4 ) ==> empty_set, cartesian_product2( skol4, singleton(
% 1.80/2.18 skol5 ) ) ==> empty_set }.
% 1.80/2.18 parent0: (7096) {G0,W12,D4,L2,V0,M2} { cartesian_product2( singleton(
% 1.80/2.18 skol5 ), skol4 ) = empty_set, cartesian_product2( skol4, singleton( skol5
% 1.80/2.18 ) ) = empty_set }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 1
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7137) {G0,W6,D2,L2,V2,M2} { ! empty_set = X, ! in( Y, X ) }.
% 1.80/2.18 parent0[0]: (2) {G0,W6,D2,L2,V2,M2} I { ! X = empty_set, ! in( Y, X ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Y
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqrefl: (7138) {G0,W3,D2,L1,V1,M1} { ! in( X, empty_set ) }.
% 1.80/2.18 parent0[0]: (7137) {G0,W6,D2,L2,V2,M2} { ! empty_set = X, ! in( Y, X ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := empty_set
% 1.80/2.18 Y := X
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (18) {G1,W3,D2,L1,V1,M1} Q(2) { ! in( X, empty_set ) }.
% 1.80/2.18 parent0: (7138) {G0,W3,D2,L1,V1,M1} { ! in( X, empty_set ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7139) {G0,W14,D4,L3,V4,M3} { ! Y = X, ! in( Z, T ), in(
% 1.80/2.18 ordered_pair( X, Z ), cartesian_product2( singleton( Y ), T ) ) }.
% 1.80/2.18 parent0[0]: (11) {G0,W14,D4,L3,V4,M3} I { ! X = Z, ! in( Y, T ), in(
% 1.80/2.18 ordered_pair( X, Y ), cartesian_product2( singleton( Z ), T ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Z
% 1.80/2.18 Z := Y
% 1.80/2.18 T := T
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqrefl: (7140) {G0,W11,D4,L2,V3,M2} { ! in( Y, Z ), in( ordered_pair( X, Y
% 1.80/2.18 ), cartesian_product2( singleton( X ), Z ) ) }.
% 1.80/2.18 parent0[0]: (7139) {G0,W14,D4,L3,V4,M3} { ! Y = X, ! in( Z, T ), in(
% 1.80/2.18 ordered_pair( X, Z ), cartesian_product2( singleton( Y ), T ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := X
% 1.80/2.18 Z := Y
% 1.80/2.18 T := Z
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (19) {G1,W11,D4,L2,V3,M2} Q(11) { ! in( X, Y ), in(
% 1.80/2.18 ordered_pair( Z, X ), cartesian_product2( singleton( Z ), Y ) ) }.
% 1.80/2.18 parent0: (7140) {G0,W11,D4,L2,V3,M2} { ! in( Y, Z ), in( ordered_pair( X,
% 1.80/2.18 Y ), cartesian_product2( singleton( X ), Z ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := Z
% 1.80/2.18 Y := X
% 1.80/2.18 Z := Y
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 1
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7141) {G0,W7,D3,L2,V1,M2} { empty_set = X, in( skol1( X ), X )
% 1.80/2.18 }.
% 1.80/2.18 parent0[1]: (3) {G0,W7,D3,L2,V1,M2} I { in( skol1( X ), X ), X = empty_set
% 1.80/2.18 }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7142) {G0,W6,D2,L2,V2,M2} { ! empty_set = X, ! in( Y, X ) }.
% 1.80/2.18 parent0[0]: (2) {G0,W6,D2,L2,V2,M2} I { ! X = empty_set, ! in( Y, X ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Y
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 paramod: (7143) {G1,W10,D3,L3,V3,M3} { ! Y = X, in( skol1( Y ), Y ), ! in
% 1.80/2.18 ( Z, X ) }.
% 1.80/2.18 parent0[0]: (7141) {G0,W7,D3,L2,V1,M2} { empty_set = X, in( skol1( X ), X
% 1.80/2.18 ) }.
% 1.80/2.18 parent1[0; 2]: (7142) {G0,W6,D2,L2,V2,M2} { ! empty_set = X, ! in( Y, X )
% 1.80/2.18 }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := Y
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Z
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7144) {G1,W10,D3,L3,V3,M3} { ! Y = X, in( skol1( X ), X ), ! in(
% 1.80/2.18 Z, Y ) }.
% 1.80/2.18 parent0[0]: (7143) {G1,W10,D3,L3,V3,M3} { ! Y = X, in( skol1( Y ), Y ), !
% 1.80/2.18 in( Z, X ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := Y
% 1.80/2.18 Y := X
% 1.80/2.18 Z := Z
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (26) {G1,W10,D3,L3,V3,M3} P(3,2) { ! Y = X, ! in( Z, Y ), in(
% 1.80/2.18 skol1( X ), X ) }.
% 1.80/2.18 parent0: (7144) {G1,W10,D3,L3,V3,M3} { ! Y = X, in( skol1( X ), X ), ! in
% 1.80/2.18 ( Z, Y ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Y
% 1.80/2.18 Z := Z
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 2
% 1.80/2.18 2 ==> 1
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7146) {G0,W3,D2,L1,V0,M1} { ! empty_set ==> skol4 }.
% 1.80/2.18 parent0[0]: (15) {G0,W3,D2,L1,V0,M1} I { ! skol4 ==> empty_set }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 paramod: (7150) {G1,W7,D3,L2,V0,M2} { ! empty_set ==> empty_set, in( skol1
% 1.80/2.18 ( skol4 ), skol4 ) }.
% 1.80/2.18 parent0[1]: (3) {G0,W7,D3,L2,V1,M2} I { in( skol1( X ), X ), X = empty_set
% 1.80/2.18 }.
% 1.80/2.18 parent1[0; 3]: (7146) {G0,W3,D2,L1,V0,M1} { ! empty_set ==> skol4 }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := skol4
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqrefl: (7200) {G0,W4,D3,L1,V0,M1} { in( skol1( skol4 ), skol4 ) }.
% 1.80/2.18 parent0[0]: (7150) {G1,W7,D3,L2,V0,M2} { ! empty_set ==> empty_set, in(
% 1.80/2.18 skol1( skol4 ), skol4 ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (28) {G1,W4,D3,L1,V0,M1} P(3,15);q { in( skol1( skol4 ), skol4
% 1.80/2.18 ) }.
% 1.80/2.18 parent0: (7200) {G0,W4,D3,L1,V0,M1} { in( skol1( skol4 ), skol4 ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7201) {G0,W14,D4,L3,V4,M3} { ! Y = X, ! in( Z, T ), in(
% 1.80/2.18 ordered_pair( Z, X ), cartesian_product2( T, singleton( Y ) ) ) }.
% 1.80/2.18 parent0[1]: (14) {G0,W14,D4,L3,V4,M3} I { ! in( X, Z ), ! Y = T, in(
% 1.80/2.18 ordered_pair( X, Y ), cartesian_product2( Z, singleton( T ) ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := Z
% 1.80/2.18 Y := X
% 1.80/2.18 Z := T
% 1.80/2.18 T := Y
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 resolution: (7202) {G1,W12,D4,L2,V2,M2} { ! X = Y, in( ordered_pair( skol1
% 1.80/2.18 ( skol4 ), Y ), cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 parent0[1]: (7201) {G0,W14,D4,L3,V4,M3} { ! Y = X, ! in( Z, T ), in(
% 1.80/2.18 ordered_pair( Z, X ), cartesian_product2( T, singleton( Y ) ) ) }.
% 1.80/2.18 parent1[0]: (28) {G1,W4,D3,L1,V0,M1} P(3,15);q { in( skol1( skol4 ), skol4
% 1.80/2.18 ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := Y
% 1.80/2.18 Y := X
% 1.80/2.18 Z := skol1( skol4 )
% 1.80/2.18 T := skol4
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7203) {G1,W12,D4,L2,V2,M2} { ! Y = X, in( ordered_pair( skol1(
% 1.80/2.18 skol4 ), Y ), cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 parent0[0]: (7202) {G1,W12,D4,L2,V2,M2} { ! X = Y, in( ordered_pair( skol1
% 1.80/2.18 ( skol4 ), Y ), cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Y
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (629) {G2,W12,D4,L2,V2,M2} R(14,28) { ! X = Y, in(
% 1.80/2.18 ordered_pair( skol1( skol4 ), X ), cartesian_product2( skol4, singleton(
% 1.80/2.18 Y ) ) ) }.
% 1.80/2.18 parent0: (7203) {G1,W12,D4,L2,V2,M2} { ! Y = X, in( ordered_pair( skol1(
% 1.80/2.18 skol4 ), Y ), cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := Y
% 1.80/2.18 Y := X
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 1
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7204) {G2,W12,D4,L2,V2,M2} { ! Y = X, in( ordered_pair( skol1(
% 1.80/2.18 skol4 ), X ), cartesian_product2( skol4, singleton( Y ) ) ) }.
% 1.80/2.18 parent0[0]: (629) {G2,W12,D4,L2,V2,M2} R(14,28) { ! X = Y, in( ordered_pair
% 1.80/2.18 ( skol1( skol4 ), X ), cartesian_product2( skol4, singleton( Y ) ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := Y
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqrefl: (7205) {G0,W9,D4,L1,V1,M1} { in( ordered_pair( skol1( skol4 ), X )
% 1.80/2.18 , cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 parent0[0]: (7204) {G2,W12,D4,L2,V2,M2} { ! Y = X, in( ordered_pair( skol1
% 1.80/2.18 ( skol4 ), X ), cartesian_product2( skol4, singleton( Y ) ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 Y := X
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (651) {G3,W9,D4,L1,V1,M1} Q(629) { in( ordered_pair( skol1(
% 1.80/2.18 skol4 ), X ), cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 parent0: (7205) {G0,W9,D4,L1,V1,M1} { in( ordered_pair( skol1( skol4 ), X
% 1.80/2.18 ), cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7206) {G1,W10,D3,L3,V3,M3} { ! Y = X, ! in( Z, X ), in( skol1( Y
% 1.80/2.18 ), Y ) }.
% 1.80/2.18 parent0[0]: (26) {G1,W10,D3,L3,V3,M3} P(3,2) { ! Y = X, ! in( Z, Y ), in(
% 1.80/2.18 skol1( X ), X ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := Y
% 1.80/2.18 Y := X
% 1.80/2.18 Z := Z
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 resolution: (7207) {G2,W7,D3,L2,V1,M2} { ! X = skol4, in( skol1( X ), X )
% 1.80/2.18 }.
% 1.80/2.18 parent0[1]: (7206) {G1,W10,D3,L3,V3,M3} { ! Y = X, ! in( Z, X ), in( skol1
% 1.80/2.18 ( Y ), Y ) }.
% 1.80/2.18 parent1[0]: (28) {G1,W4,D3,L1,V0,M1} P(3,15);q { in( skol1( skol4 ), skol4
% 1.80/2.18 ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := skol4
% 1.80/2.18 Y := X
% 1.80/2.18 Z := skol1( skol4 )
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7208) {G2,W7,D3,L2,V1,M2} { ! skol4 = X, in( skol1( X ), X ) }.
% 1.80/2.18 parent0[0]: (7207) {G2,W7,D3,L2,V1,M2} { ! X = skol4, in( skol1( X ), X )
% 1.80/2.18 }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (1228) {G2,W7,D3,L2,V1,M2} R(26,28) { ! skol4 = X, in( skol1(
% 1.80/2.18 X ), X ) }.
% 1.80/2.18 parent0: (7208) {G2,W7,D3,L2,V1,M2} { ! skol4 = X, in( skol1( X ), X ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 1 ==> 1
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7209) {G0,W12,D4,L2,V0,M2} { empty_set ==> cartesian_product2(
% 1.80/2.18 singleton( skol5 ), skol4 ), cartesian_product2( skol4, singleton( skol5
% 1.80/2.18 ) ) ==> empty_set }.
% 1.80/2.18 parent0[0]: (16) {G0,W12,D4,L2,V0,M2} I { cartesian_product2( singleton(
% 1.80/2.18 skol5 ), skol4 ) ==> empty_set, cartesian_product2( skol4, singleton(
% 1.80/2.18 skol5 ) ) ==> empty_set }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 paramod: (7212) {G1,W12,D4,L2,V0,M2} { in( ordered_pair( skol1( skol4 ),
% 1.80/2.18 skol5 ), empty_set ), empty_set ==> cartesian_product2( singleton( skol5
% 1.80/2.18 ), skol4 ) }.
% 1.80/2.18 parent0[1]: (7209) {G0,W12,D4,L2,V0,M2} { empty_set ==> cartesian_product2
% 1.80/2.18 ( singleton( skol5 ), skol4 ), cartesian_product2( skol4, singleton(
% 1.80/2.18 skol5 ) ) ==> empty_set }.
% 1.80/2.18 parent1[0; 5]: (651) {G3,W9,D4,L1,V1,M1} Q(629) { in( ordered_pair( skol1(
% 1.80/2.18 skol4 ), X ), cartesian_product2( skol4, singleton( X ) ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 X := skol5
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 resolution: (7213) {G2,W6,D4,L1,V0,M1} { empty_set ==> cartesian_product2
% 1.80/2.18 ( singleton( skol5 ), skol4 ) }.
% 1.80/2.18 parent0[0]: (18) {G1,W3,D2,L1,V1,M1} Q(2) { ! in( X, empty_set ) }.
% 1.80/2.18 parent1[0]: (7212) {G1,W12,D4,L2,V0,M2} { in( ordered_pair( skol1( skol4 )
% 1.80/2.18 , skol5 ), empty_set ), empty_set ==> cartesian_product2( singleton(
% 1.80/2.18 skol5 ), skol4 ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := ordered_pair( skol1( skol4 ), skol5 )
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7214) {G2,W6,D4,L1,V0,M1} { cartesian_product2( singleton( skol5
% 1.80/2.18 ), skol4 ) ==> empty_set }.
% 1.80/2.18 parent0[0]: (7213) {G2,W6,D4,L1,V0,M1} { empty_set ==> cartesian_product2
% 1.80/2.18 ( singleton( skol5 ), skol4 ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (6971) {G4,W6,D4,L1,V0,M1} P(16,651);r(18) {
% 1.80/2.18 cartesian_product2( singleton( skol5 ), skol4 ) ==> empty_set }.
% 1.80/2.18 parent0: (7214) {G2,W6,D4,L1,V0,M1} { cartesian_product2( singleton( skol5
% 1.80/2.18 ), skol4 ) ==> empty_set }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 paramod: (7216) {G2,W8,D3,L2,V1,M2} { in( ordered_pair( skol5, X ),
% 1.80/2.18 empty_set ), ! in( X, skol4 ) }.
% 1.80/2.18 parent0[0]: (6971) {G4,W6,D4,L1,V0,M1} P(16,651);r(18) { cartesian_product2
% 1.80/2.18 ( singleton( skol5 ), skol4 ) ==> empty_set }.
% 1.80/2.18 parent1[1; 4]: (19) {G1,W11,D4,L2,V3,M2} Q(11) { ! in( X, Y ), in(
% 1.80/2.18 ordered_pair( Z, X ), cartesian_product2( singleton( Z ), Y ) ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 X := X
% 1.80/2.18 Y := skol4
% 1.80/2.18 Z := skol5
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 resolution: (7217) {G2,W3,D2,L1,V1,M1} { ! in( X, skol4 ) }.
% 1.80/2.18 parent0[0]: (18) {G1,W3,D2,L1,V1,M1} Q(2) { ! in( X, empty_set ) }.
% 1.80/2.18 parent1[0]: (7216) {G2,W8,D3,L2,V1,M2} { in( ordered_pair( skol5, X ),
% 1.80/2.18 empty_set ), ! in( X, skol4 ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := ordered_pair( skol5, X )
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (7028) {G5,W3,D2,L1,V1,M1} P(6971,19);r(18) { ! in( X, skol4 )
% 1.80/2.18 }.
% 1.80/2.18 parent0: (7217) {G2,W3,D2,L1,V1,M1} { ! in( X, skol4 ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 0 ==> 0
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqswap: (7218) {G2,W7,D3,L2,V1,M2} { ! X = skol4, in( skol1( X ), X ) }.
% 1.80/2.18 parent0[0]: (1228) {G2,W7,D3,L2,V1,M2} R(26,28) { ! skol4 = X, in( skol1( X
% 1.80/2.18 ), X ) }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := X
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 resolution: (7219) {G3,W3,D2,L1,V0,M1} { ! skol4 = skol4 }.
% 1.80/2.18 parent0[0]: (7028) {G5,W3,D2,L1,V1,M1} P(6971,19);r(18) { ! in( X, skol4 )
% 1.80/2.18 }.
% 1.80/2.18 parent1[1]: (7218) {G2,W7,D3,L2,V1,M2} { ! X = skol4, in( skol1( X ), X )
% 1.80/2.18 }.
% 1.80/2.18 substitution0:
% 1.80/2.18 X := skol1( skol4 )
% 1.80/2.18 end
% 1.80/2.18 substitution1:
% 1.80/2.18 X := skol4
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 eqrefl: (7220) {G0,W0,D0,L0,V0,M0} { }.
% 1.80/2.18 parent0[0]: (7219) {G3,W3,D2,L1,V0,M1} { ! skol4 = skol4 }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 subsumption: (7078) {G6,W0,D0,L0,V0,M0} R(7028,1228);q { }.
% 1.80/2.18 parent0: (7220) {G0,W0,D0,L0,V0,M0} { }.
% 1.80/2.18 substitution0:
% 1.80/2.18 end
% 1.80/2.18 permutation0:
% 1.80/2.18 end
% 1.80/2.18
% 1.80/2.18 Proof check complete!
% 1.80/2.18
% 1.80/2.18 Memory use:
% 1.80/2.18
% 1.80/2.18 space for terms: 103012
% 1.80/2.18 space for clauses: 308679
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 clauses generated: 74006
% 1.80/2.18 clauses kept: 7079
% 1.80/2.18 clauses selected: 420
% 1.80/2.18 clauses deleted: 49
% 1.80/2.18 clauses inuse deleted: 7
% 1.80/2.18
% 1.80/2.18 subsentry: 234699
% 1.80/2.18 literals s-matched: 136944
% 1.80/2.18 literals matched: 135291
% 1.80/2.18 full subsumption: 55164
% 1.80/2.18
% 1.80/2.18 checksum: -495981209
% 1.80/2.18
% 1.80/2.18
% 1.80/2.18 Bliksem ended
%------------------------------------------------------------------------------