%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX223+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n007.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.45s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX223+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : bliksem %s
% 0.15/0.34 % Computer : n007.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % DateTime : Tue May 5 12:34:53 EDT 2026
% 0.15/0.34 % CPUTime :
% 2.70/3.19 *** allocated 10000 integers for termspace/termends
% 2.70/3.19 *** allocated 10000 integers for clauses
% 2.70/3.19 *** allocated 10000 integers for justifications
% 2.70/3.19 Bliksem 1.12
% 2.70/3.19
% 2.70/3.19
% 2.70/3.19 Automatic Strategy Selection
% 2.70/3.19
% 2.70/3.19
% 2.70/3.19 Clauses:
% 2.70/3.19
% 2.70/3.19 { head( cons( X, Y ) ) = X }.
% 2.70/3.19 { tail( cons( X, Y ) ) = Y }.
% 2.70/3.19 { ! nil = cons( X, Y ) }.
% 2.70/3.19 { proj1Arr( arr( X, Y ) ) = X }.
% 2.70/3.19 { proj2Arr( arr( X, Y ) ) = Y }.
% 2.70/3.19 { ! arr( X, Y ) = a }.
% 2.70/3.19 { ! arr( X, Y ) = b }.
% 2.70/3.19 { ! arr( X, Y ) = c }.
% 2.70/3.19 { ! a = b }.
% 2.70/3.19 { ! a = c }.
% 2.70/3.19 { ! b = c }.
% 2.70/3.19 { proj1Suc( suc( X ) ) = X }.
% 2.70/3.19 { ! zero = suc( X ) }.
% 2.70/3.19 { proj1Just( just( X ) ) = X }.
% 2.70/3.19 { ! nothing = just( X ) }.
% 2.70/3.19 { proj1App( app( X, Y, Z ) ) = X }.
% 2.70/3.19 { proj2App( app( X, Y, Z ) ) = Y }.
% 2.70/3.19 { proj3App( app( X, Y, Z ) ) = Z }.
% 2.70/3.19 { proj1Lam( lam( X ) ) = X }.
% 2.70/3.19 { proj1Var( var( X ) ) = X }.
% 2.70/3.19 { ! app( X, Y, Z ) = lam( T ) }.
% 2.70/3.19 { ! app( X, Y, Z ) = var( T ) }.
% 2.70/3.19 { ! lam( X ) = var( Y ) }.
% 2.70/3.19 { X = lam( proj1Lam( X ) ), ! nf( app( X, Y, Z ) ), nf( X ) }.
% 2.70/3.19 { X = lam( proj1Lam( X ) ), ! nf( app( X, Y, Z ) ), nf( Y ) }.
% 2.70/3.19 { X = lam( proj1Lam( X ) ), ! nf( X ), ! nf( Y ), nf( app( X, Y, Z ) ) }.
% 2.70/3.19 { ! nf( app( lam( Z ), X, Y ) ) }.
% 2.70/3.19 { ! nf( lam( X ) ), nf( X ) }.
% 2.70/3.19 { ! nf( X ), nf( lam( X ) ) }.
% 2.70/3.19 { nf( var( X ) ) }.
% 2.70/3.19 { index( nil, X ) = nothing }.
% 2.70/3.19 { index( cons( X, Y ), zero ) = just( X ) }.
% 2.70/3.19 { index( cons( X, Y ), suc( Z ) ) = index( Y, Z ) }.
% 2.70/3.19 { ! tc( X, app( Z, T, U ), Y ), tc( X, Z, arr( U, Y ) ) }.
% 2.70/3.19 { ! tc( X, app( Z, T, U ), Y ), tc( X, T, U ) }.
% 2.70/3.19 { ! tc( X, Z, arr( U, Y ) ), ! tc( X, T, U ), tc( X, app( Z, T, U ), Y ) }
% 2.70/3.19 .
% 2.70/3.19 { X = arr( proj1Arr( X ), proj2Arr( X ) ), ! tc( Y, lam( Z ), X ) }.
% 2.70/3.19 { ! tc( X, lam( Y ), arr( Z, T ) ), tc( cons( Z, X ), Y, T ) }.
% 2.70/3.19 { ! tc( cons( Z, X ), Y, T ), tc( X, lam( Y ), arr( Z, T ) ) }.
% 2.70/3.19 { ! index( X, Y ) = nothing, ! tc( X, var( Y ), Z ) }.
% 2.70/3.19 { ! index( X, Y ) = just( Z ), ! tc( X, var( Y ), T ), Z = T }.
% 2.70/3.19 { ! index( X, Y ) = just( Z ), ! Z = T, tc( X, var( Y ), T ) }.
% 2.70/3.19 { ! nf( X ), ! tc( nil, X, arr( arr( a, arr( a, b ) ), arr( a, b ) ) ) }.
% 2.70/3.19
% 2.70/3.19 percentage equality = 0.538462, percentage horn = 0.930233
% 2.70/3.19 This is a problem with some equality
% 2.70/3.19
% 2.70/3.19
% 2.70/3.19
% 2.70/3.19 Options Used:
% 2.70/3.19
% 2.70/3.19 useres = 1
% 2.70/3.19 useparamod = 1
% 2.70/3.19 useeqrefl = 1
% 2.70/3.19 useeqfact = 1
% 2.70/3.19 usefactor = 1
% 2.70/3.19 usesimpsplitting = 0
% 2.70/3.19 usesimpdemod = 5
% 2.70/3.19 usesimpres = 3
% 2.70/3.19
% 2.70/3.19 resimpinuse = 1000
% 2.70/3.19 resimpclauses = 20000
% 2.70/3.19 substype = eqrewr
% 2.70/3.19 backwardsubs = 1
% 2.70/3.19 selectoldest = 5
% 2.70/3.19
% 2.70/3.19 litorderings [0] = split
% 2.70/3.19 litorderings [1] = extend the termordering, first sorting on arguments
% 2.70/3.19
% 2.70/3.19 termordering = kbo
% 2.70/3.19
% 2.70/3.19 litapriori = 0
% 2.70/3.19 termapriori = 1
% 2.70/3.19 litaposteriori = 0
% 2.70/3.19 termaposteriori = 0
% 2.70/3.19 demodaposteriori = 0
% 2.70/3.19 ordereqreflfact = 0
% 2.70/3.19
% 2.70/3.19 litselect = negord
% 2.70/3.19
% 2.70/3.19 maxweight = 15
% 2.70/3.19 maxdepth = 30000
% 2.70/3.19 maxlength = 115
% 2.70/3.19 maxnrvars = 195
% 2.70/3.19 excuselevel = 1
% 2.70/3.19 increasemaxweight = 1
% 2.70/3.19
% 2.70/3.19 maxselected = 10000000
% 2.70/3.19 maxnrclauses = 10000000
% 2.70/3.19
% 2.70/3.19 showgenerated = 0
% 2.70/3.19 showkept = 0
% 2.70/3.19 showselected = 0
% 2.70/3.19 showdeleted = 0
% 2.70/3.19 showresimp = 1
% 2.70/3.19 showstatus = 2000
% 2.70/3.19
% 2.70/3.19 prologoutput = 0
% 2.70/3.19 nrgoals = 5000000
% 2.70/3.19 totalproof = 1
% 2.70/3.19
% 2.70/3.19 Symbols occurring in the translation:
% 2.70/3.19
% 2.70/3.19 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.70/3.19 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 2.70/3.19 ! [4, 1] (w:0, o:26, a:1, s:1, b:0),
% 2.70/3.19 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.70/3.19 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.70/3.19 cons [37, 2] (w:1, o:71, a:1, s:1, b:0),
% 2.70/3.19 head [38, 1] (w:1, o:31, a:1, s:1, b:0),
% 2.70/3.19 tail [39, 1] (w:1, o:33, a:1, s:1, b:0),
% 2.70/3.19 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 2.70/3.19 arr [41, 2] (w:1, o:72, a:1, s:1, b:0),
% 2.70/3.19 proj1Arr [42, 1] (w:1, o:34, a:1, s:1, b:0),
% 2.70/3.19 proj2Arr [43, 1] (w:1, o:40, a:1, s:1, b:0),
% 2.70/3.19 a [44, 0] (w:1, o:9, a:1, s:1, b:0),
% 2.70/3.19 b [45, 0] (w:1, o:10, a:1, s:1, b:0),
% 2.70/3.19 c [46, 0] (w:1, o:11, a:1, s:1, b:0),
% 2.70/3.19 suc [47, 1] (w:1, o:32, a:1, s:1, b:0),
% 2.70/3.19 proj1Suc [48, 1] (w:1, o:35, a:1, s:1, b:0),
% 2.70/3.19 zero [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 2.70/3.19 just [50, 1] (w:1, o:41, a:1, s:1, b:0),
% 2.70/3.19 proj1Just [51, 1] (w:1, o:36, a:1, s:1, b:0),
% 2.70/3.19 nothing [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 2.70/3.19 app [54, 3] (w:1, o:74, a:1, s:1, b:0),
% 12.88/13.38 proj1App [55, 1] (w:1, o:37, a:1, s:1, b:0),
% 12.88/13.38 proj2App [56, 1] (w:1, o:42, a:1, s:1, b:0),
% 12.88/13.38 proj3App [57, 1] (w:1, o:43, a:1, s:1, b:0),
% 12.88/13.38 lam [58, 1] (w:1, o:44, a:1, s:1, b:0),
% 12.88/13.38 proj1Lam [59, 1] (w:1, o:38, a:1, s:1, b:0),
% 12.88/13.38 var [60, 1] (w:1, o:45, a:1, s:1, b:0),
% 12.88/13.38 proj1Var [61, 1] (w:1, o:39, a:1, s:1, b:0),
% 12.88/13.38 nf [65, 1] (w:1, o:46, a:1, s:1, b:0),
% 12.88/13.38 index [67, 2] (w:1, o:73, a:1, s:1, b:0),
% 12.88/13.38 tc [72, 3] (w:1, o:75, a:1, s:1, b:0).
% 12.88/13.38
% 12.88/13.38
% 12.88/13.38 Starting Search:
% 12.88/13.38
% 12.88/13.38 *** allocated 15000 integers for clauses
% 12.88/13.38 *** allocated 22500 integers for clauses
% 12.88/13.38 *** allocated 33750 integers for clauses
% 12.88/13.38 *** allocated 15000 integers for termspace/termends
% 12.88/13.38 *** allocated 50625 integers for clauses
% 12.88/13.38 *** allocated 22500 integers for termspace/termends
% 12.88/13.38 *** allocated 75937 integers for clauses
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 33750 integers for termspace/termends
% 12.88/13.38 *** allocated 113905 integers for clauses
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 6419
% 12.88/13.38 Kept: 2007
% 12.88/13.38 Inuse: 165
% 12.88/13.38 Deleted: 13
% 12.88/13.38 Deletedinuse: 3
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 50625 integers for termspace/termends
% 12.88/13.38 *** allocated 170857 integers for clauses
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 75937 integers for termspace/termends
% 12.88/13.38 *** allocated 256285 integers for clauses
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 20419
% 12.88/13.38 Kept: 4242
% 12.88/13.38 Inuse: 287
% 12.88/13.38 Deleted: 31
% 12.88/13.38 Deletedinuse: 3
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 113905 integers for termspace/termends
% 12.88/13.38 *** allocated 384427 integers for clauses
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 33895
% 12.88/13.38 Kept: 6242
% 12.88/13.38 Inuse: 366
% 12.88/13.38 Deleted: 39
% 12.88/13.38 Deletedinuse: 3
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 170857 integers for termspace/termends
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 576640 integers for clauses
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 58518
% 12.88/13.38 Kept: 8246
% 12.88/13.38 Inuse: 485
% 12.88/13.38 Deleted: 39
% 12.88/13.38 Deletedinuse: 3
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 96839
% 12.88/13.38 Kept: 10353
% 12.88/13.38 Inuse: 671
% 12.88/13.38 Deleted: 48
% 12.88/13.38 Deletedinuse: 5
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 256285 integers for termspace/termends
% 12.88/13.38 *** allocated 864960 integers for clauses
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 106480
% 12.88/13.38 Kept: 13530
% 12.88/13.38 Inuse: 686
% 12.88/13.38 Deleted: 51
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 384427 integers for termspace/termends
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 117767
% 12.88/13.38 Kept: 16626
% 12.88/13.38 Inuse: 687
% 12.88/13.38 Deleted: 51
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 1297440 integers for clauses
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 128582
% 12.88/13.38 Kept: 20207
% 12.88/13.38 Inuse: 710
% 12.88/13.38 Deleted: 51
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 Resimplifying clauses:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 135814
% 12.88/13.38 Kept: 23088
% 12.88/13.38 Inuse: 711
% 12.88/13.38 Deleted: 353
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 576640 integers for termspace/termends
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 147341
% 12.88/13.38 Kept: 26185
% 12.88/13.38 Inuse: 712
% 12.88/13.38 Deleted: 353
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 1946160 integers for clauses
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 158757
% 12.88/13.38 Kept: 29975
% 12.88/13.38 Inuse: 735
% 12.88/13.38 Deleted: 353
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 170506
% 12.88/13.38 Kept: 33135
% 12.88/13.38 Inuse: 736
% 12.88/13.38 Deleted: 353
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 180497
% 12.88/13.38 Kept: 35154
% 12.88/13.38 Inuse: 780
% 12.88/13.38 Deleted: 353
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 *** allocated 864960 integers for termspace/termends
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 192930
% 12.88/13.38 Kept: 37183
% 12.88/13.38 Inuse: 821
% 12.88/13.38 Deleted: 353
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 205272
% 12.88/13.38 Kept: 39218
% 12.88/13.38 Inuse: 860
% 12.88/13.38 Deleted: 354
% 12.88/13.38 Deletedinuse: 8
% 12.88/13.38
% 12.88/13.38 Resimplifying inuse:
% 12.88/13.38 Done
% 12.88/13.38
% 12.88/13.38
% 12.88/13.38 Intermediate Status:
% 12.88/13.38 Generated: 217439
% 12.88/13.38 Kept: 41873
% 12.88/13.38 Inuse: 883
% 12.88/13.38 Deleted: 355
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying clauses:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 *** allocated 2919240 integers for clauses
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 229819
% 39.61/40.10 Kept: 45271
% 39.61/40.10 Inuse: 885
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 238041
% 39.61/40.10 Kept: 47331
% 39.61/40.10 Inuse: 892
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 246136
% 39.61/40.10 Kept: 49354
% 39.61/40.10 Inuse: 922
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 255205
% 39.61/40.10 Kept: 51360
% 39.61/40.10 Inuse: 953
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 269110
% 39.61/40.10 Kept: 53391
% 39.61/40.10 Inuse: 1002
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 *** allocated 1297440 integers for termspace/termends
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 283324
% 39.61/40.10 Kept: 55405
% 39.61/40.10 Inuse: 1034
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 294370
% 39.61/40.10 Kept: 57471
% 39.61/40.10 Inuse: 1070
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 304568
% 39.61/40.10 Kept: 59487
% 39.61/40.10 Inuse: 1105
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 315654
% 39.61/40.10 Kept: 61517
% 39.61/40.10 Inuse: 1139
% 39.61/40.10 Deleted: 845
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying clauses:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 327888
% 39.61/40.10 Kept: 63518
% 39.61/40.10 Inuse: 1174
% 39.61/40.10 Deleted: 933
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 342663
% 39.61/40.10 Kept: 65540
% 39.61/40.10 Inuse: 1217
% 39.61/40.10 Deleted: 933
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 *** allocated 4378860 integers for clauses
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 354144
% 39.61/40.10 Kept: 67603
% 39.61/40.10 Inuse: 1263
% 39.61/40.10 Deleted: 933
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 368343
% 39.61/40.10 Kept: 69660
% 39.61/40.10 Inuse: 1308
% 39.61/40.10 Deleted: 933
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 378872
% 39.61/40.10 Kept: 71729
% 39.61/40.10 Inuse: 1347
% 39.61/40.10 Deleted: 933
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 389113
% 39.61/40.10 Kept: 73741
% 39.61/40.10 Inuse: 1397
% 39.61/40.10 Deleted: 934
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 399673
% 39.61/40.10 Kept: 75769
% 39.61/40.10 Inuse: 1446
% 39.61/40.10 Deleted: 935
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 410511
% 39.61/40.10 Kept: 77813
% 39.61/40.10 Inuse: 1495
% 39.61/40.10 Deleted: 936
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 419817
% 39.61/40.10 Kept: 79840
% 39.61/40.10 Inuse: 1542
% 39.61/40.10 Deleted: 936
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 *** allocated 1946160 integers for termspace/termends
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 492038
% 39.61/40.10 Kept: 83360
% 39.61/40.10 Inuse: 1589
% 39.61/40.10 Deleted: 936
% 39.61/40.10 Deletedinuse: 8
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying clauses:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 553637
% 39.61/40.10 Kept: 85404
% 39.61/40.10 Inuse: 1626
% 39.61/40.10 Deleted: 1046
% 39.61/40.10 Deletedinuse: 9
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 611226
% 39.61/40.10 Kept: 87448
% 39.61/40.10 Inuse: 1657
% 39.61/40.10 Deleted: 1046
% 39.61/40.10 Deletedinuse: 9
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 635230
% 39.61/40.10 Kept: 90025
% 39.61/40.10 Inuse: 1671
% 39.61/40.10 Deleted: 1046
% 39.61/40.10 Deletedinuse: 9
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10 Resimplifying inuse:
% 39.61/40.10 Done
% 39.61/40.10
% 39.61/40.10
% 39.61/40.10 Intermediate Status:
% 39.61/40.10 Generated: 651401
% 111.25/111.77 Kept: 92055
% 111.25/111.77 Inuse: 1709
% 111.25/111.77 Deleted: 1047
% 111.25/111.77 Deletedinuse: 10
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 715805
% 111.25/111.77 Kept: 95754
% 111.25/111.77 Inuse: 1737
% 111.25/111.77 Deleted: 1047
% 111.25/111.77 Deletedinuse: 10
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 *** allocated 6568290 integers for clauses
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 733046
% 111.25/111.77 Kept: 97802
% 111.25/111.77 Inuse: 1774
% 111.25/111.77 Deleted: 1050
% 111.25/111.77 Deletedinuse: 13
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 749735
% 111.25/111.77 Kept: 99818
% 111.25/111.77 Inuse: 1804
% 111.25/111.77 Deleted: 1050
% 111.25/111.77 Deletedinuse: 13
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 794422
% 111.25/111.77 Kept: 102718
% 111.25/111.77 Inuse: 1820
% 111.25/111.77 Deleted: 1050
% 111.25/111.77 Deletedinuse: 13
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying clauses:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 868420
% 111.25/111.77 Kept: 104747
% 111.25/111.77 Inuse: 1856
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 918206
% 111.25/111.77 Kept: 107993
% 111.25/111.77 Inuse: 1886
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 939994
% 111.25/111.77 Kept: 110573
% 111.25/111.77 Inuse: 1889
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 995861
% 111.25/111.77 Kept: 112576
% 111.25/111.77 Inuse: 1946
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1062475
% 111.25/111.77 Kept: 114611
% 111.25/111.77 Inuse: 2004
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1173367
% 111.25/111.77 Kept: 116662
% 111.25/111.77 Inuse: 2052
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1229530
% 111.25/111.77 Kept: 118676
% 111.25/111.77 Inuse: 2109
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1285884
% 111.25/111.77 Kept: 120683
% 111.25/111.77 Inuse: 2165
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 *** allocated 2919240 integers for termspace/termends
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1334966
% 111.25/111.77 Kept: 122692
% 111.25/111.77 Inuse: 2202
% 111.25/111.77 Deleted: 1227
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying clauses:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1368557
% 111.25/111.77 Kept: 124710
% 111.25/111.77 Inuse: 2255
% 111.25/111.77 Deleted: 1382
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1398591
% 111.25/111.77 Kept: 126743
% 111.25/111.77 Inuse: 2307
% 111.25/111.77 Deleted: 1382
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1432774
% 111.25/111.77 Kept: 128787
% 111.25/111.77 Inuse: 2364
% 111.25/111.77 Deleted: 1382
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1453317
% 111.25/111.77 Kept: 130873
% 111.25/111.77 Inuse: 2377
% 111.25/111.77 Deleted: 1382
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1481729
% 111.25/111.77 Kept: 134181
% 111.25/111.77 Inuse: 2379
% 111.25/111.77 Deleted: 1382
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1505362
% 111.25/111.77 Kept: 137133
% 111.25/111.77 Inuse: 2381
% 111.25/111.77 Deleted: 1382
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1532782
% 111.25/111.77 Kept: 140412
% 111.25/111.77 Inuse: 2382
% 111.25/111.77 Deleted: 1382
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1571698
% 111.25/111.77 Kept: 143980
% 111.25/111.77 Inuse: 2385
% 111.25/111.77 Deleted: 1382
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying clauses:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77
% 111.25/111.77 Intermediate Status:
% 111.25/111.77 Generated: 1611029
% 111.25/111.77 Kept: 147525
% 111.25/111.77 Inuse: 2387
% 111.25/111.77 Deleted: 1679
% 111.25/111.77 Deletedinuse: 16
% 111.25/111.77
% 111.25/111.77 Resimplifying inuse:
% 111.25/111.77 Done
% 111.25/111.77
% 111.25/111.77 *** allocated 9852435 integers for clauses
% 111.25/111.77 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1639310
% 220.13/220.74 Kept: 150484
% 220.13/220.74 Inuse: 2390
% 220.13/220.74 Deleted: 1679
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1665232
% 220.13/220.74 Kept: 152601
% 220.13/220.74 Inuse: 2391
% 220.13/220.74 Deleted: 1679
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1706728
% 220.13/220.74 Kept: 156138
% 220.13/220.74 Inuse: 2395
% 220.13/220.74 Deleted: 1679
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1736048
% 220.13/220.74 Kept: 159225
% 220.13/220.74 Inuse: 2399
% 220.13/220.74 Deleted: 1679
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1766155
% 220.13/220.74 Kept: 162402
% 220.13/220.74 Inuse: 2404
% 220.13/220.74 Deleted: 1679
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1795932
% 220.13/220.74 Kept: 164636
% 220.13/220.74 Inuse: 2409
% 220.13/220.74 Deleted: 1679
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying clauses:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1823382
% 220.13/220.74 Kept: 167610
% 220.13/220.74 Inuse: 2411
% 220.13/220.74 Deleted: 1750
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1849581
% 220.13/220.74 Kept: 169739
% 220.13/220.74 Inuse: 2412
% 220.13/220.74 Deleted: 1750
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1890920
% 220.13/220.74 Kept: 173239
% 220.13/220.74 Inuse: 2415
% 220.13/220.74 Deleted: 1750
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1917161
% 220.13/220.74 Kept: 175346
% 220.13/220.74 Inuse: 2416
% 220.13/220.74 Deleted: 1750
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1945961
% 220.13/220.74 Kept: 178337
% 220.13/220.74 Inuse: 2419
% 220.13/220.74 Deleted: 1750
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 1973613
% 220.13/220.74 Kept: 181344
% 220.13/220.74 Inuse: 2421
% 220.13/220.74 Deleted: 1750
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 *** allocated 4378860 integers for termspace/termends
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 2003494
% 220.13/220.74 Kept: 184429
% 220.13/220.74 Inuse: 2425
% 220.13/220.74 Deleted: 1750
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying clauses:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 2031340
% 220.13/220.74 Kept: 187439
% 220.13/220.74 Inuse: 2427
% 220.13/220.74 Deleted: 1811
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 2073824
% 220.13/220.74 Kept: 191168
% 220.13/220.74 Inuse: 2431
% 220.13/220.74 Deleted: 1811
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 2116338
% 220.13/220.74 Kept: 194757
% 220.13/220.74 Inuse: 2435
% 220.13/220.74 Deleted: 1811
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 2142845
% 220.13/220.74 Kept: 196881
% 220.13/220.74 Inuse: 2436
% 220.13/220.74 Deleted: 1811
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.74 Done
% 220.13/220.74
% 220.13/220.74
% 220.13/220.74 Intermediate Status:
% 220.13/220.74 Generated: 2169385
% 220.13/220.74 Kept: 198969
% 220.13/220.74 Inuse: 2437
% 220.13/220.74 Deleted: 1811
% 220.13/220.74 Deletedinuse: 16
% 220.13/220.74
% 220.13/220.74 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75
% 220.13/220.75 Intermediate Status:
% 220.13/220.75 Generated: 2198378
% 220.13/220.75 Kept: 201937
% 220.13/220.75 Inuse: 2440
% 220.13/220.75 Deleted: 1811
% 220.13/220.75 Deletedinuse: 16
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75
% 220.13/220.75 Intermediate Status:
% 220.13/220.75 Generated: 2226362
% 220.13/220.75 Kept: 204956
% 220.13/220.75 Inuse: 2442
% 220.13/220.75 Deleted: 1811
% 220.13/220.75 Deletedinuse: 16
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75 Resimplifying clauses:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75
% 220.13/220.75 Intermediate Status:
% 220.13/220.75 Generated: 2255949
% 220.13/220.75 Kept: 207983
% 220.13/220.75 Inuse: 2445
% 220.13/220.75 Deleted: 1898
% 220.13/220.75 Deletedinuse: 16
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75
% 220.13/220.75 Intermediate Status:
% 220.13/220.75 Generated: 2276411
% 220.13/220.75 Kept: 210033
% 220.13/220.75 Inuse: 2452
% 220.13/220.75 Deleted: 1898
% 220.13/220.75 Deletedinuse: 16
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75
% 220.13/220.75 Intermediate Status:
% 220.13/220.75 Generated: 2302576
% 220.13/220.75 Kept: 212040
% 220.13/220.75 Inuse: 2477
% 220.13/220.75 Deleted: 1898
% 220.13/220.75 Deletedinuse: 16
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75 Resimplifying inuse:
% 220.13/220.75 Done
% 220.13/220.75
% 220.13/220.75
% 220.13/220.75 Intermediate Status:
% 220.13/220.75 Generated: 2364701
% 220.13/220.75 Kept: 214041
% 220.13/220.75 Inuse: 2Terminated
% 299.45/300.03 Bliksem ended
% 299.45/300.03 Terminated
%------------------------------------------------------------------------------