%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX188-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n024.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:45 PM UTC 2026
% Result : Timeout 299.50s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : SWX188-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.06 % Command : bliksem %s
% 0.07/0.24 % Computer : n024.cluster.edu
% 0.07/0.24 % Model : x86_64 x86_64
% 0.07/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.24 % Memory : 8042.1875MB
% 0.07/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % DateTime : Tue May 5 04:46:11 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.44/0.95 *** allocated 10000 integers for termspace/termends
% 0.44/0.95 *** allocated 10000 integers for clauses
% 0.44/0.95 *** allocated 10000 integers for justifications
% 0.44/0.95 Bliksem 1.12
% 0.44/0.95
% 0.44/0.95
% 0.44/0.95 Automatic Strategy Selection
% 0.44/0.95
% 0.44/0.95 Clauses:
% 0.44/0.95 [
% 0.44/0.95 [ =( aux( X, Y, btrue ), y( n( s( s( z ) ) ), opt( X ) ) ) ],
% 0.44/0.95 [ =( aux( x( X, Y ), Z, bfalse ), opt( x( X, x( Y, Z ) ) ) ) ],
% 0.44/0.95 [ =( aux( n( X ), Y, bfalse ), x( opt( n( X ) ), opt( Y ) ) ) ],
% 0.44/0.95 [ =( aux( y( X, Y ), Z, bfalse ), x( opt( y( X, Y ) ), opt( Z ) ) ) ]
% 0.44/0.95 ,
% 0.44/0.95 [ =( aux( x2, X, bfalse ), x( opt( x2 ), opt( X ) ) ) ],
% 0.44/0.95 [ =( fail2( X, Y ), aux( X, Y, eq2( X, Y ) ) ) ],
% 0.44/0.95 [ =( fail1( n( X ), n( Y ) ), n( addNat( X, Y ) ) ) ],
% 0.44/0.95 [ =( fail1( n( X ), x( Y, Z ) ), fail2( n( X ), x( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail1( n( X ), y( Y, Z ) ), fail2( n( X ), y( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail1( n( X ), x2 ), fail2( n( X ), x2 ) ) ],
% 0.44/0.95 [ =( fail1( x( X, Y ), Z ), fail2( x( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( fail1( y( X, Y ), Z ), fail2( y( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( fail1( x2, X ), fail2( x2, X ) ) ],
% 0.44/0.95 [ =( fail( X, n( s( Y ) ) ), fail1( X, n( s( Y ) ) ) ) ],
% 0.44/0.95 [ =( fail( X, n( z ) ), X ) ],
% 0.44/0.95 [ =( fail( X, x( Y, Z ) ), fail1( X, x( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail( X, y( Y, Z ) ), fail1( X, y( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail( X, x2 ), fail1( X, x2 ) ) ],
% 0.44/0.95 [ =( fail4( X, Y ), y( opt( X ), opt( Y ) ) ) ],
% 0.44/0.95 [ =( fail32( n( X ), n( Y ) ), n( mulNat( X, Y ) ) ) ],
% 0.44/0.95 [ =( fail32( n( X ), x( Y, Z ) ), fail4( n( X ), x( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail32( n( X ), y( Y, Z ) ), fail4( n( X ), y( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail32( n( X ), x2 ), fail4( n( X ), x2 ) ) ],
% 0.44/0.95 [ =( fail32( y( X, Y ), Z ), opt( y( X, y( Y, Z ) ) ) ) ],
% 0.44/0.95 [ =( fail32( x( X, Y ), Z ), fail4( x( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( fail32( x2, X ), fail4( x2, X ) ) ],
% 0.44/0.95 [ =( fail22( X, n( s( s( Y ) ) ) ), fail32( X, n( s( s( Y ) ) ) ) ) ]
% 0.44/0.95 ,
% 0.44/0.95 [ =( fail22( X, n( s( z ) ) ), X ) ],
% 0.44/0.95 [ =( fail22( X, n( z ) ), fail32( X, n( z ) ) ) ],
% 0.44/0.95 [ =( fail22( X, x( Y, Z ) ), fail32( X, x( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail22( X, y( Y, Z ) ), fail32( X, y( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail22( X, x2 ), fail32( X, x2 ) ) ],
% 0.44/0.95 [ =( fail12( n( s( s( X ) ) ), Y ), fail22( n( s( s( X ) ) ), Y ) ) ]
% 0.44/0.95 ,
% 0.44/0.95 [ =( fail12( n( s( z ) ), X ), X ) ],
% 0.44/0.95 [ =( fail12( n( z ), X ), fail22( n( z ), X ) ) ],
% 0.44/0.95 [ =( fail12( x( X, Y ), Z ), fail22( x( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( fail12( y( X, Y ), Z ), fail22( y( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( fail12( x2, X ), fail22( x2, X ) ) ],
% 0.44/0.95 [ =( fail3( X, n( s( Y ) ) ), fail12( X, n( s( Y ) ) ) ) ],
% 0.44/0.95 [ =( fail3( X, n( z ) ), n( z ) ) ],
% 0.44/0.95 [ =( fail3( X, x( Y, Z ) ), fail12( X, x( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail3( X, y( Y, Z ) ), fail12( X, y( Y, Z ) ) ) ],
% 0.44/0.95 [ =( fail3( X, x2 ), fail12( X, x2 ) ) ],
% 0.44/0.95 [ =( impl( btrue, X ), X ) ],
% 0.44/0.95 [ =( impl( bfalse, X ), btrue ) ],
% 0.44/0.95 [ =( d( n( X ) ), n( z ) ) ],
% 0.44/0.95 [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ],
% 0.44/0.95 [ =( d( y( X, Y ) ), x( y( d( X ), Y ), y( X, d( Y ) ) ) ) ],
% 0.44/0.95 [ =( d( x2 ), n( s( z ) ) ) ],
% 0.44/0.95 [ =( addNat( s( X ), Y ), s( addNat( X, Y ) ) ) ],
% 0.44/0.95 [ =( addNat( z, X ), X ) ],
% 0.44/0.95 [ =( mulNat( s( X ), Y ), addNat( Y, mulNat( X, Y ) ) ) ],
% 0.44/0.95 [ =( mulNat( z, X ), z ) ],
% 0.44/0.95 [ =( opt( x( n( s( X ) ), Y ) ), fail( n( s( X ) ), Y ) ) ],
% 0.44/0.95 [ =( opt( x( n( z ), X ) ), X ) ],
% 0.44/0.95 [ =( opt( x( x( X, Y ), Z ) ), fail( x( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( opt( x( y( X, Y ), Z ) ), fail( y( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( opt( x( x2, X ) ), fail( x2, X ) ) ],
% 0.44/0.95 [ =( opt( y( n( s( X ) ), Y ) ), fail3( n( s( X ) ), Y ) ) ],
% 0.44/0.95 [ =( opt( y( n( z ), X ) ), n( z ) ) ],
% 0.44/0.95 [ =( opt( y( x( X, Y ), Z ) ), fail3( x( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( opt( y( y( X, Y ), Z ) ), fail3( y( X, Y ), Z ) ) ],
% 0.44/0.95 [ =( opt( y( x2, X ) ), fail3( x2, X ) ) ],
% 0.44/0.95 [ =( opt( n( X ) ), n( X ) ) ],
% 0.44/0.95 [ =( opt( x2 ), x2 ) ],
% 0.44/0.95 [ =( prop1( X ), impl( eq2( opt( d( X ) ), opt( x( n( s( s( z ) ) ), x(
% 0.44/0.95 x2, x2 ) ) ) ), eq3( btrue, bfalse ) ) ) ],
% 0.44/0.95 [ =( eq3( bfalse, btrue ), bfalse ) ],
% 0.44/0.95 [ =( eq3( btrue, bfalse ), bfalse ) ],
% 0.44/0.95 [ =( eq2( n( X ), n( Y ) ), eq( X, Y ) ) ],
% 0.44/0.95 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq2( x( X, Z ), x( Y, T ) ), bfalse
% 0.44/0.95 ) ],
% 0.44/0.95 [ ~( =( eq2( X, Y ), btrue ) ), =( eq2( x( X, Z ), x( Y, T ) ), eq2( Z,
% 5.52/5.95 T ) ) ],
% 5.52/5.95 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq2( y( X, Z ), y( Y, T ) ), bfalse
% 5.52/5.95 ) ],
% 5.52/5.95 [ ~( =( eq2( X, Y ), btrue ) ), =( eq2( y( X, Z ), y( Y, T ) ), eq2( Z,
% 5.52/5.95 T ) ) ],
% 5.52/5.95 [ =( eq2( n( X ), x( Y, Z ) ), bfalse ) ],
% 5.52/5.95 [ =( eq2( n( X ), y( Y, Z ) ), bfalse ) ],
% 5.52/5.95 [ =( eq2( n( X ), x2 ), bfalse ) ],
% 5.52/5.95 [ =( eq2( x( X, Y ), n( Z ) ), bfalse ) ],
% 5.52/5.95 [ =( eq2( x( X, Y ), y( Z, T ) ), bfalse ) ],
% 5.52/5.95 [ =( eq2( x( X, Y ), x2 ), bfalse ) ],
% 5.52/5.95 [ =( eq2( y( X, Y ), n( Z ) ), bfalse ) ],
% 5.52/5.95 [ =( eq2( y( X, Y ), x( Z, T ) ), bfalse ) ],
% 5.52/5.95 [ =( eq2( y( X, Y ), x2 ), bfalse ) ],
% 5.52/5.95 [ =( eq2( x2, n( X ) ), bfalse ) ],
% 5.52/5.95 [ =( eq2( x2, x( X, Y ) ), bfalse ) ],
% 5.52/5.95 [ =( eq2( x2, y( X, Y ) ), bfalse ) ],
% 5.52/5.95 [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ],
% 5.52/5.95 [ =( eq( s( X ), z ), bfalse ) ],
% 5.52/5.95 [ =( eq( z, s( X ) ), bfalse ) ],
% 5.52/5.95 [ =( eq( X, X ), btrue ) ],
% 5.52/5.95 [ =( eq2( X, X ), btrue ) ],
% 5.52/5.95 [ =( eq3( X, X ), btrue ) ],
% 5.52/5.95 [ ~( =( eq3( prop1( X ), bfalse ), btrue ) ) ]
% 5.52/5.95 ] .
% 5.52/5.95
% 5.52/5.95
% 5.52/5.95 percentage equality = 1.000000, percentage horn = 1.000000
% 5.52/5.95 This is a pure equality problem
% 5.52/5.95
% 5.52/5.95
% 5.52/5.95
% 5.52/5.95 Options Used:
% 5.52/5.95
% 5.52/5.95 useres = 1
% 5.52/5.95 useparamod = 1
% 5.52/5.95 useeqrefl = 1
% 5.52/5.95 useeqfact = 1
% 5.52/5.95 usefactor = 1
% 5.52/5.95 usesimpsplitting = 0
% 5.52/5.95 usesimpdemod = 5
% 5.52/5.95 usesimpres = 3
% 5.52/5.95
% 5.52/5.95 resimpinuse = 1000
% 5.52/5.95 resimpclauses = 20000
% 5.52/5.95 substype = eqrewr
% 5.52/5.95 backwardsubs = 1
% 5.52/5.95 selectoldest = 5
% 5.52/5.95
% 5.52/5.95 litorderings [0] = split
% 5.52/5.95 litorderings [1] = extend the termordering, first sorting on arguments
% 5.52/5.95
% 5.52/5.95 termordering = kbo
% 5.52/5.95
% 5.52/5.95 litapriori = 0
% 5.52/5.95 termapriori = 1
% 5.52/5.95 litaposteriori = 0
% 5.52/5.95 termaposteriori = 0
% 5.52/5.95 demodaposteriori = 0
% 5.52/5.95 ordereqreflfact = 0
% 5.52/5.95
% 5.52/5.95 litselect = negord
% 5.52/5.95
% 5.52/5.95 maxweight = 15
% 5.52/5.95 maxdepth = 30000
% 5.52/5.95 maxlength = 115
% 5.52/5.95 maxnrvars = 195
% 5.52/5.95 excuselevel = 1
% 5.52/5.95 increasemaxweight = 1
% 5.52/5.95
% 5.52/5.95 maxselected = 10000000
% 5.52/5.95 maxnrclauses = 10000000
% 5.52/5.95
% 5.52/5.95 showgenerated = 0
% 5.52/5.95 showkept = 0
% 5.52/5.95 showselected = 0
% 5.52/5.95 showdeleted = 0
% 5.52/5.95 showresimp = 1
% 5.52/5.95 showstatus = 2000
% 5.52/5.95
% 5.52/5.95 prologoutput = 1
% 5.52/5.95 nrgoals = 5000000
% 5.52/5.95 totalproof = 1
% 5.52/5.95
% 5.52/5.95 Symbols occurring in the translation:
% 5.52/5.95
% 5.52/5.95 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 5.52/5.95 . [1, 2] (w:1, o:48, a:1, s:1, b:0),
% 5.52/5.95 ! [4, 1] (w:0, o:38, a:1, s:1, b:0),
% 5.52/5.95 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.52/5.95 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.52/5.95 btrue [41, 0] (w:1, o:19, a:1, s:1, b:0),
% 5.52/5.95 aux [42, 3] (w:1, o:89, a:1, s:1, b:0),
% 5.52/5.95 z [43, 0] (w:1, o:20, a:1, s:1, b:0),
% 5.52/5.95 s [44, 1] (w:1, o:43, a:1, s:1, b:0),
% 5.52/5.95 n [45, 1] (w:1, o:44, a:1, s:1, b:0),
% 5.52/5.95 opt [46, 1] (w:1, o:45, a:1, s:1, b:0),
% 5.52/5.95 y [47, 2] (w:1, o:74, a:1, s:1, b:0),
% 5.52/5.95 x [50, 2] (w:1, o:73, a:1, s:1, b:0),
% 5.52/5.95 bfalse [51, 0] (w:1, o:29, a:1, s:1, b:0),
% 5.52/5.95 x2 [54, 0] (w:1, o:30, a:1, s:1, b:0),
% 5.52/5.95 fail2 [55, 2] (w:1, o:80, a:1, s:1, b:0),
% 5.52/5.95 eq2 [56, 2] (w:1, o:75, a:1, s:1, b:0),
% 5.52/5.95 fail1 [59, 2] (w:1, o:78, a:1, s:1, b:0),
% 5.52/5.95 addNat [60, 2] (w:1, o:81, a:1, s:1, b:0),
% 5.52/5.95 fail [61, 2] (w:1, o:82, a:1, s:1, b:0),
% 5.52/5.95 fail4 [64, 2] (w:1, o:86, a:1, s:1, b:0),
% 5.52/5.95 fail32 [67, 2] (w:1, o:84, a:1, s:1, b:0),
% 5.52/5.95 mulNat [68, 2] (w:1, o:87, a:1, s:1, b:0),
% 5.52/5.95 fail22 [72, 2] (w:1, o:83, a:1, s:1, b:0),
% 5.52/5.95 fail12 [74, 2] (w:1, o:79, a:1, s:1, b:0),
% 5.52/5.95 fail3 [76, 2] (w:1, o:85, a:1, s:1, b:0),
% 5.52/5.95 impl [78, 2] (w:1, o:88, a:1, s:1, b:0),
% 5.52/5.95 d [79, 1] (w:1, o:46, a:1, s:1, b:0),
% 5.52/5.95 prop1 [87, 1] (w:1, o:47, a:1, s:1, b:0),
% 5.52/5.95 eq3 [88, 2] (w:1, o:76, a:1, s:1, b:0),
% 5.52/5.95 eq [89, 2] (w:1, o:77, a:1, s:1, b:0).
% 5.52/5.95
% 5.52/5.95
% 5.52/5.95 Starting Search:
% 5.52/5.95
% 5.52/5.95 Resimplifying inuse:
% 5.52/5.95 Done
% 5.52/5.95
% 5.52/5.95
% 5.52/5.95 Intermediate Status:
% 5.52/5.95 Generated: 5563
% 5.52/5.95 Kept: 2047
% 5.52/5.95 Inuse: 330
% 5.52/5.95 Deleted: 101
% 5.52/5.95 Deletedinuse: 10
% 5.52/5.95
% 5.52/5.95 Resimplifying inuse:
% 5.52/5.95 Done
% 5.52/5.95
% 5.52/5.95 Resimplifying inuse:
% 5.52/5.95 Done
% 5.52/5.95
% 5.52/5.95
% 5.52/5.95 Intermediate Status:
% 5.52/5.95 Generated: 11592
% 5.52/5.95 Kept: 4063
% 5.52/5.95 Inuse: 565
% 5.52/5.95 Deleted: 139
% 5.52/5.95 Deletedinuse: 14
% 5.52/5.95
% 5.52/5.95 Resimplifying inuse:
% 5.52/5.95 Done
% 5.52/5.95
% 5.52/5.95 Resimplifying inuse:
% 5.52/5.95 Done
% 5.52/5.95
% 5.52/5.95
% 5.52/5.95 Intermediate Status:
% 5.52/5.95 Generated: 17323
% 5.52/5.95 Kept: 6067
% 5.52/5.95 Inuse: 763
% 5.52/5.95 Deleted: 171
% 5.52/5.95 Deletedinuse: 14
% 5.52/5.95
% 5.52/5.95 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 22489
% 18.33/18.75 Kept: 8098
% 18.33/18.75 Inuse: 909
% 18.33/18.75 Deleted: 222
% 18.33/18.75 Deletedinuse: 18
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 28567
% 18.33/18.75 Kept: 10148
% 18.33/18.75 Inuse: 1039
% 18.33/18.75 Deleted: 230
% 18.33/18.75 Deletedinuse: 18
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 34180
% 18.33/18.75 Kept: 12156
% 18.33/18.75 Inuse: 1140
% 18.33/18.75 Deleted: 242
% 18.33/18.75 Deletedinuse: 24
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 43735
% 18.33/18.75 Kept: 14279
% 18.33/18.75 Inuse: 1312
% 18.33/18.75 Deleted: 253
% 18.33/18.75 Deletedinuse: 24
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 58062
% 18.33/18.75 Kept: 16292
% 18.33/18.75 Inuse: 1538
% 18.33/18.75 Deleted: 297
% 18.33/18.75 Deletedinuse: 26
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 64470
% 18.33/18.75 Kept: 18300
% 18.33/18.75 Inuse: 1652
% 18.33/18.75 Deleted: 330
% 18.33/18.75 Deletedinuse: 29
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying clauses:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 70343
% 18.33/18.75 Kept: 20312
% 18.33/18.75 Inuse: 1773
% 18.33/18.75 Deleted: 2918
% 18.33/18.75 Deletedinuse: 29
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 111810
% 18.33/18.75 Kept: 22320
% 18.33/18.75 Inuse: 1920
% 18.33/18.75 Deleted: 2958
% 18.33/18.75 Deletedinuse: 61
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 123443
% 18.33/18.75 Kept: 24330
% 18.33/18.75 Inuse: 2117
% 18.33/18.75 Deleted: 2964
% 18.33/18.75 Deletedinuse: 62
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 142891
% 18.33/18.75 Kept: 26340
% 18.33/18.75 Inuse: 2294
% 18.33/18.75 Deleted: 2979
% 18.33/18.75 Deletedinuse: 65
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 179098
% 18.33/18.75 Kept: 28344
% 18.33/18.75 Inuse: 2402
% 18.33/18.75 Deleted: 2992
% 18.33/18.75 Deletedinuse: 66
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 193736
% 18.33/18.75 Kept: 30344
% 18.33/18.75 Inuse: 2563
% 18.33/18.75 Deleted: 3010
% 18.33/18.75 Deletedinuse: 68
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 204504
% 18.33/18.75 Kept: 32381
% 18.33/18.75 Inuse: 2649
% 18.33/18.75 Deleted: 3014
% 18.33/18.75 Deletedinuse: 72
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 211309
% 18.33/18.75 Kept: 34383
% 18.33/18.75 Inuse: 2706
% 18.33/18.75 Deleted: 3020
% 18.33/18.75 Deletedinuse: 72
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 223160
% 18.33/18.75 Kept: 36388
% 18.33/18.75 Inuse: 2809
% 18.33/18.75 Deleted: 3022
% 18.33/18.75 Deletedinuse: 74
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 238604
% 18.33/18.75 Kept: 38404
% 18.33/18.75 Inuse: 2961
% 18.33/18.75 Deleted: 3022
% 18.33/18.75 Deletedinuse: 74
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying clauses:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 243125
% 18.33/18.75 Kept: 40451
% 18.33/18.75 Inuse: 2981
% 18.33/18.75 Deleted: 5479
% 18.33/18.75 Deletedinuse: 78
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 257188
% 18.33/18.75 Kept: 42466
% 18.33/18.75 Inuse: 3143
% 18.33/18.75 Deleted: 5484
% 18.33/18.75 Deletedinuse: 78
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 273058
% 18.33/18.75 Kept: 44473
% 18.33/18.75 Inuse: 3302
% 18.33/18.75 Deleted: 5489
% 18.33/18.75 Deletedinuse: 82
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 284326
% 18.33/18.75 Kept: 46887
% 18.33/18.75 Inuse: 3410
% 18.33/18.75 Deleted: 5494
% 18.33/18.75 Deletedinuse: 82
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 303673
% 18.33/18.75 Kept: 48887
% 18.33/18.75 Inuse: 3614
% 18.33/18.75 Deleted: 5495
% 18.33/18.75 Deletedinuse: 82
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 312656
% 18.33/18.75 Kept: 50893
% 18.33/18.75 Inuse: 3712
% 18.33/18.75 Deleted: 5500
% 18.33/18.75 Deletedinuse: 84
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 324264
% 18.33/18.75 Kept: 52894
% 18.33/18.75 Inuse: 3841
% 18.33/18.75 Deleted: 5500
% 18.33/18.75 Deletedinuse: 84
% 18.33/18.75
% 18.33/18.75 Resimplifying inuse:
% 18.33/18.75 Done
% 18.33/18.75
% 18.33/18.75
% 18.33/18.75 Intermediate Status:
% 18.33/18.75 Generated: 337465
% 18.33/18.75 Kept: 54904
% 51.12/51.51 Inuse: 3993
% 51.12/51.51 Deleted: 5505
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 347323
% 51.12/51.51 Kept: 56907
% 51.12/51.51 Inuse: 4085
% 51.12/51.51 Deleted: 5509
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 355188
% 51.12/51.51 Kept: 58919
% 51.12/51.51 Inuse: 4147
% 51.12/51.51 Deleted: 5511
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying clauses:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 364466
% 51.12/51.51 Kept: 60946
% 51.12/51.51 Inuse: 4224
% 51.12/51.51 Deleted: 7356
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 376294
% 51.12/51.51 Kept: 62954
% 51.12/51.51 Inuse: 4333
% 51.12/51.51 Deleted: 7357
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 390137
% 51.12/51.51 Kept: 64959
% 51.12/51.51 Inuse: 4470
% 51.12/51.51 Deleted: 7357
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 408678
% 51.12/51.51 Kept: 66975
% 51.12/51.51 Inuse: 4674
% 51.12/51.51 Deleted: 7359
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 419957
% 51.12/51.51 Kept: 69010
% 51.12/51.51 Inuse: 4786
% 51.12/51.51 Deleted: 7359
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 427282
% 51.12/51.51 Kept: 71015
% 51.12/51.51 Inuse: 4839
% 51.12/51.51 Deleted: 7359
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 441704
% 51.12/51.51 Kept: 73031
% 51.12/51.51 Inuse: 4981
% 51.12/51.51 Deleted: 7359
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 457739
% 51.12/51.51 Kept: 75038
% 51.12/51.51 Inuse: 5160
% 51.12/51.51 Deleted: 7365
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 473834
% 51.12/51.51 Kept: 77072
% 51.12/51.51 Inuse: 5347
% 51.12/51.51 Deleted: 7367
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 488902
% 51.12/51.51 Kept: 79079
% 51.12/51.51 Inuse: 5529
% 51.12/51.51 Deleted: 7374
% 51.12/51.51 Deletedinuse: 84
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying clauses:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 506487
% 51.12/51.51 Kept: 81114
% 51.12/51.51 Inuse: 5735
% 51.12/51.51 Deleted: 8865
% 51.12/51.51 Deletedinuse: 92
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 528047
% 51.12/51.51 Kept: 83333
% 51.12/51.51 Inuse: 5951
% 51.12/51.51 Deleted: 8865
% 51.12/51.51 Deletedinuse: 92
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 553697
% 51.12/51.51 Kept: 85336
% 51.12/51.51 Inuse: 6198
% 51.12/51.51 Deleted: 8865
% 51.12/51.51 Deletedinuse: 92
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 589720
% 51.12/51.51 Kept: 87342
% 51.12/51.51 Inuse: 6624
% 51.12/51.51 Deleted: 8888
% 51.12/51.51 Deletedinuse: 101
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 599849
% 51.12/51.51 Kept: 89350
% 51.12/51.51 Inuse: 6724
% 51.12/51.51 Deleted: 8905
% 51.12/51.51 Deletedinuse: 103
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 612122
% 51.12/51.51 Kept: 91350
% 51.12/51.51 Inuse: 6846
% 51.12/51.51 Deleted: 8914
% 51.12/51.51 Deletedinuse: 103
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 622362
% 51.12/51.51 Kept: 94377
% 51.12/51.51 Inuse: 6928
% 51.12/51.51 Deleted: 8914
% 51.12/51.51 Deletedinuse: 103
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 637996
% 51.12/51.51 Kept: 96380
% 51.12/51.51 Inuse: 7097
% 51.12/51.51 Deleted: 8914
% 51.12/51.51 Deletedinuse: 103
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 653811
% 51.12/51.51 Kept: 98393
% 51.12/51.51 Inuse: 7252
% 51.12/51.51 Deleted: 8922
% 51.12/51.51 Deletedinuse: 103
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 674318
% 51.12/51.51 Kept: 100416
% 51.12/51.51 Inuse: 7435
% 51.12/51.51 Deleted: 8956
% 51.12/51.51 Deletedinuse: 103
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying clauses:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51 Resimplifying inuse:
% 51.12/51.51 Done
% 51.12/51.51
% 51.12/51.51
% 51.12/51.51 Intermediate Status:
% 51.12/51.51 Generated: 689149
% 51.12/51.51 Kept: 102417
% 51.12/51.51 Inuse: 7563
% 51.12/51.51 Deleted: 11343
% 51.12/51.51 Deletedinuse: 103
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 711763
% 163.73/164.16 Kept: 104422
% 163.73/164.16 Inuse: 7765
% 163.73/164.16 Deleted: 11343
% 163.73/164.16 Deletedinuse: 103
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 739092
% 163.73/164.16 Kept: 106892
% 163.73/164.16 Inuse: 8038
% 163.73/164.16 Deleted: 11351
% 163.73/164.16 Deletedinuse: 103
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 786714
% 163.73/164.16 Kept: 108939
% 163.73/164.16 Inuse: 8379
% 163.73/164.16 Deleted: 11364
% 163.73/164.16 Deletedinuse: 110
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 800019
% 163.73/164.16 Kept: 110965
% 163.73/164.16 Inuse: 8485
% 163.73/164.16 Deleted: 11372
% 163.73/164.16 Deletedinuse: 110
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 809981
% 163.73/164.16 Kept: 113319
% 163.73/164.16 Inuse: 8562
% 163.73/164.16 Deleted: 11374
% 163.73/164.16 Deletedinuse: 110
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 822240
% 163.73/164.16 Kept: 116440
% 163.73/164.16 Inuse: 8673
% 163.73/164.16 Deleted: 11402
% 163.73/164.16 Deletedinuse: 116
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 836242
% 163.73/164.16 Kept: 118442
% 163.73/164.16 Inuse: 8834
% 163.73/164.16 Deleted: 11431
% 163.73/164.16 Deletedinuse: 145
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 843990
% 163.73/164.16 Kept: 121436
% 163.73/164.16 Inuse: 8869
% 163.73/164.16 Deleted: 11435
% 163.73/164.16 Deletedinuse: 149
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying clauses:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 848762
% 163.73/164.16 Kept: 123465
% 163.73/164.16 Inuse: 8876
% 163.73/164.16 Deleted: 14096
% 163.73/164.16 Deletedinuse: 175
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 858573
% 163.73/164.16 Kept: 125474
% 163.73/164.16 Inuse: 8952
% 163.73/164.16 Deleted: 14098
% 163.73/164.16 Deletedinuse: 175
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 886828
% 163.73/164.16 Kept: 127488
% 163.73/164.16 Inuse: 9153
% 163.73/164.16 Deleted: 14134
% 163.73/164.16 Deletedinuse: 203
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 916879
% 163.73/164.16 Kept: 130106
% 163.73/164.16 Inuse: 9325
% 163.73/164.16 Deleted: 14134
% 163.73/164.16 Deletedinuse: 203
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 950844
% 163.73/164.16 Kept: 132114
% 163.73/164.16 Inuse: 9599
% 163.73/164.16 Deleted: 14138
% 163.73/164.16 Deletedinuse: 203
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 977001
% 163.73/164.16 Kept: 134122
% 163.73/164.16 Inuse: 9836
% 163.73/164.16 Deleted: 14138
% 163.73/164.16 Deletedinuse: 203
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 992590
% 163.73/164.16 Kept: 136122
% 163.73/164.16 Inuse: 9955
% 163.73/164.16 Deleted: 14142
% 163.73/164.16 Deletedinuse: 203
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 1049815
% 163.73/164.16 Kept: 140521
% 163.73/164.16 Inuse: 10127
% 163.73/164.16 Deleted: 14158
% 163.73/164.16 Deletedinuse: 211
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying clauses:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 1097464
% 163.73/164.16 Kept: 142522
% 163.73/164.16 Inuse: 10526
% 163.73/164.16 Deleted: 16225
% 163.73/164.16 Deletedinuse: 211
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 1111787
% 163.73/164.16 Kept: 146208
% 163.73/164.16 Inuse: 10608
% 163.73/164.16 Deleted: 16233
% 163.73/164.16 Deletedinuse: 219
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 1138200
% 163.73/164.16 Kept: 149925
% 163.73/164.16 Inuse: 10740
% 163.73/164.16 Deleted: 16291
% 163.73/164.16 Deletedinuse: 277
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 1168063
% 163.73/164.16 Kept: 151933
% 163.73/164.16 Inuse: 10963
% 163.73/164.16 Deleted: 16303
% 163.73/164.16 Deletedinuse: 283
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 1189059
% 163.73/164.16 Kept: 153966
% 163.73/164.16 Inuse: 11114
% 163.73/164.16 Deleted: 16316
% 163.73/164.16 Deletedinuse: 291
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 1212939
% 163.73/164.16 Kept: 155984
% 163.73/164.16 Inuse: 11270
% 163.73/164.16 Deleted: 16332
% 163.73/164.16 Deletedinuse: 303
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16 Resimplifying inuse:
% 163.73/164.16 Done
% 163.73/164.16
% 163.73/164.16
% 163.73/164.16 Intermediate Status:
% 163.73/164.16 Generated: 1249622
% 163.73/164.16 Kept: 157987
% 163.73/164.16 Inuse: 11520
% 163.73/164.16 Deleted: 16355
% 163.73/164.16 DeleTerminated
% 299.50/300.03 Bliksem ended
%------------------------------------------------------------------------------