%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX227-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.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:51 PM UTC 2026
% Result : Timeout 299.65s 300.04s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX227-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n017.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 12:51:57 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.70/1.53 *** allocated 10000 integers for termspace/termends
% 0.70/1.53 *** allocated 10000 integers for clauses
% 0.70/1.53 *** allocated 10000 integers for justifications
% 0.70/1.53 Bliksem 1.12
% 0.70/1.53
% 0.70/1.53
% 0.70/1.53 Automatic Strategy Selection
% 0.70/1.53
% 0.70/1.53 Clauses:
% 0.70/1.53 [
% 0.70/1.53 [ =( aux( X, Y, nothing ), nothing ) ],
% 0.70/1.53 [ =( aux( X, Y, just( Z ) ), astep( Y, Z ) ) ],
% 0.70/1.53 [ =( fail( X, Y ), par( X, Y, step( X ), step( Y ) ) ) ],
% 0.70/1.53 [ =( par( X, Y, nothing, nothing ), nothing ) ],
% 0.70/1.53 [ =( par( X, Y, nothing, just( Z ) ), just( x( X, Z ) ) ) ],
% 0.70/1.53 [ =( par( X, Y, just( Z ), nothing ), just( x( Z, Y ) ) ) ],
% 0.70/1.53 [ =( par( X, Y, just( Z ), just( T ) ), just( x( Z, T ) ) ) ],
% 0.70/1.53 [ =( step( x( x( x( s, X ), Y ), Z ) ), just( x( x( X, Z ), x( Y, Z ) )
% 0.70/1.53 ) ) ],
% 0.70/1.53 [ =( step( x( x( x( b, X ), Y ), Z ) ), just( x( X, x( Y, Z ) ) ) ) ]
% 0.70/1.53 ,
% 0.70/1.53 [ =( step( x( x( x( c, X ), Y ), Z ) ), just( x( x( X, Z ), Y ) ) ) ]
% 0.70/1.53 ,
% 0.70/1.53 [ =( step( x( x( x( x( X, Y ), Z ), T ), U ) ), fail( x( x( x( X, Y ), Z
% 0.70/1.53 ), T ), U ) ) ],
% 0.70/1.53 [ =( step( x( x( x( theVar, X ), Y ), Z ) ), fail( x( x( theVar, X ), Y
% 0.70/1.53 ), Z ) ) ],
% 0.70/1.53 [ =( step( x( x( x( k, X ), Y ), Z ) ), fail( x( x( k, X ), Y ), Z ) ) ]
% 0.70/1.53 ,
% 0.70/1.53 [ =( step( x( x( x( i, X ), Y ), Z ) ), fail( x( x( i, X ), Y ), Z ) ) ]
% 0.70/1.53 ,
% 0.70/1.53 [ =( step( x( x( k, X ), Y ) ), just( X ) ) ],
% 0.70/1.53 [ =( step( x( x( theVar, X ), Y ) ), fail( x( theVar, X ), Y ) ) ],
% 0.70/1.53 [ =( step( x( x( i, X ), Y ) ), fail( x( i, X ), Y ) ) ],
% 0.70/1.53 [ =( step( x( x( s, X ), Y ) ), fail( x( s, X ), Y ) ) ],
% 0.70/1.53 [ =( step( x( x( b, X ), Y ) ), fail( x( b, X ), Y ) ) ],
% 0.70/1.53 [ =( step( x( x( c, X ), Y ) ), fail( x( c, X ), Y ) ) ],
% 0.70/1.53 [ =( step( x( i, X ) ), just( X ) ) ],
% 0.70/1.53 [ =( step( x( theVar, X ) ), fail( theVar, X ) ) ],
% 0.70/1.53 [ =( step( x( k, X ) ), fail( k, X ) ) ],
% 0.70/1.53 [ =( step( x( s, X ) ), fail( s, X ) ) ],
% 0.70/1.53 [ =( step( x( b, X ) ), fail( b, X ) ) ],
% 0.70/1.53 [ =( step( x( c, X ) ), fail( c, X ) ) ],
% 0.70/1.53 [ =( step( theVar ), nothing ) ],
% 0.70/1.53 [ =( step( k ), nothing ) ],
% 0.70/1.53 [ =( step( i ), nothing ) ],
% 0.70/1.53 [ =( step( s ), nothing ) ],
% 0.70/1.53 [ =( step( b ), nothing ) ],
% 0.70/1.53 [ =( step( c ), nothing ) ],
% 0.70/1.53 [ =( orb( btrue, X ), btrue ) ],
% 0.70/1.53 [ =( orb( bfalse, X ), X ) ],
% 0.70/1.53 [ =( impl( btrue, X ), X ) ],
% 0.70/1.53 [ =( impl( bfalse, X ), btrue ) ],
% 0.70/1.53 [ =( cheating( x( X, Y ) ), orb( cheating( X ), cheating( Y ) ) ) ],
% 0.70/1.53 [ =( cheating( theVar ), btrue ) ],
% 0.70/1.53 [ =( cheating( k ), bfalse ) ],
% 0.70/1.53 [ =( cheating( i ), bfalse ) ],
% 0.70/1.53 [ =( cheating( s ), bfalse ) ],
% 0.70/1.53 [ =( cheating( b ), bfalse ) ],
% 0.70/1.53 [ =( cheating( c ), bfalse ) ],
% 0.70/1.53 [ =( astep( suc( X ), Y ), aux( Y, X, step( Y ) ) ) ],
% 0.70/1.53 [ =( astep( z, X ), just( X ) ) ],
% 0.70/1.53 [ =( 'thm_why_easy_small'( X ), impl( eq3( astep( suc( suc( suc( suc( z
% 0.70/1.53 ) ) ) ), x( X, theVar ) ), just( x( theVar, x( X, theVar ) ) ) ), eq4(
% 0.70/1.53 cheating( X ), btrue ) ) ) ],
% 0.70/1.53 [ =( eq( theVar, k ), bfalse ) ],
% 0.70/1.53 [ =( eq( theVar, i ), bfalse ) ],
% 0.70/1.53 [ =( eq( theVar, s ), bfalse ) ],
% 0.70/1.53 [ =( eq( theVar, b ), bfalse ) ],
% 0.70/1.53 [ =( eq( theVar, c ), bfalse ) ],
% 0.70/1.53 [ =( eq( k, theVar ), bfalse ) ],
% 0.70/1.53 [ =( eq( k, i ), bfalse ) ],
% 0.70/1.53 [ =( eq( k, s ), bfalse ) ],
% 0.70/1.53 [ =( eq( k, b ), bfalse ) ],
% 0.70/1.53 [ =( eq( k, c ), bfalse ) ],
% 0.70/1.53 [ =( eq( i, theVar ), bfalse ) ],
% 0.70/1.53 [ =( eq( i, k ), bfalse ) ],
% 0.70/1.53 [ =( eq( i, s ), bfalse ) ],
% 0.70/1.53 [ =( eq( i, b ), bfalse ) ],
% 0.70/1.53 [ =( eq( i, c ), bfalse ) ],
% 0.70/1.53 [ =( eq( s, theVar ), bfalse ) ],
% 0.70/1.53 [ =( eq( s, k ), bfalse ) ],
% 0.70/1.53 [ =( eq( s, i ), bfalse ) ],
% 0.70/1.53 [ =( eq( s, b ), bfalse ) ],
% 0.70/1.53 [ =( eq( s, c ), bfalse ) ],
% 0.70/1.53 [ =( eq( b, theVar ), bfalse ) ],
% 0.70/1.53 [ =( eq( b, k ), bfalse ) ],
% 0.70/1.53 [ =( eq( b, i ), bfalse ) ],
% 0.70/1.53 [ =( eq( b, s ), bfalse ) ],
% 0.70/1.53 [ =( eq( b, c ), bfalse ) ],
% 0.70/1.53 [ =( eq( c, theVar ), bfalse ) ],
% 0.70/1.53 [ =( eq( c, k ), bfalse ) ],
% 0.70/1.53 [ =( eq( c, i ), bfalse ) ],
% 0.70/1.53 [ =( eq( c, s ), bfalse ) ],
% 0.70/1.53 [ =( eq( c, b ), bfalse ) ],
% 0.70/1.53 [ =( eq4( bfalse, btrue ), bfalse ) ],
% 0.70/1.53 [ =( eq4( btrue, bfalse ), bfalse ) ],
% 0.70/1.53 [ ~( =( eq( X, Y ), bfalse ) ), =( eq( x( X, Z ), x( Y, T ) ), bfalse )
% 0.70/1.53 ],
% 0.70/1.53 [ ~( =( eq( X, Y ), btrue ) ), =( eq( x( X, Z ), x( Y, T ) ), eq( Z, T )
% 0.70/1.53 ) ],
% 0.70/1.53 [ =( eq( x( X, Y ), theVar ), bfalse ) ],
% 0.70/1.53 [ =( eq( x( X, Y ), k ), bfalse ) ],
% 0.70/1.53 [ =( eq( x( X, Y ), i ), bfalse ) ],
% 12.83/13.25 [ =( eq( x( X, Y ), s ), bfalse ) ],
% 12.83/13.25 [ =( eq( x( X, Y ), b ), bfalse ) ],
% 12.83/13.25 [ =( eq( x( X, Y ), c ), bfalse ) ],
% 12.83/13.25 [ =( eq( theVar, x( X, Y ) ), bfalse ) ],
% 12.83/13.25 [ =( eq( k, x( X, Y ) ), bfalse ) ],
% 12.83/13.25 [ =( eq( i, x( X, Y ) ), bfalse ) ],
% 12.83/13.25 [ =( eq( s, x( X, Y ) ), bfalse ) ],
% 12.83/13.25 [ =( eq( b, x( X, Y ) ), bfalse ) ],
% 12.83/13.25 [ =( eq( c, x( X, Y ) ), bfalse ) ],
% 12.83/13.25 [ =( eq2( suc( X ), suc( Y ) ), eq2( X, Y ) ) ],
% 12.83/13.25 [ =( eq2( suc( X ), z ), bfalse ) ],
% 12.83/13.25 [ =( eq2( z, suc( X ) ), bfalse ) ],
% 12.83/13.25 [ =( eq( X, X ), btrue ) ],
% 12.83/13.25 [ =( eq2( X, X ), btrue ) ],
% 12.83/13.25 [ =( eq3( X, X ), btrue ) ],
% 12.83/13.25 [ =( eq4( X, X ), btrue ) ],
% 12.83/13.25 [ =( eq3( just( X ), just( Y ) ), eq( X, Y ) ) ],
% 12.83/13.25 [ =( eq3( nothing, just( X ) ), bfalse ) ],
% 12.83/13.25 [ =( eq3( just( X ), nothing ), bfalse ) ],
% 12.83/13.25 [ ~( =( eq4( 'thm_why_easy_small'( X ), bfalse ), btrue ) ) ]
% 12.83/13.25 ] .
% 12.83/13.25
% 12.83/13.25
% 12.83/13.25 percentage equality = 1.000000, percentage horn = 1.000000
% 12.83/13.25 This is a pure equality problem
% 12.83/13.25
% 12.83/13.25
% 12.83/13.25
% 12.83/13.25 Options Used:
% 12.83/13.25
% 12.83/13.25 useres = 1
% 12.83/13.25 useparamod = 1
% 12.83/13.25 useeqrefl = 1
% 12.83/13.25 useeqfact = 1
% 12.83/13.25 usefactor = 1
% 12.83/13.25 usesimpsplitting = 0
% 12.83/13.25 usesimpdemod = 5
% 12.83/13.25 usesimpres = 3
% 12.83/13.25
% 12.83/13.25 resimpinuse = 1000
% 12.83/13.25 resimpclauses = 20000
% 12.83/13.25 substype = eqrewr
% 12.83/13.25 backwardsubs = 1
% 12.83/13.25 selectoldest = 5
% 12.83/13.25
% 12.83/13.25 litorderings [0] = split
% 12.83/13.25 litorderings [1] = extend the termordering, first sorting on arguments
% 12.83/13.25
% 12.83/13.25 termordering = kbo
% 12.83/13.25
% 12.83/13.25 litapriori = 0
% 12.83/13.25 termapriori = 1
% 12.83/13.25 litaposteriori = 0
% 12.83/13.25 termaposteriori = 0
% 12.83/13.25 demodaposteriori = 0
% 12.83/13.25 ordereqreflfact = 0
% 12.83/13.25
% 12.83/13.25 litselect = negord
% 12.83/13.25
% 12.83/13.25 maxweight = 15
% 12.83/13.25 maxdepth = 30000
% 12.83/13.25 maxlength = 115
% 12.83/13.25 maxnrvars = 195
% 12.83/13.25 excuselevel = 1
% 12.83/13.25 increasemaxweight = 1
% 12.83/13.25
% 12.83/13.25 maxselected = 10000000
% 12.83/13.25 maxnrclauses = 10000000
% 12.83/13.25
% 12.83/13.25 showgenerated = 0
% 12.83/13.25 showkept = 0
% 12.83/13.25 showselected = 0
% 12.83/13.25 showdeleted = 0
% 12.83/13.25 showresimp = 1
% 12.83/13.25 showstatus = 2000
% 12.83/13.25
% 12.83/13.25 prologoutput = 1
% 12.83/13.25 nrgoals = 5000000
% 12.83/13.25 totalproof = 1
% 12.83/13.25
% 12.83/13.25 Symbols occurring in the translation:
% 12.83/13.25
% 12.83/13.25 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 12.83/13.25 . [1, 2] (w:1, o:43, a:1, s:1, b:0),
% 12.83/13.25 ! [4, 1] (w:0, o:33, a:1, s:1, b:0),
% 12.83/13.25 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 12.83/13.25 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 12.83/13.25 nothing [41, 0] (w:1, o:14, a:1, s:1, b:0),
% 12.83/13.25 aux [42, 3] (w:1, o:77, a:1, s:1, b:0),
% 12.83/13.25 just [44, 1] (w:1, o:38, a:1, s:1, b:0),
% 12.83/13.25 astep [45, 2] (w:1, o:68, a:1, s:1, b:0),
% 12.83/13.25 fail [47, 2] (w:1, o:73, a:1, s:1, b:0),
% 12.83/13.25 step [48, 1] (w:1, o:39, a:1, s:1, b:0),
% 12.83/13.25 par [49, 4] (w:1, o:78, a:1, s:1, b:0),
% 12.83/13.25 x [52, 2] (w:1, o:74, a:1, s:1, b:0),
% 12.83/13.25 s [55, 0] (w:1, o:5, a:1, s:1, b:0),
% 12.83/13.25 b [58, 0] (w:1, o:22, a:1, s:1, b:0),
% 12.83/13.25 c [59, 0] (w:1, o:25, a:1, s:1, b:0),
% 12.83/13.25 theVar [61, 0] (w:1, o:26, a:1, s:1, b:0),
% 12.83/13.25 k [62, 0] (w:1, o:27, a:1, s:1, b:0),
% 12.83/13.25 i [63, 0] (w:1, o:28, a:1, s:1, b:0),
% 12.83/13.25 btrue [64, 0] (w:1, o:23, a:1, s:1, b:0),
% 12.83/13.25 orb [66, 2] (w:1, o:75, a:1, s:1, b:0),
% 12.83/13.25 bfalse [67, 0] (w:1, o:24, a:1, s:1, b:0),
% 12.83/13.25 impl [68, 2] (w:1, o:76, a:1, s:1, b:0),
% 12.83/13.25 cheating [71, 1] (w:1, o:40, a:1, s:1, b:0),
% 12.83/13.25 suc [72, 1] (w:1, o:41, a:1, s:1, b:0),
% 12.83/13.25 z [73, 0] (w:1, o:32, a:1, s:1, b:0),
% 12.83/13.25 'thm_why_easy_small' [74, 1] (w:1, o:42, a:1, s:1, b:0),
% 12.83/13.25 eq3 [75, 2] (w:1, o:70, a:1, s:1, b:0),
% 12.83/13.25 eq4 [76, 2] (w:1, o:71, a:1, s:1, b:0),
% 12.83/13.25 eq [77, 2] (w:1, o:72, a:1, s:1, b:0),
% 12.83/13.25 eq2 [78, 2] (w:1, o:69, a:1, s:1, b:0).
% 12.83/13.25
% 12.83/13.25
% 12.83/13.25 Starting Search:
% 12.83/13.25
% 12.83/13.25 Resimplifying inuse:
% 12.83/13.25 Done
% 12.83/13.25
% 12.83/13.25
% 12.83/13.25 Intermediate Status:
% 12.83/13.25 Generated: 8836
% 12.83/13.25 Kept: 2001
% 12.83/13.25 Inuse: 744
% 12.83/13.25 Deleted: 18
% 12.83/13.25 Deletedinuse: 1
% 12.83/13.25
% 12.83/13.25 Resimplifying inuse:
% 12.83/13.25 Done
% 12.83/13.25
% 12.83/13.25 Resimplifying inuse:
% 12.83/13.25 Done
% 12.83/13.25
% 12.83/13.25
% 12.83/13.25 Intermediate Status:
% 12.83/13.25 Generated: 13441
% 12.83/13.25 Kept: 4009
% 12.83/13.25 Inuse: 1067
% 12.83/13.25 Deleted: 38
% 12.83/13.25 Deletedinuse: 1
% 12.83/13.25
% 12.83/13.25 Resimplifying inuse:
% 12.83/13.25 Done
% 12.83/13.25
% 12.83/13.25 Resimplifying inuse:
% 12.83/13.25 Done
% 12.83/13.25
% 12.83/13.25
% 12.83/13.25 Intermediate Status:
% 12.83/13.25 Generated: 19333
% 12.83/13.25 Kept: 6018
% 12.83/13.25 Inuse: 1560
% 12.83/13.25 Deleted: 42
% 12.83/13.25 Deletedinuse: 1
% 12.83/13.25
% 12.83/13.25 Resimplifying inuse:
% 12.83/13.25 Done
% 12.83/13.25
% 12.83/13.25 Resimplifying inuse:
% 12.83/13.25 Done
% 12.83/13.25
% 12.83/13.25
% 12.83/13.25 Intermediate Status:
% 12.83/13.25 Generated: 22214
% 12.83/13.25 Kept: 8026
% 12.83/13.25 Inuse: 1778
% 12.83/13.25 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 25657
% 56.22/56.65 Kept: 10036
% 56.22/56.65 Inuse: 2162
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 28958
% 56.22/56.65 Kept: 12043
% 56.22/56.65 Inuse: 2512
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 32995
% 56.22/56.65 Kept: 14050
% 56.22/56.65 Inuse: 3182
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 36394
% 56.22/56.65 Kept: 16062
% 56.22/56.65 Inuse: 3572
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 39592
% 56.22/56.65 Kept: 18073
% 56.22/56.65 Inuse: 3943
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying clauses:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 42902
% 56.22/56.65 Kept: 20078
% 56.22/56.65 Inuse: 4295
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 46167
% 56.22/56.65 Kept: 22080
% 56.22/56.65 Inuse: 4653
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 49432
% 56.22/56.65 Kept: 24088
% 56.22/56.65 Inuse: 5014
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 52681
% 56.22/56.65 Kept: 26094
% 56.22/56.65 Inuse: 5370
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 55909
% 56.22/56.65 Kept: 28094
% 56.22/56.65 Inuse: 5724
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 59128
% 56.22/56.65 Kept: 30099
% 56.22/56.65 Inuse: 6078
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 62367
% 56.22/56.65 Kept: 32108
% 56.22/56.65 Inuse: 6436
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 65658
% 56.22/56.65 Kept: 34111
% 56.22/56.65 Inuse: 6781
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 68991
% 56.22/56.65 Kept: 36123
% 56.22/56.65 Inuse: 7134
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 72276
% 56.22/56.65 Kept: 38125
% 56.22/56.65 Inuse: 7490
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying clauses:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 75574
% 56.22/56.65 Kept: 40132
% 56.22/56.65 Inuse: 7845
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 78871
% 56.22/56.65 Kept: 42132
% 56.22/56.65 Inuse: 8198
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 82159
% 56.22/56.65 Kept: 44135
% 56.22/56.65 Inuse: 8554
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 85452
% 56.22/56.65 Kept: 46140
% 56.22/56.65 Inuse: 8908
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 88800
% 56.22/56.65 Kept: 48152
% 56.22/56.65 Inuse: 9264
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 92120
% 56.22/56.65 Kept: 50156
% 56.22/56.65 Inuse: 9618
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 95470
% 56.22/56.65 Kept: 52168
% 56.22/56.65 Inuse: 9975
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 98783
% 56.22/56.65 Kept: 54176
% 56.22/56.65 Inuse: 10333
% 56.22/56.65 Deleted: 42
% 56.22/56.65 Deletedinuse: 1
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65 Resimplifying inuse:
% 56.22/56.65 Done
% 56.22/56.65
% 56.22/56.65
% 56.22/56.65 Intermediate Status:
% 56.22/56.65 Generated: 102109
% 56.22/56.65 Kept: 56182
% 56.22/56.65 Inuse: 10687
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 105439
% 141.11/141.59 Kept: 58194
% 141.11/141.59 Inuse: 11046
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying clauses:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 108747
% 141.11/141.59 Kept: 60194
% 141.11/141.59 Inuse: 11400
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 112049
% 141.11/141.59 Kept: 62194
% 141.11/141.59 Inuse: 11754
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 115363
% 141.11/141.59 Kept: 64194
% 141.11/141.59 Inuse: 12111
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 121108
% 141.11/141.59 Kept: 66202
% 141.11/141.59 Inuse: 13625
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 125241
% 141.11/141.59 Kept: 68213
% 141.11/141.59 Inuse: 14201
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 129045
% 141.11/141.59 Kept: 70217
% 141.11/141.59 Inuse: 14606
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 132857
% 141.11/141.59 Kept: 72221
% 141.11/141.59 Inuse: 15015
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 136675
% 141.11/141.59 Kept: 74226
% 141.11/141.59 Inuse: 15429
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 140491
% 141.11/141.59 Kept: 76230
% 141.11/141.59 Inuse: 15837
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 144259
% 141.11/141.59 Kept: 78234
% 141.11/141.59 Inuse: 16242
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying clauses:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 148054
% 141.11/141.59 Kept: 80238
% 141.11/141.59 Inuse: 16650
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 151872
% 141.11/141.59 Kept: 82242
% 141.11/141.59 Inuse: 17059
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 155677
% 141.11/141.59 Kept: 84247
% 141.11/141.59 Inuse: 17471
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 159491
% 141.11/141.59 Kept: 86251
% 141.11/141.59 Inuse: 17878
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 163285
% 141.11/141.59 Kept: 88255
% 141.11/141.59 Inuse: 18290
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 167105
% 141.11/141.59 Kept: 90260
% 141.11/141.59 Inuse: 18702
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 170909
% 141.11/141.59 Kept: 92265
% 141.11/141.59 Inuse: 19115
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 174746
% 141.11/141.59 Kept: 94269
% 141.11/141.59 Inuse: 19523
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 178556
% 141.11/141.59 Kept: 96274
% 141.11/141.59 Inuse: 19939
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 182370
% 141.11/141.59 Kept: 98279
% 141.11/141.59 Inuse: 20351
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying clauses:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 186164
% 141.11/141.59 Kept: 100284
% 141.11/141.59 Inuse: 20762
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59
% 141.11/141.59 Intermediate Status:
% 141.11/141.59 Generated: 189987
% 141.11/141.59 Kept: 102288
% 141.11/141.59 Inuse: 21172
% 141.11/141.59 Deleted: 42
% 141.11/141.59 Deletedinuse: 1
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 141.11/141.59 Done
% 141.11/141.59
% 141.11/141.59 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 193789
% 278.02/278.46 Kept: 104292
% 278.02/278.46 Inuse: 21582
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 197583
% 278.02/278.46 Kept: 106297
% 278.02/278.46 Inuse: 21996
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 201404
% 278.02/278.46 Kept: 108302
% 278.02/278.46 Inuse: 22407
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 205214
% 278.02/278.46 Kept: 110307
% 278.02/278.46 Inuse: 22820
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 209024
% 278.02/278.46 Kept: 112311
% 278.02/278.46 Inuse: 23228
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 212819
% 278.02/278.46 Kept: 114315
% 278.02/278.46 Inuse: 23636
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 216613
% 278.02/278.46 Kept: 116320
% 278.02/278.46 Inuse: 24044
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 220404
% 278.02/278.46 Kept: 118324
% 278.02/278.46 Inuse: 24450
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying clauses:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 224233
% 278.02/278.46 Kept: 120328
% 278.02/278.46 Inuse: 24860
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 228038
% 278.02/278.46 Kept: 122332
% 278.02/278.46 Inuse: 25267
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 231852
% 278.02/278.46 Kept: 124336
% 278.02/278.46 Inuse: 25674
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 235620
% 278.02/278.46 Kept: 126340
% 278.02/278.46 Inuse: 26079
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 239447
% 278.02/278.46 Kept: 128345
% 278.02/278.46 Inuse: 26493
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 243252
% 278.02/278.46 Kept: 130349
% 278.02/278.46 Inuse: 26903
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 247076
% 278.02/278.46 Kept: 132354
% 278.02/278.46 Inuse: 27317
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 250851
% 278.02/278.46 Kept: 134358
% 278.02/278.46 Inuse: 27724
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 254691
% 278.02/278.46 Kept: 136364
% 278.02/278.46 Inuse: 28142
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 258487
% 278.02/278.46 Kept: 138368
% 278.02/278.46 Inuse: 28549
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying clauses:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 262305
% 278.02/278.46 Kept: 140373
% 278.02/278.46 Inuse: 28966
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 266116
% 278.02/278.46 Kept: 142377
% 278.02/278.46 Inuse: 29373
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 269904
% 278.02/278.46 Kept: 144382
% 278.02/278.46 Inuse: 29784
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 273708
% 278.02/278.46 Kept: 146386
% 278.02/278.46 Inuse: 30189
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 277530
% 278.02/278.46 Kept: 148390
% 278.02/278.46 Inuse: 30600
% 278.02/278.46 Deleted: 42
% 278.02/278.46 Deletedinuse: 1
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46 Resimplifying inuse:
% 278.02/278.46 Done
% 278.02/278.46
% 278.02/278.46
% 278.02/278.46 Intermediate Status:
% 278.02/278.46 Generated: 281341
% 278.02/278.46 Kept: Terminated
% 299.65/300.04 Bliksem ended
%------------------------------------------------------------------------------