%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Tue May 5 06:56:51 PM UTC 2026
% Result : Timeout 299.61s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : bliksem %s
% 0.16/0.34 % Computer : n009.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % DateTime : Tue May 5 12:38:40 EDT 2026
% 0.16/0.34 % CPUTime :
% 7.13/7.51 *** allocated 10000 integers for termspace/termends
% 7.13/7.51 *** allocated 10000 integers for clauses
% 7.13/7.51 *** allocated 10000 integers for justifications
% 7.13/7.51 Bliksem 1.12
% 7.13/7.51
% 7.13/7.51
% 7.13/7.51 Automatic Strategy Selection
% 7.13/7.51
% 7.13/7.51
% 7.13/7.51 Clauses:
% 7.13/7.51
% 7.13/7.51 { head( cons( X, Y ) ) = X }.
% 7.13/7.51 { tail( cons( X, Y ) ) = Y }.
% 7.13/7.51 { ! nil = cons( X, Y ) }.
% 7.13/7.51 { proj1Arr( arr( X, Y ) ) = X }.
% 7.13/7.51 { proj2Arr( arr( X, Y ) ) = Y }.
% 7.13/7.51 { ! arr( X, Y ) = a }.
% 7.13/7.51 { ! arr( X, Y ) = b }.
% 7.13/7.51 { ! arr( X, Y ) = c }.
% 7.13/7.51 { ! a = b }.
% 7.13/7.51 { ! a = c }.
% 7.13/7.51 { ! b = c }.
% 7.13/7.51 { proj1Suc( suc( X ) ) = X }.
% 7.13/7.51 { ! zero = suc( X ) }.
% 7.13/7.51 { proj1Just( just( X ) ) = X }.
% 7.13/7.51 { ! nothing = just( X ) }.
% 7.13/7.51 { proj1App( app( X, Y, Z ) ) = X }.
% 7.13/7.51 { proj2App( app( X, Y, Z ) ) = Y }.
% 7.13/7.51 { proj3App( app( X, Y, Z ) ) = Z }.
% 7.13/7.51 { proj1Lam( lam( X ) ) = X }.
% 7.13/7.51 { proj1Var( var( X ) ) = X }.
% 7.13/7.51 { ! app( X, Y, Z ) = lam( T ) }.
% 7.13/7.51 { ! app( X, Y, Z ) = var( T ) }.
% 7.13/7.51 { ! lam( X ) = var( Y ) }.
% 7.13/7.51 { index( nil, X ) = nothing }.
% 7.13/7.51 { index( cons( X, Y ), zero ) = just( X ) }.
% 7.13/7.51 { index( cons( X, Y ), suc( Z ) ) = index( Y, Z ) }.
% 7.13/7.51 { ! tc( X, app( Z, T, U ), Y ), tc( X, Z, arr( U, Y ) ) }.
% 7.13/7.51 { ! tc( X, app( Z, T, U ), Y ), tc( X, T, U ) }.
% 7.13/7.51 { ! tc( X, Z, arr( U, Y ) ), ! tc( X, T, U ), tc( X, app( Z, T, U ), Y ) }
% 7.13/7.51 .
% 7.13/7.51 { X = arr( proj1Arr( X ), proj2Arr( X ) ), ! tc( Y, lam( Z ), X ) }.
% 7.13/7.51 { ! tc( X, lam( Y ), arr( Z, T ) ), tc( cons( Z, X ), Y, T ) }.
% 7.13/7.51 { ! tc( cons( Z, X ), Y, T ), tc( X, lam( Y ), arr( Z, T ) ) }.
% 7.13/7.51 { ! index( X, Y ) = nothing, ! tc( X, var( Y ), Z ) }.
% 7.13/7.51 { ! index( X, Y ) = just( Z ), ! tc( X, var( Y ), T ), Z = T }.
% 7.13/7.51 { ! index( X, Y ) = just( Z ), ! Z = T, tc( X, var( Y ), T ) }.
% 7.13/7.51 { ! tc( nil, X, arr( arr( a, arr( a, b ) ), arr( a, b ) ) ) }.
% 7.13/7.51
% 7.13/7.51 percentage equality = 0.666667, percentage horn = 1.000000
% 7.13/7.51 This is a problem with some equality
% 7.13/7.51
% 7.13/7.51
% 7.13/7.51
% 7.13/7.51 Options Used:
% 7.13/7.51
% 7.13/7.51 useres = 1
% 7.13/7.51 useparamod = 1
% 7.13/7.51 useeqrefl = 1
% 7.13/7.51 useeqfact = 1
% 7.13/7.51 usefactor = 1
% 7.13/7.51 usesimpsplitting = 0
% 7.13/7.51 usesimpdemod = 5
% 7.13/7.51 usesimpres = 3
% 7.13/7.51
% 7.13/7.51 resimpinuse = 1000
% 7.13/7.51 resimpclauses = 20000
% 7.13/7.51 substype = eqrewr
% 7.13/7.51 backwardsubs = 1
% 7.13/7.51 selectoldest = 5
% 7.13/7.51
% 7.13/7.51 litorderings [0] = split
% 7.13/7.51 litorderings [1] = extend the termordering, first sorting on arguments
% 7.13/7.51
% 7.13/7.51 termordering = kbo
% 7.13/7.51
% 7.13/7.51 litapriori = 0
% 7.13/7.51 termapriori = 1
% 7.13/7.51 litaposteriori = 0
% 7.13/7.51 termaposteriori = 0
% 7.13/7.51 demodaposteriori = 0
% 7.13/7.51 ordereqreflfact = 0
% 7.13/7.51
% 7.13/7.51 litselect = negord
% 7.13/7.51
% 7.13/7.51 maxweight = 15
% 7.13/7.51 maxdepth = 30000
% 7.13/7.51 maxlength = 115
% 7.13/7.51 maxnrvars = 195
% 7.13/7.51 excuselevel = 1
% 7.13/7.51 increasemaxweight = 1
% 7.13/7.51
% 7.13/7.51 maxselected = 10000000
% 7.13/7.51 maxnrclauses = 10000000
% 7.13/7.51
% 7.13/7.51 showgenerated = 0
% 7.13/7.51 showkept = 0
% 7.13/7.51 showselected = 0
% 7.13/7.51 showdeleted = 0
% 7.13/7.51 showresimp = 1
% 7.13/7.51 showstatus = 2000
% 7.13/7.51
% 7.13/7.51 prologoutput = 0
% 7.13/7.51 nrgoals = 5000000
% 7.13/7.51 totalproof = 1
% 7.13/7.51
% 7.13/7.51 Symbols occurring in the translation:
% 7.13/7.51
% 7.13/7.51 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 7.13/7.51 . [1, 2] (w:1, o:46, a:1, s:1, b:0),
% 7.13/7.51 ! [4, 1] (w:0, o:26, a:1, s:1, b:0),
% 7.13/7.51 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.13/7.51 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.13/7.51 cons [37, 2] (w:1, o:70, a:1, s:1, b:0),
% 7.13/7.51 head [38, 1] (w:1, o:31, a:1, s:1, b:0),
% 7.13/7.51 tail [39, 1] (w:1, o:33, a:1, s:1, b:0),
% 7.13/7.51 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 7.13/7.51 arr [41, 2] (w:1, o:71, a:1, s:1, b:0),
% 7.13/7.51 proj1Arr [42, 1] (w:1, o:34, a:1, s:1, b:0),
% 7.13/7.51 proj2Arr [43, 1] (w:1, o:40, a:1, s:1, b:0),
% 7.13/7.51 a [44, 0] (w:1, o:9, a:1, s:1, b:0),
% 7.13/7.51 b [45, 0] (w:1, o:10, a:1, s:1, b:0),
% 7.13/7.51 c [46, 0] (w:1, o:11, a:1, s:1, b:0),
% 7.13/7.51 suc [47, 1] (w:1, o:32, a:1, s:1, b:0),
% 7.13/7.51 proj1Suc [48, 1] (w:1, o:35, a:1, s:1, b:0),
% 7.13/7.51 zero [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 7.13/7.51 just [50, 1] (w:1, o:41, a:1, s:1, b:0),
% 7.13/7.51 proj1Just [51, 1] (w:1, o:36, a:1, s:1, b:0),
% 7.13/7.51 nothing [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 7.13/7.51 app [54, 3] (w:1, o:73, a:1, s:1, b:0),
% 7.13/7.51 proj1App [55, 1] (w:1, o:37, a:1, s:1, b:0),
% 7.13/7.51 proj2App [56, 1] (w:1, o:42, a:1, s:1, b:0),
% 7.13/7.51 proj3App [57, 1] (w:1, o:43, a:1, s:1, b:0),
% 7.13/7.51 lam [58, 1] (w:1, o:44, a:1, s:1, b:0),
% 7.13/7.51 proj1Lam [59, 1] (w:1, o:38, a:1, s:1, b:0),
% 7.13/7.51 var [60, 1] (w:1, o:45, a:1, s:1, b:0),
% 7.13/7.51 proj1Var [61, 1] (w:1, o:39, a:1, s:1, b:0),
% 19.53/19.91 index [64, 2] (w:1, o:72, a:1, s:1, b:0),
% 19.53/19.91 tc [70, 3] (w:1, o:74, a:1, s:1, b:0).
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Starting Search:
% 19.53/19.91
% 19.53/19.91 *** allocated 15000 integers for clauses
% 19.53/19.91 *** allocated 22500 integers for clauses
% 19.53/19.91 *** allocated 33750 integers for clauses
% 19.53/19.91 *** allocated 15000 integers for termspace/termends
% 19.53/19.91 *** allocated 50625 integers for clauses
% 19.53/19.91 *** allocated 22500 integers for termspace/termends
% 19.53/19.91 *** allocated 75937 integers for clauses
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 33750 integers for termspace/termends
% 19.53/19.91 *** allocated 113905 integers for clauses
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 9444
% 19.53/19.91 Kept: 2004
% 19.53/19.91 Inuse: 220
% 19.53/19.91 Deleted: 1
% 19.53/19.91 Deletedinuse: 1
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 50625 integers for termspace/termends
% 19.53/19.91 *** allocated 170857 integers for clauses
% 19.53/19.91 *** allocated 75937 integers for termspace/termends
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 256285 integers for clauses
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 24746
% 19.53/19.91 Kept: 4140
% 19.53/19.91 Inuse: 315
% 19.53/19.91 Deleted: 5
% 19.53/19.91 Deletedinuse: 2
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 113905 integers for termspace/termends
% 19.53/19.91 *** allocated 384427 integers for clauses
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 42703
% 19.53/19.91 Kept: 6183
% 19.53/19.91 Inuse: 381
% 19.53/19.91 Deleted: 6
% 19.53/19.91 Deletedinuse: 2
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 170857 integers for termspace/termends
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 576640 integers for clauses
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 163015
% 19.53/19.91 Kept: 8428
% 19.53/19.91 Inuse: 619
% 19.53/19.91 Deleted: 7
% 19.53/19.91 Deletedinuse: 2
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 256285 integers for termspace/termends
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 172855
% 19.53/19.91 Kept: 11171
% 19.53/19.91 Inuse: 633
% 19.53/19.91 Deleted: 11
% 19.53/19.91 Deletedinuse: 6
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 864960 integers for clauses
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 183624
% 19.53/19.91 Kept: 13890
% 19.53/19.91 Inuse: 634
% 19.53/19.91 Deleted: 11
% 19.53/19.91 Deletedinuse: 6
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 384427 integers for termspace/termends
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 202731
% 19.53/19.91 Kept: 17109
% 19.53/19.91 Inuse: 657
% 19.53/19.91 Deleted: 11
% 19.53/19.91 Deletedinuse: 6
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 1297440 integers for clauses
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 209436
% 19.53/19.91 Kept: 19624
% 19.53/19.91 Inuse: 658
% 19.53/19.91 Deleted: 12
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 220461
% 19.53/19.91 Kept: 22380
% 19.53/19.91 Inuse: 659
% 19.53/19.91 Deleted: 12
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 Resimplifying clauses:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 576640 integers for termspace/termends
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 241336
% 19.53/19.91 Kept: 25796
% 19.53/19.91 Inuse: 682
% 19.53/19.91 Deleted: 297
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 1946160 integers for clauses
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 252599
% 19.53/19.91 Kept: 28581
% 19.53/19.91 Inuse: 683
% 19.53/19.91 Deleted: 297
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 283265
% 19.53/19.91 Kept: 30591
% 19.53/19.91 Inuse: 727
% 19.53/19.91 Deleted: 297
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 314571
% 19.53/19.91 Kept: 32616
% 19.53/19.91 Inuse: 768
% 19.53/19.91 Deleted: 297
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 363682
% 19.53/19.91 Kept: 34639
% 19.53/19.91 Inuse: 811
% 19.53/19.91 Deleted: 298
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 *** allocated 864960 integers for termspace/termends
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 376034
% 19.53/19.91 Kept: 37670
% 19.53/19.91 Inuse: 814
% 19.53/19.91 Deleted: 298
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 388356
% 19.53/19.91 Kept: 40690
% 19.53/19.91 Inuse: 817
% 19.53/19.91 Deleted: 298
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 Resimplifying clauses:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 410430
% 19.53/19.91 Kept: 42714
% 19.53/19.91 Inuse: 849
% 19.53/19.91 Deleted: 652
% 19.53/19.91 Deletedinuse: 7
% 19.53/19.91
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91 *** allocated 2919240 integers for clauses
% 19.53/19.91 Resimplifying inuse:
% 19.53/19.91 Done
% 19.53/19.91
% 19.53/19.91
% 19.53/19.91 Intermediate Status:
% 19.53/19.91 Generated: 425847
% 19.53/19.91 Kept: 44765
% 42.53/42.90 Inuse: 882
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 455199
% 42.53/42.90 Kept: 46766
% 42.53/42.90 Inuse: 927
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 474687
% 42.53/42.90 Kept: 48826
% 42.53/42.90 Inuse: 968
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 493554
% 42.53/42.90 Kept: 50863
% 42.53/42.90 Inuse: 1003
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 523070
% 42.53/42.90 Kept: 52908
% 42.53/42.90 Inuse: 1037
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 *** allocated 1297440 integers for termspace/termends
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 544085
% 42.53/42.90 Kept: 54980
% 42.53/42.90 Inuse: 1071
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 566108
% 42.53/42.90 Kept: 56990
% 42.53/42.90 Inuse: 1111
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 588318
% 42.53/42.90 Kept: 59008
% 42.53/42.90 Inuse: 1156
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 610236
% 42.53/42.90 Kept: 61019
% 42.53/42.90 Inuse: 1199
% 42.53/42.90 Deleted: 652
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying clauses:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 639148
% 42.53/42.90 Kept: 63171
% 42.53/42.90 Inuse: 1250
% 42.53/42.90 Deleted: 737
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 671802
% 42.53/42.90 Kept: 65510
% 42.53/42.90 Inuse: 1285
% 42.53/42.90 Deleted: 737
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 *** allocated 4378860 integers for clauses
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 698047
% 42.53/42.90 Kept: 67873
% 42.53/42.90 Inuse: 1300
% 42.53/42.90 Deleted: 737
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 735775
% 42.53/42.90 Kept: 69896
% 42.53/42.90 Inuse: 1349
% 42.53/42.90 Deleted: 737
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 762336
% 42.53/42.90 Kept: 71904
% 42.53/42.90 Inuse: 1398
% 42.53/42.90 Deleted: 737
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 790509
% 42.53/42.90 Kept: 73952
% 42.53/42.90 Inuse: 1448
% 42.53/42.90 Deleted: 737
% 42.53/42.90 Deletedinuse: 7
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 815325
% 42.53/42.90 Kept: 76039
% 42.53/42.90 Inuse: 1461
% 42.53/42.90 Deleted: 738
% 42.53/42.90 Deletedinuse: 8
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 839822
% 42.53/42.90 Kept: 78107
% 42.53/42.90 Inuse: 1499
% 42.53/42.90 Deleted: 738
% 42.53/42.90 Deletedinuse: 8
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 861474
% 42.53/42.90 Kept: 80119
% 42.53/42.90 Inuse: 1529
% 42.53/42.90 Deleted: 738
% 42.53/42.90 Deletedinuse: 8
% 42.53/42.90
% 42.53/42.90 *** allocated 1946160 integers for termspace/termends
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 886962
% 42.53/42.90 Kept: 82378
% 42.53/42.90 Inuse: 1541
% 42.53/42.90 Deleted: 738
% 42.53/42.90 Deletedinuse: 8
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying clauses:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 908287
% 42.53/42.90 Kept: 84444
% 42.53/42.90 Inuse: 1578
% 42.53/42.90 Deleted: 778
% 42.53/42.90 Deletedinuse: 9
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 946878
% 42.53/42.90 Kept: 87995
% 42.53/42.90 Inuse: 1607
% 42.53/42.90 Deleted: 778
% 42.53/42.90 Deletedinuse: 9
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 966444
% 42.53/42.90 Kept: 90029
% 42.53/42.90 Inuse: 1642
% 42.53/42.90 Deleted: 781
% 42.53/42.90 Deletedinuse: 12
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 987308
% 42.53/42.90 Kept: 92051
% 42.53/42.90 Inuse: 1672
% 42.53/42.90 Deleted: 781
% 42.53/42.90 Deletedinuse: 12
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90 Resimplifying inuse:
% 42.53/42.90 Done
% 42.53/42.90
% 42.53/42.90
% 42.53/42.90 Intermediate Status:
% 42.53/42.90 Generated: 1018342
% 42.53/42.90 Kept: 94865
% 42.53/42.90 Inuse: 1689
% 42.53/42.90 Deleted: 781
% 108.80/109.24 Deletedinuse: 12
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 *** allocated 6568290 integers for clauses
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1039459
% 108.80/109.24 Kept: 96878
% 108.80/109.24 Inuse: 1724
% 108.80/109.24 Deleted: 784
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1062367
% 108.80/109.24 Kept: 98930
% 108.80/109.24 Inuse: 1754
% 108.80/109.24 Deleted: 784
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1084399
% 108.80/109.24 Kept: 101088
% 108.80/109.24 Inuse: 1771
% 108.80/109.24 Deleted: 784
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1105095
% 108.80/109.24 Kept: 103366
% 108.80/109.24 Inuse: 1773
% 108.80/109.24 Deleted: 784
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying clauses:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1137101
% 108.80/109.24 Kept: 105383
% 108.80/109.24 Inuse: 1828
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1174118
% 108.80/109.24 Kept: 107404
% 108.80/109.24 Inuse: 1886
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1203301
% 108.80/109.24 Kept: 109435
% 108.80/109.24 Inuse: 1932
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1236866
% 108.80/109.24 Kept: 111438
% 108.80/109.24 Inuse: 1984
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1275708
% 108.80/109.24 Kept: 113444
% 108.80/109.24 Inuse: 2041
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1309569
% 108.80/109.24 Kept: 115469
% 108.80/109.24 Inuse: 2091
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1339209
% 108.80/109.24 Kept: 117482
% 108.80/109.24 Inuse: 2141
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1372366
% 108.80/109.24 Kept: 119504
% 108.80/109.24 Inuse: 2193
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 *** allocated 2919240 integers for termspace/termends
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1412312
% 108.80/109.24 Kept: 123941
% 108.80/109.24 Inuse: 2198
% 108.80/109.24 Deleted: 973
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying clauses:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1436296
% 108.80/109.24 Kept: 126602
% 108.80/109.24 Inuse: 2201
% 108.80/109.24 Deleted: 1170
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1463001
% 108.80/109.24 Kept: 129601
% 108.80/109.24 Inuse: 2202
% 108.80/109.24 Deleted: 1170
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1499781
% 108.80/109.24 Kept: 132836
% 108.80/109.24 Inuse: 2204
% 108.80/109.24 Deleted: 1170
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1539097
% 108.80/109.24 Kept: 136065
% 108.80/109.24 Inuse: 2207
% 108.80/109.24 Deleted: 1170
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1565135
% 108.80/109.24 Kept: 138687
% 108.80/109.24 Inuse: 2209
% 108.80/109.24 Deleted: 1170
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1604596
% 108.80/109.24 Kept: 141938
% 108.80/109.24 Inuse: 2212
% 108.80/109.24 Deleted: 1170
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1642839
% 108.80/109.24 Kept: 144984
% 108.80/109.24 Inuse: 2214
% 108.80/109.24 Deleted: 1170
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying clauses:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 *** allocated 9852435 integers for clauses
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1670306
% 108.80/109.24 Kept: 147646
% 108.80/109.24 Inuse: 2217
% 108.80/109.24 Deleted: 1275
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 108.80/109.24 Intermediate Status:
% 108.80/109.24 Generated: 1711390
% 108.80/109.24 Kept: 150977
% 108.80/109.24 Inuse: 2221
% 108.80/109.24 Deleted: 1275
% 108.80/109.24 Deletedinuse: 15
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24 Resimplifying inuse:
% 108.80/109.24 Done
% 108.80/109.24
% 108.80/109.24
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 1737714
% 190.30/190.75 Kept: 153613
% 190.30/190.75 Inuse: 2223
% 190.30/190.75 Deleted: 1275
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 1777931
% 190.30/190.75 Kept: 156882
% 190.30/190.75 Inuse: 2226
% 190.30/190.75 Deleted: 1275
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 1828867
% 190.30/190.75 Kept: 160539
% 190.30/190.75 Inuse: 2228
% 190.30/190.75 Deleted: 1275
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 1856133
% 190.30/190.75 Kept: 163183
% 190.30/190.75 Inuse: 2231
% 190.30/190.75 Deleted: 1275
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 1882844
% 190.30/190.75 Kept: 165872
% 190.30/190.75 Inuse: 2233
% 190.30/190.75 Deleted: 1275
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying clauses:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 1912278
% 190.30/190.75 Kept: 168631
% 190.30/190.75 Inuse: 2237
% 190.30/190.75 Deleted: 1343
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 1939109
% 190.30/190.75 Kept: 171322
% 190.30/190.75 Inuse: 2239
% 190.30/190.75 Deleted: 1343
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 1981026
% 190.30/190.75 Kept: 174701
% 190.30/190.75 Inuse: 2243
% 190.30/190.75 Deleted: 1343
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2020787
% 190.30/190.75 Kept: 177785
% 190.30/190.75 Inuse: 2246
% 190.30/190.75 Deleted: 1343
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 *** allocated 4378860 integers for termspace/termends
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2072588
% 190.30/190.75 Kept: 181678
% 190.30/190.75 Inuse: 2248
% 190.30/190.75 Deleted: 1343
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2101213
% 190.30/190.75 Kept: 184307
% 190.30/190.75 Inuse: 2251
% 190.30/190.75 Deleted: 1343
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2128216
% 190.30/190.75 Kept: 186980
% 190.30/190.75 Inuse: 2253
% 190.30/190.75 Deleted: 1343
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying clauses:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2157161
% 190.30/190.75 Kept: 189687
% 190.30/190.75 Inuse: 2256
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2179105
% 190.30/190.75 Kept: 191754
% 190.30/190.75 Inuse: 2265
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2205308
% 190.30/190.75 Kept: 193818
% 190.30/190.75 Inuse: 2289
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2246472
% 190.30/190.75 Kept: 195833
% 190.30/190.75 Inuse: 2338
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2288561
% 190.30/190.75 Kept: 197854
% 190.30/190.75 Inuse: 2386
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2317850
% 190.30/190.75 Kept: 199861
% 190.30/190.75 Inuse: 2411
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2356191
% 190.30/190.75 Kept: 201886
% 190.30/190.75 Inuse: 2442
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2401411
% 190.30/190.75 Kept: 203919
% 190.30/190.75 Inuse: 2482
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2438382
% 190.30/190.75 Kept: 206010
% 190.30/190.75 Inuse: 2511
% 190.30/190.75 Deleted: 1429
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying clauses:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2466508
% 190.30/190.75 Kept: 208038
% 190.30/190.75 Inuse: 2536
% 190.30/190.75 Deleted: 1504
% 190.30/190.75 Deletedinuse: 15
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75 Resimplifying inuse:
% 190.30/190.75 Done
% 190.30/190.75
% 190.30/190.75
% 190.30/190.75 Intermediate Status:
% 190.30/190.75 Generated: 2511136
% 190.30/190.75 Kept: 210087
% 190.30/190.75 Inuse: 2553
% 190.30/190.75 Deleted: 1504
% 190.30/190.75 DelTerminated
% 299.61/300.03 Bliksem ended
%------------------------------------------------------------------------------