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