%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX219+1 : TPTP v9.3.0. Released v9.3.0.
% 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 : Tue May 5 06:56:50 PM UTC 2026
% Result : Timeout 299.31s 300.04s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX219+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.17/0.34 % Computer : n020.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % DateTime : Tue May 5 12:21:04 EDT 2026
% 0.17/0.34 % CPUTime :
% 7.14/7.58 *** allocated 10000 integers for termspace/termends
% 7.14/7.58 *** allocated 10000 integers for clauses
% 7.14/7.58 *** allocated 10000 integers for justifications
% 7.14/7.58 Bliksem 1.12
% 7.14/7.58
% 7.14/7.58
% 7.14/7.58 Automatic Strategy Selection
% 7.14/7.58
% 7.14/7.58
% 7.14/7.58 Clauses:
% 7.14/7.58
% 7.14/7.58 { head( cons( X, Y ) ) = X }.
% 7.14/7.58 { tail( cons( X, Y ) ) = Y }.
% 7.14/7.58 { ! nil = cons( X, Y ) }.
% 7.14/7.58 { proj1Arr( arr( X, Y ) ) = X }.
% 7.14/7.58 { proj2Arr( arr( X, Y ) ) = Y }.
% 7.14/7.58 { ! arr( X, Y ) = a }.
% 7.14/7.58 { ! arr( X, Y ) = b }.
% 7.14/7.58 { ! arr( X, Y ) = c }.
% 7.14/7.58 { ! a = b }.
% 7.14/7.58 { ! a = c }.
% 7.14/7.58 { ! b = c }.
% 7.14/7.58 { proj1Suc( suc( X ) ) = X }.
% 7.14/7.58 { ! zero = suc( X ) }.
% 7.14/7.58 { proj1Just( just( X ) ) = X }.
% 7.14/7.58 { ! nothing = just( X ) }.
% 7.14/7.58 { proj1App( app( X, Y, Z ) ) = X }.
% 7.14/7.58 { proj2App( app( X, Y, Z ) ) = Y }.
% 7.14/7.58 { proj3App( app( X, Y, Z ) ) = Z }.
% 7.14/7.58 { proj1Lam( lam( X ) ) = X }.
% 7.14/7.58 { proj1Var( var( X ) ) = X }.
% 7.14/7.58 { ! app( X, Y, Z ) = lam( T ) }.
% 7.14/7.58 { ! app( X, Y, Z ) = var( T ) }.
% 7.14/7.58 { ! lam( X ) = var( Y ) }.
% 7.14/7.58 { index( nil, X ) = nothing }.
% 7.14/7.58 { index( cons( X, Y ), zero ) = just( X ) }.
% 7.14/7.58 { index( cons( X, Y ), suc( Z ) ) = index( Y, Z ) }.
% 7.14/7.58 { ! tc( X, app( Z, T, U ), Y ), tc( X, Z, arr( U, Y ) ) }.
% 7.14/7.58 { ! tc( X, app( Z, T, U ), Y ), tc( X, T, U ) }.
% 7.14/7.58 { ! tc( X, Z, arr( U, Y ) ), ! tc( X, T, U ), tc( X, app( Z, T, U ), Y ) }
% 7.14/7.58 .
% 7.14/7.58 { X = arr( proj1Arr( X ), proj2Arr( X ) ), ! tc( Y, lam( Z ), X ) }.
% 7.14/7.58 { ! tc( X, lam( Y ), arr( Z, T ) ), tc( cons( Z, X ), Y, T ) }.
% 7.14/7.58 { ! tc( cons( Z, X ), Y, T ), tc( X, lam( Y ), arr( Z, T ) ) }.
% 7.14/7.58 { ! index( X, Y ) = nothing, ! tc( X, var( Y ), Z ) }.
% 7.14/7.58 { ! index( X, Y ) = just( Z ), ! tc( X, var( Y ), T ), Z = T }.
% 7.14/7.58 { ! index( X, Y ) = just( Z ), ! Z = T, tc( X, var( Y ), T ) }.
% 7.14/7.58 { ! tc( nil, X, arr( arr( b, c ), arr( arr( a, b ), arr( a, c ) ) ) ) }.
% 7.14/7.58
% 7.14/7.58 percentage equality = 0.666667, percentage horn = 1.000000
% 7.14/7.58 This is a problem with some equality
% 7.14/7.58
% 7.14/7.58
% 7.14/7.58
% 7.14/7.58 Options Used:
% 7.14/7.58
% 7.14/7.58 useres = 1
% 7.14/7.58 useparamod = 1
% 7.14/7.58 useeqrefl = 1
% 7.14/7.58 useeqfact = 1
% 7.14/7.58 usefactor = 1
% 7.14/7.58 usesimpsplitting = 0
% 7.14/7.58 usesimpdemod = 5
% 7.14/7.58 usesimpres = 3
% 7.14/7.58
% 7.14/7.58 resimpinuse = 1000
% 7.14/7.58 resimpclauses = 20000
% 7.14/7.58 substype = eqrewr
% 7.14/7.58 backwardsubs = 1
% 7.14/7.58 selectoldest = 5
% 7.14/7.58
% 7.14/7.58 litorderings [0] = split
% 7.14/7.58 litorderings [1] = extend the termordering, first sorting on arguments
% 7.14/7.58
% 7.14/7.58 termordering = kbo
% 7.14/7.58
% 7.14/7.58 litapriori = 0
% 7.14/7.58 termapriori = 1
% 7.14/7.58 litaposteriori = 0
% 7.14/7.58 termaposteriori = 0
% 7.14/7.58 demodaposteriori = 0
% 7.14/7.58 ordereqreflfact = 0
% 7.14/7.58
% 7.14/7.58 litselect = negord
% 7.14/7.58
% 7.14/7.58 maxweight = 15
% 7.14/7.58 maxdepth = 30000
% 7.14/7.58 maxlength = 115
% 7.14/7.58 maxnrvars = 195
% 7.14/7.58 excuselevel = 1
% 7.14/7.58 increasemaxweight = 1
% 7.14/7.58
% 7.14/7.58 maxselected = 10000000
% 7.14/7.58 maxnrclauses = 10000000
% 7.14/7.58
% 7.14/7.58 showgenerated = 0
% 7.14/7.58 showkept = 0
% 7.14/7.58 showselected = 0
% 7.14/7.58 showdeleted = 0
% 7.14/7.58 showresimp = 1
% 7.14/7.58 showstatus = 2000
% 7.14/7.58
% 7.14/7.58 prologoutput = 0
% 7.14/7.58 nrgoals = 5000000
% 7.14/7.58 totalproof = 1
% 7.14/7.58
% 7.14/7.58 Symbols occurring in the translation:
% 7.14/7.58
% 7.14/7.58 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 7.14/7.58 . [1, 2] (w:1, o:46, a:1, s:1, b:0),
% 7.14/7.58 ! [4, 1] (w:0, o:26, a:1, s:1, b:0),
% 7.14/7.58 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.14/7.58 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.14/7.58 cons [37, 2] (w:1, o:70, a:1, s:1, b:0),
% 7.14/7.58 head [38, 1] (w:1, o:31, a:1, s:1, b:0),
% 7.14/7.58 tail [39, 1] (w:1, o:33, a:1, s:1, b:0),
% 7.14/7.58 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 7.14/7.58 arr [41, 2] (w:1, o:71, a:1, s:1, b:0),
% 7.14/7.58 proj1Arr [42, 1] (w:1, o:34, a:1, s:1, b:0),
% 7.14/7.58 proj2Arr [43, 1] (w:1, o:40, a:1, s:1, b:0),
% 7.14/7.58 a [44, 0] (w:1, o:9, a:1, s:1, b:0),
% 7.14/7.58 b [45, 0] (w:1, o:10, a:1, s:1, b:0),
% 7.14/7.58 c [46, 0] (w:1, o:11, a:1, s:1, b:0),
% 7.14/7.58 suc [47, 1] (w:1, o:32, a:1, s:1, b:0),
% 7.14/7.58 proj1Suc [48, 1] (w:1, o:35, a:1, s:1, b:0),
% 7.14/7.58 zero [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 7.14/7.58 just [50, 1] (w:1, o:41, a:1, s:1, b:0),
% 7.14/7.58 proj1Just [51, 1] (w:1, o:36, a:1, s:1, b:0),
% 7.14/7.58 nothing [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 7.14/7.58 app [54, 3] (w:1, o:73, a:1, s:1, b:0),
% 7.14/7.58 proj1App [55, 1] (w:1, o:37, a:1, s:1, b:0),
% 7.14/7.58 proj2App [56, 1] (w:1, o:42, a:1, s:1, b:0),
% 7.14/7.58 proj3App [57, 1] (w:1, o:43, a:1, s:1, b:0),
% 7.14/7.58 lam [58, 1] (w:1, o:44, a:1, s:1, b:0),
% 7.14/7.58 proj1Lam [59, 1] (w:1, o:38, a:1, s:1, b:0),
% 7.14/7.58 var [60, 1] (w:1, o:45, a:1, s:1, b:0),
% 7.14/7.58 proj1Var [61, 1] (w:1, o:39, a:1, s:1, b:0),
% 19.94/20.33 index [64, 2] (w:1, o:72, a:1, s:1, b:0),
% 19.94/20.33 tc [70, 3] (w:1, o:74, a:1, s:1, b:0).
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Starting Search:
% 19.94/20.33
% 19.94/20.33 *** allocated 15000 integers for clauses
% 19.94/20.33 *** allocated 22500 integers for clauses
% 19.94/20.33 *** allocated 33750 integers for clauses
% 19.94/20.33 *** allocated 15000 integers for termspace/termends
% 19.94/20.33 *** allocated 50625 integers for clauses
% 19.94/20.33 *** allocated 22500 integers for termspace/termends
% 19.94/20.33 *** allocated 75937 integers for clauses
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 33750 integers for termspace/termends
% 19.94/20.33 *** allocated 113905 integers for clauses
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 9398
% 19.94/20.33 Kept: 2000
% 19.94/20.33 Inuse: 219
% 19.94/20.33 Deleted: 1
% 19.94/20.33 Deletedinuse: 1
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 50625 integers for termspace/termends
% 19.94/20.33 *** allocated 170857 integers for clauses
% 19.94/20.33 *** allocated 75937 integers for termspace/termends
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 256285 integers for clauses
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 24768
% 19.94/20.33 Kept: 4144
% 19.94/20.33 Inuse: 315
% 19.94/20.33 Deleted: 5
% 19.94/20.33 Deletedinuse: 2
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 113905 integers for termspace/termends
% 19.94/20.33 *** allocated 384427 integers for clauses
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 42737
% 19.94/20.33 Kept: 6186
% 19.94/20.33 Inuse: 381
% 19.94/20.33 Deleted: 6
% 19.94/20.33 Deletedinuse: 2
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 170857 integers for termspace/termends
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 576640 integers for clauses
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 163104
% 19.94/20.33 Kept: 8431
% 19.94/20.33 Inuse: 619
% 19.94/20.33 Deleted: 7
% 19.94/20.33 Deletedinuse: 2
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 256285 integers for termspace/termends
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 172946
% 19.94/20.33 Kept: 11174
% 19.94/20.33 Inuse: 633
% 19.94/20.33 Deleted: 11
% 19.94/20.33 Deletedinuse: 6
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 864960 integers for clauses
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 183718
% 19.94/20.33 Kept: 13892
% 19.94/20.33 Inuse: 634
% 19.94/20.33 Deleted: 11
% 19.94/20.33 Deletedinuse: 6
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 384427 integers for termspace/termends
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 202831
% 19.94/20.33 Kept: 17111
% 19.94/20.33 Inuse: 657
% 19.94/20.33 Deleted: 11
% 19.94/20.33 Deletedinuse: 6
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 1297440 integers for clauses
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 209538
% 19.94/20.33 Kept: 19626
% 19.94/20.33 Inuse: 658
% 19.94/20.33 Deleted: 12
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 220566
% 19.94/20.33 Kept: 22381
% 19.94/20.33 Inuse: 659
% 19.94/20.33 Deleted: 12
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 Resimplifying clauses:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 576640 integers for termspace/termends
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 241447
% 19.94/20.33 Kept: 25797
% 19.94/20.33 Inuse: 682
% 19.94/20.33 Deleted: 297
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 1946160 integers for clauses
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 252713
% 19.94/20.33 Kept: 28581
% 19.94/20.33 Inuse: 683
% 19.94/20.33 Deleted: 297
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 283389
% 19.94/20.33 Kept: 30591
% 19.94/20.33 Inuse: 727
% 19.94/20.33 Deleted: 297
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 314703
% 19.94/20.33 Kept: 32616
% 19.94/20.33 Inuse: 768
% 19.94/20.33 Deleted: 297
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 363832
% 19.94/20.33 Kept: 34639
% 19.94/20.33 Inuse: 811
% 19.94/20.33 Deleted: 298
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 *** allocated 864960 integers for termspace/termends
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 376188
% 19.94/20.33 Kept: 37670
% 19.94/20.33 Inuse: 814
% 19.94/20.33 Deleted: 298
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 388514
% 19.94/20.33 Kept: 40690
% 19.94/20.33 Inuse: 817
% 19.94/20.33 Deleted: 298
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 Resimplifying clauses:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 410592
% 19.94/20.33 Kept: 42714
% 19.94/20.33 Inuse: 849
% 19.94/20.33 Deleted: 652
% 19.94/20.33 Deletedinuse: 7
% 19.94/20.33
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33 *** allocated 2919240 integers for clauses
% 19.94/20.33 Resimplifying inuse:
% 19.94/20.33 Done
% 19.94/20.33
% 19.94/20.33
% 19.94/20.33 Intermediate Status:
% 19.94/20.33 Generated: 426009
% 43.14/43.50 Kept: 44765
% 43.14/43.50 Inuse: 882
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 455365
% 43.14/43.50 Kept: 46766
% 43.14/43.50 Inuse: 927
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 474853
% 43.14/43.50 Kept: 48826
% 43.14/43.50 Inuse: 968
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 493720
% 43.14/43.50 Kept: 50863
% 43.14/43.50 Inuse: 1003
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 523240
% 43.14/43.50 Kept: 52908
% 43.14/43.50 Inuse: 1037
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 *** allocated 1297440 integers for termspace/termends
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 544255
% 43.14/43.50 Kept: 54980
% 43.14/43.50 Inuse: 1071
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 566278
% 43.14/43.50 Kept: 56990
% 43.14/43.50 Inuse: 1111
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 588488
% 43.14/43.50 Kept: 59008
% 43.14/43.50 Inuse: 1156
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 610406
% 43.14/43.50 Kept: 61019
% 43.14/43.50 Inuse: 1199
% 43.14/43.50 Deleted: 652
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying clauses:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 639320
% 43.14/43.50 Kept: 63171
% 43.14/43.50 Inuse: 1250
% 43.14/43.50 Deleted: 737
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 671980
% 43.14/43.50 Kept: 65510
% 43.14/43.50 Inuse: 1285
% 43.14/43.50 Deleted: 737
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 *** allocated 4378860 integers for clauses
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 698231
% 43.14/43.50 Kept: 67873
% 43.14/43.50 Inuse: 1300
% 43.14/43.50 Deleted: 737
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 735963
% 43.14/43.50 Kept: 69896
% 43.14/43.50 Inuse: 1349
% 43.14/43.50 Deleted: 737
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 762524
% 43.14/43.50 Kept: 71904
% 43.14/43.50 Inuse: 1398
% 43.14/43.50 Deleted: 737
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 792660
% 43.14/43.50 Kept: 73948
% 43.14/43.50 Inuse: 1448
% 43.14/43.50 Deleted: 737
% 43.14/43.50 Deletedinuse: 7
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 817784
% 43.14/43.50 Kept: 76035
% 43.14/43.50 Inuse: 1461
% 43.14/43.50 Deleted: 738
% 43.14/43.50 Deletedinuse: 8
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 845418
% 43.14/43.50 Kept: 78092
% 43.14/43.50 Inuse: 1499
% 43.14/43.50 Deleted: 738
% 43.14/43.50 Deletedinuse: 8
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 871065
% 43.14/43.50 Kept: 80152
% 43.14/43.50 Inuse: 1531
% 43.14/43.50 Deleted: 738
% 43.14/43.50 Deletedinuse: 8
% 43.14/43.50
% 43.14/43.50 *** allocated 1946160 integers for termspace/termends
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 895607
% 43.14/43.50 Kept: 82341
% 43.14/43.50 Inuse: 1541
% 43.14/43.50 Deleted: 738
% 43.14/43.50 Deletedinuse: 8
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying clauses:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 917153
% 43.14/43.50 Kept: 84415
% 43.14/43.50 Inuse: 1578
% 43.14/43.50 Deleted: 778
% 43.14/43.50 Deletedinuse: 9
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 955911
% 43.14/43.50 Kept: 87966
% 43.14/43.50 Inuse: 1607
% 43.14/43.50 Deleted: 778
% 43.14/43.50 Deletedinuse: 9
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 976319
% 43.14/43.50 Kept: 90020
% 43.14/43.50 Inuse: 1642
% 43.14/43.50 Deleted: 781
% 43.14/43.50 Deletedinuse: 12
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 997350
% 43.14/43.50 Kept: 92035
% 43.14/43.50 Inuse: 1672
% 43.14/43.50 Deleted: 781
% 43.14/43.50 Deletedinuse: 12
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50 Resimplifying inuse:
% 43.14/43.50 Done
% 43.14/43.50
% 43.14/43.50
% 43.14/43.50 Intermediate Status:
% 43.14/43.50 Generated: 1028161
% 43.14/43.50 Kept: 94841
% 43.14/43.50 Inuse: 1689
% 126.88/127.50 Deleted: 781
% 126.88/127.50 Deletedinuse: 12
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 *** allocated 6568290 integers for clauses
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1049904
% 126.88/127.50 Kept: 96902
% 126.88/127.50 Inuse: 1726
% 126.88/127.50 Deleted: 784
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1072959
% 126.88/127.50 Kept: 98984
% 126.88/127.50 Inuse: 1756
% 126.88/127.50 Deleted: 784
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1094087
% 126.88/127.50 Kept: 101068
% 126.88/127.50 Inuse: 1771
% 126.88/127.50 Deleted: 784
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1114957
% 126.88/127.50 Kept: 103346
% 126.88/127.50 Inuse: 1773
% 126.88/127.50 Deleted: 784
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying clauses:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1147126
% 126.88/127.50 Kept: 105378
% 126.88/127.50 Inuse: 1829
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1184052
% 126.88/127.50 Kept: 107439
% 126.88/127.50 Inuse: 1887
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1213493
% 126.88/127.50 Kept: 109484
% 126.88/127.50 Inuse: 1933
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1248787
% 126.88/127.50 Kept: 111512
% 126.88/127.50 Inuse: 1987
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1286957
% 126.88/127.50 Kept: 113525
% 126.88/127.50 Inuse: 2043
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1320545
% 126.88/127.50 Kept: 115572
% 126.88/127.50 Inuse: 2093
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1350649
% 126.88/127.50 Kept: 117580
% 126.88/127.50 Inuse: 2143
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1383788
% 126.88/127.50 Kept: 119582
% 126.88/127.50 Inuse: 2196
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 *** allocated 2919240 integers for termspace/termends
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1422218
% 126.88/127.50 Kept: 123933
% 126.88/127.50 Inuse: 2198
% 126.88/127.50 Deleted: 972
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying clauses:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1445900
% 126.88/127.50 Kept: 126581
% 126.88/127.50 Inuse: 2201
% 126.88/127.50 Deleted: 1169
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1472766
% 126.88/127.50 Kept: 129579
% 126.88/127.50 Inuse: 2202
% 126.88/127.50 Deleted: 1169
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1509787
% 126.88/127.50 Kept: 132813
% 126.88/127.50 Inuse: 2204
% 126.88/127.50 Deleted: 1169
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50 Resimplifying inuse:
% 126.88/127.50 Done
% 126.88/127.50
% 126.88/127.50
% 126.88/127.50 Intermediate Status:
% 126.88/127.50 Generated: 1549344
% 126.88/127.50 Kept: 136041
% 126.88/127.50 Inuse: 2207
% 126.88/127.50 Deleted: 1169
% 126.88/127.50 Deletedinuse: 15
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51
% 126.88/127.51 Intermediate Status:
% 126.88/127.51 Generated: 1575542
% 126.88/127.51 Kept: 138663
% 126.88/127.51 Inuse: 2209
% 126.88/127.51 Deleted: 1169
% 126.88/127.51 Deletedinuse: 15
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51
% 126.88/127.51 Intermediate Status:
% 126.88/127.51 Generated: 1615244
% 126.88/127.51 Kept: 141913
% 126.88/127.51 Inuse: 2212
% 126.88/127.51 Deleted: 1169
% 126.88/127.51 Deletedinuse: 15
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51
% 126.88/127.51 Intermediate Status:
% 126.88/127.51 Generated: 1653728
% 126.88/127.51 Kept: 144959
% 126.88/127.51 Inuse: 2214
% 126.88/127.51 Deleted: 1169
% 126.88/127.51 Deletedinuse: 15
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51 Resimplifying clauses:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51 *** allocated 9852435 integers for clauses
% 126.88/127.51
% 126.88/127.51 Intermediate Status:
% 126.88/127.51 Generated: 1680761
% 126.88/127.51 Kept: 147621
% 126.88/127.51 Inuse: 2217
% 126.88/127.51 Deleted: 1274
% 126.88/127.51 Deletedinuse: 15
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51
% 126.88/127.51 Intermediate Status:
% 126.88/127.51 Generated: 1721714
% 126.88/127.51 Kept: 150969
% 126.88/127.51 Inuse: 2221
% 126.88/127.51 Deleted: 1274
% 126.88/127.51 Deletedinuse: 15
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51 Resimplifying inuse:
% 126.88/127.51 Done
% 126.88/127.51
% 126.88/127.51
% 126.88/127.51 Intermediate Status:
% 206.19/206.89 Generated: 1748184
% 206.19/206.89 Kept: 153605
% 206.19/206.89 Inuse: 2223
% 206.19/206.89 Deleted: 1274
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 1788404
% 206.19/206.89 Kept: 156874
% 206.19/206.89 Inuse: 2226
% 206.19/206.89 Deleted: 1274
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 1839624
% 206.19/206.89 Kept: 160531
% 206.19/206.89 Inuse: 2228
% 206.19/206.89 Deleted: 1274
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 1867546
% 206.19/206.89 Kept: 163175
% 206.19/206.89 Inuse: 2231
% 206.19/206.89 Deleted: 1274
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 1894407
% 206.19/206.89 Kept: 165864
% 206.19/206.89 Inuse: 2233
% 206.19/206.89 Deleted: 1274
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying clauses:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 1923632
% 206.19/206.89 Kept: 168623
% 206.19/206.89 Inuse: 2237
% 206.19/206.89 Deleted: 1342
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 1950607
% 206.19/206.89 Kept: 171314
% 206.19/206.89 Inuse: 2239
% 206.19/206.89 Deleted: 1342
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 1992819
% 206.19/206.89 Kept: 174693
% 206.19/206.89 Inuse: 2243
% 206.19/206.89 Deleted: 1342
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2033665
% 206.19/206.89 Kept: 177777
% 206.19/206.89 Inuse: 2246
% 206.19/206.89 Deleted: 1342
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 *** allocated 4378860 integers for termspace/termends
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2085782
% 206.19/206.89 Kept: 181670
% 206.19/206.89 Inuse: 2248
% 206.19/206.89 Deleted: 1342
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2113589
% 206.19/206.89 Kept: 184299
% 206.19/206.89 Inuse: 2251
% 206.19/206.89 Deleted: 1342
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2140736
% 206.19/206.89 Kept: 186972
% 206.19/206.89 Inuse: 2253
% 206.19/206.89 Deleted: 1342
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying clauses:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2169903
% 206.19/206.89 Kept: 189679
% 206.19/206.89 Inuse: 2256
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2193382
% 206.19/206.89 Kept: 191731
% 206.19/206.89 Inuse: 2266
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2218306
% 206.19/206.89 Kept: 193748
% 206.19/206.89 Inuse: 2289
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2259855
% 206.19/206.89 Kept: 195757
% 206.19/206.89 Inuse: 2336
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2300464
% 206.19/206.89 Kept: 197758
% 206.19/206.89 Inuse: 2384
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2331864
% 206.19/206.89 Kept: 199845
% 206.19/206.89 Inuse: 2411
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2370152
% 206.19/206.89 Kept: 201867
% 206.19/206.89 Inuse: 2442
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2415568
% 206.19/206.89 Kept: 203898
% 206.19/206.89 Inuse: 2482
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2452360
% 206.19/206.89 Kept: 205991
% 206.19/206.89 Inuse: 2511
% 206.19/206.89 Deleted: 1428
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying clauses:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2480545
% 206.19/206.89 Kept: 208012
% 206.19/206.89 Inuse: 2536
% 206.19/206.89 Deleted: 1503
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89 Resimplifying inuse:
% 206.19/206.89 Done
% 206.19/206.89
% 206.19/206.89
% 206.19/206.89 Intermediate Status:
% 206.19/206.89 Generated: 2506913
% 206.19/206.89 Kept: 210057
% 206.19/206.89 Inuse: 2559
% 206.19/206.89 Deleted: 1503
% 206.19/206.89 Deletedinuse: 15
% 206.19/206.89
% 206.19/206.89 ReTerminated
% 299.31/300.04 Bliksem ended
% 299.31/300.04 Terminated
%------------------------------------------------------------------------------