%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SEU217+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n008.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:11:30 EDT 2022
% Result : Theorem 0.75s 1.24s
% Output : Refutation 0.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SEU217+1 : TPTP v8.1.0. Released v3.3.0.
% 0.06/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n008.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 : Mon Jun 20 14:02:22 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.75/1.24 *** allocated 10000 integers for termspace/termends
% 0.75/1.24 *** allocated 10000 integers for clauses
% 0.75/1.24 *** allocated 10000 integers for justifications
% 0.75/1.24 Bliksem 1.12
% 0.75/1.24
% 0.75/1.24
% 0.75/1.24 Automatic Strategy Selection
% 0.75/1.24
% 0.75/1.24
% 0.75/1.24 Clauses:
% 0.75/1.24
% 0.75/1.24 { relation( skol1 ) }.
% 0.75/1.24 { relation_empty_yielding( skol1 ) }.
% 0.75/1.24 { && }.
% 0.75/1.24 { empty( empty_set ) }.
% 0.75/1.24 { relation( empty_set ) }.
% 0.75/1.24 { empty( empty_set ) }.
% 0.75/1.24 { relation( empty_set ) }.
% 0.75/1.24 { relation_empty_yielding( empty_set ) }.
% 0.75/1.24 { empty( empty_set ) }.
% 0.75/1.24 { element( skol2( X ), X ) }.
% 0.75/1.24 { && }.
% 0.75/1.24 { ! empty( X ), function( X ) }.
% 0.75/1.24 { empty( skol3 ) }.
% 0.75/1.24 { relation( skol3 ) }.
% 0.75/1.24 { ! empty( X ), relation( X ) }.
% 0.75/1.24 { ! empty( skol4 ) }.
% 0.75/1.24 { relation( skol4 ) }.
% 0.75/1.24 { empty( X ), ! relation( X ), ! empty( relation_dom( X ) ) }.
% 0.75/1.24 { ! empty( X ), empty( relation_dom( X ) ) }.
% 0.75/1.24 { ! empty( X ), relation( relation_dom( X ) ) }.
% 0.75/1.24 { empty( skol5 ) }.
% 0.75/1.24 { ! empty( skol6 ) }.
% 0.75/1.24 { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 0.75/1.24 { ! empty( X ), X = empty_set }.
% 0.75/1.24 { ! empty( X ), X = Y, ! empty( Y ) }.
% 0.75/1.24 { ! in( X, Y ), ! in( Y, X ) }.
% 0.75/1.24 { && }.
% 0.75/1.24 { && }.
% 0.75/1.24 { relation( identity_relation( X ) ) }.
% 0.75/1.24 { relation( skol7 ) }.
% 0.75/1.24 { function( skol7 ) }.
% 0.75/1.24 { relation( identity_relation( X ) ) }.
% 0.75/1.24 { function( identity_relation( X ) ) }.
% 0.75/1.24 { ! in( X, Y ), element( X, Y ) }.
% 0.75/1.24 { ! in( X, Y ), ! empty( Y ) }.
% 0.75/1.24 { in( skol10, skol8 ) }.
% 0.75/1.24 { ! apply( identity_relation( skol8 ), skol10 ) = skol10 }.
% 0.75/1.24 { ! relation( X ), ! function( X ), ! X = identity_relation( Y ),
% 0.75/1.24 relation_dom( X ) = Y }.
% 0.75/1.24 { ! relation( X ), ! function( X ), ! X = identity_relation( Y ), alpha1( X
% 0.75/1.24 , Y ) }.
% 0.75/1.24 { ! relation( X ), ! function( X ), ! relation_dom( X ) = Y, ! alpha1( X, Y
% 0.75/1.24 ), X = identity_relation( Y ) }.
% 0.75/1.24 { ! alpha1( X, Y ), ! in( Z, Y ), apply( X, Z ) = Z }.
% 0.75/1.24 { in( skol9( Z, Y ), Y ), alpha1( X, Y ) }.
% 0.75/1.24 { ! apply( X, skol9( X, Y ) ) = skol9( X, Y ), alpha1( X, Y ) }.
% 0.75/1.24
% 0.75/1.24 percentage equality = 0.156250, percentage horn = 0.944444
% 0.75/1.24 This is a problem with some equality
% 0.75/1.24
% 0.75/1.24
% 0.75/1.24
% 0.75/1.24 Options Used:
% 0.75/1.24
% 0.75/1.24 useres = 1
% 0.75/1.24 useparamod = 1
% 0.75/1.24 useeqrefl = 1
% 0.75/1.24 useeqfact = 1
% 0.75/1.24 usefactor = 1
% 0.75/1.24 usesimpsplitting = 0
% 0.75/1.24 usesimpdemod = 5
% 0.75/1.24 usesimpres = 3
% 0.75/1.24
% 0.75/1.24 resimpinuse = 1000
% 0.75/1.24 resimpclauses = 20000
% 0.75/1.24 substype = eqrewr
% 0.75/1.24 backwardsubs = 1
% 0.75/1.24 selectoldest = 5
% 0.75/1.24
% 0.75/1.24 litorderings [0] = split
% 0.75/1.24 litorderings [1] = extend the termordering, first sorting on arguments
% 0.75/1.24
% 0.75/1.24 termordering = kbo
% 0.75/1.24
% 0.75/1.24 litapriori = 0
% 0.75/1.24 termapriori = 1
% 0.75/1.24 litaposteriori = 0
% 0.75/1.24 termaposteriori = 0
% 0.75/1.24 demodaposteriori = 0
% 0.75/1.24 ordereqreflfact = 0
% 0.75/1.24
% 0.75/1.24 litselect = negord
% 0.75/1.24
% 0.75/1.24 maxweight = 15
% 0.75/1.24 maxdepth = 30000
% 0.75/1.24 maxlength = 115
% 0.75/1.24 maxnrvars = 195
% 0.75/1.24 excuselevel = 1
% 0.75/1.24 increasemaxweight = 1
% 0.75/1.24
% 0.75/1.24 maxselected = 10000000
% 0.75/1.24 maxnrclauses = 10000000
% 0.75/1.24
% 0.75/1.24 showgenerated = 0
% 0.75/1.24 showkept = 0
% 0.75/1.24 showselected = 0
% 0.75/1.24 showdeleted = 0
% 0.75/1.24 showresimp = 1
% 0.75/1.24 showstatus = 2000
% 0.75/1.24
% 0.75/1.24 prologoutput = 0
% 0.75/1.24 nrgoals = 5000000
% 0.75/1.24 totalproof = 1
% 0.75/1.24
% 0.75/1.24 Symbols occurring in the translation:
% 0.75/1.24
% 0.75/1.24 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.75/1.24 . [1, 2] (w:1, o:30, a:1, s:1, b:0),
% 0.75/1.24 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 0.75/1.24 ! [4, 1] (w:0, o:18, a:1, s:1, b:0),
% 0.75/1.24 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.75/1.24 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.75/1.24 relation [36, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.75/1.24 relation_empty_yielding [37, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.75/1.24 empty_set [38, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.75/1.24 empty [39, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.75/1.24 element [41, 2] (w:1, o:54, a:1, s:1, b:0),
% 0.75/1.24 function [42, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.75/1.24 relation_dom [43, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.75/1.24 in [44, 2] (w:1, o:55, a:1, s:1, b:0),
% 0.75/1.24 identity_relation [45, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.75/1.24 apply [46, 2] (w:1, o:56, a:1, s:1, b:0),
% 0.75/1.24 alpha1 [48, 2] (w:1, o:57, a:1, s:1, b:1),
% 0.75/1.24 skol1 [49, 0] (w:1, o:10, a:1, s:1, b:1),
% 0.75/1.24 skol2 [50, 1] (w:1, o:29, a:1, s:1, b:1),
% 0.75/1.24 skol3 [51, 0] (w:1, o:11, a:1, s:1, b:1),
% 0.75/1.24 skol4 [52, 0] (w:1, o:12, a:1, s:1, b:1),
% 0.75/1.24 skol5 [53, 0] (w:1, o:13, a:1, s:1, b:1),
% 0.75/1.24 skol6 [54, 0] (w:1, o:14, a:1, s:1, b:1),
% 0.75/1.24 skol7 [55, 0] (w:1, o:15, a:1, s:1, b:1),
% 0.75/1.24 skol8 [56, 0] (w:1, o:16, a:1, s:1, b:1),
% 0.75/1.24 skol9 [57, 2] (w:1, o:58, a:1, s:1, b:1),
% 0.75/1.24 skol10 [58, 0] (w:1, o:17, a:1, s:1, b:1).
% 0.75/1.24
% 0.75/1.24
% 0.75/1.24 Starting Search:
% 0.75/1.24
% 0.75/1.24 *** allocated 15000 integers for clauses
% 0.75/1.24 *** allocated 22500 integers for clauses
% 0.75/1.24 *** allocated 33750 integers for clauses
% 0.75/1.24 *** allocated 50625 integers for clauses
% 0.75/1.24 *** allocated 15000 integers for termspace/termends
% 0.75/1.24 Resimplifying inuse:
% 0.75/1.24 Done
% 0.75/1.24
% 0.75/1.24 *** allocated 75937 integers for clauses
% 0.75/1.24 *** allocated 22500 integers for termspace/termends
% 0.75/1.24 *** allocated 113905 integers for clauses
% 0.75/1.24 *** allocated 33750 integers for termspace/termends
% 0.75/1.24
% 0.75/1.24 Bliksems!, er is een bewijs:
% 0.75/1.24 % SZS status Theorem
% 0.75/1.24 % SZS output start Refutation
% 0.75/1.24
% 0.75/1.24 (22) {G0,W3,D3,L1,V1,M1} I { relation( identity_relation( X ) ) }.
% 0.75/1.24 (25) {G0,W3,D3,L1,V1,M1} I { function( identity_relation( X ) ) }.
% 0.75/1.24 (28) {G0,W3,D2,L1,V0,M1} I { in( skol10, skol8 ) }.
% 0.75/1.24 (29) {G0,W6,D4,L1,V0,M1} I { ! apply( identity_relation( skol8 ), skol10 )
% 0.75/1.24 ==> skol10 }.
% 0.75/1.24 (31) {G0,W11,D3,L4,V2,M4} I { ! relation( X ), ! function( X ), ! X =
% 0.75/1.24 identity_relation( Y ), alpha1( X, Y ) }.
% 0.75/1.24 (33) {G0,W11,D3,L3,V3,M3} I { ! alpha1( X, Y ), ! in( Z, Y ), apply( X, Z )
% 0.75/1.24 ==> Z }.
% 0.75/1.24 (214) {G1,W9,D3,L2,V2,M2} R(31,22);r(25) { ! identity_relation( X ) =
% 0.75/1.24 identity_relation( Y ), alpha1( identity_relation( X ), Y ) }.
% 0.75/1.24 (222) {G2,W4,D3,L1,V1,M1} Q(214) { alpha1( identity_relation( X ), X ) }.
% 0.75/1.24 (299) {G1,W7,D3,L2,V1,M2} R(33,29) { ! alpha1( identity_relation( skol8 ),
% 0.75/1.24 X ), ! in( skol10, X ) }.
% 0.75/1.24 (1775) {G3,W0,D0,L0,V0,M0} R(299,222);r(28) { }.
% 0.75/1.24
% 0.75/1.24
% 0.75/1.24 % SZS output end Refutation
% 0.75/1.24 found a proof!
% 0.75/1.24
% 0.75/1.24
% 0.75/1.24 Unprocessed initial clauses:
% 0.75/1.24
% 0.75/1.24 (1777) {G0,W2,D2,L1,V0,M1} { relation( skol1 ) }.
% 0.75/1.24 (1778) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( skol1 ) }.
% 0.75/1.24 (1779) {G0,W1,D1,L1,V0,M1} { && }.
% 0.75/1.24 (1780) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.75/1.24 (1781) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 0.75/1.24 (1782) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.75/1.24 (1783) {G0,W2,D2,L1,V0,M1} { relation( empty_set ) }.
% 0.75/1.24 (1784) {G0,W2,D2,L1,V0,M1} { relation_empty_yielding( empty_set ) }.
% 0.75/1.24 (1785) {G0,W2,D2,L1,V0,M1} { empty( empty_set ) }.
% 0.75/1.24 (1786) {G0,W4,D3,L1,V1,M1} { element( skol2( X ), X ) }.
% 0.75/1.24 (1787) {G0,W1,D1,L1,V0,M1} { && }.
% 0.75/1.24 (1788) {G0,W4,D2,L2,V1,M2} { ! empty( X ), function( X ) }.
% 0.75/1.24 (1789) {G0,W2,D2,L1,V0,M1} { empty( skol3 ) }.
% 0.75/1.24 (1790) {G0,W2,D2,L1,V0,M1} { relation( skol3 ) }.
% 0.75/1.24 (1791) {G0,W4,D2,L2,V1,M2} { ! empty( X ), relation( X ) }.
% 0.75/1.24 (1792) {G0,W2,D2,L1,V0,M1} { ! empty( skol4 ) }.
% 0.75/1.24 (1793) {G0,W2,D2,L1,V0,M1} { relation( skol4 ) }.
% 0.75/1.24 (1794) {G0,W7,D3,L3,V1,M3} { empty( X ), ! relation( X ), ! empty(
% 0.75/1.24 relation_dom( X ) ) }.
% 0.75/1.24 (1795) {G0,W5,D3,L2,V1,M2} { ! empty( X ), empty( relation_dom( X ) ) }.
% 0.75/1.24 (1796) {G0,W5,D3,L2,V1,M2} { ! empty( X ), relation( relation_dom( X ) )
% 0.75/1.24 }.
% 0.75/1.24 (1797) {G0,W2,D2,L1,V0,M1} { empty( skol5 ) }.
% 0.75/1.24 (1798) {G0,W2,D2,L1,V0,M1} { ! empty( skol6 ) }.
% 0.75/1.24 (1799) {G0,W8,D2,L3,V2,M3} { ! element( X, Y ), empty( Y ), in( X, Y ) }.
% 0.75/1.24 (1800) {G0,W5,D2,L2,V1,M2} { ! empty( X ), X = empty_set }.
% 0.75/1.24 (1801) {G0,W7,D2,L3,V2,M3} { ! empty( X ), X = Y, ! empty( Y ) }.
% 0.75/1.24 (1802) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), ! in( Y, X ) }.
% 0.75/1.24 (1803) {G0,W1,D1,L1,V0,M1} { && }.
% 0.75/1.24 (1804) {G0,W1,D1,L1,V0,M1} { && }.
% 0.75/1.24 (1805) {G0,W3,D3,L1,V1,M1} { relation( identity_relation( X ) ) }.
% 0.75/1.24 (1806) {G0,W2,D2,L1,V0,M1} { relation( skol7 ) }.
% 0.75/1.24 (1807) {G0,W2,D2,L1,V0,M1} { function( skol7 ) }.
% 0.75/1.24 (1808) {G0,W3,D3,L1,V1,M1} { relation( identity_relation( X ) ) }.
% 0.75/1.24 (1809) {G0,W3,D3,L1,V1,M1} { function( identity_relation( X ) ) }.
% 0.75/1.24 (1810) {G0,W6,D2,L2,V2,M2} { ! in( X, Y ), element( X, Y ) }.
% 0.75/1.24 (1811) {G0,W5,D2,L2,V2,M2} { ! in( X, Y ), ! empty( Y ) }.
% 0.75/1.24 (1812) {G0,W3,D2,L1,V0,M1} { in( skol10, skol8 ) }.
% 0.75/1.24 (1813) {G0,W6,D4,L1,V0,M1} { ! apply( identity_relation( skol8 ), skol10 )
% 0.75/1.24 = skol10 }.
% 0.75/1.24 (1814) {G0,W12,D3,L4,V2,M4} { ! relation( X ), ! function( X ), ! X =
% 0.75/1.24 identity_relation( Y ), relation_dom( X ) = Y }.
% 0.75/1.24 (1815) {G0,W11,D3,L4,V2,M4} { ! relation( X ), ! function( X ), ! X =
% 0.75/1.24 identity_relation( Y ), alpha1( X, Y ) }.
% 0.75/1.24 (1816) {G0,W15,D3,L5,V2,M5} { ! relation( X ), ! function( X ), !
% 0.75/1.24 relation_dom( X ) = Y, ! alpha1( X, Y ), X = identity_relation( Y ) }.
% 0.75/1.24 (1817) {G0,W11,D3,L3,V3,M3} { ! alpha1( X, Y ), ! in( Z, Y ), apply( X, Z
% 0.75/1.24 ) = Z }.
% 0.75/1.24 (1818) {G0,W8,D3,L2,V3,M2} { in( skol9( Z, Y ), Y ), alpha1( X, Y ) }.
% 0.75/1.24 (1819) {G0,W12,D4,L2,V2,M2} { ! apply( X, skol9( X, Y ) ) = skol9( X, Y )
% 0.75/1.24 , alpha1( X, Y ) }.
% 0.75/1.24
% 0.75/1.24
% 0.75/1.24 Total Proof:
% 0.75/1.24
% 0.75/1.24 subsumption: (22) {G0,W3,D3,L1,V1,M1} I { relation( identity_relation( X )
% 0.75/1.24 ) }.
% 0.75/1.24 parent0: (1805) {G0,W3,D3,L1,V1,M1} { relation( identity_relation( X ) )
% 0.75/1.24 }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 end
% 0.75/1.24 permutation0:
% 0.75/1.24 0 ==> 0
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 subsumption: (25) {G0,W3,D3,L1,V1,M1} I { function( identity_relation( X )
% 0.75/1.24 ) }.
% 0.75/1.24 parent0: (1809) {G0,W3,D3,L1,V1,M1} { function( identity_relation( X ) )
% 0.75/1.24 }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 end
% 0.75/1.24 permutation0:
% 0.75/1.24 0 ==> 0
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 subsumption: (28) {G0,W3,D2,L1,V0,M1} I { in( skol10, skol8 ) }.
% 0.75/1.24 parent0: (1812) {G0,W3,D2,L1,V0,M1} { in( skol10, skol8 ) }.
% 0.75/1.24 substitution0:
% 0.75/1.24 end
% 0.75/1.24 permutation0:
% 0.75/1.24 0 ==> 0
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 subsumption: (29) {G0,W6,D4,L1,V0,M1} I { ! apply( identity_relation( skol8
% 0.75/1.24 ), skol10 ) ==> skol10 }.
% 0.75/1.24 parent0: (1813) {G0,W6,D4,L1,V0,M1} { ! apply( identity_relation( skol8 )
% 0.75/1.24 , skol10 ) = skol10 }.
% 0.75/1.24 substitution0:
% 0.75/1.24 end
% 0.75/1.24 permutation0:
% 0.75/1.24 0 ==> 0
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 subsumption: (31) {G0,W11,D3,L4,V2,M4} I { ! relation( X ), ! function( X )
% 0.75/1.24 , ! X = identity_relation( Y ), alpha1( X, Y ) }.
% 0.75/1.24 parent0: (1815) {G0,W11,D3,L4,V2,M4} { ! relation( X ), ! function( X ), !
% 0.75/1.24 X = identity_relation( Y ), alpha1( X, Y ) }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 Y := Y
% 0.75/1.24 end
% 0.75/1.24 permutation0:
% 0.75/1.24 0 ==> 0
% 0.75/1.24 1 ==> 1
% 0.75/1.24 2 ==> 2
% 0.75/1.24 3 ==> 3
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 subsumption: (33) {G0,W11,D3,L3,V3,M3} I { ! alpha1( X, Y ), ! in( Z, Y ),
% 0.75/1.24 apply( X, Z ) ==> Z }.
% 0.75/1.24 parent0: (1817) {G0,W11,D3,L3,V3,M3} { ! alpha1( X, Y ), ! in( Z, Y ),
% 0.75/1.24 apply( X, Z ) = Z }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 Y := Y
% 0.75/1.24 Z := Z
% 0.75/1.24 end
% 0.75/1.24 permutation0:
% 0.75/1.24 0 ==> 0
% 0.75/1.24 1 ==> 1
% 0.75/1.24 2 ==> 2
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 eqswap: (1853) {G0,W11,D3,L4,V2,M4} { ! identity_relation( Y ) = X, !
% 0.75/1.24 relation( X ), ! function( X ), alpha1( X, Y ) }.
% 0.75/1.24 parent0[2]: (31) {G0,W11,D3,L4,V2,M4} I { ! relation( X ), ! function( X )
% 0.75/1.24 , ! X = identity_relation( Y ), alpha1( X, Y ) }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 Y := Y
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 resolution: (1854) {G1,W12,D3,L3,V2,M3} { ! identity_relation( X ) =
% 0.75/1.24 identity_relation( Y ), ! function( identity_relation( Y ) ), alpha1(
% 0.75/1.24 identity_relation( Y ), X ) }.
% 0.75/1.24 parent0[1]: (1853) {G0,W11,D3,L4,V2,M4} { ! identity_relation( Y ) = X, !
% 0.75/1.24 relation( X ), ! function( X ), alpha1( X, Y ) }.
% 0.75/1.24 parent1[0]: (22) {G0,W3,D3,L1,V1,M1} I { relation( identity_relation( X ) )
% 0.75/1.24 }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := identity_relation( Y )
% 0.75/1.24 Y := X
% 0.75/1.24 end
% 0.75/1.24 substitution1:
% 0.75/1.24 X := Y
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 resolution: (1855) {G1,W9,D3,L2,V2,M2} { ! identity_relation( X ) =
% 0.75/1.24 identity_relation( Y ), alpha1( identity_relation( Y ), X ) }.
% 0.75/1.24 parent0[1]: (1854) {G1,W12,D3,L3,V2,M3} { ! identity_relation( X ) =
% 0.75/1.24 identity_relation( Y ), ! function( identity_relation( Y ) ), alpha1(
% 0.75/1.24 identity_relation( Y ), X ) }.
% 0.75/1.24 parent1[0]: (25) {G0,W3,D3,L1,V1,M1} I { function( identity_relation( X ) )
% 0.75/1.24 }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 Y := Y
% 0.75/1.24 end
% 0.75/1.24 substitution1:
% 0.75/1.24 X := Y
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 eqswap: (1856) {G1,W9,D3,L2,V2,M2} { ! identity_relation( Y ) =
% 0.75/1.24 identity_relation( X ), alpha1( identity_relation( Y ), X ) }.
% 0.75/1.24 parent0[0]: (1855) {G1,W9,D3,L2,V2,M2} { ! identity_relation( X ) =
% 0.75/1.24 identity_relation( Y ), alpha1( identity_relation( Y ), X ) }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 Y := Y
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 subsumption: (214) {G1,W9,D3,L2,V2,M2} R(31,22);r(25) { ! identity_relation
% 0.75/1.24 ( X ) = identity_relation( Y ), alpha1( identity_relation( X ), Y ) }.
% 0.75/1.24 parent0: (1856) {G1,W9,D3,L2,V2,M2} { ! identity_relation( Y ) =
% 0.75/1.24 identity_relation( X ), alpha1( identity_relation( Y ), X ) }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := Y
% 0.75/1.24 Y := X
% 0.75/1.24 end
% 0.75/1.24 permutation0:
% 0.75/1.24 0 ==> 0
% 0.75/1.24 1 ==> 1
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 eqswap: (1857) {G1,W9,D3,L2,V2,M2} { ! identity_relation( Y ) =
% 0.75/1.24 identity_relation( X ), alpha1( identity_relation( X ), Y ) }.
% 0.75/1.24 parent0[0]: (214) {G1,W9,D3,L2,V2,M2} R(31,22);r(25) { ! identity_relation
% 0.75/1.24 ( X ) = identity_relation( Y ), alpha1( identity_relation( X ), Y ) }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 Y := Y
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 eqrefl: (1858) {G0,W4,D3,L1,V1,M1} { alpha1( identity_relation( X ), X )
% 0.75/1.24 }.
% 0.75/1.24 parent0[0]: (1857) {G1,W9,D3,L2,V2,M2} { ! identity_relation( Y ) =
% 0.75/1.24 identity_relation( X ), alpha1( identity_relation( X ), Y ) }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 Y := X
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 subsumption: (222) {G2,W4,D3,L1,V1,M1} Q(214) { alpha1( identity_relation(
% 0.75/1.24 X ), X ) }.
% 0.75/1.24 parent0: (1858) {G0,W4,D3,L1,V1,M1} { alpha1( identity_relation( X ), X )
% 0.75/1.24 }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 end
% 0.75/1.24 permutation0:
% 0.75/1.24 0 ==> 0
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 eqswap: (1859) {G0,W11,D3,L3,V3,M3} { Y ==> apply( X, Y ), ! alpha1( X, Z
% 0.75/1.24 ), ! in( Y, Z ) }.
% 0.75/1.24 parent0[2]: (33) {G0,W11,D3,L3,V3,M3} I { ! alpha1( X, Y ), ! in( Z, Y ),
% 0.75/1.24 apply( X, Z ) ==> Z }.
% 0.75/1.24 substitution0:
% 0.75/1.24 X := X
% 0.75/1.24 Y := Z
% 0.75/1.24 Z := Y
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 eqswap: (1860) {G0,W6,D4,L1,V0,M1} { ! skol10 ==> apply( identity_relation
% 0.75/1.24 ( skol8 ), skol10 ) }.
% 0.75/1.24 parent0[0]: (29) {G0,W6,D4,L1,V0,M1} I { ! apply( identity_relation( skol8
% 0.75/1.24 ), skol10 ) ==> skol10 }.
% 0.75/1.24 substitution0:
% 0.75/1.24 end
% 0.75/1.24
% 0.75/1.24 resolution: (1861) {G1,W7,D3,L2,V1,M2} { ! alpha1( identity_relation(
% 0.75/1.24 skol8 ), X ), ! in( skol10, X ) }.
% 0.75/1.25 parent0[0]: (1860) {G0,W6,D4,L1,V0,M1} { ! skol10 ==> apply(
% 0.75/1.25 identity_relation( skol8 ), skol10 ) }.
% 0.75/1.25 parent1[0]: (1859) {G0,W11,D3,L3,V3,M3} { Y ==> apply( X, Y ), ! alpha1( X
% 0.75/1.25 , Z ), ! in( Y, Z ) }.
% 0.75/1.25 substitution0:
% 0.75/1.25 end
% 0.75/1.25 substitution1:
% 0.75/1.25 X := identity_relation( skol8 )
% 0.75/1.25 Y := skol10
% 0.75/1.25 Z := X
% 0.75/1.25 end
% 0.75/1.25
% 0.75/1.25 subsumption: (299) {G1,W7,D3,L2,V1,M2} R(33,29) { ! alpha1(
% 0.75/1.25 identity_relation( skol8 ), X ), ! in( skol10, X ) }.
% 0.75/1.25 parent0: (1861) {G1,W7,D3,L2,V1,M2} { ! alpha1( identity_relation( skol8 )
% 0.75/1.25 , X ), ! in( skol10, X ) }.
% 0.75/1.25 substitution0:
% 0.75/1.25 X := X
% 0.75/1.25 end
% 0.75/1.25 permutation0:
% 0.75/1.25 0 ==> 0
% 0.75/1.25 1 ==> 1
% 0.75/1.25 end
% 0.75/1.25
% 0.75/1.25 resolution: (1862) {G2,W3,D2,L1,V0,M1} { ! in( skol10, skol8 ) }.
% 0.75/1.25 parent0[0]: (299) {G1,W7,D3,L2,V1,M2} R(33,29) { ! alpha1(
% 0.75/1.25 identity_relation( skol8 ), X ), ! in( skol10, X ) }.
% 0.75/1.25 parent1[0]: (222) {G2,W4,D3,L1,V1,M1} Q(214) { alpha1( identity_relation( X
% 0.75/1.25 ), X ) }.
% 0.75/1.25 substitution0:
% 0.75/1.25 X := skol8
% 0.75/1.25 end
% 0.75/1.25 substitution1:
% 0.75/1.25 X := skol8
% 0.75/1.25 end
% 0.75/1.25
% 0.75/1.25 resolution: (1863) {G1,W0,D0,L0,V0,M0} { }.
% 0.75/1.25 parent0[0]: (1862) {G2,W3,D2,L1,V0,M1} { ! in( skol10, skol8 ) }.
% 0.75/1.25 parent1[0]: (28) {G0,W3,D2,L1,V0,M1} I { in( skol10, skol8 ) }.
% 0.75/1.25 substitution0:
% 0.75/1.25 end
% 0.75/1.25 substitution1:
% 0.75/1.25 end
% 0.75/1.25
% 0.75/1.25 subsumption: (1775) {G3,W0,D0,L0,V0,M0} R(299,222);r(28) { }.
% 0.75/1.25 parent0: (1863) {G1,W0,D0,L0,V0,M0} { }.
% 0.75/1.25 substitution0:
% 0.75/1.25 end
% 0.75/1.25 permutation0:
% 0.75/1.25 end
% 0.75/1.25
% 0.75/1.25 Proof check complete!
% 0.75/1.25
% 0.75/1.25 Memory use:
% 0.75/1.25
% 0.75/1.25 space for terms: 23239
% 0.75/1.25 space for clauses: 80747
% 0.75/1.25
% 0.75/1.25
% 0.75/1.25 clauses generated: 9724
% 0.75/1.25 clauses kept: 1776
% 0.75/1.25 clauses selected: 205
% 0.75/1.25 clauses deleted: 72
% 0.75/1.25 clauses inuse deleted: 27
% 0.75/1.25
% 0.75/1.25 subsentry: 15389
% 0.75/1.25 literals s-matched: 13131
% 0.75/1.25 literals matched: 13056
% 0.75/1.25 full subsumption: 2203
% 0.75/1.25
% 0.75/1.25 checksum: -506301895
% 0.75/1.25
% 0.75/1.25
% 0.75/1.25 Bliksem ended
%------------------------------------------------------------------------------