%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX241_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n013.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:53 PM UTC 2026
% Result : Timeout 299.57s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX241_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n013.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 13:26:10 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.72/1.34 *** allocated 10000 integers for termspace/termends
% 0.72/1.34 *** allocated 10000 integers for clauses
% 0.72/1.34 *** allocated 10000 integers for justifications
% 0.72/1.34 Bliksem 1.12
% 0.72/1.34
% 0.72/1.34
% 0.72/1.34 Automatic Strategy Selection
% 0.72/1.34
% 0.72/1.34
% 0.72/1.34 Clauses:
% 0.72/1.34
% 0.72/1.34 { head( cons( X, Y ) ) = X }.
% 0.72/1.34 { tail( cons( X, Y ) ) = Y }.
% 0.72/1.34 { ! nil = cons( X, Y ) }.
% 0.72/1.34 { proj1Suc( suc( X ) ) = X }.
% 0.72/1.34 { ! zero = suc( X ) }.
% 0.72/1.34 { proj1High( high( X ) ) = X }.
% 0.72/1.34 { proj1Low( low( X ) ) = X }.
% 0.72/1.34 { ! high( X ) = low( Y ) }.
% 0.72/1.34 { proj1Nand( nand( X, Y ) ) = X }.
% 0.72/1.34 { proj2Nand( nand( X, Y ) ) = Y }.
% 0.72/1.34 { proj1Var( var( X ) ) = X }.
% 0.72/1.34 { ! nand( X, Y ) = tT }.
% 0.72/1.34 { ! nand( X, Y ) = fF }.
% 0.72/1.34 { ! nand( X, Y ) = var( Z ) }.
% 0.72/1.34 { ! tT = fF }.
% 0.72/1.34 { ! tT = var( X ) }.
% 0.72/1.34 { ! fF = var( X ) }.
% 0.72/1.34 { proj1Assign( assign( X, Y ) ) = X }.
% 0.72/1.34 { proj2Assign( assign( X, Y ) ) = Y }.
% 0.72/1.34 { proj1Seq( seq( X, Y ) ) = X }.
% 0.72/1.34 { proj2Seq( seq( X, Y ) ) = Y }.
% 0.72/1.34 { proj1IfThenElse( ifThenElse( X, Y, Z ) ) = X }.
% 0.72/1.34 { proj2IfThenElse( ifThenElse( X, Y, Z ) ) = Y }.
% 0.72/1.34 { proj3IfThenElse( ifThenElse( X, Y, Z ) ) = Z }.
% 0.72/1.34 { proj1While( while( X, Y ) ) = X }.
% 0.72/1.34 { proj2While( while( X, Y ) ) = Y }.
% 0.72/1.34 { ! skip = assign( X, Y ) }.
% 0.72/1.34 { ! skip = seq( X, Y ) }.
% 0.72/1.34 { ! skip = ifThenElse( X, Y, Z ) }.
% 0.72/1.34 { ! skip = while( X, Y ) }.
% 0.72/1.34 { ! assign( X, Y ) = seq( Z, T ) }.
% 0.72/1.34 { ! assign( X, Y ) = ifThenElse( Z, T, U ) }.
% 0.72/1.34 { ! assign( X, Y ) = while( Z, T ) }.
% 0.72/1.34 { ! seq( X, Y ) = ifThenElse( Z, T, U ) }.
% 0.72/1.34 { ! seq( X, Y ) = while( Z, T ) }.
% 0.72/1.34 { ! ifThenElse( X, Y, Z ) = while( T, U ) }.
% 0.72/1.34 { X = nand( proj1Nand( X ), proj2Nand( X ) ), X = var( proj1Var( X ) ), !
% 0.72/1.34 secret( X ) }.
% 0.72/1.34 { ! secret( nand( X, Y ) ), secret( X ), secret( Y ) }.
% 0.72/1.34 { ! secret( X ), secret( nand( X, Y ) ) }.
% 0.72/1.34 { ! secret( Y ), secret( nand( X, Y ) ) }.
% 0.72/1.34 { secret( var( high( X ) ) ) }.
% 0.72/1.34 { ! secret( var( low( X ) ) ) }.
% 0.72/1.34 { typeCorrect( skip ) }.
% 0.72/1.34 { typeCorrect( assign( high( Y ), X ) ) }.
% 0.72/1.34 { ! typeCorrect( assign( low( Y ), X ) ), ! secret( X ) }.
% 0.72/1.34 { secret( X ), typeCorrect( assign( low( Y ), X ) ) }.
% 0.72/1.34 { ! typeCorrect( seq( X, Y ) ), typeCorrect( X ) }.
% 0.72/1.34 { ! typeCorrect( seq( X, Y ) ), typeCorrect( Y ) }.
% 0.72/1.34 { ! typeCorrect( X ), ! typeCorrect( Y ), typeCorrect( seq( X, Y ) ) }.
% 0.72/1.34 { ! typeCorrect( ifThenElse( X, Y, Z ) ), typeCorrect( Y ) }.
% 0.72/1.34 { ! typeCorrect( ifThenElse( X, Y, Z ) ), typeCorrect( Z ) }.
% 0.72/1.34 { ! typeCorrect( Y ), ! typeCorrect( Z ), typeCorrect( ifThenElse( X, Y, Z
% 0.72/1.34 ) ) }.
% 0.72/1.34 { ! typeCorrect( while( X, Y ) ), typeCorrect( Y ) }.
% 0.72/1.34 { ! typeCorrect( Y ), typeCorrect( while( X, Y ) ) }.
% 0.72/1.34 { l = low( zero ) }.
% 0.72/1.34 { h = high( zero ) }.
% 0.72/1.34 { ! elem( X, nil ) }.
% 0.72/1.34 { ! elem( X, cons( Y, Z ) ), Y = X, elem( X, Z ) }.
% 0.72/1.34 { ! Y = X, elem( X, cons( Y, Z ) ) }.
% 0.72/1.34 { ! elem( X, Z ), elem( X, cons( Y, Z ) ) }.
% 0.72/1.34 { ! eval( X, nand( Y, Z ) ), ! eval( X, Y ), ! eval( X, Z ) }.
% 0.72/1.34 { eval( X, Y ), eval( X, nand( Y, Z ) ) }.
% 0.72/1.34 { eval( X, Z ), eval( X, nand( Y, Z ) ) }.
% 0.72/1.34 { eval( X, tT ) }.
% 0.72/1.34 { ! eval( X, fF ) }.
% 0.72/1.34 { ! eval( X, var( Y ) ), elem( Y, X ) }.
% 0.72/1.34 { ! elem( Y, X ), eval( X, var( Y ) ) }.
% 0.72/1.34 { del( X, nil ) = nil }.
% 0.72/1.34 { ! X = Y, del( X, cons( Y, Z ) ) = del( X, Z ) }.
% 0.72/1.34 { X = Y, del( X, cons( Y, Z ) ) = cons( Y, del( X, Z ) ) }.
% 0.72/1.34 { run( X, skip ) = X }.
% 0.72/1.34 { ! eval( X, Y ), run( X, assign( Z, Y ) ) = cons( Z, X ) }.
% 0.72/1.34 { eval( X, Y ), run( X, assign( Z, Y ) ) = del( Z, X ) }.
% 0.72/1.34 { run( X, seq( Y, Z ) ) = run( run( X, Y ), Z ) }.
% 0.72/1.34 { ! eval( X, Y ), run( X, ifThenElse( Y, Z, T ) ) = run( X, Z ) }.
% 0.72/1.34 { eval( X, Y ), run( X, ifThenElse( Y, Z, T ) ) = run( X, T ) }.
% 0.72/1.34 { run( X, while( Y, Z ) ) = run( X, ifThenElse( Y, seq( Z, while( Y, Z ) )
% 0.72/1.34 , skip ) ) }.
% 0.72/1.34 { ! typeCorrect( X ), ! elem( l, run( Y, X ) ), elem( l, run( cons( h, Y )
% 0.72/1.34 , X ) ) }.
% 0.72/1.34 { ! typeCorrect( X ), ! elem( l, run( cons( h, Y ), X ) ), elem( l, run( Y
% 0.72/1.34 , X ) ) }.
% 0.72/1.34
% 0.72/1.34 percentage equality = 0.461538, percentage horn = 0.886076
% 0.72/1.34 This is a problem with some equality
% 0.72/1.34
% 0.72/1.34
% 0.72/1.34
% 0.72/1.34 Options Used:
% 0.72/1.34
% 0.72/1.34 useres = 1
% 0.72/1.34 useparamod = 1
% 0.72/1.34 useeqrefl = 1
% 0.72/1.34 useeqfact = 1
% 0.72/1.34 usefactor = 1
% 0.72/1.34 usesimpsplitting = 0
% 0.72/1.34 usesimpdemod = 5
% 0.72/1.34 usesimpres = 3
% 0.72/1.34
% 0.72/1.34 resimpinuse = 1000
% 0.72/1.34 resimpclauses = 20000
% 0.72/1.34 substype = eqrewr
% 0.72/1.34 backwardsubs = 1
% 0.72/1.34 selectoldest = 5
% 0.72/1.34
% 0.72/1.34 litorderings [0] = split
% 0.72/1.34 litorderings [1] = extend the termordering, first sorting on arguments
% 0.72/1.34
% 0.72/1.34 termordering = kbo
% 6.77/7.16
% 6.77/7.16 litapriori = 0
% 6.77/7.16 termapriori = 1
% 6.77/7.16 litaposteriori = 0
% 6.77/7.16 termaposteriori = 0
% 6.77/7.16 demodaposteriori = 0
% 6.77/7.16 ordereqreflfact = 0
% 6.77/7.16
% 6.77/7.16 litselect = negord
% 6.77/7.16
% 6.77/7.16 maxweight = 15
% 6.77/7.16 maxdepth = 30000
% 6.77/7.16 maxlength = 115
% 6.77/7.16 maxnrvars = 195
% 6.77/7.16 excuselevel = 1
% 6.77/7.16 increasemaxweight = 1
% 6.77/7.16
% 6.77/7.16 maxselected = 10000000
% 6.77/7.16 maxnrclauses = 10000000
% 6.77/7.16
% 6.77/7.16 showgenerated = 0
% 6.77/7.16 showkept = 0
% 6.77/7.16 showselected = 0
% 6.77/7.16 showdeleted = 0
% 6.77/7.16 showresimp = 1
% 6.77/7.16 showstatus = 2000
% 6.77/7.16
% 6.77/7.16 prologoutput = 0
% 6.77/7.16 nrgoals = 5000000
% 6.77/7.16 totalproof = 1
% 6.77/7.16
% 6.77/7.16 Symbols occurring in the translation:
% 6.77/7.16
% 6.77/7.16 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 6.77/7.16 . [1, 2] (w:1, o:61, a:1, s:1, b:0),
% 6.77/7.16 ! [4, 1] (w:0, o:33, a:1, s:1, b:0),
% 6.77/7.16 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 6.77/7.16 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 6.77/7.16 cons [37, 2] (w:1, o:85, a:1, s:1, b:0),
% 6.77/7.16 head [38, 1] (w:1, o:38, a:1, s:1, b:0),
% 6.77/7.16 tail [39, 1] (w:1, o:41, a:1, s:1, b:0),
% 6.77/7.16 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 6.77/7.16 suc [41, 1] (w:1, o:39, a:1, s:1, b:0),
% 6.77/7.16 proj1Suc [42, 1] (w:1, o:42, a:1, s:1, b:0),
% 6.77/7.16 zero [43, 0] (w:1, o:9, a:1, s:1, b:0),
% 6.77/7.16 high [44, 1] (w:1, o:43, a:1, s:1, b:0),
% 6.77/7.16 proj1High [45, 1] (w:1, o:44, a:1, s:1, b:0),
% 6.77/7.16 low [46, 1] (w:1, o:45, a:1, s:1, b:0),
% 6.77/7.16 proj1Low [47, 1] (w:1, o:46, a:1, s:1, b:0),
% 6.77/7.16 nand [48, 2] (w:1, o:86, a:1, s:1, b:0),
% 6.77/7.16 proj1Nand [49, 1] (w:1, o:47, a:1, s:1, b:0),
% 6.77/7.16 proj2Nand [50, 1] (w:1, o:53, a:1, s:1, b:0),
% 6.77/7.16 var [51, 1] (w:1, o:54, a:1, s:1, b:0),
% 6.77/7.16 proj1Var [52, 1] (w:1, o:48, a:1, s:1, b:0),
% 6.77/7.16 tT [53, 0] (w:1, o:11, a:1, s:1, b:0),
% 6.77/7.16 fF [54, 0] (w:1, o:12, a:1, s:1, b:0),
% 6.77/7.16 assign [56, 2] (w:1, o:87, a:1, s:1, b:0),
% 6.77/7.16 proj1Assign [57, 1] (w:1, o:49, a:1, s:1, b:0),
% 6.77/7.16 proj2Assign [58, 1] (w:1, o:55, a:1, s:1, b:0),
% 6.77/7.16 seq [59, 2] (w:1, o:89, a:1, s:1, b:0),
% 6.77/7.16 proj1Seq [60, 1] (w:1, o:50, a:1, s:1, b:0),
% 6.77/7.16 proj2Seq [61, 1] (w:1, o:56, a:1, s:1, b:0),
% 6.77/7.16 ifThenElse [62, 3] (w:1, o:94, a:1, s:1, b:0),
% 6.77/7.16 proj1IfThenElse [63, 1] (w:1, o:51, a:1, s:1, b:0),
% 6.77/7.16 proj2IfThenElse [64, 1] (w:1, o:57, a:1, s:1, b:0),
% 6.77/7.16 proj3IfThenElse [65, 1] (w:1, o:59, a:1, s:1, b:0),
% 6.77/7.16 while [66, 2] (w:1, o:90, a:1, s:1, b:0),
% 6.77/7.16 proj1While [67, 1] (w:1, o:52, a:1, s:1, b:0),
% 6.77/7.16 proj2While [68, 1] (w:1, o:58, a:1, s:1, b:0),
% 6.77/7.16 skip [69, 0] (w:1, o:10, a:1, s:1, b:0),
% 6.77/7.16 secret [72, 1] (w:1, o:40, a:1, s:1, b:0),
% 6.77/7.16 typeCorrect [76, 1] (w:1, o:60, a:1, s:1, b:0),
% 6.77/7.16 l [85, 0] (w:1, o:28, a:1, s:1, b:0),
% 6.77/7.16 h [86, 0] (w:1, o:29, a:1, s:1, b:0),
% 6.77/7.16 elem [87, 2] (w:1, o:92, a:1, s:1, b:0),
% 6.77/7.16 eval [89, 2] (w:1, o:93, a:1, s:1, b:0),
% 6.77/7.16 del [90, 2] (w:1, o:91, a:1, s:1, b:0),
% 6.77/7.16 run [92, 2] (w:1, o:88, a:1, s:1, b:0).
% 6.77/7.16
% 6.77/7.16
% 6.77/7.16 Starting Search:
% 6.77/7.16
% 6.77/7.16 *** allocated 15000 integers for clauses
% 6.77/7.16 *** allocated 22500 integers for clauses
% 6.77/7.16 *** allocated 33750 integers for clauses
% 6.77/7.16 *** allocated 50625 integers for clauses
% 6.77/7.16 *** allocated 15000 integers for termspace/termends
% 6.77/7.16 *** allocated 75937 integers for clauses
% 6.77/7.16 Resimplifying inuse:
% 6.77/7.16 Done
% 6.77/7.16
% 6.77/7.16 *** allocated 22500 integers for termspace/termends
% 6.77/7.16 *** allocated 113905 integers for clauses
% 6.77/7.16 *** allocated 33750 integers for termspace/termends
% 6.77/7.16
% 6.77/7.16 Intermediate Status:
% 6.77/7.16 Generated: 3343
% 6.77/7.16 Kept: 2007
% 6.77/7.16 Inuse: 163
% 6.77/7.16 Deleted: 0
% 6.77/7.16 Deletedinuse: 0
% 6.77/7.16
% 6.77/7.16 *** allocated 170857 integers for clauses
% 6.77/7.16 Resimplifying inuse:
% 6.77/7.16 Done
% 6.77/7.16
% 6.77/7.16 *** allocated 50625 integers for termspace/termends
% 6.77/7.16 Resimplifying inuse:
% 6.77/7.16 Done
% 6.77/7.16
% 6.77/7.16 *** allocated 256285 integers for clauses
% 6.77/7.16 *** allocated 75937 integers for termspace/termends
% 6.77/7.16
% 6.77/7.16 Intermediate Status:
% 6.77/7.16 Generated: 7009
% 6.77/7.16 Kept: 4017
% 6.77/7.16 Inuse: 257
% 6.77/7.16 Deleted: 0
% 6.77/7.16 Deletedinuse: 0
% 6.77/7.16
% 6.77/7.16 Resimplifying inuse:
% 6.77/7.16 Done
% 6.77/7.16
% 6.77/7.16 *** allocated 384427 integers for clauses
% 6.77/7.16 *** allocated 113905 integers for termspace/termends
% 6.77/7.16
% 6.77/7.16 Intermediate Status:
% 6.77/7.16 Generated: 10124
% 6.77/7.16 Kept: 6053
% 6.77/7.16 Inuse: 279
% 6.77/7.16 Deleted: 0
% 6.77/7.16 Deletedinuse: 0
% 6.77/7.16
% 6.77/7.16 Resimplifying inuse:
% 6.77/7.16 Done
% 6.77/7.16
% 6.77/7.16 Resimplifying inuse:
% 6.77/7.16 Done
% 6.77/7.16
% 6.77/7.16 *** allocated 576640 integers for clauses
% 6.77/7.16
% 6.77/7.16 Intermediate Status:
% 33.21/33.61 Generated: 16624
% 33.21/33.61 Kept: 8058
% 33.21/33.61 Inuse: 344
% 33.21/33.61 Deleted: 1
% 33.21/33.61 Deletedinuse: 0
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 *** allocated 170857 integers for termspace/termends
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 22705
% 33.21/33.61 Kept: 11118
% 33.21/33.61 Inuse: 389
% 33.21/33.61 Deleted: 1
% 33.21/33.61 Deletedinuse: 0
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 *** allocated 864960 integers for clauses
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 *** allocated 256285 integers for termspace/termends
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 27259
% 33.21/33.61 Kept: 13187
% 33.21/33.61 Inuse: 455
% 33.21/33.61 Deleted: 1
% 33.21/33.61 Deletedinuse: 0
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 32398
% 33.21/33.61 Kept: 15219
% 33.21/33.61 Inuse: 520
% 33.21/33.61 Deleted: 1
% 33.21/33.61 Deletedinuse: 0
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 38173
% 33.21/33.61 Kept: 17247
% 33.21/33.61 Inuse: 545
% 33.21/33.61 Deleted: 4
% 33.21/33.61 Deletedinuse: 3
% 33.21/33.61
% 33.21/33.61 *** allocated 1297440 integers for clauses
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 *** allocated 384427 integers for termspace/termends
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 47199
% 33.21/33.61 Kept: 20045
% 33.21/33.61 Inuse: 581
% 33.21/33.61 Deleted: 15
% 33.21/33.61 Deletedinuse: 7
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 Resimplifying clauses:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 52657
% 33.21/33.61 Kept: 22149
% 33.21/33.61 Inuse: 601
% 33.21/33.61 Deleted: 364
% 33.21/33.61 Deletedinuse: 9
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 63210
% 33.21/33.61 Kept: 25361
% 33.21/33.61 Inuse: 638
% 33.21/33.61 Deleted: 373
% 33.21/33.61 Deletedinuse: 11
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 *** allocated 1946160 integers for clauses
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 70204
% 33.21/33.61 Kept: 28150
% 33.21/33.61 Inuse: 663
% 33.21/33.61 Deleted: 378
% 33.21/33.61 Deletedinuse: 15
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 *** allocated 576640 integers for termspace/termends
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 82651
% 33.21/33.61 Kept: 31897
% 33.21/33.61 Inuse: 704
% 33.21/33.61 Deleted: 387
% 33.21/33.61 Deletedinuse: 17
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61 Resimplifying inuse:
% 33.21/33.61 Done
% 33.21/33.61
% 33.21/33.61
% 33.21/33.61 Intermediate Status:
% 33.21/33.61 Generated: 90807
% 33.21/33.61 Kept: 35383
% 33.21/33.61 Inuse: 733
% 33.21/33.61 Deleted: 392
% 33.21/33.62 Deletedinuse: 21
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 95738
% 33.21/33.62 Kept: 37452
% 33.21/33.62 Inuse: 767
% 33.21/33.62 Deleted: 392
% 33.21/33.62 Deletedinuse: 21
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 104643
% 33.21/33.62 Kept: 40112
% 33.21/33.62 Inuse: 774
% 33.21/33.62 Deleted: 403
% 33.21/33.62 Deletedinuse: 25
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying clauses:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 *** allocated 2919240 integers for clauses
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 109402
% 33.21/33.62 Kept: 42112
% 33.21/33.62 Inuse: 810
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 *** allocated 864960 integers for termspace/termends
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 115896
% 33.21/33.62 Kept: 44124
% 33.21/33.62 Inuse: 840
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 123221
% 33.21/33.62 Kept: 46149
% 33.21/33.62 Inuse: 875
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 129789
% 33.21/33.62 Kept: 48168
% 33.21/33.62 Inuse: 911
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 139153
% 33.21/33.62 Kept: 50175
% 33.21/33.62 Inuse: 955
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 144661
% 33.21/33.62 Kept: 52206
% 33.21/33.62 Inuse: 977
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 149160
% 33.21/33.62 Kept: 54286
% 33.21/33.62 Inuse: 993
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 155873
% 33.21/33.62 Kept: 56341
% 33.21/33.62 Inuse: 1019
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62
% 33.21/33.62 Intermediate Status:
% 33.21/33.62 Generated: 160680
% 33.21/33.62 Kept: 58446
% 33.21/33.62 Inuse: 1035
% 33.21/33.62 Deleted: 1682
% 33.21/33.62 Deletedinuse: 27
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying inuse:
% 33.21/33.62 Done
% 33.21/33.62
% 33.21/33.62 Resimplifying clauses:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12
% 85.64/86.12 Intermediate Status:
% 85.64/86.12 Generated: 167042
% 85.64/86.12 Kept: 60518
% 85.64/86.12 Inuse: 1060
% 85.64/86.12 Deleted: 1993
% 85.64/86.12 Deletedinuse: 27
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12 *** allocated 1297440 integers for termspace/termends
% 85.64/86.12
% 85.64/86.12 Intermediate Status:
% 85.64/86.12 Generated: 172175
% 85.64/86.12 Kept: 62520
% 85.64/86.12 Inuse: 1081
% 85.64/86.12 Deleted: 1993
% 85.64/86.12 Deletedinuse: 27
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12 *** allocated 4378860 integers for clauses
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12
% 85.64/86.12 Intermediate Status:
% 85.64/86.12 Generated: 178766
% 85.64/86.12 Kept: 64553
% 85.64/86.12 Inuse: 1110
% 85.64/86.12 Deleted: 1994
% 85.64/86.12 Deletedinuse: 28
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12
% 85.64/86.12 Intermediate Status:
% 85.64/86.12 Generated: 185356
% 85.64/86.12 Kept: 66741
% 85.64/86.12 Inuse: 1135
% 85.64/86.12 Deleted: 1994
% 85.64/86.12 Deletedinuse: 28
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12
% 85.64/86.12 Intermediate Status:
% 85.64/86.12 Generated: 191094
% 85.64/86.12 Kept: 68822
% 85.64/86.12 Inuse: 1158
% 85.64/86.12 Deleted: 1994
% 85.64/86.12 Deletedinuse: 28
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12 Resimplifying inuse:
% 85.64/86.12 Done
% 85.64/86.12
% 85.64/86.12
% 85.64/86.12 Intermediate Status:
% 85.64/86.12 Generated: 197005
% 85.64/86.13 Kept: 70880
% 85.64/86.13 Inuse: 1181
% 85.64/86.13 Deleted: 1994
% 85.64/86.13 Deletedinuse: 28
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 202814
% 85.64/86.13 Kept: 73382
% 85.64/86.13 Inuse: 1195
% 85.64/86.13 Deleted: 1994
% 85.64/86.13 Deletedinuse: 28
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 208527
% 85.64/86.13 Kept: 75568
% 85.64/86.13 Inuse: 1214
% 85.64/86.13 Deleted: 1995
% 85.64/86.13 Deletedinuse: 29
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 212615
% 85.64/86.13 Kept: 77709
% 85.64/86.13 Inuse: 1225
% 85.64/86.13 Deleted: 1996
% 85.64/86.13 Deletedinuse: 30
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 217021
% 85.64/86.13 Kept: 79875
% 85.64/86.13 Inuse: 1239
% 85.64/86.13 Deleted: 1996
% 85.64/86.13 Deletedinuse: 30
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying clauses:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 221548
% 85.64/86.13 Kept: 82053
% 85.64/86.13 Inuse: 1251
% 85.64/86.13 Deleted: 2213
% 85.64/86.13 Deletedinuse: 32
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 226593
% 85.64/86.13 Kept: 84081
% 85.64/86.13 Inuse: 1265
% 85.64/86.13 Deleted: 2216
% 85.64/86.13 Deletedinuse: 35
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 232262
% 85.64/86.13 Kept: 86100
% 85.64/86.13 Inuse: 1281
% 85.64/86.13 Deleted: 2216
% 85.64/86.13 Deletedinuse: 35
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 237358
% 85.64/86.13 Kept: 88174
% 85.64/86.13 Inuse: 1296
% 85.64/86.13 Deleted: 2217
% 85.64/86.13 Deletedinuse: 36
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 242151
% 85.64/86.13 Kept: 90223
% 85.64/86.13 Inuse: 1317
% 85.64/86.13 Deleted: 2219
% 85.64/86.13 Deletedinuse: 38
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 *** allocated 1946160 integers for termspace/termends
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 249509
% 85.64/86.13 Kept: 92294
% 85.64/86.13 Inuse: 1333
% 85.64/86.13 Deleted: 2220
% 85.64/86.13 Deletedinuse: 39
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 255765
% 85.64/86.13 Kept: 94579
% 85.64/86.13 Inuse: 1346
% 85.64/86.13 Deleted: 2220
% 85.64/86.13 Deletedinuse: 39
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 *** allocated 6568290 integers for clauses
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 260023
% 85.64/86.13 Kept: 96699
% 85.64/86.13 Inuse: 1353
% 85.64/86.13 Deleted: 2220
% 85.64/86.13 Deletedinuse: 39
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 264218
% 85.64/86.13 Kept: 98945
% 85.64/86.13 Inuse: 1360
% 85.64/86.13 Deleted: 2221
% 85.64/86.13 Deletedinuse: 40
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying clauses:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 268420
% 85.64/86.13 Kept: 101080
% 85.64/86.13 Inuse: 1367
% 85.64/86.13 Deleted: 2363
% 85.64/86.13 Deletedinuse: 40
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 272784
% 85.64/86.13 Kept: 103358
% 85.64/86.13 Inuse: 1375
% 85.64/86.13 Deleted: 2364
% 85.64/86.13 Deletedinuse: 41
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 277085
% 85.64/86.13 Kept: 105503
% 85.64/86.13 Inuse: 1382
% 85.64/86.13 Deleted: 2365
% 85.64/86.13 Deletedinuse: 42
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13 Resimplifying inuse:
% 85.64/86.13 Done
% 85.64/86.13
% 85.64/86.13
% 85.64/86.13 Intermediate Status:
% 85.64/86.13 Generated: 281445
% 250.96/251.40 Kept: 107713
% 250.96/251.40 Inuse: 1389
% 250.96/251.40 Deleted: 2365
% 250.96/251.40 Deletedinuse: 42
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 285515
% 250.96/251.40 Kept: 109908
% 250.96/251.40 Inuse: 1395
% 250.96/251.40 Deleted: 2365
% 250.96/251.40 Deletedinuse: 42
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 290182
% 250.96/251.40 Kept: 111988
% 250.96/251.40 Inuse: 1402
% 250.96/251.40 Deleted: 2365
% 250.96/251.40 Deletedinuse: 42
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 295818
% 250.96/251.40 Kept: 114066
% 250.96/251.40 Inuse: 1414
% 250.96/251.40 Deleted: 2365
% 250.96/251.40 Deletedinuse: 42
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 299927
% 250.96/251.40 Kept: 116118
% 250.96/251.40 Inuse: 1424
% 250.96/251.40 Deleted: 2365
% 250.96/251.40 Deletedinuse: 42
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 303901
% 250.96/251.40 Kept: 118216
% 250.96/251.40 Inuse: 1434
% 250.96/251.40 Deleted: 2365
% 250.96/251.40 Deletedinuse: 42
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 307602
% 250.96/251.40 Kept: 120253
% 250.96/251.40 Inuse: 1442
% 250.96/251.40 Deleted: 2366
% 250.96/251.40 Deletedinuse: 43
% 250.96/251.40
% 250.96/251.40 Resimplifying clauses:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 311661
% 250.96/251.40 Kept: 122521
% 250.96/251.40 Inuse: 1450
% 250.96/251.40 Deleted: 2448
% 250.96/251.40 Deletedinuse: 43
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 315140
% 250.96/251.40 Kept: 124588
% 250.96/251.40 Inuse: 1460
% 250.96/251.40 Deleted: 2449
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 320758
% 250.96/251.40 Kept: 126627
% 250.96/251.40 Inuse: 1481
% 250.96/251.40 Deleted: 2449
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 326006
% 250.96/251.40 Kept: 128631
% 250.96/251.40 Inuse: 1500
% 250.96/251.40 Deleted: 2449
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 331510
% 250.96/251.40 Kept: 130687
% 250.96/251.40 Inuse: 1515
% 250.96/251.40 Deleted: 2449
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 337060
% 250.96/251.40 Kept: 132776
% 250.96/251.40 Inuse: 1527
% 250.96/251.40 Deleted: 2449
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 341832
% 250.96/251.40 Kept: 134813
% 250.96/251.40 Inuse: 1539
% 250.96/251.40 Deleted: 2449
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 346030
% 250.96/251.40 Kept: 136911
% 250.96/251.40 Inuse: 1550
% 250.96/251.40 Deleted: 2449
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 *** allocated 2919240 integers for termspace/termends
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 351241
% 250.96/251.40 Kept: 138955
% 250.96/251.40 Inuse: 1578
% 250.96/251.40 Deleted: 2449
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying clauses:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 357962
% 250.96/251.40 Kept: 141404
% 250.96/251.40 Inuse: 1605
% 250.96/251.40 Deleted: 2781
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 *** allocated 9852435 integers for clauses
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 361901
% 250.96/251.40 Kept: 143407
% 250.96/251.40 Inuse: 1615
% 250.96/251.40 Deleted: 2781
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 366998
% 250.96/251.40 Kept: 145459
% 250.96/251.40 Inuse: 1642
% 250.96/251.40 Deleted: 2781
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 372723
% 250.96/251.40 Kept: 147488
% 250.96/251.40 Inuse: 1663
% 250.96/251.40 Deleted: 2781
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 378078
% 250.96/251.40 Kept: 149893
% 250.96/251.40 Inuse: 1675
% 250.96/251.40 Deleted: 2781
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 383376
% 250.96/251.40 Kept: 152602
% 250.96/251.40 Inuse: 1685
% 250.96/251.40 Deleted: 2781
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 Generated: 388068
% 250.96/251.40 Kept: 154642
% 250.96/251.40 Inuse: 1701
% 250.96/251.40 Deleted: 2781
% 250.96/251.40 Deletedinuse: 44
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40 Resimplifying inuse:
% 250.96/251.40 Done
% 250.96/251.40
% 250.96/251.40
% 250.96/251.40 Intermediate Status:
% 250.96/251.40 GenerTerminated
% 299.57/300.03 Bliksem ended
%------------------------------------------------------------------------------