%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX193-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n021.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:46 PM UTC 2026
% Result : Timeout 299.51s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX193-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n021.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 10:17:55 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.73/1.26 *** allocated 10000 integers for termspace/termends
% 0.73/1.26 *** allocated 10000 integers for clauses
% 0.73/1.26 *** allocated 10000 integers for justifications
% 0.73/1.26 Bliksem 1.12
% 0.73/1.26
% 0.73/1.26
% 0.73/1.26 Automatic Strategy Selection
% 0.73/1.26
% 0.73/1.26 Clauses:
% 0.73/1.26 [
% 0.73/1.26 [ =( aux( X, Y, btrue ), y( n( s( s( z ) ) ), opt( X ) ) ) ],
% 0.73/1.26 [ =( aux( x( X, Y ), Z, bfalse ), opt( x( X, x( Y, Z ) ) ) ) ],
% 0.73/1.26 [ =( aux( n( X ), Y, bfalse ), x( opt( n( X ) ), opt( Y ) ) ) ],
% 0.73/1.26 [ =( aux( y( X, Y ), Z, bfalse ), x( opt( y( X, Y ) ), opt( Z ) ) ) ]
% 0.73/1.26 ,
% 0.73/1.26 [ =( aux( x2, X, bfalse ), x( opt( x2 ), opt( X ) ) ) ],
% 0.73/1.26 [ =( fail2( X, Y ), aux( X, Y, eq2( X, Y ) ) ) ],
% 0.73/1.26 [ =( fail1( n( X ), n( Y ) ), n( addNat( X, Y ) ) ) ],
% 0.73/1.26 [ =( fail1( n( X ), x( Y, Z ) ), fail2( n( X ), x( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail1( n( X ), y( Y, Z ) ), fail2( n( X ), y( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail1( n( X ), x2 ), fail2( n( X ), x2 ) ) ],
% 0.73/1.26 [ =( fail1( x( X, Y ), Z ), fail2( x( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( fail1( y( X, Y ), Z ), fail2( y( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( fail1( x2, X ), fail2( x2, X ) ) ],
% 0.73/1.26 [ =( fail( X, n( s( Y ) ) ), fail1( X, n( s( Y ) ) ) ) ],
% 0.73/1.26 [ =( fail( X, n( z ) ), X ) ],
% 0.73/1.26 [ =( fail( X, x( Y, Z ) ), fail1( X, x( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail( X, y( Y, Z ) ), fail1( X, y( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail( X, x2 ), fail1( X, x2 ) ) ],
% 0.73/1.26 [ =( fail4( X, Y ), y( opt( X ), opt( Y ) ) ) ],
% 0.73/1.26 [ =( fail32( n( X ), n( Y ) ), n( mulNat( X, Y ) ) ) ],
% 0.73/1.26 [ =( fail32( n( X ), x( Y, Z ) ), fail4( n( X ), x( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail32( n( X ), y( Y, Z ) ), fail4( n( X ), y( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail32( n( X ), x2 ), fail4( n( X ), x2 ) ) ],
% 0.73/1.26 [ =( fail32( y( X, Y ), Z ), opt( y( X, y( Y, Z ) ) ) ) ],
% 0.73/1.26 [ =( fail32( x( X, Y ), Z ), fail4( x( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( fail32( x2, X ), fail4( x2, X ) ) ],
% 0.73/1.26 [ =( fail22( X, n( s( s( Y ) ) ) ), fail32( X, n( s( s( Y ) ) ) ) ) ]
% 0.73/1.26 ,
% 0.73/1.26 [ =( fail22( X, n( s( z ) ) ), X ) ],
% 0.73/1.26 [ =( fail22( X, n( z ) ), fail32( X, n( z ) ) ) ],
% 0.73/1.26 [ =( fail22( X, x( Y, Z ) ), fail32( X, x( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail22( X, y( Y, Z ) ), fail32( X, y( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail22( X, x2 ), fail32( X, x2 ) ) ],
% 0.73/1.26 [ =( fail12( n( s( s( X ) ) ), Y ), fail22( n( s( s( X ) ) ), Y ) ) ]
% 0.73/1.26 ,
% 0.73/1.26 [ =( fail12( n( s( z ) ), X ), X ) ],
% 0.73/1.26 [ =( fail12( n( z ), X ), fail22( n( z ), X ) ) ],
% 0.73/1.26 [ =( fail12( x( X, Y ), Z ), fail22( x( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( fail12( y( X, Y ), Z ), fail22( y( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( fail12( x2, X ), fail22( x2, X ) ) ],
% 0.73/1.26 [ =( fail3( X, n( s( Y ) ) ), fail12( X, n( s( Y ) ) ) ) ],
% 0.73/1.26 [ =( fail3( X, n( z ) ), n( z ) ) ],
% 0.73/1.26 [ =( fail3( X, x( Y, Z ) ), fail12( X, x( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail3( X, y( Y, Z ) ), fail12( X, y( Y, Z ) ) ) ],
% 0.73/1.26 [ =( fail3( X, x2 ), fail12( X, x2 ) ) ],
% 0.73/1.26 [ =( impl( btrue, X ), X ) ],
% 0.73/1.26 [ =( impl( bfalse, X ), btrue ) ],
% 0.73/1.26 [ =( d( n( X ) ), n( z ) ) ],
% 0.73/1.26 [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ],
% 0.73/1.26 [ =( d( y( X, Y ) ), x( y( d( X ), Y ), y( X, d( Y ) ) ) ) ],
% 0.73/1.26 [ =( d( x2 ), n( s( z ) ) ) ],
% 0.73/1.26 [ =( addNat( s( X ), Y ), s( addNat( X, Y ) ) ) ],
% 0.73/1.26 [ =( addNat( z, X ), X ) ],
% 0.73/1.26 [ =( mulNat( s( X ), Y ), addNat( Y, mulNat( X, Y ) ) ) ],
% 0.73/1.26 [ =( mulNat( z, X ), z ) ],
% 0.73/1.26 [ =( opt( x( n( s( X ) ), Y ) ), fail( n( s( X ) ), Y ) ) ],
% 0.73/1.26 [ =( opt( x( n( z ), X ) ), X ) ],
% 0.73/1.26 [ =( opt( x( x( X, Y ), Z ) ), fail( x( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( opt( x( y( X, Y ), Z ) ), fail( y( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( opt( x( x2, X ) ), fail( x2, X ) ) ],
% 0.73/1.26 [ =( opt( y( n( s( X ) ), Y ) ), fail3( n( s( X ) ), Y ) ) ],
% 0.73/1.26 [ =( opt( y( n( z ), X ) ), n( z ) ) ],
% 0.73/1.26 [ =( opt( y( x( X, Y ), Z ) ), fail3( x( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( opt( y( y( X, Y ), Z ) ), fail3( y( X, Y ), Z ) ) ],
% 0.73/1.26 [ =( opt( y( x2, X ) ), fail3( x2, X ) ) ],
% 0.73/1.26 [ =( opt( n( X ) ), n( X ) ) ],
% 0.73/1.26 [ =( opt( x2 ), x2 ) ],
% 0.73/1.26 [ =( propm6( X ), impl( eq2( opt( d( X ) ), x( y( x2, y( x2, y( x2, y(
% 0.73/1.26 x2, x2 ) ) ) ), y( x2, x( y( x2, y( x2, y( x2, x2 ) ) ), y( x2, x( y( x2
% 0.73/1.26 , y( x2, x2 ) ), y( x2, x( y( x2, x2 ), y( x2, x( x2, x2 ) ) ) ) ) ) ) )
% 0.73/1.26 ) ), eq3( btrue, bfalse ) ) ) ],
% 0.73/1.26 [ =( eq3( bfalse, btrue ), bfalse ) ],
% 0.73/1.26 [ =( eq3( btrue, bfalse ), bfalse ) ],
% 0.73/1.26 [ =( eq2( n( X ), n( Y ) ), eq( X, Y ) ) ],
% 0.73/1.26 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq2( x( X, Z ), x( Y, T ) ), bfalse
% 4.93/5.31 ) ],
% 4.93/5.31 [ ~( =( eq2( X, Y ), btrue ) ), =( eq2( x( X, Z ), x( Y, T ) ), eq2( Z,
% 4.93/5.31 T ) ) ],
% 4.93/5.31 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq2( y( X, Z ), y( Y, T ) ), bfalse
% 4.93/5.31 ) ],
% 4.93/5.31 [ ~( =( eq2( X, Y ), btrue ) ), =( eq2( y( X, Z ), y( Y, T ) ), eq2( Z,
% 4.93/5.31 T ) ) ],
% 4.93/5.31 [ =( eq2( n( X ), x( Y, Z ) ), bfalse ) ],
% 4.93/5.31 [ =( eq2( n( X ), y( Y, Z ) ), bfalse ) ],
% 4.93/5.31 [ =( eq2( n( X ), x2 ), bfalse ) ],
% 4.93/5.31 [ =( eq2( x( X, Y ), n( Z ) ), bfalse ) ],
% 4.93/5.31 [ =( eq2( x( X, Y ), y( Z, T ) ), bfalse ) ],
% 4.93/5.31 [ =( eq2( x( X, Y ), x2 ), bfalse ) ],
% 4.93/5.31 [ =( eq2( y( X, Y ), n( Z ) ), bfalse ) ],
% 4.93/5.31 [ =( eq2( y( X, Y ), x( Z, T ) ), bfalse ) ],
% 4.93/5.31 [ =( eq2( y( X, Y ), x2 ), bfalse ) ],
% 4.93/5.31 [ =( eq2( x2, n( X ) ), bfalse ) ],
% 4.93/5.31 [ =( eq2( x2, x( X, Y ) ), bfalse ) ],
% 4.93/5.31 [ =( eq2( x2, y( X, Y ) ), bfalse ) ],
% 4.93/5.31 [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ],
% 4.93/5.31 [ =( eq( s( X ), z ), bfalse ) ],
% 4.93/5.31 [ =( eq( z, s( X ) ), bfalse ) ],
% 4.93/5.31 [ =( eq( X, X ), btrue ) ],
% 4.93/5.31 [ =( eq2( X, X ), btrue ) ],
% 4.93/5.31 [ =( eq3( X, X ), btrue ) ],
% 4.93/5.31 [ ~( =( eq3( propm6( X ), bfalse ), btrue ) ) ]
% 4.93/5.31 ] .
% 4.93/5.31
% 4.93/5.31
% 4.93/5.31 percentage equality = 1.000000, percentage horn = 1.000000
% 4.93/5.31 This is a pure equality problem
% 4.93/5.31
% 4.93/5.31
% 4.93/5.31
% 4.93/5.31 Options Used:
% 4.93/5.31
% 4.93/5.31 useres = 1
% 4.93/5.31 useparamod = 1
% 4.93/5.31 useeqrefl = 1
% 4.93/5.31 useeqfact = 1
% 4.93/5.31 usefactor = 1
% 4.93/5.31 usesimpsplitting = 0
% 4.93/5.31 usesimpdemod = 5
% 4.93/5.31 usesimpres = 3
% 4.93/5.31
% 4.93/5.31 resimpinuse = 1000
% 4.93/5.31 resimpclauses = 20000
% 4.93/5.31 substype = eqrewr
% 4.93/5.31 backwardsubs = 1
% 4.93/5.31 selectoldest = 5
% 4.93/5.31
% 4.93/5.31 litorderings [0] = split
% 4.93/5.31 litorderings [1] = extend the termordering, first sorting on arguments
% 4.93/5.31
% 4.93/5.31 termordering = kbo
% 4.93/5.31
% 4.93/5.31 litapriori = 0
% 4.93/5.31 termapriori = 1
% 4.93/5.31 litaposteriori = 0
% 4.93/5.31 termaposteriori = 0
% 4.93/5.31 demodaposteriori = 0
% 4.93/5.31 ordereqreflfact = 0
% 4.93/5.31
% 4.93/5.31 litselect = negord
% 4.93/5.31
% 4.93/5.31 maxweight = 15
% 4.93/5.31 maxdepth = 30000
% 4.93/5.31 maxlength = 115
% 4.93/5.31 maxnrvars = 195
% 4.93/5.31 excuselevel = 1
% 4.93/5.31 increasemaxweight = 1
% 4.93/5.31
% 4.93/5.31 maxselected = 10000000
% 4.93/5.31 maxnrclauses = 10000000
% 4.93/5.31
% 4.93/5.31 showgenerated = 0
% 4.93/5.31 showkept = 0
% 4.93/5.31 showselected = 0
% 4.93/5.31 showdeleted = 0
% 4.93/5.31 showresimp = 1
% 4.93/5.31 showstatus = 2000
% 4.93/5.31
% 4.93/5.31 prologoutput = 1
% 4.93/5.31 nrgoals = 5000000
% 4.93/5.31 totalproof = 1
% 4.93/5.31
% 4.93/5.31 Symbols occurring in the translation:
% 4.93/5.31
% 4.93/5.31 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 4.93/5.31 . [1, 2] (w:1, o:48, a:1, s:1, b:0),
% 4.93/5.31 ! [4, 1] (w:0, o:38, a:1, s:1, b:0),
% 4.93/5.31 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 4.93/5.31 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 4.93/5.31 btrue [41, 0] (w:1, o:19, a:1, s:1, b:0),
% 4.93/5.31 aux [42, 3] (w:1, o:89, a:1, s:1, b:0),
% 4.93/5.31 z [43, 0] (w:1, o:20, a:1, s:1, b:0),
% 4.93/5.31 s [44, 1] (w:1, o:43, a:1, s:1, b:0),
% 4.93/5.31 n [45, 1] (w:1, o:44, a:1, s:1, b:0),
% 4.93/5.31 opt [46, 1] (w:1, o:45, a:1, s:1, b:0),
% 4.93/5.31 y [47, 2] (w:1, o:74, a:1, s:1, b:0),
% 4.93/5.31 x [50, 2] (w:1, o:73, a:1, s:1, b:0),
% 4.93/5.31 bfalse [51, 0] (w:1, o:29, a:1, s:1, b:0),
% 4.93/5.31 x2 [54, 0] (w:1, o:30, a:1, s:1, b:0),
% 4.93/5.31 fail2 [55, 2] (w:1, o:80, a:1, s:1, b:0),
% 4.93/5.31 eq2 [56, 2] (w:1, o:75, a:1, s:1, b:0),
% 4.93/5.31 fail1 [59, 2] (w:1, o:78, a:1, s:1, b:0),
% 4.93/5.31 addNat [60, 2] (w:1, o:81, a:1, s:1, b:0),
% 4.93/5.31 fail [61, 2] (w:1, o:82, a:1, s:1, b:0),
% 4.93/5.31 fail4 [64, 2] (w:1, o:86, a:1, s:1, b:0),
% 4.93/5.31 fail32 [67, 2] (w:1, o:84, a:1, s:1, b:0),
% 4.93/5.31 mulNat [68, 2] (w:1, o:87, a:1, s:1, b:0),
% 4.93/5.31 fail22 [72, 2] (w:1, o:83, a:1, s:1, b:0),
% 4.93/5.31 fail12 [74, 2] (w:1, o:79, a:1, s:1, b:0),
% 4.93/5.31 fail3 [76, 2] (w:1, o:85, a:1, s:1, b:0),
% 4.93/5.31 impl [78, 2] (w:1, o:88, a:1, s:1, b:0),
% 4.93/5.31 d [79, 1] (w:1, o:46, a:1, s:1, b:0),
% 4.93/5.31 propm6 [87, 1] (w:1, o:47, a:1, s:1, b:0),
% 4.93/5.31 eq3 [88, 2] (w:1, o:76, a:1, s:1, b:0),
% 4.93/5.31 eq [89, 2] (w:1, o:77, a:1, s:1, b:0).
% 4.93/5.31
% 4.93/5.31
% 4.93/5.31 Starting Search:
% 4.93/5.31
% 4.93/5.31 Resimplifying inuse:
% 4.93/5.31 Done
% 4.93/5.31
% 4.93/5.31
% 4.93/5.31 Intermediate Status:
% 4.93/5.31 Generated: 5557
% 4.93/5.31 Kept: 2048
% 4.93/5.31 Inuse: 330
% 4.93/5.31 Deleted: 101
% 4.93/5.31 Deletedinuse: 10
% 4.93/5.31
% 4.93/5.31 Resimplifying inuse:
% 4.93/5.31 Done
% 4.93/5.31
% 4.93/5.31 Resimplifying inuse:
% 4.93/5.31 Done
% 4.93/5.31
% 4.93/5.31
% 4.93/5.31 Intermediate Status:
% 4.93/5.31 Generated: 11560
% 4.93/5.31 Kept: 4048
% 4.93/5.31 Inuse: 564
% 4.93/5.31 Deleted: 139
% 4.93/5.31 Deletedinuse: 14
% 4.93/5.31
% 4.93/5.31 Resimplifying inuse:
% 4.93/5.31 Done
% 4.93/5.31
% 4.93/5.31 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 17263
% 15.53/15.99 Kept: 6051
% 15.53/15.99 Inuse: 760
% 15.53/15.99 Deleted: 171
% 15.53/15.99 Deletedinuse: 14
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 22437
% 15.53/15.99 Kept: 8065
% 15.53/15.99 Inuse: 908
% 15.53/15.99 Deleted: 222
% 15.53/15.99 Deletedinuse: 18
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 28561
% 15.53/15.99 Kept: 10153
% 15.53/15.99 Inuse: 1039
% 15.53/15.99 Deleted: 230
% 15.53/15.99 Deletedinuse: 18
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 34174
% 15.53/15.99 Kept: 12161
% 15.53/15.99 Inuse: 1140
% 15.53/15.99 Deleted: 242
% 15.53/15.99 Deletedinuse: 24
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 43729
% 15.53/15.99 Kept: 14284
% 15.53/15.99 Inuse: 1312
% 15.53/15.99 Deleted: 253
% 15.53/15.99 Deletedinuse: 24
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 58198
% 15.53/15.99 Kept: 16292
% 15.53/15.99 Inuse: 1549
% 15.53/15.99 Deleted: 297
% 15.53/15.99 Deletedinuse: 26
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 64575
% 15.53/15.99 Kept: 18300
% 15.53/15.99 Inuse: 1663
% 15.53/15.99 Deleted: 330
% 15.53/15.99 Deletedinuse: 29
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying clauses:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 70373
% 15.53/15.99 Kept: 20311
% 15.53/15.99 Inuse: 1780
% 15.53/15.99 Deleted: 2946
% 15.53/15.99 Deletedinuse: 29
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 111651
% 15.53/15.99 Kept: 22312
% 15.53/15.99 Inuse: 1926
% 15.53/15.99 Deleted: 2986
% 15.53/15.99 Deletedinuse: 61
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 123515
% 15.53/15.99 Kept: 24316
% 15.53/15.99 Inuse: 2126
% 15.53/15.99 Deleted: 2992
% 15.53/15.99 Deletedinuse: 62
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 143295
% 15.53/15.99 Kept: 26435
% 15.53/15.99 Inuse: 2304
% 15.53/15.99 Deleted: 3008
% 15.53/15.99 Deletedinuse: 66
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 179689
% 15.53/15.99 Kept: 28438
% 15.53/15.99 Inuse: 2418
% 15.53/15.99 Deleted: 3022
% 15.53/15.99 Deletedinuse: 68
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 194360
% 15.53/15.99 Kept: 30443
% 15.53/15.99 Inuse: 2579
% 15.53/15.99 Deleted: 3038
% 15.53/15.99 Deletedinuse: 68
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 204860
% 15.53/15.99 Kept: 32454
% 15.53/15.99 Inuse: 2662
% 15.53/15.99 Deleted: 3042
% 15.53/15.99 Deletedinuse: 72
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 212708
% 15.53/15.99 Kept: 34478
% 15.53/15.99 Inuse: 2728
% 15.53/15.99 Deleted: 3048
% 15.53/15.99 Deletedinuse: 72
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 223766
% 15.53/15.99 Kept: 36479
% 15.53/15.99 Inuse: 2824
% 15.53/15.99 Deleted: 3050
% 15.53/15.99 Deletedinuse: 74
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 239244
% 15.53/15.99 Kept: 38866
% 15.53/15.99 Inuse: 2970
% 15.53/15.99 Deleted: 3050
% 15.53/15.99 Deletedinuse: 74
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying clauses:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 246802
% 15.53/15.99 Kept: 40877
% 15.53/15.99 Inuse: 3026
% 15.53/15.99 Deleted: 5490
% 15.53/15.99 Deletedinuse: 78
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 262024
% 15.53/15.99 Kept: 42879
% 15.53/15.99 Inuse: 3208
% 15.53/15.99 Deleted: 5496
% 15.53/15.99 Deletedinuse: 78
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 275991
% 15.53/15.99 Kept: 44896
% 15.53/15.99 Inuse: 3339
% 15.53/15.99 Deleted: 5500
% 15.53/15.99 Deletedinuse: 82
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 284425
% 15.53/15.99 Kept: 46911
% 15.53/15.99 Inuse: 3420
% 15.53/15.99 Deleted: 5505
% 15.53/15.99 Deletedinuse: 82
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 303814
% 15.53/15.99 Kept: 48914
% 15.53/15.99 Inuse: 3626
% 15.53/15.99 Deleted: 5505
% 15.53/15.99 Deletedinuse: 82
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 312941
% 15.53/15.99 Kept: 50941
% 15.53/15.99 Inuse: 3726
% 15.53/15.99 Deleted: 5511
% 15.53/15.99 Deletedinuse: 84
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99 Resimplifying inuse:
% 15.53/15.99 Done
% 15.53/15.99
% 15.53/15.99
% 15.53/15.99 Intermediate Status:
% 15.53/15.99 Generated: 324591
% 15.53/15.99 Kept: 52943
% 40.65/41.04 Inuse: 3855
% 40.65/41.04 Deleted: 5511
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 337687
% 40.65/41.04 Kept: 54952
% 40.65/41.04 Inuse: 4007
% 40.65/41.04 Deleted: 5516
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 347659
% 40.65/41.04 Kept: 56976
% 40.65/41.04 Inuse: 4100
% 40.65/41.04 Deleted: 5520
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 355676
% 40.65/41.04 Kept: 58987
% 40.65/41.04 Inuse: 4163
% 40.65/41.04 Deleted: 5522
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying clauses:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 364959
% 40.65/41.04 Kept: 60989
% 40.65/41.04 Inuse: 4240
% 40.65/41.04 Deleted: 7368
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 376770
% 40.65/41.04 Kept: 63001
% 40.65/41.04 Inuse: 4349
% 40.65/41.04 Deleted: 7369
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 390543
% 40.65/41.04 Kept: 65008
% 40.65/41.04 Inuse: 4486
% 40.65/41.04 Deleted: 7369
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 408936
% 40.65/41.04 Kept: 67008
% 40.65/41.04 Inuse: 4688
% 40.65/41.04 Deleted: 7371
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 420215
% 40.65/41.04 Kept: 69043
% 40.65/41.04 Inuse: 4800
% 40.65/41.04 Deleted: 7371
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 427542
% 40.65/41.04 Kept: 71048
% 40.65/41.04 Inuse: 4853
% 40.65/41.04 Deleted: 7371
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 441964
% 40.65/41.04 Kept: 73064
% 40.65/41.04 Inuse: 4995
% 40.65/41.04 Deleted: 7371
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 457999
% 40.65/41.04 Kept: 75071
% 40.65/41.04 Inuse: 5174
% 40.65/41.04 Deleted: 7377
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 474094
% 40.65/41.04 Kept: 77105
% 40.65/41.04 Inuse: 5361
% 40.65/41.04 Deleted: 7379
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 489162
% 40.65/41.04 Kept: 79112
% 40.65/41.04 Inuse: 5543
% 40.65/41.04 Deleted: 7386
% 40.65/41.04 Deletedinuse: 84
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying clauses:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 506747
% 40.65/41.04 Kept: 81147
% 40.65/41.04 Inuse: 5749
% 40.65/41.04 Deleted: 8874
% 40.65/41.04 Deletedinuse: 92
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 528307
% 40.65/41.04 Kept: 83366
% 40.65/41.04 Inuse: 5965
% 40.65/41.04 Deleted: 8874
% 40.65/41.04 Deletedinuse: 92
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 553957
% 40.65/41.04 Kept: 85369
% 40.65/41.04 Inuse: 6212
% 40.65/41.04 Deleted: 8874
% 40.65/41.04 Deletedinuse: 92
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 589961
% 40.65/41.04 Kept: 87383
% 40.65/41.04 Inuse: 6648
% 40.65/41.04 Deleted: 8899
% 40.65/41.04 Deletedinuse: 101
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 600398
% 40.65/41.04 Kept: 89392
% 40.65/41.04 Inuse: 6747
% 40.65/41.04 Deleted: 8916
% 40.65/41.04 Deletedinuse: 105
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 612670
% 40.65/41.04 Kept: 91392
% 40.65/41.04 Inuse: 6869
% 40.65/41.04 Deleted: 8925
% 40.65/41.04 Deletedinuse: 105
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 621941
% 40.65/41.04 Kept: 94166
% 40.65/41.04 Inuse: 6942
% 40.65/41.04 Deleted: 8925
% 40.65/41.04 Deletedinuse: 105
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 637302
% 40.65/41.04 Kept: 96174
% 40.65/41.04 Inuse: 7106
% 40.65/41.04 Deleted: 8925
% 40.65/41.04 Deletedinuse: 105
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 652634
% 40.65/41.04 Kept: 98178
% 40.65/41.04 Inuse: 7256
% 40.65/41.04 Deleted: 8929
% 40.65/41.04 Deletedinuse: 105
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04
% 40.65/41.04 Intermediate Status:
% 40.65/41.04 Generated: 673670
% 40.65/41.04 Kept: 100208
% 40.65/41.04 Inuse: 7446
% 40.65/41.04 Deleted: 8967
% 40.65/41.04 Deletedinuse: 105
% 40.65/41.04
% 40.65/41.04 Resimplifying inuse:
% 40.65/41.04 Done
% 40.65/41.04
% 40.65/41.04 Resimplifying clauses:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 688870
% 155.53/156.03 Kept: 102210
% 155.53/156.03 Inuse: 7578
% 155.53/156.03 Deleted: 11354
% 155.53/156.03 Deletedinuse: 105
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 709489
% 155.53/156.03 Kept: 104215
% 155.53/156.03 Inuse: 7756
% 155.53/156.03 Deleted: 11354
% 155.53/156.03 Deletedinuse: 105
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 733655
% 155.53/156.03 Kept: 106221
% 155.53/156.03 Inuse: 8008
% 155.53/156.03 Deleted: 11362
% 155.53/156.03 Deletedinuse: 105
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 774886
% 155.53/156.03 Kept: 108223
% 155.53/156.03 Inuse: 8220
% 155.53/156.03 Deleted: 11369
% 155.53/156.03 Deletedinuse: 111
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 796331
% 155.53/156.03 Kept: 110237
% 155.53/156.03 Inuse: 8469
% 155.53/156.03 Deleted: 11383
% 155.53/156.03 Deletedinuse: 112
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 810014
% 155.53/156.03 Kept: 113322
% 155.53/156.03 Inuse: 8578
% 155.53/156.03 Deleted: 11383
% 155.53/156.03 Deletedinuse: 112
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 822823
% 155.53/156.03 Kept: 116519
% 155.53/156.03 Inuse: 8696
% 155.53/156.03 Deleted: 11413
% 155.53/156.03 Deletedinuse: 118
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 836947
% 155.53/156.03 Kept: 118521
% 155.53/156.03 Inuse: 8857
% 155.53/156.03 Deleted: 11442
% 155.53/156.03 Deletedinuse: 147
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 844341
% 155.53/156.03 Kept: 120560
% 155.53/156.03 Inuse: 8889
% 155.53/156.03 Deleted: 11442
% 155.53/156.03 Deletedinuse: 147
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying clauses:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 850243
% 155.53/156.03 Kept: 123692
% 155.53/156.03 Inuse: 8913
% 155.53/156.03 Deleted: 13918
% 155.53/156.03 Deletedinuse: 151
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 860785
% 155.53/156.03 Kept: 125701
% 155.53/156.03 Inuse: 8986
% 155.53/156.03 Deleted: 13946
% 155.53/156.03 Deletedinuse: 177
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 890226
% 155.53/156.03 Kept: 127702
% 155.53/156.03 Inuse: 9198
% 155.53/156.03 Deleted: 13982
% 155.53/156.03 Deletedinuse: 205
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 916018
% 155.53/156.03 Kept: 130038
% 155.53/156.03 Inuse: 9339
% 155.53/156.03 Deleted: 13982
% 155.53/156.03 Deletedinuse: 205
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 950441
% 155.53/156.03 Kept: 132047
% 155.53/156.03 Inuse: 9614
% 155.53/156.03 Deleted: 13984
% 155.53/156.03 Deletedinuse: 205
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 975851
% 155.53/156.03 Kept: 134049
% 155.53/156.03 Inuse: 9844
% 155.53/156.03 Deleted: 13986
% 155.53/156.03 Deletedinuse: 205
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 991022
% 155.53/156.03 Kept: 136050
% 155.53/156.03 Inuse: 9961
% 155.53/156.03 Deleted: 13994
% 155.53/156.03 Deletedinuse: 205
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 1046452
% 155.53/156.03 Kept: 138150
% 155.53/156.03 Inuse: 10146
% 155.53/156.03 Deleted: 14006
% 155.53/156.03 Deletedinuse: 205
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 1049977
% 155.53/156.03 Kept: 140558
% 155.53/156.03 Inuse: 10147
% 155.53/156.03 Deleted: 14014
% 155.53/156.03 Deletedinuse: 213
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying clauses:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 1099078
% 155.53/156.03 Kept: 142570
% 155.53/156.03 Inuse: 10552
% 155.53/156.03 Deleted: 16143
% 155.53/156.03 Deletedinuse: 213
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 1112085
% 155.53/156.03 Kept: 146247
% 155.53/156.03 Inuse: 10628
% 155.53/156.03 Deleted: 16151
% 155.53/156.03 Deletedinuse: 221
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 1138437
% 155.53/156.03 Kept: 149967
% 155.53/156.03 Inuse: 10760
% 155.53/156.03 Deleted: 16209
% 155.53/156.03 Deletedinuse: 279
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 1168336
% 155.53/156.03 Kept: 151977
% 155.53/156.03 Inuse: 10983
% 155.53/156.03 Deleted: 16221
% 155.53/156.03 Deletedinuse: 285
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 1189578
% 155.53/156.03 Kept: 153996
% 155.53/156.03 Inuse: 11135
% 155.53/156.03 Deleted: 16234
% 155.53/156.03 Deletedinuse: 293
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03 Resimplifying inuse:
% 155.53/156.03 Done
% 155.53/156.03
% 155.53/156.03
% 155.53/156.03 Intermediate Status:
% 155.53/156.03 Generated: 1212662
% 155.53/156.03 Kept:Terminated
% 299.51/300.03 Bliksem ended
%------------------------------------------------------------------------------