%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SET013-4 : TPTP v8.1.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.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:45:18 EDT 2022
% Result : Unsatisfiable 13.81s 14.20s
% Output : Refutation 13.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SET013-4 : TPTP v8.1.0. Bugfixed v1.2.1.
% 0.04/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n020.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 : Sun Jul 10 05:38:13 EDT 2022
% 0.12/0.33 % CPUTime :
% 13.81/14.20 *** allocated 10000 integers for termspace/termends
% 13.81/14.20 *** allocated 10000 integers for clauses
% 13.81/14.20 *** allocated 10000 integers for justifications
% 13.81/14.20 Bliksem 1.12
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Automatic Strategy Selection
% 13.81/14.20
% 13.81/14.20 Clauses:
% 13.81/14.20 [
% 13.81/14.20 [ ~( member( X, Y ) ), 'little_set'( X ) ],
% 13.81/14.20 [ 'little_set'( f1( X, Y ) ), =( X, Y ) ],
% 13.81/14.20 [ member( f1( X, Y ), X ), member( f1( X, Y ), Y ), =( X, Y ) ],
% 13.81/14.20 [ ~( member( f1( X, Y ), X ) ), ~( member( f1( X, Y ), Y ) ), =( X, Y )
% 13.81/14.20 ],
% 13.81/14.20 [ ~( member( X, intersection( Y, Z ) ) ), member( X, Y ) ],
% 13.81/14.20 [ ~( member( X, intersection( Y, Z ) ) ), member( X, Z ) ],
% 13.81/14.20 [ member( X, intersection( Y, Z ) ), ~( member( X, Y ) ), ~( member( X,
% 13.81/14.20 Z ) ) ],
% 13.81/14.20 [ ~( member( X, 'empty_set' ) ) ],
% 13.81/14.20 [ member( X, 'universal_set' ), ~( 'little_set'( X ) ) ],
% 13.81/14.20 [ =( intersection( as, bs ), cs ) ],
% 13.81/14.20 [ =( intersection( bs, as ), ds ) ],
% 13.81/14.20 [ ~( =( cs, ds ) ) ]
% 13.81/14.20 ] .
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 percentage equality = 0.260870, percentage horn = 0.833333
% 13.81/14.20 This is a problem with some equality
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Options Used:
% 13.81/14.20
% 13.81/14.20 useres = 1
% 13.81/14.20 useparamod = 1
% 13.81/14.20 useeqrefl = 1
% 13.81/14.20 useeqfact = 1
% 13.81/14.20 usefactor = 1
% 13.81/14.20 usesimpsplitting = 0
% 13.81/14.20 usesimpdemod = 5
% 13.81/14.20 usesimpres = 3
% 13.81/14.20
% 13.81/14.20 resimpinuse = 1000
% 13.81/14.20 resimpclauses = 20000
% 13.81/14.20 substype = eqrewr
% 13.81/14.20 backwardsubs = 1
% 13.81/14.20 selectoldest = 5
% 13.81/14.20
% 13.81/14.20 litorderings [0] = split
% 13.81/14.20 litorderings [1] = extend the termordering, first sorting on arguments
% 13.81/14.20
% 13.81/14.20 termordering = kbo
% 13.81/14.20
% 13.81/14.20 litapriori = 0
% 13.81/14.20 termapriori = 1
% 13.81/14.20 litaposteriori = 0
% 13.81/14.20 termaposteriori = 0
% 13.81/14.20 demodaposteriori = 0
% 13.81/14.20 ordereqreflfact = 0
% 13.81/14.20
% 13.81/14.20 litselect = negord
% 13.81/14.20
% 13.81/14.20 maxweight = 15
% 13.81/14.20 maxdepth = 30000
% 13.81/14.20 maxlength = 115
% 13.81/14.20 maxnrvars = 195
% 13.81/14.20 excuselevel = 1
% 13.81/14.20 increasemaxweight = 1
% 13.81/14.20
% 13.81/14.20 maxselected = 10000000
% 13.81/14.20 maxnrclauses = 10000000
% 13.81/14.20
% 13.81/14.20 showgenerated = 0
% 13.81/14.20 showkept = 0
% 13.81/14.20 showselected = 0
% 13.81/14.20 showdeleted = 0
% 13.81/14.20 showresimp = 1
% 13.81/14.20 showstatus = 2000
% 13.81/14.20
% 13.81/14.20 prologoutput = 1
% 13.81/14.20 nrgoals = 5000000
% 13.81/14.20 totalproof = 1
% 13.81/14.20
% 13.81/14.20 Symbols occurring in the translation:
% 13.81/14.20
% 13.81/14.20 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 13.81/14.20 . [1, 2] (w:1, o:24, a:1, s:1, b:0),
% 13.81/14.20 ! [4, 1] (w:0, o:18, a:1, s:1, b:0),
% 13.81/14.20 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 13.81/14.20 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 13.81/14.20 member [41, 2] (w:1, o:49, a:1, s:1, b:0),
% 13.81/14.20 'little_set' [42, 1] (w:1, o:23, a:1, s:1, b:0),
% 13.81/14.20 f1 [43, 2] (w:1, o:50, a:1, s:1, b:0),
% 13.81/14.20 intersection [45, 2] (w:1, o:51, a:1, s:1, b:0),
% 13.81/14.20 'empty_set' [46, 0] (w:1, o:13, a:1, s:1, b:0),
% 13.81/14.20 'universal_set' [47, 0] (w:1, o:14, a:1, s:1, b:0),
% 13.81/14.20 as [48, 0] (w:1, o:15, a:1, s:1, b:0),
% 13.81/14.20 bs [49, 0] (w:1, o:16, a:1, s:1, b:0),
% 13.81/14.20 cs [50, 0] (w:1, o:17, a:1, s:1, b:0),
% 13.81/14.20 ds [51, 0] (w:1, o:12, a:1, s:1, b:0).
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Starting Search:
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 3615
% 13.81/14.20 Kept: 2050
% 13.81/14.20 Inuse: 67
% 13.81/14.20 Deleted: 11
% 13.81/14.20 Deletedinuse: 1
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 9682
% 13.81/14.20 Kept: 4073
% 13.81/14.20 Inuse: 146
% 13.81/14.20 Deleted: 28
% 13.81/14.20 Deletedinuse: 5
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 16891
% 13.81/14.20 Kept: 6077
% 13.81/14.20 Inuse: 195
% 13.81/14.20 Deleted: 36
% 13.81/14.20 Deletedinuse: 13
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 26489
% 13.81/14.20 Kept: 8105
% 13.81/14.20 Inuse: 250
% 13.81/14.20 Deleted: 95
% 13.81/14.20 Deletedinuse: 52
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 41729
% 13.81/14.20 Kept: 10106
% 13.81/14.20 Inuse: 300
% 13.81/14.20 Deleted: 107
% 13.81/14.20 Deletedinuse: 55
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 50430
% 13.81/14.20 Kept: 12122
% 13.81/14.20 Inuse: 349
% 13.81/14.20 Deleted: 121
% 13.81/14.20 Deletedinuse: 65
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 65571
% 13.81/14.20 Kept: 14154
% 13.81/14.20 Inuse: 403
% 13.81/14.20 Deleted: 143
% 13.81/14.20 Deletedinuse: 71
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 104765
% 13.81/14.20 Kept: 16176
% 13.81/14.20 Inuse: 470
% 13.81/14.20 Deleted: 186
% 13.81/14.20 Deletedinuse: 71
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 149214
% 13.81/14.20 Kept: 18183
% 13.81/14.20 Inuse: 558
% 13.81/14.20 Deleted: 250
% 13.81/14.20 Deletedinuse: 81
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying clauses:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 168743
% 13.81/14.20 Kept: 20258
% 13.81/14.20 Inuse: 608
% 13.81/14.20 Deleted: 5065
% 13.81/14.20 Deletedinuse: 126
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Intermediate Status:
% 13.81/14.20 Generated: 195885
% 13.81/14.20 Kept: 22260
% 13.81/14.20 Inuse: 660
% 13.81/14.20 Deleted: 5071
% 13.81/14.20 Deletedinuse: 128
% 13.81/14.20
% 13.81/14.20 Resimplifying inuse:
% 13.81/14.20 Done
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 Bliksems!, er is een bewijs:
% 13.81/14.20 % SZS status Unsatisfiable
% 13.81/14.20 % SZS output start Refutation
% 13.81/14.20
% 13.81/14.20 clause( 2, [ member( f1( X, Y ), X ), member( f1( X, Y ), Y ), =( X, Y ) ]
% 13.81/14.20 )
% 13.81/14.20 .
% 13.81/14.20 clause( 3, [ ~( member( f1( X, Y ), X ) ), ~( member( f1( X, Y ), Y ) ),
% 13.81/14.20 =( X, Y ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 4, [ ~( member( X, intersection( Y, Z ) ) ), member( X, Y ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 5, [ ~( member( X, intersection( Y, Z ) ) ), member( X, Z ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 6, [ member( X, intersection( Y, Z ) ), ~( member( X, Y ) ), ~(
% 13.81/14.20 member( X, Z ) ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 9, [ =( intersection( as, bs ), cs ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 10, [ =( intersection( bs, as ), ds ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 11, [ ~( =( cs, ds ) ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 90, [ ~( =( X, ds ) ), member( f1( X, cs ), X ), member( f1( X, cs
% 13.81/14.20 ), cs ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 173, [ ~( =( X, ds ) ), ~( member( f1( X, cs ), X ) ), ~( member(
% 13.81/14.20 f1( X, cs ), cs ) ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 174, [ ~( member( f1( ds, cs ), ds ) ), ~( member( f1( ds, cs ), cs
% 13.81/14.20 ) ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 209, [ ~( member( X, cs ) ), member( X, as ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 214, [ ~( member( X, ds ) ), member( X, bs ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 276, [ ~( member( X, cs ) ), member( X, bs ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 281, [ ~( member( X, ds ) ), member( X, as ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 382, [ member( X, cs ), ~( member( X, as ) ), ~( member( X, bs ) )
% 13.81/14.20 ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 387, [ member( X, ds ), ~( member( X, bs ) ), ~( member( X, as ) )
% 13.81/14.20 ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 11324, [ member( f1( ds, cs ), as ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 11326, [ member( f1( ds, cs ), bs ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 18346, [ member( f1( ds, cs ), cs ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 18509, [ ~( member( f1( ds, cs ), ds ) ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 22664, [ ~( member( f1( ds, cs ), as ) ) ] )
% 13.81/14.20 .
% 13.81/14.20 clause( 22719, [] )
% 13.81/14.20 .
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 % SZS output end Refutation
% 13.81/14.20 found a proof!
% 13.81/14.20
% 13.81/14.20 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 13.81/14.20
% 13.81/14.20 initialclauses(
% 13.81/14.20 [ clause( 22721, [ ~( member( X, Y ) ), 'little_set'( X ) ] )
% 13.81/14.20 , clause( 22722, [ 'little_set'( f1( X, Y ) ), =( X, Y ) ] )
% 13.81/14.20 , clause( 22723, [ member( f1( X, Y ), X ), member( f1( X, Y ), Y ), =( X,
% 13.81/14.20 Y ) ] )
% 13.81/14.20 , clause( 22724, [ ~( member( f1( X, Y ), X ) ), ~( member( f1( X, Y ), Y )
% 13.81/14.20 ), =( X, Y ) ] )
% 13.81/14.20 , clause( 22725, [ ~( member( X, intersection( Y, Z ) ) ), member( X, Y ) ]
% 13.81/14.20 )
% 13.81/14.20 , clause( 22726, [ ~( member( X, intersection( Y, Z ) ) ), member( X, Z ) ]
% 13.81/14.20 )
% 13.81/14.20 , clause( 22727, [ member( X, intersection( Y, Z ) ), ~( member( X, Y ) ),
% 13.81/14.20 ~( member( X, Z ) ) ] )
% 13.81/14.20 , clause( 22728, [ ~( member( X, 'empty_set' ) ) ] )
% 13.81/14.20 , clause( 22729, [ member( X, 'universal_set' ), ~( 'little_set'( X ) ) ]
% 13.81/14.20 )
% 13.81/14.20 , clause( 22730, [ =( intersection( as, bs ), cs ) ] )
% 13.81/14.20 , clause( 22731, [ =( intersection( bs, as ), ds ) ] )
% 13.81/14.20 , clause( 22732, [ ~( =( cs, ds ) ) ] )
% 13.81/14.20 ] ).
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 subsumption(
% 13.81/14.20 clause( 2, [ member( f1( X, Y ), X ), member( f1( X, Y ), Y ), =( X, Y ) ]
% 13.81/14.20 )
% 13.81/14.20 , clause( 22723, [ member( f1( X, Y ), X ), member( f1( X, Y ), Y ), =( X,
% 13.81/14.20 Y ) ] )
% 13.81/14.20 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 13.81/14.20 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 subsumption(
% 13.81/14.20 clause( 3, [ ~( member( f1( X, Y ), X ) ), ~( member( f1( X, Y ), Y ) ),
% 13.81/14.20 =( X, Y ) ] )
% 13.81/14.20 , clause( 22724, [ ~( member( f1( X, Y ), X ) ), ~( member( f1( X, Y ), Y )
% 13.81/14.20 ), =( X, Y ) ] )
% 13.81/14.20 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 13.81/14.20 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 subsumption(
% 13.81/14.20 clause( 4, [ ~( member( X, intersection( Y, Z ) ) ), member( X, Y ) ] )
% 13.81/14.20 , clause( 22725, [ ~( member( X, intersection( Y, Z ) ) ), member( X, Y ) ]
% 13.81/14.20 )
% 13.81/14.20 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 13.81/14.20 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 13.81/14.20
% 13.81/14.20
% 13.81/14.20 subsumption(
% 13.81/14.20 clause( 5, [ ~( member( X, intersection( Y, Z ) ) ), member( X, Z ) ] )
% 13.81/14.20 , clause(Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------