%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX218+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n003.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.57s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX218+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n003.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:17:41 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.67/1.09 *** allocated 10000 integers for termspace/termends
% 0.67/1.09 *** allocated 10000 integers for clauses
% 0.67/1.09 *** allocated 10000 integers for justifications
% 0.67/1.09 Bliksem 1.12
% 0.67/1.09
% 0.67/1.09
% 0.67/1.09 Automatic Strategy Selection
% 0.67/1.09
% 0.67/1.09
% 0.67/1.09 Clauses:
% 0.67/1.09
% 0.67/1.09 { proj1tuple( tuple2( X, Y, Z ) ) = X }.
% 0.67/1.09 { proj2tuple( tuple2( X, Y, Z ) ) = Y }.
% 0.67/1.09 { proj3tuple( tuple2( X, Y, Z ) ) = Z }.
% 0.67/1.09 { proj1pair( pair22( X, Y ) ) = X }.
% 0.67/1.09 { proj2pair( pair22( X, Y ) ) = Y }.
% 0.67/1.09 { proj1pair2( pair23( X, Y ) ) = X }.
% 0.67/1.09 { proj2pair2( pair23( X, Y ) ) = Y }.
% 0.67/1.09 { proj1pair3( pair24( X, Y ) ) = X }.
% 0.67/1.09 { proj2pair3( pair24( X, Y ) ) = Y }.
% 0.67/1.09 { proj1pair4( pair25( X, Y ) ) = X }.
% 0.67/1.09 { proj2pair4( pair25( X, Y ) ) = Y }.
% 0.67/1.09 { head( cons( X, Y ) ) = X }.
% 0.67/1.09 { tail( cons( X, Y ) ) = Y }.
% 0.67/1.09 { ! nil = cons( X, Y ) }.
% 0.67/1.09 { head2( cons2( X, Y ) ) = X }.
% 0.67/1.09 { tail2( cons2( X, Y ) ) = Y }.
% 0.67/1.09 { ! nil2 = cons2( X, Y ) }.
% 0.67/1.09 { proj1Succ( succ( X ) ) = X }.
% 0.67/1.09 { ! zero = succ( X ) }.
% 0.67/1.09 { proj1Left( left( X ) ) = X }.
% 0.67/1.09 { proj1Right( right( X ) ) = X }.
% 0.67/1.09 { ! left( X ) = right( Y ) }.
% 0.67/1.09 { proj1Lft( lft( X ) ) = X }.
% 0.67/1.09 { proj1Rgt( rgt( X ) ) = X }.
% 0.67/1.09 { ! lft( X ) = rgt( Y ) }.
% 0.67/1.09 { ! lft( X ) = stp }.
% 0.67/1.09 { ! rgt( X ) = stp }.
% 0.67/1.09 { ! o = a2 }.
% 0.67/1.09 { ! o = b }.
% 0.67/1.09 { ! a2 = b }.
% 0.67/1.09 { split( nil2 ) = pair24( o, nil2 ) }.
% 0.67/1.09 { split( cons2( X, Y ) ) = pair24( X, Y ) }.
% 0.67/1.09 { rev( nil2, X ) = X }.
% 0.67/1.09 { X = o, rev( cons2( X, Z ), Y ) = rev( Z, cons2( X, Y ) ) }.
% 0.67/1.09 { rev( cons2( o, Y ), X ) = X }.
% 0.67/1.09 { one = succ( zero ) }.
% 0.67/1.09 { two = succ( one ) }.
% 0.67/1.09 { apply( nil, X ) = pair25( o, stp ) }.
% 0.67/1.09 { ! Y = X, apply( cons( pair22( Y, T ), Z ), X ) = T }.
% 0.67/1.09 { Y = X, apply( cons( pair22( Y, T ), Z ), X ) = apply( Z, X ) }.
% 0.67/1.09 { ! split( X ) = pair24( Y, Z ), act( lft( W ), X, T, U ) = right( tuple2(
% 0.67/1.09 W, Z, cons2( Y, cons2( T, U ) ) ) ) }.
% 0.67/1.09 { act( rgt( T ), X, Y, Z ) = right( tuple2( T, cons2( Y, X ), Z ) ) }.
% 0.67/1.09 { act( stp, X, Y, Z ) = left( rev( X, cons2( Y, Z ) ) ) }.
% 0.67/1.09 { ! split( X ) = pair24( Y, Z ), ! apply( T, pair23( U, Y ) ) = pair25( W,
% 0.67/1.09 V0 ), step( T, tuple2( U, V1, X ) ) = act( V0, V1, W, Z ) }.
% 0.67/1.09 { ! step( X, Y ) = left( Z ), steps( X, Y ) = Z }.
% 0.67/1.09 { ! step( X, Y ) = right( Z ), steps( X, Y ) = steps( X, Z ) }.
% 0.67/1.09 { runt( X, Y ) = steps( X, tuple2( zero, nil2, Y ) ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = nil2, ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( Y, Z ), Y = a2, ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = nil2, ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = cons2( Y, Z ), Y = a2, ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = cons2( a2, nil2 ), ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = cons2( a2, cons2( Y, Z ) ), Y = a2, ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = cons2( a2, cons2( a2, nil2 ) ), ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = cons2( a2, cons2( a2, cons2( Y, Z ) ) ), Y = a2, ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = cons2( a2, cons2( a2, cons2( a2, nil2 ) ) ), ! prog0( X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = cons2( a2, cons2( a2, cons2( a2, cons2( Y, Z ) ) ) ), Y = a2, ! prog0(
% 0.67/1.09 X ) }.
% 0.67/1.09 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 0.67/1.09 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 0.67/1.09 = cons2( a2, cons2( a2, cons2( a2, cons2( a2, nil2 ) ) ) ), ! prog0( X )
% 3.43/3.86 }.
% 3.43/3.86 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 3.43/3.86 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 3.43/3.86 = cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( Y, Z ) ) ) ) ), Y =
% 3.43/3.86 b, ! prog0( X ) }.
% 3.43/3.86 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 3.43/3.86 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 3.43/3.86 = cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ), !
% 3.43/3.86 prog0( X ) }.
% 3.43/3.86 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 3.43/3.86 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 3.43/3.86 = cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, cons2( Y, Z ) ) )
% 3.43/3.86 ) ) ), Y = b, ! prog0( X ) }.
% 3.43/3.86 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 3.43/3.86 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 3.43/3.86 = cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, cons2( b, nil2 )
% 3.43/3.86 ) ) ) ) ), prog0( X ) }.
% 3.43/3.86 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, nil2 ), ! runt( X, cons2( b,
% 3.43/3.86 cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) )
% 3.43/3.86 = cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, cons2( b, cons2(
% 3.43/3.86 Y, Z ) ) ) ) ) ) ), ! prog0( X ) }.
% 3.43/3.86 { ! runt( X, cons2( a2, nil2 ) ) = cons2( a2, cons2( Y, Z ) ), ! prog0( X )
% 3.43/3.86 }.
% 3.43/3.86 { ! prog0( cons( pair22( pair23( zero, a2 ), X ), cons( pair22( pair23(
% 3.43/3.86 zero, b ), Y ), cons( pair22( pair23( one, a2 ), Z ), cons( pair22(
% 3.43/3.86 pair23( one, b ), T ), cons( pair22( pair23( two, a2 ), U ), nil ) ) ) )
% 3.43/3.86 ) ) }.
% 3.43/3.86
% 3.43/3.86 percentage equality = 0.837838, percentage horn = 0.969231
% 3.43/3.86 This is a pure equality problem
% 3.43/3.86
% 3.43/3.86
% 3.43/3.86
% 3.43/3.86 Options Used:
% 3.43/3.86
% 3.43/3.86 useres = 1
% 3.43/3.86 useparamod = 1
% 3.43/3.86 useeqrefl = 1
% 3.43/3.86 useeqfact = 1
% 3.43/3.86 usefactor = 1
% 3.43/3.86 usesimpsplitting = 0
% 3.43/3.86 usesimpdemod = 5
% 3.43/3.86 usesimpres = 3
% 3.43/3.86
% 3.43/3.86 resimpinuse = 1000
% 3.43/3.86 resimpclauses = 20000
% 3.43/3.86 substype = eqrewr
% 3.43/3.86 backwardsubs = 1
% 3.43/3.86 selectoldest = 5
% 3.43/3.86
% 3.43/3.86 litorderings [0] = split
% 3.43/3.86 litorderings [1] = extend the termordering, first sorting on arguments
% 3.43/3.86
% 3.43/3.86 termordering = kbo
% 3.43/3.86
% 3.43/3.86 litapriori = 0
% 3.43/3.86 termapriori = 1
% 3.43/3.86 litaposteriori = 0
% 3.43/3.86 termaposteriori = 0
% 3.43/3.86 demodaposteriori = 0
% 3.43/3.86 ordereqreflfact = 0
% 3.43/3.86
% 3.43/3.86 litselect = negord
% 3.43/3.86
% 3.43/3.86 maxweight = 15
% 3.43/3.86 maxdepth = 30000
% 3.43/3.86 maxlength = 115
% 3.43/3.86 maxnrvars = 195
% 3.43/3.86 excuselevel = 1
% 3.43/3.86 increasemaxweight = 1
% 3.43/3.86
% 3.43/3.86 maxselected = 10000000
% 3.43/3.86 maxnrclauses = 10000000
% 3.43/3.86
% 3.43/3.86 showgenerated = 0
% 3.43/3.86 showkept = 0
% 3.43/3.86 showselected = 0
% 3.43/3.86 showdeleted = 0
% 3.43/3.86 showresimp = 1
% 3.43/3.86 showstatus = 2000
% 3.43/3.86
% 3.43/3.86 prologoutput = 0
% 3.43/3.86 nrgoals = 5000000
% 3.43/3.86 totalproof = 1
% 3.43/3.86
% 3.43/3.86 Symbols occurring in the translation:
% 3.43/3.86
% 3.43/3.86 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.43/3.86 . [1, 2] (w:1, o:83, a:1, s:1, b:0),
% 3.43/3.86 ! [4, 1] (w:0, o:51, a:1, s:1, b:0),
% 3.43/3.86 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.43/3.86 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.43/3.86 tuple2 [38, 3] (w:1, o:118, a:1, s:1, b:0),
% 3.43/3.86 proj1tuple [39, 1] (w:1, o:56, a:1, s:1, b:0),
% 3.43/3.86 proj2tuple [40, 1] (w:1, o:66, a:1, s:1, b:0),
% 3.43/3.86 proj3tuple [41, 1] (w:1, o:71, a:1, s:1, b:0),
% 3.43/3.86 pair22 [42, 2] (w:1, o:107, a:1, s:1, b:0),
% 3.43/3.86 proj1pair [43, 1] (w:1, o:57, a:1, s:1, b:0),
% 3.43/3.86 proj2pair [44, 1] (w:1, o:67, a:1, s:1, b:0),
% 3.43/3.86 pair23 [45, 2] (w:1, o:108, a:1, s:1, b:0),
% 3.43/3.86 proj1pair2 [46, 1] (w:1, o:58, a:1, s:1, b:0),
% 3.43/3.86 proj2pair2 [47, 1] (w:1, o:68, a:1, s:1, b:0),
% 3.43/3.86 pair24 [48, 2] (w:1, o:109, a:1, s:1, b:0),
% 3.43/3.86 proj1pair3 [49, 1] (w:1, o:59, a:1, s:1, b:0),
% 3.43/3.86 proj2pair3 [50, 1] (w:1, o:69, a:1, s:1, b:0),
% 3.43/3.86 pair25 [51, 2] (w:1, o:110, a:1, s:1, b:0),
% 3.43/3.86 proj1pair4 [52, 1] (w:1, o:60, a:1, s:1, b:0),
% 3.43/3.86 proj2pair4 [53, 1] (w:1, o:70, a:1, s:1, b:0),
% 3.43/3.86 cons [54, 2] (w:1, o:111, a:1, s:1, b:0),
% 3.43/3.86 head [55, 1] (w:1, o:72, a:1, s:1, b:0),
% 3.43/3.86 tail [56, 1] (w:1, o:77, a:1, s:1, b:0),
% 3.43/3.86 nil [57, 0] (w:1, o:21, a:1, s:1, b:0),
% 3.43/3.86 cons2 [58, 2] (w:1, o:112, a:1, s:1, b:0),
% 3.43/3.86 head2 [59, 1] (w:1, o:78, a:1, s:1, b:0),
% 3.43/3.86 tail2 [60, 1] (w:1, o:79, a:1, s:1, b:0),
% 19.66/20.04 nil2 [61, 0] (w:1, o:22, a:1, s:1, b:0),
% 19.66/20.04 succ [62, 1] (w:1, o:75, a:1, s:1, b:0),
% 19.66/20.04 proj1Succ [63, 1] (w:1, o:63, a:1, s:1, b:0),
% 19.66/20.04 zero [64, 0] (w:1, o:23, a:1, s:1, b:0),
% 19.66/20.04 left [65, 1] (w:1, o:80, a:1, s:1, b:0),
% 19.66/20.04 proj1Left [66, 1] (w:1, o:64, a:1, s:1, b:0),
% 19.66/20.04 right [67, 1] (w:1, o:73, a:1, s:1, b:0),
% 19.66/20.04 proj1Right [68, 1] (w:1, o:61, a:1, s:1, b:0),
% 19.66/20.04 lft [69, 1] (w:1, o:81, a:1, s:1, b:0),
% 19.66/20.04 proj1Lft [70, 1] (w:1, o:65, a:1, s:1, b:0),
% 19.66/20.04 rgt [71, 1] (w:1, o:74, a:1, s:1, b:0),
% 19.66/20.04 proj1Rgt [72, 1] (w:1, o:62, a:1, s:1, b:0),
% 19.66/20.04 stp [73, 0] (w:1, o:24, a:1, s:1, b:0),
% 19.66/20.04 o [74, 0] (w:1, o:25, a:1, s:1, b:0),
% 19.66/20.04 a2 [75, 0] (w:1, o:26, a:1, s:1, b:0),
% 19.66/20.04 b [76, 0] (w:1, o:27, a:1, s:1, b:0),
% 19.66/20.04 split [77, 1] (w:1, o:76, a:1, s:1, b:0),
% 19.66/20.04 rev [80, 2] (w:1, o:113, a:1, s:1, b:0),
% 19.66/20.04 one [82, 0] (w:1, o:38, a:1, s:1, b:0),
% 19.66/20.04 two [83, 0] (w:1, o:39, a:1, s:1, b:0),
% 19.66/20.04 apply [84, 2] (w:1, o:114, a:1, s:1, b:0),
% 19.66/20.04 act [91, 4] (w:1, o:119, a:1, s:1, b:0),
% 19.66/20.04 step [99, 2] (w:1, o:116, a:1, s:1, b:0),
% 19.66/20.04 steps [101, 2] (w:1, o:117, a:1, s:1, b:0),
% 19.66/20.04 runt [103, 2] (w:1, o:115, a:1, s:1, b:0),
% 19.66/20.04 prog0 [104, 1] (w:1, o:82, a:1, s:1, b:0).
% 19.66/20.04
% 19.66/20.04
% 19.66/20.04 Starting Search:
% 19.66/20.04
% 19.66/20.04 *** allocated 15000 integers for clauses
% 19.66/20.04 *** allocated 22500 integers for clauses
% 19.66/20.04 *** allocated 33750 integers for clauses
% 19.66/20.04 *** allocated 50625 integers for clauses
% 19.66/20.04 *** allocated 15000 integers for termspace/termends
% 19.66/20.04 *** allocated 75937 integers for clauses
% 19.66/20.04 *** allocated 22500 integers for termspace/termends
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 *** allocated 33750 integers for termspace/termends
% 19.66/20.04 *** allocated 113905 integers for clauses
% 19.66/20.04 *** allocated 50625 integers for termspace/termends
% 19.66/20.04 *** allocated 75937 integers for termspace/termends
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 7343
% 19.66/20.04 Kept: 2093
% 19.66/20.04 Inuse: 114
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 *** allocated 170857 integers for clauses
% 19.66/20.04 *** allocated 113905 integers for termspace/termends
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 *** allocated 170857 integers for termspace/termends
% 19.66/20.04 *** allocated 256285 integers for clauses
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 16837
% 19.66/20.04 Kept: 4205
% 19.66/20.04 Inuse: 139
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 *** allocated 256285 integers for termspace/termends
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 *** allocated 384427 integers for clauses
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 27391
% 19.66/20.04 Kept: 6278
% 19.66/20.04 Inuse: 177
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 *** allocated 576640 integers for clauses
% 19.66/20.04 *** allocated 384427 integers for termspace/termends
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 44057
% 19.66/20.04 Kept: 8484
% 19.66/20.04 Inuse: 235
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 61261
% 19.66/20.04 Kept: 10488
% 19.66/20.04 Inuse: 285
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 *** allocated 864960 integers for clauses
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 75774
% 19.66/20.04 Kept: 12651
% 19.66/20.04 Inuse: 308
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 92880
% 19.66/20.04 Kept: 14687
% 19.66/20.04 Inuse: 366
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 107986
% 19.66/20.04 Kept: 16735
% 19.66/20.04 Inuse: 413
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 *** allocated 576640 integers for termspace/termends
% 19.66/20.04 *** allocated 1297440 integers for clauses
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 126232
% 19.66/20.04 Kept: 18781
% 19.66/20.04 Inuse: 457
% 19.66/20.04 Deleted: 3
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 Resimplifying clauses:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 19.66/20.04 Generated: 155230
% 19.66/20.04 Kept: 20820
% 19.66/20.04 Inuse: 506
% 19.66/20.04 Deleted: 634
% 19.66/20.04 Deletedinuse: 1
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04 Resimplifying inuse:
% 19.66/20.04 Done
% 19.66/20.04
% 19.66/20.04
% 19.66/20.04 Intermediate Status:
% 49.03/49.40 Generated: 178930
% 49.03/49.40 Kept: 22839
% 49.03/49.40 Inuse: 557
% 49.03/49.40 Deleted: 634
% 49.03/49.40 Deletedinuse: 1
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 209207
% 49.03/49.40 Kept: 24872
% 49.03/49.40 Inuse: 595
% 49.03/49.40 Deleted: 634
% 49.03/49.40 Deletedinuse: 1
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 229189
% 49.03/49.40 Kept: 26881
% 49.03/49.40 Inuse: 651
% 49.03/49.40 Deleted: 634
% 49.03/49.40 Deletedinuse: 1
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 *** allocated 1946160 integers for clauses
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 265564
% 49.03/49.40 Kept: 28919
% 49.03/49.40 Inuse: 700
% 49.03/49.40 Deleted: 636
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 *** allocated 864960 integers for termspace/termends
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 291790
% 49.03/49.40 Kept: 30980
% 49.03/49.40 Inuse: 739
% 49.03/49.40 Deleted: 636
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 320005
% 49.03/49.40 Kept: 34634
% 49.03/49.40 Inuse: 763
% 49.03/49.40 Deleted: 636
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 326682
% 49.03/49.40 Kept: 36749
% 49.03/49.40 Inuse: 765
% 49.03/49.40 Deleted: 636
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 332925
% 49.03/49.40 Kept: 38864
% 49.03/49.40 Inuse: 766
% 49.03/49.40 Deleted: 636
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 339190
% 49.03/49.40 Kept: 40984
% 49.03/49.40 Inuse: 767
% 49.03/49.40 Deleted: 636
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying clauses:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 *** allocated 2919240 integers for clauses
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 345469
% 49.03/49.40 Kept: 43110
% 49.03/49.40 Inuse: 768
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 352151
% 49.03/49.40 Kept: 45242
% 49.03/49.40 Inuse: 770
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 358450
% 49.03/49.40 Kept: 47375
% 49.03/49.40 Inuse: 771
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 *** allocated 1297440 integers for termspace/termends
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 364759
% 49.03/49.40 Kept: 49512
% 49.03/49.40 Inuse: 772
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 371080
% 49.03/49.40 Kept: 51651
% 49.03/49.40 Inuse: 773
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 380911
% 49.03/49.40 Kept: 53808
% 49.03/49.40 Inuse: 775
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 387261
% 49.03/49.40 Kept: 55955
% 49.03/49.40 Inuse: 776
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 393625
% 49.03/49.40 Kept: 58108
% 49.03/49.40 Inuse: 777
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 406356
% 49.03/49.40 Kept: 60140
% 49.03/49.40 Inuse: 802
% 49.03/49.40 Deleted: 1079
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying clauses:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 425527
% 49.03/49.40 Kept: 62226
% 49.03/49.40 Inuse: 828
% 49.03/49.40 Deleted: 1084
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 438471
% 49.03/49.40 Kept: 64252
% 49.03/49.40 Inuse: 855
% 49.03/49.40 Deleted: 1084
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 *** allocated 4378860 integers for clauses
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 455337
% 49.03/49.40 Kept: 66264
% 49.03/49.40 Inuse: 881
% 49.03/49.40 Deleted: 1084
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 502652
% 49.03/49.40 Kept: 68274
% 49.03/49.40 Inuse: 907
% 49.03/49.40 Deleted: 1084
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 552897
% 49.03/49.40 Kept: 70301
% 49.03/49.40 Inuse: 935
% 49.03/49.40 Deleted: 1084
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 592289
% 49.03/49.40 Kept: 72305
% 49.03/49.40 Inuse: 961
% 49.03/49.40 Deleted: 1084
% 49.03/49.40 Deletedinuse: 3
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40 Resimplifying inuse:
% 49.03/49.40 Done
% 49.03/49.40
% 49.03/49.40
% 49.03/49.40 Intermediate Status:
% 49.03/49.40 Generated: 610677
% 69.51/70.00 Kept: 74339
% 69.51/70.00 Inuse: 987
% 69.51/70.00 Deleted: 1084
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 628915
% 69.51/70.00 Kept: 76365
% 69.51/70.00 Inuse: 1013
% 69.51/70.00 Deleted: 1084
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 *** allocated 1946160 integers for termspace/termends
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 647773
% 69.51/70.00 Kept: 78375
% 69.51/70.00 Inuse: 1041
% 69.51/70.00 Deleted: 1084
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 695016
% 69.51/70.00 Kept: 80443
% 69.51/70.00 Inuse: 1070
% 69.51/70.00 Deleted: 1084
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying clauses:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 742062
% 69.51/70.00 Kept: 82454
% 69.51/70.00 Inuse: 1098
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 770640
% 69.51/70.00 Kept: 84526
% 69.51/70.00 Inuse: 1123
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 800648
% 69.51/70.00 Kept: 86559
% 69.51/70.00 Inuse: 1153
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 847322
% 69.51/70.00 Kept: 88580
% 69.51/70.00 Inuse: 1180
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 862991
% 69.51/70.00 Kept: 92160
% 69.51/70.00 Inuse: 1188
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 875253
% 69.51/70.00 Kept: 95003
% 69.51/70.00 Inuse: 1191
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 911801
% 69.51/70.00 Kept: 97107
% 69.51/70.00 Inuse: 1210
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 949039
% 69.51/70.00 Kept: 99135
% 69.51/70.00 Inuse: 1230
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 *** allocated 6568290 integers for clauses
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 965797
% 69.51/70.00 Kept: 102407
% 69.51/70.00 Inuse: 1238
% 69.51/70.00 Deleted: 1118
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying clauses:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1001915
% 69.51/70.00 Kept: 104423
% 69.51/70.00 Inuse: 1275
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1038141
% 69.51/70.00 Kept: 106473
% 69.51/70.00 Inuse: 1300
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1072900
% 69.51/70.00 Kept: 108593
% 69.51/70.00 Inuse: 1318
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1114576
% 69.51/70.00 Kept: 110704
% 69.51/70.00 Inuse: 1338
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1156878
% 69.51/70.00 Kept: 112707
% 69.51/70.00 Inuse: 1365
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1190596
% 69.51/70.00 Kept: 114765
% 69.51/70.00 Inuse: 1391
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1217184
% 69.51/70.00 Kept: 116795
% 69.51/70.00 Inuse: 1421
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 *** allocated 2919240 integers for termspace/termends
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1254978
% 69.51/70.00 Kept: 118827
% 69.51/70.00 Inuse: 1451
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1283556
% 69.51/70.00 Kept: 120889
% 69.51/70.00 Inuse: 1481
% 69.51/70.00 Deleted: 1289
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying clauses:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1324255
% 69.51/70.00 Kept: 122938
% 69.51/70.00 Inuse: 1513
% 69.51/70.00 Deleted: 1525
% 69.51/70.00 Deletedinuse: 3
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00 Resimplifying inuse:
% 69.51/70.00 Done
% 69.51/70.00
% 69.51/70.00
% 69.51/70.00 Intermediate Status:
% 69.51/70.00 Generated: 1345585
% 109.20/109.68 Kept: 124996
% 109.20/109.68 Inuse: 1530
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1365161
% 109.20/109.68 Kept: 126998
% 109.20/109.68 Inuse: 1545
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1385315
% 109.20/109.68 Kept: 129130
% 109.20/109.68 Inuse: 1561
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1404020
% 109.20/109.68 Kept: 131152
% 109.20/109.68 Inuse: 1576
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1423896
% 109.20/109.68 Kept: 133293
% 109.20/109.68 Inuse: 1592
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1443642
% 109.20/109.68 Kept: 135428
% 109.20/109.68 Inuse: 1608
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1462122
% 109.20/109.68 Kept: 137440
% 109.20/109.68 Inuse: 1623
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1482809
% 109.20/109.68 Kept: 139561
% 109.20/109.68 Inuse: 1640
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1502753
% 109.20/109.68 Kept: 141708
% 109.20/109.68 Inuse: 1656
% 109.20/109.68 Deleted: 1525
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying clauses:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1523382
% 109.20/109.68 Kept: 143861
% 109.20/109.68 Inuse: 1672
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1533753
% 109.20/109.68 Kept: 146481
% 109.20/109.68 Inuse: 1674
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1548356
% 109.20/109.68 Kept: 149827
% 109.20/109.68 Inuse: 1679
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1567937
% 109.20/109.68 Kept: 151971
% 109.20/109.68 Inuse: 1695
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1587748
% 109.20/109.68 Kept: 154133
% 109.20/109.68 Inuse: 1711
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 *** allocated 9852435 integers for clauses
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1636567
% 109.20/109.68 Kept: 156216
% 109.20/109.68 Inuse: 1727
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1663335
% 109.20/109.68 Kept: 158239
% 109.20/109.68 Inuse: 1742
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1694311
% 109.20/109.68 Kept: 160300
% 109.20/109.68 Inuse: 1755
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1713353
% 109.20/109.68 Kept: 162315
% 109.20/109.68 Inuse: 1770
% 109.20/109.68 Deleted: 1748
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying clauses:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1732208
% 109.20/109.68 Kept: 164400
% 109.20/109.68 Inuse: 1785
% 109.20/109.68 Deleted: 1894
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1751911
% 109.20/109.68 Kept: 166525
% 109.20/109.68 Inuse: 1800
% 109.20/109.68 Deleted: 1894
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1772744
% 109.20/109.68 Kept: 169848
% 109.20/109.68 Inuse: 1809
% 109.20/109.68 Deleted: 1894
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1790604
% 109.20/109.68 Kept: 171961
% 109.20/109.68 Inuse: 1822
% 109.20/109.68 Deleted: 1894
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1810683
% 109.20/109.68 Kept: 175757
% 109.20/109.68 Inuse: 1829
% 109.20/109.68 Deleted: 1894
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 109.20/109.68 Done
% 109.20/109.68
% 109.20/109.68 *** allocated 4378860 integers for termspace/termends
% 109.20/109.68
% 109.20/109.68 Intermediate Status:
% 109.20/109.68 Generated: 1827262
% 109.20/109.68 Kept: 178948
% 109.20/109.68 Inuse: 1834
% 109.20/109.68 Deleted: 1894
% 109.20/109.68 Deletedinuse: 3
% 109.20/109.68
% 109.20/109.68 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 1844588
% 153.49/153.90 Kept: 182217
% 153.49/153.90 Inuse: 1839
% 153.49/153.90 Deleted: 1894
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying clauses:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 1864985
% 153.49/153.90 Kept: 184334
% 153.49/153.90 Inuse: 1855
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 1885957
% 153.49/153.90 Kept: 186492
% 153.49/153.90 Inuse: 1872
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 1911029
% 153.49/153.90 Kept: 188572
% 153.49/153.90 Inuse: 1888
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 1938431
% 153.49/153.90 Kept: 190682
% 153.49/153.90 Inuse: 1905
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 1981178
% 153.49/153.90 Kept: 192790
% 153.49/153.90 Inuse: 1921
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2013975
% 153.49/153.90 Kept: 194798
% 153.49/153.90 Inuse: 1936
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2048984
% 153.49/153.90 Kept: 196911
% 153.49/153.90 Inuse: 1952
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2075080
% 153.49/153.90 Kept: 199076
% 153.49/153.90 Inuse: 1968
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2103433
% 153.49/153.90 Kept: 201210
% 153.49/153.90 Inuse: 1985
% 153.49/153.90 Deleted: 2010
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying clauses:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2129275
% 153.49/153.90 Kept: 203368
% 153.49/153.90 Inuse: 2001
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2153502
% 153.49/153.90 Kept: 205390
% 153.49/153.90 Inuse: 2016
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2178898
% 153.49/153.90 Kept: 207523
% 153.49/153.90 Inuse: 2032
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2202780
% 153.49/153.90 Kept: 209561
% 153.49/153.90 Inuse: 2047
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2227634
% 153.49/153.90 Kept: 211659
% 153.49/153.90 Inuse: 2063
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2250488
% 153.49/153.90 Kept: 213814
% 153.49/153.90 Inuse: 2080
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2271652
% 153.49/153.90 Kept: 215948
% 153.49/153.90 Inuse: 2096
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2292039
% 153.49/153.90 Kept: 218115
% 153.49/153.90 Inuse: 2112
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2312957
% 153.49/153.90 Kept: 220277
% 153.49/153.90 Inuse: 2128
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2334821
% 153.49/153.90 Kept: 222429
% 153.49/153.90 Inuse: 2145
% 153.49/153.90 Deleted: 2225
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying clauses:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2353432
% 153.49/153.90 Kept: 224456
% 153.49/153.90 Inuse: 2158
% 153.49/153.90 Deleted: 2431
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2377246
% 153.49/153.90 Kept: 226600
% 153.49/153.90 Inuse: 2173
% 153.49/153.90 Deleted: 2431
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate Status:
% 153.49/153.90 Generated: 2403649
% 153.49/153.90 Kept: 228721
% 153.49/153.90 Inuse: 2190
% 153.49/153.90 Deleted: 2431
% 153.49/153.90 Deletedinuse: 3
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90 Resimplifying inuse:
% 153.49/153.90 Done
% 153.49/153.90
% 153.49/153.90
% 153.49/153.90 Intermediate StaTerminated
% 299.57/300.03 Bliksem ended
%------------------------------------------------------------------------------