%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX220+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.53s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX220+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/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:25:19 EDT 2026
% 0.17/0.34 % CPUTime :
% 7.03/7.46 *** allocated 10000 integers for termspace/termends
% 7.03/7.46 *** allocated 10000 integers for clauses
% 7.03/7.46 *** allocated 10000 integers for justifications
% 7.03/7.46 Bliksem 1.12
% 7.03/7.46
% 7.03/7.46
% 7.03/7.46 Automatic Strategy Selection
% 7.03/7.46
% 7.03/7.46
% 7.03/7.46 Clauses:
% 7.03/7.46
% 7.03/7.46 { head( cons( X, Y ) ) = X }.
% 7.03/7.46 { tail( cons( X, Y ) ) = Y }.
% 7.03/7.46 { ! nil = cons( X, Y ) }.
% 7.03/7.46 { proj1Arr( arr( X, Y ) ) = X }.
% 7.03/7.46 { proj2Arr( arr( X, Y ) ) = Y }.
% 7.03/7.46 { ! arr( X, Y ) = a }.
% 7.03/7.46 { ! arr( X, Y ) = b }.
% 7.03/7.46 { ! arr( X, Y ) = c }.
% 7.03/7.46 { ! a = b }.
% 7.03/7.46 { ! a = c }.
% 7.03/7.46 { ! b = c }.
% 7.03/7.46 { proj1Suc( suc( X ) ) = X }.
% 7.03/7.46 { ! zero = suc( X ) }.
% 7.03/7.46 { proj1Just( just( X ) ) = X }.
% 7.03/7.46 { ! nothing = just( X ) }.
% 7.03/7.46 { proj1App( app( X, Y, Z ) ) = X }.
% 7.03/7.46 { proj2App( app( X, Y, Z ) ) = Y }.
% 7.03/7.46 { proj3App( app( X, Y, Z ) ) = Z }.
% 7.03/7.46 { proj1Lam( lam( X ) ) = X }.
% 7.03/7.46 { proj1Var( var( X ) ) = X }.
% 7.03/7.46 { ! app( X, Y, Z ) = lam( T ) }.
% 7.03/7.46 { ! app( X, Y, Z ) = var( T ) }.
% 7.03/7.46 { ! lam( X ) = var( Y ) }.
% 7.03/7.46 { index( nil, X ) = nothing }.
% 7.03/7.46 { index( cons( X, Y ), zero ) = just( X ) }.
% 7.03/7.46 { index( cons( X, Y ), suc( Z ) ) = index( Y, Z ) }.
% 7.03/7.46 { ! tc( X, app( Z, T, U ), Y ), tc( X, Z, arr( U, Y ) ) }.
% 7.03/7.46 { ! tc( X, app( Z, T, U ), Y ), tc( X, T, U ) }.
% 7.03/7.46 { ! tc( X, Z, arr( U, Y ) ), ! tc( X, T, U ), tc( X, app( Z, T, U ), Y ) }
% 7.03/7.46 .
% 7.03/7.46 { X = arr( proj1Arr( X ), proj2Arr( X ) ), ! tc( Y, lam( Z ), X ) }.
% 7.03/7.46 { ! tc( X, lam( Y ), arr( Z, T ) ), tc( cons( Z, X ), Y, T ) }.
% 7.03/7.46 { ! tc( cons( Z, X ), Y, T ), tc( X, lam( Y ), arr( Z, T ) ) }.
% 7.03/7.46 { ! index( X, Y ) = nothing, ! tc( X, var( Y ), Z ) }.
% 7.03/7.46 { ! index( X, Y ) = just( Z ), ! tc( X, var( Y ), T ), Z = T }.
% 7.03/7.46 { ! index( X, Y ) = just( Z ), ! Z = T, tc( X, var( Y ), T ) }.
% 7.03/7.46 { ! tc( nil, X, arr( arr( a, arr( b, c ) ), arr( b, arr( a, c ) ) ) ) }.
% 7.03/7.46
% 7.03/7.46 percentage equality = 0.666667, percentage horn = 1.000000
% 7.03/7.46 This is a problem with some equality
% 7.03/7.46
% 7.03/7.46
% 7.03/7.46
% 7.03/7.46 Options Used:
% 7.03/7.46
% 7.03/7.46 useres = 1
% 7.03/7.46 useparamod = 1
% 7.03/7.46 useeqrefl = 1
% 7.03/7.46 useeqfact = 1
% 7.03/7.46 usefactor = 1
% 7.03/7.46 usesimpsplitting = 0
% 7.03/7.46 usesimpdemod = 5
% 7.03/7.46 usesimpres = 3
% 7.03/7.46
% 7.03/7.46 resimpinuse = 1000
% 7.03/7.46 resimpclauses = 20000
% 7.03/7.46 substype = eqrewr
% 7.03/7.46 backwardsubs = 1
% 7.03/7.46 selectoldest = 5
% 7.03/7.46
% 7.03/7.46 litorderings [0] = split
% 7.03/7.46 litorderings [1] = extend the termordering, first sorting on arguments
% 7.03/7.46
% 7.03/7.46 termordering = kbo
% 7.03/7.46
% 7.03/7.46 litapriori = 0
% 7.03/7.46 termapriori = 1
% 7.03/7.46 litaposteriori = 0
% 7.03/7.46 termaposteriori = 0
% 7.03/7.46 demodaposteriori = 0
% 7.03/7.46 ordereqreflfact = 0
% 7.03/7.46
% 7.03/7.46 litselect = negord
% 7.03/7.46
% 7.03/7.46 maxweight = 15
% 7.03/7.46 maxdepth = 30000
% 7.03/7.46 maxlength = 115
% 7.03/7.46 maxnrvars = 195
% 7.03/7.46 excuselevel = 1
% 7.03/7.46 increasemaxweight = 1
% 7.03/7.46
% 7.03/7.46 maxselected = 10000000
% 7.03/7.46 maxnrclauses = 10000000
% 7.03/7.46
% 7.03/7.46 showgenerated = 0
% 7.03/7.46 showkept = 0
% 7.03/7.46 showselected = 0
% 7.03/7.46 showdeleted = 0
% 7.03/7.46 showresimp = 1
% 7.03/7.46 showstatus = 2000
% 7.03/7.46
% 7.03/7.46 prologoutput = 0
% 7.03/7.46 nrgoals = 5000000
% 7.03/7.46 totalproof = 1
% 7.03/7.46
% 7.03/7.46 Symbols occurring in the translation:
% 7.03/7.46
% 7.03/7.46 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 7.03/7.46 . [1, 2] (w:1, o:46, a:1, s:1, b:0),
% 7.03/7.46 ! [4, 1] (w:0, o:26, a:1, s:1, b:0),
% 7.03/7.46 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.03/7.46 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.03/7.46 cons [37, 2] (w:1, o:70, a:1, s:1, b:0),
% 7.03/7.46 head [38, 1] (w:1, o:31, a:1, s:1, b:0),
% 7.03/7.46 tail [39, 1] (w:1, o:33, a:1, s:1, b:0),
% 7.03/7.46 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 7.03/7.46 arr [41, 2] (w:1, o:71, a:1, s:1, b:0),
% 7.03/7.46 proj1Arr [42, 1] (w:1, o:34, a:1, s:1, b:0),
% 7.03/7.46 proj2Arr [43, 1] (w:1, o:40, a:1, s:1, b:0),
% 7.03/7.46 a [44, 0] (w:1, o:9, a:1, s:1, b:0),
% 7.03/7.46 b [45, 0] (w:1, o:10, a:1, s:1, b:0),
% 7.03/7.46 c [46, 0] (w:1, o:11, a:1, s:1, b:0),
% 7.03/7.46 suc [47, 1] (w:1, o:32, a:1, s:1, b:0),
% 7.03/7.46 proj1Suc [48, 1] (w:1, o:35, a:1, s:1, b:0),
% 7.03/7.46 zero [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 7.03/7.46 just [50, 1] (w:1, o:41, a:1, s:1, b:0),
% 7.03/7.46 proj1Just [51, 1] (w:1, o:36, a:1, s:1, b:0),
% 7.03/7.46 nothing [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 7.03/7.46 app [54, 3] (w:1, o:73, a:1, s:1, b:0),
% 7.03/7.46 proj1App [55, 1] (w:1, o:37, a:1, s:1, b:0),
% 7.03/7.46 proj2App [56, 1] (w:1, o:42, a:1, s:1, b:0),
% 7.03/7.46 proj3App [57, 1] (w:1, o:43, a:1, s:1, b:0),
% 7.03/7.46 lam [58, 1] (w:1, o:44, a:1, s:1, b:0),
% 7.03/7.46 proj1Lam [59, 1] (w:1, o:38, a:1, s:1, b:0),
% 7.03/7.46 var [60, 1] (w:1, o:45, a:1, s:1, b:0),
% 7.03/7.46 proj1Var [61, 1] (w:1, o:39, a:1, s:1, b:0),
% 19.23/19.66 index [64, 2] (w:1, o:72, a:1, s:1, b:0),
% 19.23/19.66 tc [70, 3] (w:1, o:74, a:1, s:1, b:0).
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Starting Search:
% 19.23/19.66
% 19.23/19.66 *** allocated 15000 integers for clauses
% 19.23/19.66 *** allocated 22500 integers for clauses
% 19.23/19.66 *** allocated 33750 integers for clauses
% 19.23/19.66 *** allocated 15000 integers for termspace/termends
% 19.23/19.66 *** allocated 50625 integers for clauses
% 19.23/19.66 *** allocated 22500 integers for termspace/termends
% 19.23/19.66 *** allocated 75937 integers for clauses
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 33750 integers for termspace/termends
% 19.23/19.66 *** allocated 113905 integers for clauses
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 9398
% 19.23/19.66 Kept: 2000
% 19.23/19.66 Inuse: 219
% 19.23/19.66 Deleted: 1
% 19.23/19.66 Deletedinuse: 1
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 50625 integers for termspace/termends
% 19.23/19.66 *** allocated 170857 integers for clauses
% 19.23/19.66 *** allocated 75937 integers for termspace/termends
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 256285 integers for clauses
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 24768
% 19.23/19.66 Kept: 4144
% 19.23/19.66 Inuse: 315
% 19.23/19.66 Deleted: 5
% 19.23/19.66 Deletedinuse: 2
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 113905 integers for termspace/termends
% 19.23/19.66 *** allocated 384427 integers for clauses
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 42737
% 19.23/19.66 Kept: 6186
% 19.23/19.66 Inuse: 381
% 19.23/19.66 Deleted: 6
% 19.23/19.66 Deletedinuse: 2
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 170857 integers for termspace/termends
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 576640 integers for clauses
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 163104
% 19.23/19.66 Kept: 8431
% 19.23/19.66 Inuse: 619
% 19.23/19.66 Deleted: 7
% 19.23/19.66 Deletedinuse: 2
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 256285 integers for termspace/termends
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 172946
% 19.23/19.66 Kept: 11174
% 19.23/19.66 Inuse: 633
% 19.23/19.66 Deleted: 11
% 19.23/19.66 Deletedinuse: 6
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 864960 integers for clauses
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 183718
% 19.23/19.66 Kept: 13892
% 19.23/19.66 Inuse: 634
% 19.23/19.66 Deleted: 11
% 19.23/19.66 Deletedinuse: 6
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 384427 integers for termspace/termends
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 202831
% 19.23/19.66 Kept: 17111
% 19.23/19.66 Inuse: 657
% 19.23/19.66 Deleted: 11
% 19.23/19.66 Deletedinuse: 6
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 1297440 integers for clauses
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 209538
% 19.23/19.66 Kept: 19626
% 19.23/19.66 Inuse: 658
% 19.23/19.66 Deleted: 12
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 220566
% 19.23/19.66 Kept: 22381
% 19.23/19.66 Inuse: 659
% 19.23/19.66 Deleted: 12
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 Resimplifying clauses:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 576640 integers for termspace/termends
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 241447
% 19.23/19.66 Kept: 25797
% 19.23/19.66 Inuse: 682
% 19.23/19.66 Deleted: 297
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 1946160 integers for clauses
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 252713
% 19.23/19.66 Kept: 28581
% 19.23/19.66 Inuse: 683
% 19.23/19.66 Deleted: 297
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 283389
% 19.23/19.66 Kept: 30591
% 19.23/19.66 Inuse: 727
% 19.23/19.66 Deleted: 297
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 314703
% 19.23/19.66 Kept: 32616
% 19.23/19.66 Inuse: 768
% 19.23/19.66 Deleted: 297
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 363832
% 19.23/19.66 Kept: 34639
% 19.23/19.66 Inuse: 811
% 19.23/19.66 Deleted: 298
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 *** allocated 864960 integers for termspace/termends
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 376188
% 19.23/19.66 Kept: 37670
% 19.23/19.66 Inuse: 814
% 19.23/19.66 Deleted: 298
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 388514
% 19.23/19.66 Kept: 40690
% 19.23/19.66 Inuse: 817
% 19.23/19.66 Deleted: 298
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 Resimplifying clauses:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 410592
% 19.23/19.66 Kept: 42714
% 19.23/19.66 Inuse: 849
% 19.23/19.66 Deleted: 652
% 19.23/19.66 Deletedinuse: 7
% 19.23/19.66
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66 *** allocated 2919240 integers for clauses
% 19.23/19.66 Resimplifying inuse:
% 19.23/19.66 Done
% 19.23/19.66
% 19.23/19.66
% 19.23/19.66 Intermediate Status:
% 19.23/19.66 Generated: 426009
% 41.84/42.23 Kept: 44765
% 41.84/42.23 Inuse: 882
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 455365
% 41.84/42.23 Kept: 46766
% 41.84/42.23 Inuse: 927
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 474853
% 41.84/42.23 Kept: 48826
% 41.84/42.23 Inuse: 968
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 493720
% 41.84/42.23 Kept: 50863
% 41.84/42.23 Inuse: 1003
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 523240
% 41.84/42.23 Kept: 52908
% 41.84/42.23 Inuse: 1037
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 *** allocated 1297440 integers for termspace/termends
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 544255
% 41.84/42.23 Kept: 54980
% 41.84/42.23 Inuse: 1071
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 566278
% 41.84/42.23 Kept: 56990
% 41.84/42.23 Inuse: 1111
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 588488
% 41.84/42.23 Kept: 59008
% 41.84/42.23 Inuse: 1156
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 610406
% 41.84/42.23 Kept: 61019
% 41.84/42.23 Inuse: 1199
% 41.84/42.23 Deleted: 652
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying clauses:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 639320
% 41.84/42.23 Kept: 63171
% 41.84/42.23 Inuse: 1250
% 41.84/42.23 Deleted: 737
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 671980
% 41.84/42.23 Kept: 65510
% 41.84/42.23 Inuse: 1285
% 41.84/42.23 Deleted: 737
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 *** allocated 4378860 integers for clauses
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 698231
% 41.84/42.23 Kept: 67873
% 41.84/42.23 Inuse: 1300
% 41.84/42.23 Deleted: 737
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 735963
% 41.84/42.23 Kept: 69896
% 41.84/42.23 Inuse: 1349
% 41.84/42.23 Deleted: 737
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 762524
% 41.84/42.23 Kept: 71904
% 41.84/42.23 Inuse: 1398
% 41.84/42.23 Deleted: 737
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 792660
% 41.84/42.23 Kept: 73946
% 41.84/42.23 Inuse: 1448
% 41.84/42.23 Deleted: 737
% 41.84/42.23 Deletedinuse: 7
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 817786
% 41.84/42.23 Kept: 76033
% 41.84/42.23 Inuse: 1461
% 41.84/42.23 Deleted: 738
% 41.84/42.23 Deletedinuse: 8
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 845004
% 41.84/42.23 Kept: 78090
% 41.84/42.23 Inuse: 1499
% 41.84/42.23 Deleted: 738
% 41.84/42.23 Deletedinuse: 8
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 871070
% 41.84/42.23 Kept: 80150
% 41.84/42.23 Inuse: 1531
% 41.84/42.23 Deleted: 738
% 41.84/42.23 Deletedinuse: 8
% 41.84/42.23
% 41.84/42.23 *** allocated 1946160 integers for termspace/termends
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 895612
% 41.84/42.23 Kept: 82339
% 41.84/42.23 Inuse: 1541
% 41.84/42.23 Deleted: 738
% 41.84/42.23 Deletedinuse: 8
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying clauses:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 917158
% 41.84/42.23 Kept: 84413
% 41.84/42.23 Inuse: 1578
% 41.84/42.23 Deleted: 778
% 41.84/42.23 Deletedinuse: 9
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 955916
% 41.84/42.23 Kept: 87964
% 41.84/42.23 Inuse: 1607
% 41.84/42.23 Deleted: 778
% 41.84/42.23 Deletedinuse: 9
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 976324
% 41.84/42.23 Kept: 90018
% 41.84/42.23 Inuse: 1642
% 41.84/42.23 Deleted: 781
% 41.84/42.23 Deletedinuse: 12
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 997355
% 41.84/42.23 Kept: 92033
% 41.84/42.23 Inuse: 1672
% 41.84/42.23 Deleted: 781
% 41.84/42.23 Deletedinuse: 12
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23 Resimplifying inuse:
% 41.84/42.23 Done
% 41.84/42.23
% 41.84/42.23
% 41.84/42.23 Intermediate Status:
% 41.84/42.23 Generated: 1028166
% 41.84/42.23 Kept: 94839
% 41.84/42.23 Inuse: 1689
% 126.54/127.12 Deleted: 781
% 126.54/127.12 Deletedinuse: 12
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 *** allocated 6568290 integers for clauses
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1049905
% 126.54/127.12 Kept: 96899
% 126.54/127.12 Inuse: 1726
% 126.54/127.12 Deleted: 784
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1072972
% 126.54/127.12 Kept: 98981
% 126.54/127.12 Inuse: 1756
% 126.54/127.12 Deleted: 784
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1094100
% 126.54/127.12 Kept: 101065
% 126.54/127.12 Inuse: 1771
% 126.54/127.12 Deleted: 784
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1114970
% 126.54/127.12 Kept: 103343
% 126.54/127.12 Inuse: 1773
% 126.54/127.12 Deleted: 784
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying clauses:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1147139
% 126.54/127.12 Kept: 105375
% 126.54/127.12 Inuse: 1829
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1184065
% 126.54/127.12 Kept: 107436
% 126.54/127.12 Inuse: 1887
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1213506
% 126.54/127.12 Kept: 109481
% 126.54/127.12 Inuse: 1933
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1248800
% 126.54/127.12 Kept: 111509
% 126.54/127.12 Inuse: 1987
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1286970
% 126.54/127.12 Kept: 113522
% 126.54/127.12 Inuse: 2043
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1320558
% 126.54/127.12 Kept: 115569
% 126.54/127.12 Inuse: 2093
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1350662
% 126.54/127.12 Kept: 117577
% 126.54/127.12 Inuse: 2143
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1383801
% 126.54/127.12 Kept: 119579
% 126.54/127.12 Inuse: 2196
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 *** allocated 2919240 integers for termspace/termends
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1422231
% 126.54/127.12 Kept: 123930
% 126.54/127.12 Inuse: 2198
% 126.54/127.12 Deleted: 971
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying clauses:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1445913
% 126.54/127.12 Kept: 126578
% 126.54/127.12 Inuse: 2201
% 126.54/127.12 Deleted: 1168
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1472779
% 126.54/127.12 Kept: 129576
% 126.54/127.12 Inuse: 2202
% 126.54/127.12 Deleted: 1168
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1509800
% 126.54/127.12 Kept: 132810
% 126.54/127.12 Inuse: 2204
% 126.54/127.12 Deleted: 1168
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1549357
% 126.54/127.12 Kept: 136038
% 126.54/127.12 Inuse: 2207
% 126.54/127.12 Deleted: 1168
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1575555
% 126.54/127.12 Kept: 138660
% 126.54/127.12 Inuse: 2209
% 126.54/127.12 Deleted: 1168
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1615257
% 126.54/127.12 Kept: 141910
% 126.54/127.12 Inuse: 2212
% 126.54/127.12 Deleted: 1168
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1653741
% 126.54/127.12 Kept: 144956
% 126.54/127.12 Inuse: 2214
% 126.54/127.12 Deleted: 1168
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying clauses:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 *** allocated 9852435 integers for clauses
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1680774
% 126.54/127.12 Kept: 147618
% 126.54/127.12 Inuse: 2217
% 126.54/127.12 Deleted: 1273
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 126.54/127.12 Generated: 1721727
% 126.54/127.12 Kept: 150966
% 126.54/127.12 Inuse: 2221
% 126.54/127.12 Deleted: 1273
% 126.54/127.12 Deletedinuse: 15
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12 Resimplifying inuse:
% 126.54/127.12 Done
% 126.54/127.12
% 126.54/127.12
% 126.54/127.12 Intermediate Status:
% 216.73/217.23 Generated: 1748197
% 216.73/217.23 Kept: 153602
% 216.73/217.23 Inuse: 2223
% 216.73/217.23 Deleted: 1273
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 1788417
% 216.73/217.23 Kept: 156871
% 216.73/217.23 Inuse: 2226
% 216.73/217.23 Deleted: 1273
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 1839637
% 216.73/217.23 Kept: 160528
% 216.73/217.23 Inuse: 2228
% 216.73/217.23 Deleted: 1273
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 1867559
% 216.73/217.23 Kept: 163172
% 216.73/217.23 Inuse: 2231
% 216.73/217.23 Deleted: 1273
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 1894420
% 216.73/217.23 Kept: 165861
% 216.73/217.23 Inuse: 2233
% 216.73/217.23 Deleted: 1273
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying clauses:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 1923645
% 216.73/217.23 Kept: 168620
% 216.73/217.23 Inuse: 2237
% 216.73/217.23 Deleted: 1341
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 1950620
% 216.73/217.23 Kept: 171311
% 216.73/217.23 Inuse: 2239
% 216.73/217.23 Deleted: 1341
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 1992832
% 216.73/217.23 Kept: 174690
% 216.73/217.23 Inuse: 2243
% 216.73/217.23 Deleted: 1341
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2033678
% 216.73/217.23 Kept: 177774
% 216.73/217.23 Inuse: 2246
% 216.73/217.23 Deleted: 1341
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 *** allocated 4378860 integers for termspace/termends
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2085795
% 216.73/217.23 Kept: 181667
% 216.73/217.23 Inuse: 2248
% 216.73/217.23 Deleted: 1341
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2113602
% 216.73/217.23 Kept: 184296
% 216.73/217.23 Inuse: 2251
% 216.73/217.23 Deleted: 1341
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2140749
% 216.73/217.23 Kept: 186969
% 216.73/217.23 Inuse: 2253
% 216.73/217.23 Deleted: 1341
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying clauses:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2169916
% 216.73/217.23 Kept: 189676
% 216.73/217.23 Inuse: 2256
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2193395
% 216.73/217.23 Kept: 191728
% 216.73/217.23 Inuse: 2266
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2218319
% 216.73/217.23 Kept: 193745
% 216.73/217.23 Inuse: 2289
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2259868
% 216.73/217.23 Kept: 195754
% 216.73/217.23 Inuse: 2336
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2300477
% 216.73/217.23 Kept: 197755
% 216.73/217.23 Inuse: 2384
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2331877
% 216.73/217.23 Kept: 199842
% 216.73/217.23 Inuse: 2411
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2370165
% 216.73/217.23 Kept: 201864
% 216.73/217.23 Inuse: 2442
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2415581
% 216.73/217.23 Kept: 203895
% 216.73/217.23 Inuse: 2482
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2452373
% 216.73/217.23 Kept: 205988
% 216.73/217.23 Inuse: 2511
% 216.73/217.23 Deleted: 1427
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying clauses:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2480558
% 216.73/217.23 Kept: 208009
% 216.73/217.23 Inuse: 2536
% 216.73/217.23 Deleted: 1502
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23 Resimplifying inuse:
% 216.73/217.23 Done
% 216.73/217.23
% 216.73/217.23
% 216.73/217.23 Intermediate Status:
% 216.73/217.23 Generated: 2506926
% 216.73/217.23 Kept: 210054
% 216.73/217.23 Inuse: 2559
% 216.73/217.23 Deleted: 1502
% 216.73/217.23 Deletedinuse: 15
% 216.73/217.23
% 216.73/217.23 ReTerminated
% 299.53/300.03 Bliksem ended
%------------------------------------------------------------------------------