%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX221+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n029.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.64s 300.04s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX221+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n029.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % DateTime : Tue May 5 12:28:59 EDT 2026
% 0.15/0.33 % CPUTime :
% 2.65/3.12 *** allocated 10000 integers for termspace/termends
% 2.65/3.12 *** allocated 10000 integers for clauses
% 2.65/3.12 *** allocated 10000 integers for justifications
% 2.65/3.12 Bliksem 1.12
% 2.65/3.12
% 2.65/3.12
% 2.65/3.12 Automatic Strategy Selection
% 2.65/3.12
% 2.65/3.12
% 2.65/3.12 Clauses:
% 2.65/3.12
% 2.65/3.12 { head( cons( X, Y ) ) = X }.
% 2.65/3.12 { tail( cons( X, Y ) ) = Y }.
% 2.65/3.12 { ! nil = cons( X, Y ) }.
% 2.65/3.12 { proj1Arr( arr( X, Y ) ) = X }.
% 2.65/3.12 { proj2Arr( arr( X, Y ) ) = Y }.
% 2.65/3.12 { ! arr( X, Y ) = a }.
% 2.65/3.12 { ! arr( X, Y ) = b }.
% 2.65/3.12 { ! arr( X, Y ) = c }.
% 2.65/3.12 { ! a = b }.
% 2.65/3.12 { ! a = c }.
% 2.65/3.12 { ! b = c }.
% 2.65/3.12 { proj1Suc( suc( X ) ) = X }.
% 2.65/3.12 { ! zero = suc( X ) }.
% 2.65/3.12 { proj1Just( just( X ) ) = X }.
% 2.65/3.12 { ! nothing = just( X ) }.
% 2.65/3.12 { proj1App( app( X, Y, Z ) ) = X }.
% 2.65/3.12 { proj2App( app( X, Y, Z ) ) = Y }.
% 2.65/3.12 { proj3App( app( X, Y, Z ) ) = Z }.
% 2.65/3.12 { proj1Lam( lam( X ) ) = X }.
% 2.65/3.12 { proj1Var( var( X ) ) = X }.
% 2.65/3.12 { ! app( X, Y, Z ) = lam( T ) }.
% 2.65/3.12 { ! app( X, Y, Z ) = var( T ) }.
% 2.65/3.12 { ! lam( X ) = var( Y ) }.
% 2.65/3.12 { X = lam( proj1Lam( X ) ), ! nf( app( X, Y, Z ) ), nf( X ) }.
% 2.65/3.12 { X = lam( proj1Lam( X ) ), ! nf( app( X, Y, Z ) ), nf( Y ) }.
% 2.65/3.12 { X = lam( proj1Lam( X ) ), ! nf( X ), ! nf( Y ), nf( app( X, Y, Z ) ) }.
% 2.65/3.12 { ! nf( app( lam( Z ), X, Y ) ) }.
% 2.65/3.12 { ! nf( lam( X ) ), nf( X ) }.
% 2.65/3.12 { ! nf( X ), nf( lam( X ) ) }.
% 2.65/3.12 { nf( var( X ) ) }.
% 2.65/3.12 { index( nil, X ) = nothing }.
% 2.65/3.12 { index( cons( X, Y ), zero ) = just( X ) }.
% 2.65/3.12 { index( cons( X, Y ), suc( Z ) ) = index( Y, Z ) }.
% 2.65/3.12 { ! tc( X, app( Z, T, U ), Y ), tc( X, Z, arr( U, Y ) ) }.
% 2.65/3.12 { ! tc( X, app( Z, T, U ), Y ), tc( X, T, U ) }.
% 2.65/3.12 { ! tc( X, Z, arr( U, Y ) ), ! tc( X, T, U ), tc( X, app( Z, T, U ), Y ) }
% 2.65/3.12 .
% 2.65/3.12 { X = arr( proj1Arr( X ), proj2Arr( X ) ), ! tc( Y, lam( Z ), X ) }.
% 2.65/3.12 { ! tc( X, lam( Y ), arr( Z, T ) ), tc( cons( Z, X ), Y, T ) }.
% 2.65/3.12 { ! tc( cons( Z, X ), Y, T ), tc( X, lam( Y ), arr( Z, T ) ) }.
% 2.65/3.12 { ! index( X, Y ) = nothing, ! tc( X, var( Y ), Z ) }.
% 2.65/3.12 { ! index( X, Y ) = just( Z ), ! tc( X, var( Y ), T ), Z = T }.
% 2.65/3.12 { ! index( X, Y ) = just( Z ), ! Z = T, tc( X, var( Y ), T ) }.
% 2.65/3.12 { ! nf( X ), ! tc( nil, X, arr( arr( a, arr( b, c ) ), arr( b, arr( a, c )
% 2.65/3.12 ) ) ) }.
% 2.65/3.12
% 2.65/3.12 percentage equality = 0.538462, percentage horn = 0.930233
% 2.65/3.12 This is a problem with some equality
% 2.65/3.12
% 2.65/3.12
% 2.65/3.12
% 2.65/3.12 Options Used:
% 2.65/3.12
% 2.65/3.12 useres = 1
% 2.65/3.12 useparamod = 1
% 2.65/3.12 useeqrefl = 1
% 2.65/3.12 useeqfact = 1
% 2.65/3.12 usefactor = 1
% 2.65/3.12 usesimpsplitting = 0
% 2.65/3.12 usesimpdemod = 5
% 2.65/3.12 usesimpres = 3
% 2.65/3.12
% 2.65/3.12 resimpinuse = 1000
% 2.65/3.12 resimpclauses = 20000
% 2.65/3.12 substype = eqrewr
% 2.65/3.12 backwardsubs = 1
% 2.65/3.12 selectoldest = 5
% 2.65/3.12
% 2.65/3.12 litorderings [0] = split
% 2.65/3.12 litorderings [1] = extend the termordering, first sorting on arguments
% 2.65/3.12
% 2.65/3.12 termordering = kbo
% 2.65/3.12
% 2.65/3.12 litapriori = 0
% 2.65/3.12 termapriori = 1
% 2.65/3.12 litaposteriori = 0
% 2.65/3.12 termaposteriori = 0
% 2.65/3.12 demodaposteriori = 0
% 2.65/3.12 ordereqreflfact = 0
% 2.65/3.12
% 2.65/3.12 litselect = negord
% 2.65/3.12
% 2.65/3.12 maxweight = 15
% 2.65/3.12 maxdepth = 30000
% 2.65/3.12 maxlength = 115
% 2.65/3.12 maxnrvars = 195
% 2.65/3.12 excuselevel = 1
% 2.65/3.12 increasemaxweight = 1
% 2.65/3.12
% 2.65/3.12 maxselected = 10000000
% 2.65/3.12 maxnrclauses = 10000000
% 2.65/3.12
% 2.65/3.12 showgenerated = 0
% 2.65/3.12 showkept = 0
% 2.65/3.12 showselected = 0
% 2.65/3.12 showdeleted = 0
% 2.65/3.12 showresimp = 1
% 2.65/3.12 showstatus = 2000
% 2.65/3.12
% 2.65/3.12 prologoutput = 0
% 2.65/3.12 nrgoals = 5000000
% 2.65/3.12 totalproof = 1
% 2.65/3.12
% 2.65/3.12 Symbols occurring in the translation:
% 2.65/3.12
% 2.65/3.12 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.65/3.12 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 2.65/3.12 ! [4, 1] (w:0, o:26, a:1, s:1, b:0),
% 2.65/3.12 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.65/3.12 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.65/3.12 cons [37, 2] (w:1, o:71, a:1, s:1, b:0),
% 2.65/3.12 head [38, 1] (w:1, o:31, a:1, s:1, b:0),
% 2.65/3.12 tail [39, 1] (w:1, o:33, a:1, s:1, b:0),
% 2.65/3.12 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 2.65/3.12 arr [41, 2] (w:1, o:72, a:1, s:1, b:0),
% 2.65/3.12 proj1Arr [42, 1] (w:1, o:34, a:1, s:1, b:0),
% 2.65/3.12 proj2Arr [43, 1] (w:1, o:40, a:1, s:1, b:0),
% 2.65/3.12 a [44, 0] (w:1, o:9, a:1, s:1, b:0),
% 2.65/3.12 b [45, 0] (w:1, o:10, a:1, s:1, b:0),
% 2.65/3.12 c [46, 0] (w:1, o:11, a:1, s:1, b:0),
% 2.65/3.12 suc [47, 1] (w:1, o:32, a:1, s:1, b:0),
% 2.65/3.12 proj1Suc [48, 1] (w:1, o:35, a:1, s:1, b:0),
% 2.65/3.12 zero [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 2.65/3.12 just [50, 1] (w:1, o:41, a:1, s:1, b:0),
% 2.65/3.12 proj1Just [51, 1] (w:1, o:36, a:1, s:1, b:0),
% 2.65/3.12 nothing [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 2.65/3.12 app [54, 3] (w:1, o:74, a:1, s:1, b:0),
% 12.82/13.29 proj1App [55, 1] (w:1, o:37, a:1, s:1, b:0),
% 12.82/13.29 proj2App [56, 1] (w:1, o:42, a:1, s:1, b:0),
% 12.82/13.29 proj3App [57, 1] (w:1, o:43, a:1, s:1, b:0),
% 12.82/13.29 lam [58, 1] (w:1, o:44, a:1, s:1, b:0),
% 12.82/13.29 proj1Lam [59, 1] (w:1, o:38, a:1, s:1, b:0),
% 12.82/13.29 var [60, 1] (w:1, o:45, a:1, s:1, b:0),
% 12.82/13.29 proj1Var [61, 1] (w:1, o:39, a:1, s:1, b:0),
% 12.82/13.29 nf [65, 1] (w:1, o:46, a:1, s:1, b:0),
% 12.82/13.29 index [67, 2] (w:1, o:73, a:1, s:1, b:0),
% 12.82/13.29 tc [72, 3] (w:1, o:75, a:1, s:1, b:0).
% 12.82/13.29
% 12.82/13.29
% 12.82/13.29 Starting Search:
% 12.82/13.29
% 12.82/13.29 *** allocated 15000 integers for clauses
% 12.82/13.29 *** allocated 22500 integers for clauses
% 12.82/13.29 *** allocated 33750 integers for clauses
% 12.82/13.29 *** allocated 15000 integers for termspace/termends
% 12.82/13.29 *** allocated 50625 integers for clauses
% 12.82/13.29 *** allocated 22500 integers for termspace/termends
% 12.82/13.29 *** allocated 75937 integers for clauses
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 33750 integers for termspace/termends
% 12.82/13.29 *** allocated 113905 integers for clauses
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 6430
% 12.82/13.29 Kept: 2011
% 12.82/13.29 Inuse: 165
% 12.82/13.29 Deleted: 13
% 12.82/13.29 Deletedinuse: 3
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 50625 integers for termspace/termends
% 12.82/13.29 *** allocated 170857 integers for clauses
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 75937 integers for termspace/termends
% 12.82/13.29 *** allocated 256285 integers for clauses
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 20440
% 12.82/13.29 Kept: 4246
% 12.82/13.29 Inuse: 287
% 12.82/13.29 Deleted: 31
% 12.82/13.29 Deletedinuse: 3
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 113905 integers for termspace/termends
% 12.82/13.29 *** allocated 384427 integers for clauses
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 33924
% 12.82/13.29 Kept: 6246
% 12.82/13.29 Inuse: 366
% 12.82/13.29 Deleted: 39
% 12.82/13.29 Deletedinuse: 3
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 170857 integers for termspace/termends
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 576640 integers for clauses
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 58553
% 12.82/13.29 Kept: 8250
% 12.82/13.29 Inuse: 485
% 12.82/13.29 Deleted: 39
% 12.82/13.29 Deletedinuse: 3
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 96878
% 12.82/13.29 Kept: 10357
% 12.82/13.29 Inuse: 671
% 12.82/13.29 Deleted: 48
% 12.82/13.29 Deletedinuse: 5
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 256285 integers for termspace/termends
% 12.82/13.29 *** allocated 864960 integers for clauses
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 106521
% 12.82/13.29 Kept: 13534
% 12.82/13.29 Inuse: 686
% 12.82/13.29 Deleted: 51
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 384427 integers for termspace/termends
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 117812
% 12.82/13.29 Kept: 16630
% 12.82/13.29 Inuse: 687
% 12.82/13.29 Deleted: 51
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 1297440 integers for clauses
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 128629
% 12.82/13.29 Kept: 20211
% 12.82/13.29 Inuse: 710
% 12.82/13.29 Deleted: 51
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 Resimplifying clauses:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 135863
% 12.82/13.29 Kept: 23092
% 12.82/13.29 Inuse: 711
% 12.82/13.29 Deleted: 353
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 576640 integers for termspace/termends
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 147394
% 12.82/13.29 Kept: 26189
% 12.82/13.29 Inuse: 712
% 12.82/13.29 Deleted: 353
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 1946160 integers for clauses
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 158812
% 12.82/13.29 Kept: 29979
% 12.82/13.29 Inuse: 735
% 12.82/13.29 Deleted: 353
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 170565
% 12.82/13.29 Kept: 33139
% 12.82/13.29 Inuse: 736
% 12.82/13.29 Deleted: 353
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 180556
% 12.82/13.29 Kept: 35158
% 12.82/13.29 Inuse: 780
% 12.82/13.29 Deleted: 353
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 *** allocated 864960 integers for termspace/termends
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 192989
% 12.82/13.29 Kept: 37187
% 12.82/13.29 Inuse: 821
% 12.82/13.29 Deleted: 353
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 205331
% 12.82/13.29 Kept: 39222
% 12.82/13.29 Inuse: 860
% 12.82/13.29 Deleted: 354
% 12.82/13.29 Deletedinuse: 8
% 12.82/13.29
% 12.82/13.29 Resimplifying inuse:
% 12.82/13.29 Done
% 12.82/13.29
% 12.82/13.29
% 12.82/13.29 Intermediate Status:
% 12.82/13.29 Generated: 217500
% 12.82/13.29 Kept: 41877
% 12.82/13.29 Inuse: 883
% 38.73/39.13 Deleted: 355
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying clauses:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 *** allocated 2919240 integers for clauses
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 229884
% 38.73/39.13 Kept: 45275
% 38.73/39.13 Inuse: 885
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 238108
% 38.73/39.13 Kept: 47335
% 38.73/39.13 Inuse: 892
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 246203
% 38.73/39.13 Kept: 49358
% 38.73/39.13 Inuse: 922
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 255272
% 38.73/39.13 Kept: 51364
% 38.73/39.13 Inuse: 953
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 269177
% 38.73/39.13 Kept: 53395
% 38.73/39.13 Inuse: 1002
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 *** allocated 1297440 integers for termspace/termends
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 283391
% 38.73/39.13 Kept: 55409
% 38.73/39.13 Inuse: 1034
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 294437
% 38.73/39.13 Kept: 57475
% 38.73/39.13 Inuse: 1070
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 304635
% 38.73/39.13 Kept: 59491
% 38.73/39.13 Inuse: 1105
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 315721
% 38.73/39.13 Kept: 61521
% 38.73/39.13 Inuse: 1139
% 38.73/39.13 Deleted: 845
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying clauses:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 327955
% 38.73/39.13 Kept: 63522
% 38.73/39.13 Inuse: 1174
% 38.73/39.13 Deleted: 933
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 342730
% 38.73/39.13 Kept: 65544
% 38.73/39.13 Inuse: 1217
% 38.73/39.13 Deleted: 933
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 *** allocated 4378860 integers for clauses
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 354211
% 38.73/39.13 Kept: 67607
% 38.73/39.13 Inuse: 1263
% 38.73/39.13 Deleted: 933
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 368410
% 38.73/39.13 Kept: 69664
% 38.73/39.13 Inuse: 1308
% 38.73/39.13 Deleted: 933
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 378939
% 38.73/39.13 Kept: 71733
% 38.73/39.13 Inuse: 1347
% 38.73/39.13 Deleted: 933
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 389180
% 38.73/39.13 Kept: 73745
% 38.73/39.13 Inuse: 1397
% 38.73/39.13 Deleted: 934
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 399740
% 38.73/39.13 Kept: 75773
% 38.73/39.13 Inuse: 1446
% 38.73/39.13 Deleted: 935
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 410578
% 38.73/39.13 Kept: 77817
% 38.73/39.13 Inuse: 1495
% 38.73/39.13 Deleted: 936
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 419884
% 38.73/39.13 Kept: 79844
% 38.73/39.13 Inuse: 1542
% 38.73/39.13 Deleted: 936
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 *** allocated 1946160 integers for termspace/termends
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 492121
% 38.73/39.13 Kept: 83364
% 38.73/39.13 Inuse: 1589
% 38.73/39.13 Deleted: 936
% 38.73/39.13 Deletedinuse: 8
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying clauses:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 553735
% 38.73/39.13 Kept: 85408
% 38.73/39.13 Inuse: 1626
% 38.73/39.13 Deleted: 1046
% 38.73/39.13 Deletedinuse: 9
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 611336
% 38.73/39.13 Kept: 87452
% 38.73/39.13 Inuse: 1657
% 38.73/39.13 Deleted: 1046
% 38.73/39.13 Deletedinuse: 9
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 38.73/39.13 Generated: 635344
% 38.73/39.13 Kept: 90029
% 38.73/39.13 Inuse: 1671
% 38.73/39.13 Deleted: 1046
% 38.73/39.13 Deletedinuse: 9
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13 Resimplifying inuse:
% 38.73/39.13 Done
% 38.73/39.13
% 38.73/39.13
% 38.73/39.13 Intermediate Status:
% 94.74/95.16 Generated: 651515
% 94.74/95.16 Kept: 92059
% 94.74/95.16 Inuse: 1709
% 94.74/95.16 Deleted: 1047
% 94.74/95.16 Deletedinuse: 10
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 715931
% 94.74/95.16 Kept: 95758
% 94.74/95.16 Inuse: 1737
% 94.74/95.16 Deleted: 1047
% 94.74/95.16 Deletedinuse: 10
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 *** allocated 6568290 integers for clauses
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 733172
% 94.74/95.16 Kept: 97806
% 94.74/95.16 Inuse: 1774
% 94.74/95.16 Deleted: 1050
% 94.74/95.16 Deletedinuse: 13
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 749861
% 94.74/95.16 Kept: 99822
% 94.74/95.16 Inuse: 1804
% 94.74/95.16 Deleted: 1050
% 94.74/95.16 Deletedinuse: 13
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 794556
% 94.74/95.16 Kept: 102722
% 94.74/95.16 Inuse: 1820
% 94.74/95.16 Deleted: 1050
% 94.74/95.16 Deletedinuse: 13
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying clauses:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 868566
% 94.74/95.16 Kept: 104751
% 94.74/95.16 Inuse: 1856
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 918358
% 94.74/95.16 Kept: 107997
% 94.74/95.16 Inuse: 1886
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 940150
% 94.74/95.16 Kept: 110577
% 94.74/95.16 Inuse: 1889
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 996023
% 94.74/95.16 Kept: 112580
% 94.74/95.16 Inuse: 1946
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1062645
% 94.74/95.16 Kept: 114615
% 94.74/95.16 Inuse: 2004
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1173555
% 94.74/95.16 Kept: 116666
% 94.74/95.16 Inuse: 2052
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1229722
% 94.74/95.16 Kept: 118680
% 94.74/95.16 Inuse: 2109
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1286080
% 94.74/95.16 Kept: 120687
% 94.74/95.16 Inuse: 2165
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 *** allocated 2919240 integers for termspace/termends
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1335166
% 94.74/95.16 Kept: 122696
% 94.74/95.16 Inuse: 2202
% 94.74/95.16 Deleted: 1227
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying clauses:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1368757
% 94.74/95.16 Kept: 124714
% 94.74/95.16 Inuse: 2255
% 94.74/95.16 Deleted: 1382
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1398791
% 94.74/95.16 Kept: 126747
% 94.74/95.16 Inuse: 2307
% 94.74/95.16 Deleted: 1382
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1432974
% 94.74/95.16 Kept: 128791
% 94.74/95.16 Inuse: 2364
% 94.74/95.16 Deleted: 1382
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1453519
% 94.74/95.16 Kept: 130877
% 94.74/95.16 Inuse: 2377
% 94.74/95.16 Deleted: 1382
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1481935
% 94.74/95.16 Kept: 134185
% 94.74/95.16 Inuse: 2379
% 94.74/95.16 Deleted: 1382
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1505572
% 94.74/95.16 Kept: 137137
% 94.74/95.16 Inuse: 2381
% 94.74/95.16 Deleted: 1382
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1532996
% 94.74/95.16 Kept: 140416
% 94.74/95.16 Inuse: 2382
% 94.74/95.16 Deleted: 1382
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1571918
% 94.74/95.16 Kept: 143984
% 94.74/95.16 Inuse: 2385
% 94.74/95.16 Deleted: 1382
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying clauses:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16
% 94.74/95.16 Intermediate Status:
% 94.74/95.16 Generated: 1611255
% 94.74/95.16 Kept: 147529
% 94.74/95.16 Inuse: 2387
% 94.74/95.16 Deleted: 1679
% 94.74/95.16 Deletedinuse: 16
% 94.74/95.16
% 94.74/95.16 Resimplifying inuse:
% 94.74/95.16 Done
% 94.74/95.16
% 94.74/95.16 *** allocated 9852435 integers for clauses
% 94.74/95.16 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1639540
% 187.82/188.26 Kept: 150488
% 187.82/188.26 Inuse: 2390
% 187.82/188.26 Deleted: 1679
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1665466
% 187.82/188.26 Kept: 152605
% 187.82/188.26 Inuse: 2391
% 187.82/188.26 Deleted: 1679
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1706968
% 187.82/188.26 Kept: 156142
% 187.82/188.26 Inuse: 2395
% 187.82/188.26 Deleted: 1679
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1736292
% 187.82/188.26 Kept: 159229
% 187.82/188.26 Inuse: 2399
% 187.82/188.26 Deleted: 1679
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1766403
% 187.82/188.26 Kept: 162406
% 187.82/188.26 Inuse: 2404
% 187.82/188.26 Deleted: 1679
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1796184
% 187.82/188.26 Kept: 164640
% 187.82/188.26 Inuse: 2409
% 187.82/188.26 Deleted: 1679
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 Resimplifying clauses:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1823638
% 187.82/188.26 Kept: 167614
% 187.82/188.26 Inuse: 2411
% 187.82/188.26 Deleted: 1750
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1849841
% 187.82/188.26 Kept: 169743
% 187.82/188.26 Inuse: 2412
% 187.82/188.26 Deleted: 1750
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1891186
% 187.82/188.26 Kept: 173243
% 187.82/188.26 Inuse: 2415
% 187.82/188.26 Deleted: 1750
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1917431
% 187.82/188.26 Kept: 175350
% 187.82/188.26 Inuse: 2416
% 187.82/188.26 Deleted: 1750
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1946235
% 187.82/188.26 Kept: 178341
% 187.82/188.26 Inuse: 2419
% 187.82/188.26 Deleted: 1750
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26
% 187.82/188.26 Intermediate Status:
% 187.82/188.26 Generated: 1973891
% 187.82/188.26 Kept: 181348
% 187.82/188.26 Inuse: 2421
% 187.82/188.26 Deleted: 1750
% 187.82/188.26 Deletedinuse: 16
% 187.82/188.26
% 187.82/188.26 Resimplifying inuse:
% 187.82/188.26 Done
% 187.82/188.26
% 187.82/188.26 *** allocated 4378860 integers for termspace/termends
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2003776
% 187.82/188.27 Kept: 184433
% 187.82/188.27 Inuse: 2425
% 187.82/188.27 Deleted: 1750
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying clauses:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2031626
% 187.82/188.27 Kept: 187443
% 187.82/188.27 Inuse: 2427
% 187.82/188.27 Deleted: 1811
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2074116
% 187.82/188.27 Kept: 191172
% 187.82/188.27 Inuse: 2431
% 187.82/188.27 Deleted: 1811
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2116636
% 187.82/188.27 Kept: 194761
% 187.82/188.27 Inuse: 2435
% 187.82/188.27 Deleted: 1811
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2143147
% 187.82/188.27 Kept: 196885
% 187.82/188.27 Inuse: 2436
% 187.82/188.27 Deleted: 1811
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2169691
% 187.82/188.27 Kept: 198973
% 187.82/188.27 Inuse: 2437
% 187.82/188.27 Deleted: 1811
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2198688
% 187.82/188.27 Kept: 201941
% 187.82/188.27 Inuse: 2440
% 187.82/188.27 Deleted: 1811
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2226676
% 187.82/188.27 Kept: 204960
% 187.82/188.27 Inuse: 2442
% 187.82/188.27 Deleted: 1811
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying clauses:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2256267
% 187.82/188.27 Kept: 207987
% 187.82/188.27 Inuse: 2445
% 187.82/188.27 Deleted: 1898
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2276731
% 187.82/188.27 Kept: 210037
% 187.82/188.27 Inuse: 2452
% 187.82/188.27 Deleted: 1898
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2302896
% 187.82/188.27 Kept: 212044
% 187.82/188.27 Inuse: 2477
% 187.82/188.27 Deleted: 1898
% 187.82/188.27 Deletedinuse: 16
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27 Resimplifying inuse:
% 187.82/188.27 Done
% 187.82/188.27
% 187.82/188.27
% 187.82/188.27 Intermediate Status:
% 187.82/188.27 Generated: 2365025
% 187.82/188.27 Kept: 214045
% 187.82/188.27 InTerminated
% 299.64/300.04 Bliksem ended
%------------------------------------------------------------------------------