%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX201-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n016.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 298.36s 298.73s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX201-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.18/0.34 % Computer : n016.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % DateTime : Tue May 5 11:18:21 EDT 2026
% 0.18/0.35 % CPUTime :
% 8.44/8.87 *** allocated 10000 integers for termspace/termends
% 8.44/8.87 *** allocated 10000 integers for clauses
% 8.44/8.87 *** allocated 10000 integers for justifications
% 8.44/8.87 Bliksem 1.12
% 8.44/8.87
% 8.44/8.87
% 8.44/8.87 Automatic Strategy Selection
% 8.44/8.87
% 8.44/8.87 Clauses:
% 8.44/8.87 [
% 8.44/8.87 [ =( aux( X, Y, Z, pair2( T, U ) ), pair2( cons( Y, T ), U ) ) ],
% 8.44/8.87 [ =( aux2( X, Y, Z, T, btrue ), cons( X, merge( Y, cons( Z, T ) ) ) ) ]
% 8.44/8.87 ,
% 8.44/8.87 [ =( aux2( X, Y, Z, T, bfalse ), cons( Z, merge( cons( X, Y ), T ) ) ) ]
% 8.44/8.87 ,
% 8.44/8.87 [ =( aux3( X, Y, Z, pair2( T, U ) ), merge( msort( T ), msort( U ) ) ) ]
% 8.44/8.87 ,
% 8.44/8.87 [ =( aux4( X, Y, Z, btrue ), s( count( X, Z ) ) ) ],
% 8.44/8.87 [ =( aux4( X, Y, Z, bfalse ), count( X, Z ) ) ],
% 8.44/8.87 [ =( splitAtNat( z, X ), pair2( nil, X ) ) ],
% 8.44/8.87 [ =( splitAtNat( s( X ), nil ), pair2( nil, nil ) ) ],
% 8.44/8.87 [ =( splitAtNat( s( X ), cons( Y, Z ) ), aux( X, Y, Z, splitAtNat( X, Z
% 8.44/8.87 ) ) ) ],
% 8.44/8.87 [ =( leqNat( z, X ), btrue ) ],
% 8.44/8.87 [ =( leqNat( s( X ), z ), bfalse ) ],
% 8.44/8.87 [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ],
% 8.44/8.87 [ =( merge( nil, X ), X ) ],
% 8.44/8.87 [ =( merge( cons( X, Y ), nil ), cons( X, Y ) ) ],
% 8.44/8.87 [ =( merge( cons( X, Y ), cons( Z, T ) ), aux2( X, Y, Z, T, leqNat( X, Z
% 8.44/8.87 ) ) ) ],
% 8.44/8.87 [ =( lengthNat( nil ), z ) ],
% 8.44/8.87 [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ],
% 8.44/8.87 [ =( impl( btrue, X ), X ) ],
% 8.44/8.87 [ =( impl( bfalse, X ), btrue ) ],
% 8.44/8.87 [ =( div2( z ), z ) ],
% 8.44/8.87 [ =( div2( s( z ) ), z ) ],
% 8.44/8.87 [ =( div2( s( s( X ) ) ), s( div2( X ) ) ) ],
% 8.44/8.87 [ =( msort( nil ), nil ) ],
% 8.44/8.87 [ =( msort( cons( X, nil ) ), cons( X, nil ) ) ],
% 8.44/8.87 [ =( msort( cons( X, cons( Y, Z ) ) ), aux3( X, Y, Z, splitAtNat( div2(
% 8.44/8.87 lengthNat( cons( X, cons( Y, Z ) ) ) ), cons( X, cons( Y, Z ) ) ) ) ) ]
% 8.44/8.87 ,
% 8.44/8.87 [ =( count( X, nil ), z ) ],
% 8.44/8.87 [ =( count( X, cons( Y, Z ) ), aux4( X, Y, Z, eq( Y, X ) ) ) ],
% 8.44/8.87 [ =( 'prop_msort_permutation_wrong1'( X, Y ), impl( eq2( leqNat( count(
% 8.44/8.87 Y, X ), s( s( s( s( s( z ) ) ) ) ) ), bfalse ), eq( count( Y, X ), count(
% 8.44/8.87 s( Y ), msort( X ) ) ) ) ) ],
% 8.44/8.87 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 8.44/8.87 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 8.44/8.87 [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ],
% 8.44/8.87 [ =( eq( z, s( X ) ), bfalse ) ],
% 8.44/8.87 [ =( eq( s( X ), z ), bfalse ) ],
% 8.44/8.87 [ =( eq( X, X ), btrue ) ],
% 8.44/8.87 [ =( eq2( X, X ), btrue ) ],
% 8.44/8.87 [ ~( =( eq2( 'prop_msort_permutation_wrong1'( X, Y ), bfalse ), btrue )
% 8.44/8.87 ) ]
% 8.44/8.87 ] .
% 8.44/8.87
% 8.44/8.87
% 8.44/8.87 percentage equality = 1.000000, percentage horn = 1.000000
% 8.44/8.87 This is a pure equality problem
% 8.44/8.87
% 8.44/8.87
% 8.44/8.87
% 8.44/8.87 Options Used:
% 8.44/8.87
% 8.44/8.87 useres = 1
% 8.44/8.87 useparamod = 1
% 8.44/8.87 useeqrefl = 1
% 8.44/8.87 useeqfact = 1
% 8.44/8.87 usefactor = 1
% 8.44/8.87 usesimpsplitting = 0
% 8.44/8.87 usesimpdemod = 5
% 8.44/8.87 usesimpres = 3
% 8.44/8.87
% 8.44/8.87 resimpinuse = 1000
% 8.44/8.87 resimpclauses = 20000
% 8.44/8.87 substype = eqrewr
% 8.44/8.87 backwardsubs = 1
% 8.44/8.87 selectoldest = 5
% 8.44/8.87
% 8.44/8.87 litorderings [0] = split
% 8.44/8.87 litorderings [1] = extend the termordering, first sorting on arguments
% 8.44/8.87
% 8.44/8.87 termordering = kbo
% 8.44/8.87
% 8.44/8.87 litapriori = 0
% 8.44/8.87 termapriori = 1
% 8.44/8.87 litaposteriori = 0
% 8.44/8.87 termaposteriori = 0
% 8.44/8.87 demodaposteriori = 0
% 8.44/8.87 ordereqreflfact = 0
% 8.44/8.87
% 8.44/8.87 litselect = negord
% 8.44/8.87
% 8.44/8.87 maxweight = 15
% 8.44/8.87 maxdepth = 30000
% 8.44/8.87 maxlength = 115
% 8.44/8.87 maxnrvars = 195
% 8.44/8.87 excuselevel = 1
% 8.44/8.87 increasemaxweight = 1
% 8.44/8.87
% 8.44/8.87 maxselected = 10000000
% 8.44/8.87 maxnrclauses = 10000000
% 8.44/8.87
% 8.44/8.87 showgenerated = 0
% 8.44/8.87 showkept = 0
% 8.44/8.87 showselected = 0
% 8.44/8.87 showdeleted = 0
% 8.44/8.87 showresimp = 1
% 8.44/8.87 showstatus = 2000
% 8.44/8.87
% 8.44/8.87 prologoutput = 1
% 8.44/8.87 nrgoals = 5000000
% 8.44/8.87 totalproof = 1
% 8.44/8.87
% 8.44/8.87 Symbols occurring in the translation:
% 8.44/8.87
% 8.44/8.87 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 8.44/8.87 . [1, 2] (w:1, o:35, a:1, s:1, b:0),
% 8.44/8.87 ! [4, 1] (w:0, o:26, a:1, s:1, b:0),
% 8.44/8.87 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 8.44/8.87 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 8.44/8.87 pair2 [44, 2] (w:1, o:60, a:1, s:1, b:0),
% 8.44/8.87 aux [45, 4] (w:1, o:70, a:1, s:1, b:0),
% 8.44/8.87 cons [46, 2] (w:1, o:61, a:1, s:1, b:0),
% 8.44/8.87 btrue [50, 0] (w:1, o:19, a:1, s:1, b:0),
% 8.44/8.87 aux2 [51, 5] (w:1, o:73, a:1, s:1, b:0),
% 8.44/8.87 merge [52, 2] (w:1, o:63, a:1, s:1, b:0),
% 8.44/8.87 bfalse [53, 0] (w:1, o:20, a:1, s:1, b:0),
% 8.44/8.87 aux3 [55, 4] (w:1, o:71, a:1, s:1, b:0),
% 8.44/8.87 msort [56, 1] (w:1, o:32, a:1, s:1, b:0),
% 8.44/8.87 aux4 [58, 4] (w:1, o:72, a:1, s:1, b:0),
% 96.15/96.50 count [59, 2] (w:1, o:64, a:1, s:1, b:0),
% 96.15/96.50 s [60, 1] (w:1, o:33, a:1, s:1, b:0),
% 96.15/96.50 z [61, 0] (w:1, o:21, a:1, s:1, b:0),
% 96.15/96.50 splitAtNat [62, 2] (w:1, o:65, a:1, s:1, b:0),
% 96.15/96.50 nil [63, 0] (w:1, o:22, a:1, s:1, b:0),
% 96.15/96.50 leqNat [64, 2] (w:1, o:62, a:1, s:1, b:0),
% 96.15/96.50 lengthNat [66, 1] (w:1, o:31, a:1, s:1, b:0),
% 96.15/96.50 impl [68, 2] (w:1, o:66, a:1, s:1, b:0),
% 96.15/96.50 div2 [69, 1] (w:1, o:34, a:1, s:1, b:0),
% 96.15/96.50 eq [71, 2] (w:1, o:67, a:1, s:1, b:0),
% 96.15/96.50 'prop_msort_permutation_wrong1' [72, 2] (w:1, o:68, a:1, s:1, b:0),
% 96.15/96.50 eq2 [73, 2] (w:1, o:69, a:1, s:1, b:0).
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 15
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 631
% 96.15/96.50 Kept: 90
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 16
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 16
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 631
% 96.15/96.50 Kept: 90
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 17
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 17
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 968
% 96.15/96.50 Kept: 121
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 18
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 18
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 1102
% 96.15/96.50 Kept: 133
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 19
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 19
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 1434
% 96.15/96.50 Kept: 156
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 20
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 20
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 1506
% 96.15/96.50 Kept: 163
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 21
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 21
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 3856
% 96.15/96.50 Kept: 326
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 22
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 22
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 5295
% 96.15/96.50 Kept: 410
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 23
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 23
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 17210
% 96.15/96.50 Kept: 914
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 24
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 24
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 36886
% 96.15/96.50 Kept: 1369
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 25
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 Intermediate Status:
% 96.15/96.50 Generated: 22870
% 96.15/96.50 Kept: 2001
% 96.15/96.50 Inuse: 810
% 96.15/96.50 Deleted: 85
% 96.15/96.50 Deletedinuse: 11
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 25
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 103446
% 96.15/96.50 Kept: 2327
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 26
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 Intermediate Status:
% 96.15/96.50 Generated: 14502
% 96.15/96.50 Kept: 2001
% 96.15/96.50 Inuse: 583
% 96.15/96.50 Deleted: 72
% 96.15/96.50 Deletedinuse: 10
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 26
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 154014
% 96.15/96.50 Kept: 2837
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 27
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 Intermediate Status:
% 96.15/96.50 Generated: 11949
% 96.15/96.50 Kept: 2004
% 96.15/96.50 Inuse: 510
% 96.15/96.50 Deleted: 88
% 96.15/96.50 Deletedinuse: 10
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 Intermediate Status:
% 96.15/96.50 Generated: 80414
% 96.15/96.50 Kept: 4005
% 96.15/96.50 Inuse: 1478
% 96.15/96.50 Deleted: 169
% 96.15/96.50 Deletedinuse: 15
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50 Failed to find proof!
% 96.15/96.50 maxweight = 27
% 96.15/96.50 maxnrclauses = 10000000
% 96.15/96.50 Generated: 490570
% 96.15/96.50 Kept: 4558
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 The strategy used was not complete!
% 96.15/96.50
% 96.15/96.50 Increased maxweight to 28
% 96.15/96.50
% 96.15/96.50 Starting Search:
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 96.15/96.50 Done
% 96.15/96.50
% 96.15/96.50
% 96.15/96.50 Intermediate Status:
% 96.15/96.50 Generated: 8935
% 96.15/96.50 Kept: 2003
% 96.15/96.50 Inuse: 459
% 96.15/96.50 Deleted: 96
% 96.15/96.50 Deletedinuse: 11
% 96.15/96.50
% 96.15/96.50 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 40296
% 298.36/298.73 Kept: 4007
% 298.36/298.73 Inuse: 963
% 298.36/298.73 Deleted: 127
% 298.36/298.73 Deletedinuse: 12
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 113651
% 298.36/298.73 Kept: 6008
% 298.36/298.73 Inuse: 1692
% 298.36/298.73 Deleted: 236
% 298.36/298.73 Deletedinuse: 25
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 558018
% 298.36/298.73 Kept: 8010
% 298.36/298.73 Inuse: 4200
% 298.36/298.73 Deleted: 529
% 298.36/298.73 Deletedinuse: 37
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 1388035
% 298.36/298.73 Kept: 10010
% 298.36/298.73 Inuse: 8232
% 298.36/298.73 Deleted: 1171
% 298.36/298.73 Deletedinuse: 86
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Failed to find proof!
% 298.36/298.73 maxweight = 28
% 298.36/298.73 maxnrclauses = 10000000
% 298.36/298.73 Generated: 1551497
% 298.36/298.73 Kept: 10171
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 The strategy used was not complete!
% 298.36/298.73
% 298.36/298.73 Increased maxweight to 29
% 298.36/298.73
% 298.36/298.73 Starting Search:
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 8619
% 298.36/298.73 Kept: 2005
% 298.36/298.73 Inuse: 447
% 298.36/298.73 Deleted: 96
% 298.36/298.73 Deletedinuse: 11
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 31127
% 298.36/298.73 Kept: 4008
% 298.36/298.73 Inuse: 788
% 298.36/298.73 Deleted: 122
% 298.36/298.73 Deletedinuse: 12
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 82111
% 298.36/298.73 Kept: 6011
% 298.36/298.73 Inuse: 1234
% 298.36/298.73 Deleted: 168
% 298.36/298.73 Deletedinuse: 16
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 120646
% 298.36/298.73 Kept: 8011
% 298.36/298.73 Inuse: 1641
% 298.36/298.73 Deleted: 230
% 298.36/298.73 Deletedinuse: 28
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 224705
% 298.36/298.73 Kept: 10012
% 298.36/298.73 Inuse: 2623
% 298.36/298.73 Deleted: 366
% 298.36/298.73 Deletedinuse: 35
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 607040
% 298.36/298.73 Kept: 12013
% 298.36/298.73 Inuse: 4162
% 298.36/298.73 Deleted: 588
% 298.36/298.73 Deletedinuse: 51
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 1235570
% 298.36/298.73 Kept: 14013
% 298.36/298.73 Inuse: 6890
% 298.36/298.73 Deleted: 977
% 298.36/298.73 Deletedinuse: 102
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 2606775
% 298.36/298.73 Kept: 16048
% 298.36/298.73 Inuse: 10815
% 298.36/298.73 Deleted: 1716
% 298.36/298.73 Deletedinuse: 223
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Failed to find proof!
% 298.36/298.73 maxweight = 29
% 298.36/298.73 maxnrclauses = 10000000
% 298.36/298.73 Generated: 4739188
% 298.36/298.73 Kept: 17269
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 The strategy used was not complete!
% 298.36/298.73
% 298.36/298.73 Increased maxweight to 30
% 298.36/298.73
% 298.36/298.73 Starting Search:
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 8858
% 298.36/298.73 Kept: 2031
% 298.36/298.73 Inuse: 448
% 298.36/298.73 Deleted: 84
% 298.36/298.73 Deletedinuse: 11
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 25467
% 298.36/298.73 Kept: 4034
% 298.36/298.73 Inuse: 754
% 298.36/298.73 Deleted: 136
% 298.36/298.73 Deletedinuse: 12
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 53207
% 298.36/298.73 Kept: 6040
% 298.36/298.73 Inuse: 1083
% 298.36/298.73 Deleted: 175
% 298.36/298.73 Deletedinuse: 16
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 96065
% 298.36/298.73 Kept: 8040
% 298.36/298.73 Inuse: 1378
% 298.36/298.73 Deleted: 202
% 298.36/298.73 Deletedinuse: 20
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 126357
% 298.36/298.73 Kept: 10043
% 298.36/298.73 Inuse: 1676
% 298.36/298.73 Deleted: 249
% 298.36/298.73 Deletedinuse: 33
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 193441
% 298.36/298.73 Kept: 12047
% 298.36/298.73 Inuse: 2281
% 298.36/298.73 Deleted: 342
% 298.36/298.73 Deletedinuse: 36
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 248925
% 298.36/298.73 Kept: 14053
% 298.36/298.73 Inuse: 2764
% 298.36/298.73 Deleted: 446
% 298.36/298.73 Deletedinuse: 38
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 551585
% 298.36/298.73 Kept: 16062
% 298.36/298.73 Inuse: 3826
% 298.36/298.73 Deleted: 649
% 298.36/298.73 Deletedinuse: 52
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 Intermediate Status:
% 298.36/298.73 Generated: 1047476
% 298.36/298.73 Kept: 18063
% 298.36/298.73 Inuse: 6089
% 298.36/298.73 Deleted: 954
% 298.36/298.73 Deletedinuse: 60
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying inuse:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73 Resimplifying clauses:
% 298.36/298.73 Done
% 298.36/298.73
% 298.36/298.73
% 298.36/298.73 ITerminated
% 299.68/300.02 Bliksem ended
%------------------------------------------------------------------------------