%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX198-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n009.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 May 5 06:56:47 PM UTC 2026
% Result : Timeout 299.49s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX198-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.16/0.33 % Computer : n009.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % DateTime : Tue May 5 11:08:55 EDT 2026
% 0.16/0.33 % CPUTime :
% 7.83/8.23 *** allocated 10000 integers for termspace/termends
% 7.83/8.23 *** allocated 10000 integers for clauses
% 7.83/8.23 *** allocated 10000 integers for justifications
% 7.83/8.23 Bliksem 1.12
% 7.83/8.23
% 7.83/8.23
% 7.83/8.23 Automatic Strategy Selection
% 7.83/8.23
% 7.83/8.23 Clauses:
% 7.83/8.23 [
% 7.83/8.23 [ =( ltNat( z, z ), bfalse ) ],
% 7.83/8.23 [ =( ltNat( z, s( X ) ), btrue ) ],
% 7.83/8.23 [ =( ltNat( s( X ), z ), bfalse ) ],
% 7.83/8.23 [ =( ltNat( s( X ), s( Y ) ), ltNat( X, Y ) ) ],
% 7.83/8.23 [ =( leqNat( z, X ), btrue ) ],
% 7.83/8.23 [ =( leqNat( s( X ), z ), bfalse ) ],
% 7.83/8.23 [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ],
% 7.83/8.23 [ =( lengthNat( nil ), z ) ],
% 7.83/8.23 [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ],
% 7.83/8.23 [ =( impl( btrue, X ), X ) ],
% 7.83/8.23 [ =( impl( bfalse, X ), btrue ) ],
% 7.83/8.23 [ =( append( nil, X ), X ) ],
% 7.83/8.23 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 7.83/8.23 [ =( rev( nil ), nil ) ],
% 7.83/8.23 [ =( rev( cons( X, Y ) ), append( rev( Y ), cons( X, nil ) ) ) ],
% 7.83/8.23 [ =( andb( btrue, X ), X ) ],
% 7.83/8.23 [ =( andb( bfalse, X ), bfalse ) ],
% 7.83/8.23 [ =( usorted( nil ), btrue ) ],
% 7.83/8.23 [ =( usorted( cons( X, nil ) ), btrue ) ],
% 7.83/8.23 [ =( usorted( cons( X, cons( Y, Z ) ) ), andb( ltNat( X, Y ), usorted(
% 7.83/8.23 cons( Y, Z ) ) ) ) ],
% 7.83/8.23 [ =( allsmall( X, nil ), btrue ) ],
% 7.83/8.23 [ =( allsmall( X, cons( Y, Z ) ), andb( ltNat( Y, X ), allsmall( X, Z )
% 7.83/8.23 ) ) ],
% 7.83/8.23 [ =( pallsmall( X ), impl( eq2( usorted( rev( X ) ), btrue ), impl( eq2(
% 7.83/8.23 allsmall( s( z ), X ), btrue ), eq2( leqNat( lengthNat( X ), s( s( z ) )
% 7.83/8.23 ), btrue ) ) ) ) ],
% 7.83/8.23 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 7.83/8.23 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 7.83/8.23 [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ],
% 7.83/8.23 [ =( eq( z, s( X ) ), bfalse ) ],
% 7.83/8.23 [ =( eq( s( X ), z ), bfalse ) ],
% 7.83/8.23 [ =( eq( X, X ), btrue ) ],
% 7.83/8.23 [ =( eq2( X, X ), btrue ) ],
% 7.83/8.23 [ ~( =( eq2( pallsmall( X ), bfalse ), btrue ) ) ]
% 7.83/8.23 ] .
% 7.83/8.23
% 7.83/8.23
% 7.83/8.23 percentage equality = 1.000000, percentage horn = 1.000000
% 7.83/8.23 This is a pure equality problem
% 7.83/8.23
% 7.83/8.23
% 7.83/8.23
% 7.83/8.23 Options Used:
% 7.83/8.23
% 7.83/8.23 useres = 1
% 7.83/8.23 useparamod = 1
% 7.83/8.23 useeqrefl = 1
% 7.83/8.23 useeqfact = 1
% 7.83/8.23 usefactor = 1
% 7.83/8.23 usesimpsplitting = 0
% 7.83/8.23 usesimpdemod = 5
% 7.83/8.23 usesimpres = 3
% 7.83/8.23
% 7.83/8.23 resimpinuse = 1000
% 7.83/8.23 resimpclauses = 20000
% 7.83/8.23 substype = eqrewr
% 7.83/8.23 backwardsubs = 1
% 7.83/8.23 selectoldest = 5
% 7.83/8.23
% 7.83/8.23 litorderings [0] = split
% 7.83/8.23 litorderings [1] = extend the termordering, first sorting on arguments
% 7.83/8.23
% 7.83/8.23 termordering = kbo
% 7.83/8.23
% 7.83/8.23 litapriori = 0
% 7.83/8.23 termapriori = 1
% 7.83/8.23 litaposteriori = 0
% 7.83/8.23 termaposteriori = 0
% 7.83/8.23 demodaposteriori = 0
% 7.83/8.23 ordereqreflfact = 0
% 7.83/8.23
% 7.83/8.23 litselect = negord
% 7.83/8.23
% 7.83/8.23 maxweight = 15
% 7.83/8.23 maxdepth = 30000
% 7.83/8.23 maxlength = 115
% 7.83/8.23 maxnrvars = 195
% 7.83/8.23 excuselevel = 1
% 7.83/8.23 increasemaxweight = 1
% 7.83/8.23
% 7.83/8.23 maxselected = 10000000
% 7.83/8.23 maxnrclauses = 10000000
% 7.83/8.23
% 7.83/8.23 showgenerated = 0
% 7.83/8.23 showkept = 0
% 7.83/8.23 showselected = 0
% 7.83/8.23 showdeleted = 0
% 7.83/8.23 showresimp = 1
% 7.83/8.23 showstatus = 2000
% 7.83/8.23
% 7.83/8.23 prologoutput = 1
% 7.83/8.23 nrgoals = 5000000
% 7.83/8.23 totalproof = 1
% 7.83/8.23
% 7.83/8.23 Symbols occurring in the translation:
% 7.83/8.23
% 7.83/8.23 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 7.83/8.23 . [1, 2] (w:1, o:31, a:1, s:1, b:0),
% 7.83/8.23 ! [4, 1] (w:0, o:21, a:1, s:1, b:0),
% 7.83/8.23 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.83/8.23 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.83/8.23 z [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 7.83/8.23 ltNat [40, 2] (w:1, o:56, a:1, s:1, b:0),
% 7.83/8.23 bfalse [41, 0] (w:1, o:10, a:1, s:1, b:0),
% 7.83/8.23 s [43, 1] (w:1, o:27, a:1, s:1, b:0),
% 7.83/8.23 btrue [44, 0] (w:1, o:16, a:1, s:1, b:0),
% 7.83/8.23 leqNat [48, 2] (w:1, o:57, a:1, s:1, b:0),
% 7.83/8.23 nil [49, 0] (w:1, o:19, a:1, s:1, b:0),
% 7.83/8.23 lengthNat [50, 1] (w:1, o:28, a:1, s:1, b:0),
% 7.83/8.23 cons [52, 2] (w:1, o:58, a:1, s:1, b:0),
% 7.83/8.23 impl [54, 2] (w:1, o:59, a:1, s:1, b:0),
% 7.83/8.23 append [55, 2] (w:1, o:60, a:1, s:1, b:0),
% 7.83/8.23 rev [56, 1] (w:1, o:26, a:1, s:1, b:0),
% 7.83/8.23 andb [57, 2] (w:1, o:61, a:1, s:1, b:0),
% 7.83/8.23 usorted [58, 1] (w:1, o:29, a:1, s:1, b:0),
% 7.83/8.23 allsmall [61, 2] (w:1, o:62, a:1, s:1, b:0),
% 7.83/8.23 pallsmall [62, 1] (w:1, o:30, a:1, s:1, b:0),
% 7.83/8.23 eq2 [63, 2] (w:1, o:63, a:1, s:1, b:0),
% 7.83/8.23 eq [64, 2] (w:1, o:64, a:1, s:1, b:0).
% 7.83/8.23
% 7.83/8.23
% 7.83/8.23 Starting Search:
% 7.83/8.23
% 7.83/8.23 Resimplifying inuse:
% 7.83/8.23 Done
% 7.83/8.23
% 7.83/8.23 Failed to find proof!
% 7.83/8.23 maxweight = 15
% 7.83/8.23 maxnrclauses = 10000000
% 7.83/8.23 Generated: 270
% 7.83/8.23 Kept: 60
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 16
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 16
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 314
% 69.12/69.53 Kept: 67
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 17
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 17
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 348
% 69.12/69.53 Kept: 72
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 18
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 18
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 401
% 69.12/69.53 Kept: 77
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 19
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 19
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 620
% 69.12/69.53 Kept: 95
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 20
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 20
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 891
% 69.12/69.53 Kept: 119
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 21
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 21
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 1298
% 69.12/69.53 Kept: 134
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 22
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 22
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 1650
% 69.12/69.53 Kept: 150
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 23
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 23
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 2828
% 69.12/69.53 Kept: 201
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 24
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 24
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 3881
% 69.12/69.53 Kept: 226
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 25
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 25
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 5436
% 69.12/69.53 Kept: 274
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 26
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 26
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 8764
% 69.12/69.53 Kept: 345
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 27
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 27
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 17334
% 69.12/69.53 Kept: 593
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 28
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 28
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 21631
% 69.12/69.53 Kept: 669
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 29
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 29
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 33451
% 69.12/69.53 Kept: 846
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 30
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 30
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 53367
% 69.12/69.53 Kept: 1120
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 31
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 31
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 85215
% 69.12/69.53 Kept: 1491
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 32
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 32
% 69.12/69.53 maxnrclauses = 10000000
% 69.12/69.53 Generated: 136949
% 69.12/69.53 Kept: 1901
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 The strategy used was not complete!
% 69.12/69.53
% 69.12/69.53 Increased maxweight to 33
% 69.12/69.53
% 69.12/69.53 Starting Search:
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 Intermediate Status:
% 69.12/69.53 Generated: 78486
% 69.12/69.53 Kept: 2014
% 69.12/69.53 Inuse: 1119
% 69.12/69.53 Deleted: 352
% 69.12/69.53 Deletedinuse: 19
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53
% 69.12/69.53 Intermediate Status:
% 69.12/69.53 Generated: 196867
% 69.12/69.53 Kept: 4014
% 69.12/69.53 Inuse: 2396
% 69.12/69.53 Deleted: 1201
% 69.12/69.53 Deletedinuse: 188
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Resimplifying inuse:
% 69.12/69.53 Done
% 69.12/69.53
% 69.12/69.53 Failed to find proof!
% 69.12/69.53 maxweight = 33
% 143.52/143.96 maxnrclauses = 10000000
% 143.52/143.96 Generated: 266930
% 143.52/143.96 Kept: 4420
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 The strategy used was not complete!
% 143.52/143.96
% 143.52/143.96 Increased maxweight to 34
% 143.52/143.96
% 143.52/143.96 Starting Search:
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 59450
% 143.52/143.96 Kept: 2001
% 143.52/143.96 Inuse: 1002
% 143.52/143.96 Deleted: 245
% 143.52/143.96 Deletedinuse: 12
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 211075
% 143.52/143.96 Kept: 4004
% 143.52/143.96 Inuse: 2160
% 143.52/143.96 Deleted: 899
% 143.52/143.96 Deletedinuse: 171
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 387843
% 143.52/143.96 Kept: 6007
% 143.52/143.96 Inuse: 3697
% 143.52/143.96 Deleted: 1806
% 143.52/143.96 Deletedinuse: 321
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Failed to find proof!
% 143.52/143.96 maxweight = 34
% 143.52/143.96 maxnrclauses = 10000000
% 143.52/143.96 Generated: 449931
% 143.52/143.96 Kept: 6319
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 The strategy used was not complete!
% 143.52/143.96
% 143.52/143.96 Increased maxweight to 35
% 143.52/143.96
% 143.52/143.96 Starting Search:
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 39619
% 143.52/143.96 Kept: 2009
% 143.52/143.96 Inuse: 810
% 143.52/143.96 Deleted: 193
% 143.52/143.96 Deletedinuse: 11
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 204714
% 143.52/143.96 Kept: 4013
% 143.52/143.96 Inuse: 2013
% 143.52/143.96 Deleted: 694
% 143.52/143.96 Deletedinuse: 140
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 397969
% 143.52/143.96 Kept: 6015
% 143.52/143.96 Inuse: 3375
% 143.52/143.96 Deleted: 1808
% 143.52/143.96 Deletedinuse: 319
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Failed to find proof!
% 143.52/143.96 maxweight = 35
% 143.52/143.96 maxnrclauses = 10000000
% 143.52/143.96 Generated: 577744
% 143.52/143.96 Kept: 6597
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 The strategy used was not complete!
% 143.52/143.96
% 143.52/143.96 Increased maxweight to 36
% 143.52/143.96
% 143.52/143.96 Starting Search:
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 33582
% 143.52/143.96 Kept: 2000
% 143.52/143.96 Inuse: 696
% 143.52/143.96 Deleted: 155
% 143.52/143.96 Deletedinuse: 11
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 186447
% 143.52/143.96 Kept: 4002
% 143.52/143.96 Inuse: 1878
% 143.52/143.96 Deleted: 638
% 143.52/143.96 Deletedinuse: 136
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 290139
% 143.52/143.96 Kept: 6002
% 143.52/143.96 Inuse: 2795
% 143.52/143.96 Deleted: 1411
% 143.52/143.96 Deletedinuse: 301
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 437164
% 143.52/143.96 Kept: 8005
% 143.52/143.96 Inuse: 3804
% 143.52/143.96 Deleted: 2259
% 143.52/143.96 Deletedinuse: 504
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 506152
% 143.52/143.96 Kept: 10005
% 143.52/143.96 Inuse: 4230
% 143.52/143.96 Deleted: 2426
% 143.52/143.96 Deletedinuse: 551
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 601772
% 143.52/143.96 Kept: 12005
% 143.52/143.96 Inuse: 4841
% 143.52/143.96 Deleted: 2710
% 143.52/143.96 Deletedinuse: 606
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 701938
% 143.52/143.96 Kept: 14014
% 143.52/143.96 Inuse: 5362
% 143.52/143.96 Deleted: 3002
% 143.52/143.96 Deletedinuse: 672
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 763511
% 143.52/143.96 Kept: 16015
% 143.52/143.96 Inuse: 5997
% 143.52/143.96 Deleted: 3468
% 143.52/143.96 Deletedinuse: 741
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 837182
% 143.52/143.96 Kept: 18018
% 143.52/143.96 Inuse: 6840
% 143.52/143.96 Deleted: 4098
% 143.52/143.96 Deletedinuse: 831
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying clauses:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 938380
% 143.52/143.96 Kept: 20018
% 143.52/143.96 Inuse: 7993
% 143.52/143.96 Deleted: 8310
% 143.52/143.96 Deletedinuse: 928
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 1064366
% 143.52/143.96 Kept: 22021
% 143.52/143.96 Inuse: 9138
% 143.52/143.96 Deleted: 8504
% 143.52/143.96 Deletedinuse: 1053
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 1222683
% 143.52/143.96 Kept: 24024
% 143.52/143.96 Inuse: 10860
% 143.52/143.96 Deleted: 8883
% 143.52/143.96 Deletedinuse: 1175
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 1439239
% 143.52/143.96 Kept: 26024
% 143.52/143.96 Inuse: 13056
% 143.52/143.96 Deleted: 9612
% 143.52/143.96 Deletedinuse: 1333
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96
% 143.52/143.96 Intermediate Status:
% 143.52/143.96 Generated: 1722756
% 143.52/143.96 Kept: 28026
% 143.52/143.96 Inuse: 16388
% 143.52/143.96 Deleted: 11275
% 143.52/143.96 Deletedinuse: 1548
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Resimplifying inuse:
% 143.52/143.96 Done
% 143.52/143.96
% 143.52/143.96 Failed to find proof!
% 256.07/256.65 maxweight = 36
% 256.07/256.65 maxnrclauses = 10000000
% 256.07/256.65 Generated: 1868924
% 256.07/256.65 Kept: 28673
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 The strategy used was not complete!
% 256.07/256.65
% 256.07/256.65 Increased maxweight to 37
% 256.07/256.65
% 256.07/256.65 Starting Search:
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 33281
% 256.07/256.65 Kept: 2073
% 256.07/256.65 Inuse: 655
% 256.07/256.65 Deleted: 153
% 256.07/256.65 Deletedinuse: 12
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 183750
% 256.07/256.65 Kept: 4086
% 256.07/256.65 Inuse: 1793
% 256.07/256.65 Deleted: 615
% 256.07/256.65 Deletedinuse: 111
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 262113
% 256.07/256.65 Kept: 6088
% 256.07/256.65 Inuse: 2535
% 256.07/256.65 Deleted: 1182
% 256.07/256.65 Deletedinuse: 255
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 504790
% 256.07/256.65 Kept: 8089
% 256.07/256.65 Inuse: 3957
% 256.07/256.65 Deleted: 2327
% 256.07/256.65 Deletedinuse: 429
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 599166
% 256.07/256.65 Kept: 10127
% 256.07/256.65 Inuse: 4455
% 256.07/256.65 Deleted: 2754
% 256.07/256.65 Deletedinuse: 615
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 678643
% 256.07/256.65 Kept: 12148
% 256.07/256.65 Inuse: 4948
% 256.07/256.65 Deleted: 2945
% 256.07/256.65 Deletedinuse: 649
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 774337
% 256.07/256.65 Kept: 14159
% 256.07/256.65 Inuse: 5461
% 256.07/256.65 Deleted: 3179
% 256.07/256.65 Deletedinuse: 707
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 892161
% 256.07/256.65 Kept: 16161
% 256.07/256.65 Inuse: 6088
% 256.07/256.65 Deleted: 3507
% 256.07/256.65 Deletedinuse: 761
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 976568
% 256.07/256.65 Kept: 18170
% 256.07/256.65 Inuse: 6596
% 256.07/256.65 Deleted: 3846
% 256.07/256.65 Deletedinuse: 818
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying clauses:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 1047539
% 256.07/256.65 Kept: 20179
% 256.07/256.65 Inuse: 7309
% 256.07/256.65 Deleted: 8117
% 256.07/256.65 Deletedinuse: 902
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 1148717
% 256.07/256.65 Kept: 22181
% 256.07/256.65 Inuse: 8154
% 256.07/256.65 Deleted: 8254
% 256.07/256.65 Deletedinuse: 978
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 1334022
% 256.07/256.65 Kept: 24184
% 256.07/256.65 Inuse: 9208
% 256.07/256.65 Deleted: 8509
% 256.07/256.65 Deletedinuse: 1098
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 1482321
% 256.07/256.65 Kept: 26186
% 256.07/256.65 Inuse: 10316
% 256.07/256.65 Deleted: 8800
% 256.07/256.65 Deletedinuse: 1207
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 1632349
% 256.07/256.65 Kept: 28186
% 256.07/256.65 Inuse: 11766
% 256.07/256.65 Deleted: 9312
% 256.07/256.65 Deletedinuse: 1301
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 1809932
% 256.07/256.65 Kept: 30188
% 256.07/256.65 Inuse: 13472
% 256.07/256.65 Deleted: 10134
% 256.07/256.65 Deletedinuse: 1414
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 2067798
% 256.07/256.65 Kept: 32190
% 256.07/256.65 Inuse: 15702
% 256.07/256.65 Deleted: 11514
% 256.07/256.65 Deletedinuse: 1566
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 2356769
% 256.07/256.65 Kept: 34190
% 256.07/256.65 Inuse: 18640
% 256.07/256.65 Deleted: 13481
% 256.07/256.65 Deletedinuse: 1774
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Failed to find proof!
% 256.07/256.65 maxweight = 37
% 256.07/256.65 maxnrclauses = 10000000
% 256.07/256.65 Generated: 2694348
% 256.07/256.65 Kept: 35589
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 The strategy used was not complete!
% 256.07/256.65
% 256.07/256.65 Increased maxweight to 38
% 256.07/256.65
% 256.07/256.65 Starting Search:
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 27655
% 256.07/256.65 Kept: 2016
% 256.07/256.65 Inuse: 618
% 256.07/256.65 Deleted: 157
% 256.07/256.65 Deletedinuse: 11
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 127801
% 256.07/256.65 Kept: 4018
% 256.07/256.65 Inuse: 1482
% 256.07/256.65 Deleted: 435
% 256.07/256.65 Deletedinuse: 88
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 223177
% 256.07/256.65 Kept: 6019
% 256.07/256.65 Inuse: 2250
% 256.07/256.65 Deleted: 913
% 256.07/256.65 Deletedinuse: 222
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65
% 256.07/256.65 Intermediate Status:
% 256.07/256.65 Generated: 373129
% 256.07/256.65 Kept: 8041
% 256.07/256.65 Inuse: 3293
% 256.07/256.65 Deleted: 1815
% 256.07/256.65 Deletedinuse: 357
% 256.07/256.65
% 256.07/256.65 Resimplifying inuse:
% 256.07/256.65 Done
% 256.07/256.65
% 256.07/256.65 Resimplifying Terminated
% 299.49/300.03 Bliksem ended
%------------------------------------------------------------------------------