%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM532+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Mon Jul 18 06:23:18 EDT 2022
% Result : Theorem 0.77s 1.17s
% Output : Refutation 0.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM532+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : bliksem %s
% 0.12/0.34 % Computer : n013.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Tue Jul 5 08:09:59 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.77/1.17 *** allocated 10000 integers for termspace/termends
% 0.77/1.17 *** allocated 10000 integers for clauses
% 0.77/1.17 *** allocated 10000 integers for justifications
% 0.77/1.17 Bliksem 1.12
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Automatic Strategy Selection
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Clauses:
% 0.77/1.17
% 0.77/1.17 { && }.
% 0.77/1.17 { && }.
% 0.77/1.17 { ! aSet0( X ), ! aElementOf0( Y, X ), aElement0( Y ) }.
% 0.77/1.17 { && }.
% 0.77/1.17 { ! X = slcrc0, aSet0( X ) }.
% 0.77/1.17 { ! X = slcrc0, ! aElementOf0( Y, X ) }.
% 0.77/1.17 { ! aSet0( X ), aElementOf0( skol1( X ), X ), X = slcrc0 }.
% 0.77/1.17 { isFinite0( slcrc0 ) }.
% 0.77/1.17 { && }.
% 0.77/1.17 { ! aSet0( X ), ! isCountable0( X ), ! isFinite0( X ) }.
% 0.77/1.17 { ! aSet0( X ), ! isCountable0( X ), ! X = slcrc0 }.
% 0.77/1.17 { ! aSet0( X ), ! aSubsetOf0( Y, X ), aSet0( Y ) }.
% 0.77/1.17 { ! aSet0( X ), ! aSubsetOf0( Y, X ), alpha1( X, Y ) }.
% 0.77/1.17 { ! aSet0( X ), ! aSet0( Y ), ! alpha1( X, Y ), aSubsetOf0( Y, X ) }.
% 0.77/1.17 { ! alpha1( X, Y ), ! aElementOf0( Z, Y ), aElementOf0( Z, X ) }.
% 0.77/1.17 { aElementOf0( skol2( Z, Y ), Y ), alpha1( X, Y ) }.
% 0.77/1.17 { ! aElementOf0( skol2( X, Y ), X ), alpha1( X, Y ) }.
% 0.77/1.17 { ! aSet0( X ), ! isFinite0( X ), ! aSubsetOf0( Y, X ), isFinite0( Y ) }.
% 0.77/1.17 { aSet0( xA ) }.
% 0.77/1.17 { ! aSubsetOf0( xA, xA ) }.
% 0.77/1.17
% 0.77/1.17 percentage equality = 0.097561, percentage horn = 0.882353
% 0.77/1.17 This is a problem with some equality
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Options Used:
% 0.77/1.17
% 0.77/1.17 useres = 1
% 0.77/1.17 useparamod = 1
% 0.77/1.17 useeqrefl = 1
% 0.77/1.17 useeqfact = 1
% 0.77/1.17 usefactor = 1
% 0.77/1.17 usesimpsplitting = 0
% 0.77/1.17 usesimpdemod = 5
% 0.77/1.17 usesimpres = 3
% 0.77/1.17
% 0.77/1.17 resimpinuse = 1000
% 0.77/1.17 resimpclauses = 20000
% 0.77/1.17 substype = eqrewr
% 0.77/1.17 backwardsubs = 1
% 0.77/1.17 selectoldest = 5
% 0.77/1.17
% 0.77/1.17 litorderings [0] = split
% 0.77/1.17 litorderings [1] = extend the termordering, first sorting on arguments
% 0.77/1.17
% 0.77/1.17 termordering = kbo
% 0.77/1.17
% 0.77/1.17 litapriori = 0
% 0.77/1.17 termapriori = 1
% 0.77/1.17 litaposteriori = 0
% 0.77/1.17 termaposteriori = 0
% 0.77/1.17 demodaposteriori = 0
% 0.77/1.17 ordereqreflfact = 0
% 0.77/1.17
% 0.77/1.17 litselect = negord
% 0.77/1.17
% 0.77/1.17 maxweight = 15
% 0.77/1.17 maxdepth = 30000
% 0.77/1.17 maxlength = 115
% 0.77/1.17 maxnrvars = 195
% 0.77/1.17 excuselevel = 1
% 0.77/1.17 increasemaxweight = 1
% 0.77/1.17
% 0.77/1.17 maxselected = 10000000
% 0.77/1.17 maxnrclauses = 10000000
% 0.77/1.17
% 0.77/1.17 showgenerated = 0
% 0.77/1.17 showkept = 0
% 0.77/1.17 showselected = 0
% 0.77/1.17 showdeleted = 0
% 0.77/1.17 showresimp = 1
% 0.77/1.17 showstatus = 2000
% 0.77/1.17
% 0.77/1.17 prologoutput = 0
% 0.77/1.17 nrgoals = 5000000
% 0.77/1.17 totalproof = 1
% 0.77/1.17
% 0.77/1.17 Symbols occurring in the translation:
% 0.77/1.17
% 0.77/1.17 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.77/1.17 . [1, 2] (w:1, o:21, a:1, s:1, b:0),
% 0.77/1.17 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 0.77/1.17 ! [4, 1] (w:0, o:11, a:1, s:1, b:0),
% 0.77/1.17 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.77/1.17 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.77/1.17 aSet0 [36, 1] (w:1, o:16, a:1, s:1, b:0),
% 0.77/1.17 aElement0 [37, 1] (w:1, o:17, a:1, s:1, b:0),
% 0.77/1.17 aElementOf0 [39, 2] (w:1, o:45, a:1, s:1, b:0),
% 0.77/1.17 isFinite0 [40, 1] (w:1, o:18, a:1, s:1, b:0),
% 0.77/1.17 slcrc0 [41, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.77/1.17 isCountable0 [42, 1] (w:1, o:19, a:1, s:1, b:0),
% 0.77/1.17 aSubsetOf0 [43, 2] (w:1, o:46, a:1, s:1, b:0),
% 0.77/1.17 xA [45, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.77/1.17 alpha1 [46, 2] (w:1, o:47, a:1, s:1, b:1),
% 0.77/1.17 skol1 [47, 1] (w:1, o:20, a:1, s:1, b:1),
% 0.77/1.17 skol2 [48, 2] (w:1, o:48, a:1, s:1, b:1).
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Starting Search:
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Bliksems!, er is een bewijs:
% 0.77/1.17 % SZS status Theorem
% 0.77/1.17 % SZS output start Refutation
% 0.77/1.17
% 0.77/1.17 (10) {G0,W10,D2,L4,V2,M4} I { ! aSet0( X ), ! aSet0( Y ), ! alpha1( X, Y )
% 0.77/1.17 , aSubsetOf0( Y, X ) }.
% 0.77/1.17 (12) {G0,W8,D3,L2,V3,M2} I { aElementOf0( skol2( Z, Y ), Y ), alpha1( X, Y
% 0.77/1.17 ) }.
% 0.77/1.17 (13) {G0,W8,D3,L2,V2,M2} I { ! aElementOf0( skol2( X, Y ), X ), alpha1( X,
% 0.77/1.17 Y ) }.
% 0.77/1.17 (15) {G0,W2,D2,L1,V0,M1} I { aSet0( xA ) }.
% 0.77/1.17 (16) {G0,W3,D2,L1,V0,M1} I { ! aSubsetOf0( xA, xA ) }.
% 0.77/1.17 (69) {G1,W3,D2,L1,V0,M1} R(10,16);f;r(15) { ! alpha1( xA, xA ) }.
% 0.77/1.17 (121) {G2,W5,D3,L1,V1,M1} R(12,69) { aElementOf0( skol2( X, xA ), xA ) }.
% 0.77/1.17 (146) {G3,W0,D0,L0,V0,M0} R(13,69);r(121) { }.
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 % SZS output end Refutation
% 0.77/1.17 found a proof!
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Unprocessed initial clauses:
% 0.77/1.17
% 0.77/1.17 (148) {G0,W1,D1,L1,V0,M1} { && }.
% 0.77/1.17 (149) {G0,W1,D1,L1,V0,M1} { && }.
% 0.77/1.17 (150) {G0,W7,D2,L3,V2,M3} { ! aSet0( X ), ! aElementOf0( Y, X ), aElement0
% 0.77/1.17 ( Y ) }.
% 0.77/1.17 (151) {G0,W1,D1,L1,V0,M1} { && }.
% 0.77/1.17 (152) {G0,W5,D2,L2,V1,M2} { ! X = slcrc0, aSet0( X ) }.
% 0.77/1.17 (153) {G0,W6,D2,L2,V2,M2} { ! X = slcrc0, ! aElementOf0( Y, X ) }.
% 0.77/1.17 (154) {G0,W9,D3,L3,V1,M3} { ! aSet0( X ), aElementOf0( skol1( X ), X ), X
% 0.77/1.17 = slcrc0 }.
% 0.77/1.17 (155) {G0,W2,D2,L1,V0,M1} { isFinite0( slcrc0 ) }.
% 0.77/1.17 (156) {G0,W1,D1,L1,V0,M1} { && }.
% 0.77/1.17 (157) {G0,W6,D2,L3,V1,M3} { ! aSet0( X ), ! isCountable0( X ), ! isFinite0
% 0.77/1.17 ( X ) }.
% 0.77/1.17 (158) {G0,W7,D2,L3,V1,M3} { ! aSet0( X ), ! isCountable0( X ), ! X =
% 0.77/1.17 slcrc0 }.
% 0.77/1.17 (159) {G0,W7,D2,L3,V2,M3} { ! aSet0( X ), ! aSubsetOf0( Y, X ), aSet0( Y )
% 0.77/1.17 }.
% 0.77/1.17 (160) {G0,W8,D2,L3,V2,M3} { ! aSet0( X ), ! aSubsetOf0( Y, X ), alpha1( X
% 0.77/1.17 , Y ) }.
% 0.77/1.17 (161) {G0,W10,D2,L4,V2,M4} { ! aSet0( X ), ! aSet0( Y ), ! alpha1( X, Y )
% 0.77/1.17 , aSubsetOf0( Y, X ) }.
% 0.77/1.17 (162) {G0,W9,D2,L3,V3,M3} { ! alpha1( X, Y ), ! aElementOf0( Z, Y ),
% 0.77/1.17 aElementOf0( Z, X ) }.
% 0.77/1.17 (163) {G0,W8,D3,L2,V3,M2} { aElementOf0( skol2( Z, Y ), Y ), alpha1( X, Y
% 0.77/1.17 ) }.
% 0.77/1.17 (164) {G0,W8,D3,L2,V2,M2} { ! aElementOf0( skol2( X, Y ), X ), alpha1( X,
% 0.77/1.17 Y ) }.
% 0.77/1.17 (165) {G0,W9,D2,L4,V2,M4} { ! aSet0( X ), ! isFinite0( X ), ! aSubsetOf0(
% 0.77/1.17 Y, X ), isFinite0( Y ) }.
% 0.77/1.17 (166) {G0,W2,D2,L1,V0,M1} { aSet0( xA ) }.
% 0.77/1.17 (167) {G0,W3,D2,L1,V0,M1} { ! aSubsetOf0( xA, xA ) }.
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Total Proof:
% 0.77/1.17
% 0.77/1.17 subsumption: (10) {G0,W10,D2,L4,V2,M4} I { ! aSet0( X ), ! aSet0( Y ), !
% 0.77/1.17 alpha1( X, Y ), aSubsetOf0( Y, X ) }.
% 0.77/1.17 parent0: (161) {G0,W10,D2,L4,V2,M4} { ! aSet0( X ), ! aSet0( Y ), ! alpha1
% 0.77/1.17 ( X, Y ), aSubsetOf0( Y, X ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 X := X
% 0.77/1.17 Y := Y
% 0.77/1.17 end
% 0.77/1.17 permutation0:
% 0.77/1.17 0 ==> 0
% 0.77/1.17 1 ==> 1
% 0.77/1.17 2 ==> 2
% 0.77/1.17 3 ==> 3
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 subsumption: (12) {G0,W8,D3,L2,V3,M2} I { aElementOf0( skol2( Z, Y ), Y ),
% 0.77/1.17 alpha1( X, Y ) }.
% 0.77/1.17 parent0: (163) {G0,W8,D3,L2,V3,M2} { aElementOf0( skol2( Z, Y ), Y ),
% 0.77/1.17 alpha1( X, Y ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 X := X
% 0.77/1.17 Y := Y
% 0.77/1.17 Z := Z
% 0.77/1.17 end
% 0.77/1.17 permutation0:
% 0.77/1.17 0 ==> 0
% 0.77/1.17 1 ==> 1
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 subsumption: (13) {G0,W8,D3,L2,V2,M2} I { ! aElementOf0( skol2( X, Y ), X )
% 0.77/1.17 , alpha1( X, Y ) }.
% 0.77/1.17 parent0: (164) {G0,W8,D3,L2,V2,M2} { ! aElementOf0( skol2( X, Y ), X ),
% 0.77/1.17 alpha1( X, Y ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 X := X
% 0.77/1.17 Y := Y
% 0.77/1.17 end
% 0.77/1.17 permutation0:
% 0.77/1.17 0 ==> 0
% 0.77/1.17 1 ==> 1
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 subsumption: (15) {G0,W2,D2,L1,V0,M1} I { aSet0( xA ) }.
% 0.77/1.17 parent0: (166) {G0,W2,D2,L1,V0,M1} { aSet0( xA ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 permutation0:
% 0.77/1.17 0 ==> 0
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 subsumption: (16) {G0,W3,D2,L1,V0,M1} I { ! aSubsetOf0( xA, xA ) }.
% 0.77/1.17 parent0: (167) {G0,W3,D2,L1,V0,M1} { ! aSubsetOf0( xA, xA ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 permutation0:
% 0.77/1.17 0 ==> 0
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 resolution: (193) {G1,W7,D2,L3,V0,M3} { ! aSet0( xA ), ! aSet0( xA ), !
% 0.77/1.17 alpha1( xA, xA ) }.
% 0.77/1.17 parent0[0]: (16) {G0,W3,D2,L1,V0,M1} I { ! aSubsetOf0( xA, xA ) }.
% 0.77/1.17 parent1[3]: (10) {G0,W10,D2,L4,V2,M4} I { ! aSet0( X ), ! aSet0( Y ), !
% 0.77/1.17 alpha1( X, Y ), aSubsetOf0( Y, X ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 substitution1:
% 0.77/1.17 X := xA
% 0.77/1.17 Y := xA
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 factor: (194) {G1,W5,D2,L2,V0,M2} { ! aSet0( xA ), ! alpha1( xA, xA ) }.
% 0.77/1.17 parent0[0, 1]: (193) {G1,W7,D2,L3,V0,M3} { ! aSet0( xA ), ! aSet0( xA ), !
% 0.77/1.17 alpha1( xA, xA ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 resolution: (196) {G1,W3,D2,L1,V0,M1} { ! alpha1( xA, xA ) }.
% 0.77/1.17 parent0[0]: (194) {G1,W5,D2,L2,V0,M2} { ! aSet0( xA ), ! alpha1( xA, xA )
% 0.77/1.17 }.
% 0.77/1.17 parent1[0]: (15) {G0,W2,D2,L1,V0,M1} I { aSet0( xA ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 substitution1:
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 subsumption: (69) {G1,W3,D2,L1,V0,M1} R(10,16);f;r(15) { ! alpha1( xA, xA )
% 0.77/1.17 }.
% 0.77/1.17 parent0: (196) {G1,W3,D2,L1,V0,M1} { ! alpha1( xA, xA ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 permutation0:
% 0.77/1.17 0 ==> 0
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 resolution: (197) {G1,W5,D3,L1,V1,M1} { aElementOf0( skol2( X, xA ), xA )
% 0.77/1.17 }.
% 0.77/1.17 parent0[0]: (69) {G1,W3,D2,L1,V0,M1} R(10,16);f;r(15) { ! alpha1( xA, xA )
% 0.77/1.17 }.
% 0.77/1.17 parent1[1]: (12) {G0,W8,D3,L2,V3,M2} I { aElementOf0( skol2( Z, Y ), Y ),
% 0.77/1.17 alpha1( X, Y ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 substitution1:
% 0.77/1.17 X := xA
% 0.77/1.17 Y := xA
% 0.77/1.17 Z := X
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 subsumption: (121) {G2,W5,D3,L1,V1,M1} R(12,69) { aElementOf0( skol2( X, xA
% 0.77/1.17 ), xA ) }.
% 0.77/1.17 parent0: (197) {G1,W5,D3,L1,V1,M1} { aElementOf0( skol2( X, xA ), xA ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 X := X
% 0.77/1.17 end
% 0.77/1.17 permutation0:
% 0.77/1.17 0 ==> 0
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 resolution: (198) {G1,W5,D3,L1,V0,M1} { ! aElementOf0( skol2( xA, xA ), xA
% 0.77/1.17 ) }.
% 0.77/1.17 parent0[0]: (69) {G1,W3,D2,L1,V0,M1} R(10,16);f;r(15) { ! alpha1( xA, xA )
% 0.77/1.17 }.
% 0.77/1.17 parent1[1]: (13) {G0,W8,D3,L2,V2,M2} I { ! aElementOf0( skol2( X, Y ), X )
% 0.77/1.17 , alpha1( X, Y ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 substitution1:
% 0.77/1.17 X := xA
% 0.77/1.17 Y := xA
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 resolution: (199) {G2,W0,D0,L0,V0,M0} { }.
% 0.77/1.17 parent0[0]: (198) {G1,W5,D3,L1,V0,M1} { ! aElementOf0( skol2( xA, xA ), xA
% 0.77/1.17 ) }.
% 0.77/1.17 parent1[0]: (121) {G2,W5,D3,L1,V1,M1} R(12,69) { aElementOf0( skol2( X, xA
% 0.77/1.17 ), xA ) }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 substitution1:
% 0.77/1.17 X := xA
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 subsumption: (146) {G3,W0,D0,L0,V0,M0} R(13,69);r(121) { }.
% 0.77/1.17 parent0: (199) {G2,W0,D0,L0,V0,M0} { }.
% 0.77/1.17 substitution0:
% 0.77/1.17 end
% 0.77/1.17 permutation0:
% 0.77/1.17 end
% 0.77/1.17
% 0.77/1.17 Proof check complete!
% 0.77/1.17
% 0.77/1.17 Memory use:
% 0.77/1.17
% 0.77/1.17 space for terms: 1796
% 0.77/1.17 space for clauses: 6464
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 clauses generated: 383
% 0.77/1.17 clauses kept: 147
% 0.77/1.17 clauses selected: 41
% 0.77/1.17 clauses deleted: 0
% 0.77/1.17 clauses inuse deleted: 0
% 0.77/1.17
% 0.77/1.17 subsentry: 410
% 0.77/1.17 literals s-matched: 301
% 0.77/1.17 literals matched: 301
% 0.77/1.17 full subsumption: 23
% 0.77/1.17
% 0.77/1.17 checksum: 1022468059
% 0.77/1.17
% 0.77/1.17
% 0.77/1.17 Bliksem ended
%------------------------------------------------------------------------------