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