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