%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX221-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.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:50 PM UTC 2026
% Result : Timeout 299.64s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX221-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : bliksem %s
% 0.16/0.34 % Computer : n020.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % DateTime : Tue May 5 12:31:04 EDT 2026
% 0.16/0.34 % CPUTime :
% 5.66/6.10 *** allocated 10000 integers for termspace/termends
% 5.66/6.10 *** allocated 10000 integers for clauses
% 5.66/6.10 *** allocated 10000 integers for justifications
% 5.66/6.10 Bliksem 1.12
% 5.66/6.10
% 5.66/6.10
% 5.66/6.10 Automatic Strategy Selection
% 5.66/6.10
% 5.66/6.10 Clauses:
% 5.66/6.10 [
% 5.66/6.10 [ =( aux( X, Y, Z, nothing ), bfalse ) ],
% 5.66/6.10 [ =( aux( X, Y, Z, just( T ) ), eq( T, Y ) ) ],
% 5.66/6.10 [ =( notb( btrue ), bfalse ) ],
% 5.66/6.10 [ =( notb( bfalse ), btrue ) ],
% 5.66/6.10 [ =( index( nil, X ), nothing ) ],
% 5.66/6.10 [ =( index( cons( X, Y ), zero ), just( X ) ) ],
% 5.66/6.10 [ =( index( cons( X, Y ), suc( Z ) ), index( Y, Z ) ) ],
% 5.66/6.10 [ =( andb( btrue, X ), X ) ],
% 5.66/6.10 [ =( andb( bfalse, X ), bfalse ) ],
% 5.66/6.10 [ =( nf( app( lam( X ), Y, Z ) ), bfalse ) ],
% 5.66/6.10 [ =( nf( app( app( X, Y, Z ), T, U ) ), andb( nf( app( X, Y, Z ) ), nf(
% 5.66/6.10 T ) ) ) ],
% 5.66/6.10 [ =( nf( app( var( X ), Y, Z ) ), andb( nf( var( X ) ), nf( Y ) ) ) ]
% 5.66/6.10 ,
% 5.66/6.10 [ =( nf( lam( X ) ), nf( X ) ) ],
% 5.66/6.10 [ =( nf( var( X ) ), btrue ) ],
% 5.66/6.10 [ =( tc( X, app( Y, Z, T ), U ), andb( tc( X, Y, arr( T, U ) ), tc( X, Z
% 5.66/6.10 , T ) ) ) ],
% 5.66/6.10 [ =( tc( X, lam( Y ), arr( Z, T ) ), tc( cons( Z, X ), Y, T ) ) ],
% 5.66/6.10 [ =( tc( X, lam( Y ), a ), bfalse ) ],
% 5.66/6.10 [ =( tc( X, lam( Y ), b ), bfalse ) ],
% 5.66/6.10 [ =( tc( X, lam( Y ), c ), bfalse ) ],
% 5.66/6.10 [ =( tc( X, var( Y ), Z ), aux( X, Z, Y, index( X, Y ) ) ) ],
% 5.66/6.10 [ =( 'sat_synth_nf_flip'( X ), notb( andb( nf( X ), tc( nil, X, arr( arr(
% 5.66/6.10 a, arr( b, c ) ), arr( b, arr( a, c ) ) ) ) ) ) ) ],
% 5.66/6.10 [ =( eq( a, b ), bfalse ) ],
% 5.66/6.10 [ =( eq( a, c ), bfalse ) ],
% 5.66/6.10 [ =( eq( b, a ), bfalse ) ],
% 5.66/6.10 [ =( eq( b, c ), bfalse ) ],
% 5.66/6.10 [ =( eq( c, a ), bfalse ) ],
% 5.66/6.10 [ =( eq( c, b ), bfalse ) ],
% 5.66/6.10 [ =( eq4( bfalse, btrue ), bfalse ) ],
% 5.66/6.10 [ =( eq4( btrue, bfalse ), bfalse ) ],
% 5.66/6.10 [ =( eq2( suc( X ), suc( Y ) ), eq2( X, Y ) ) ],
% 5.66/6.10 [ =( eq2( zero, suc( X ) ), bfalse ) ],
% 5.66/6.10 [ =( eq2( suc( X ), zero ), bfalse ) ],
% 5.66/6.10 [ ~( =( eq( X, Y ), bfalse ) ), =( eq( arr( X, Z ), arr( Y, T ) ),
% 5.66/6.10 bfalse ) ],
% 5.66/6.10 [ ~( =( eq( X, Y ), btrue ) ), =( eq( arr( X, Z ), arr( Y, T ) ), eq( Z
% 5.66/6.10 , T ) ) ],
% 5.66/6.10 [ =( eq( arr( X, Y ), a ), bfalse ) ],
% 5.66/6.10 [ =( eq( arr( X, Y ), b ), bfalse ) ],
% 5.66/6.10 [ =( eq( arr( X, Y ), c ), bfalse ) ],
% 5.66/6.10 [ =( eq( a, arr( X, Y ) ), bfalse ) ],
% 5.66/6.10 [ =( eq( b, arr( X, Y ) ), bfalse ) ],
% 5.66/6.10 [ =( eq( c, arr( X, Y ) ), bfalse ) ],
% 5.66/6.10 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( app( X, Z, T ), app( Y, U, W )
% 5.66/6.10 ), bfalse ) ],
% 5.66/6.10 [ ~( =( eq3( X, Y ), bfalse ) ), ~( =( eq3( Z, T ), btrue ) ), =( eq3(
% 5.66/6.10 app( Z, X, U ), app( T, Y, W ) ), bfalse ) ],
% 5.66/6.10 [ ~( =( eq3( X, Y ), btrue ) ), ~( =( eq3( Z, T ), btrue ) ), =( eq3(
% 5.66/6.10 app( X, Z, U ), app( Y, T, W ) ), eq( U, W ) ) ],
% 5.66/6.10 [ =( eq3( lam( X ), lam( Y ) ), eq3( X, Y ) ) ],
% 5.66/6.10 [ =( eq3( var( X ), var( Y ) ), eq2( X, Y ) ) ],
% 5.66/6.10 [ =( eq3( app( X, Y, Z ), lam( T ) ), bfalse ) ],
% 5.66/6.10 [ =( eq3( app( X, Y, Z ), var( T ) ), bfalse ) ],
% 5.66/6.10 [ =( eq3( lam( X ), app( Y, Z, T ) ), bfalse ) ],
% 5.66/6.10 [ =( eq3( lam( X ), var( Y ) ), bfalse ) ],
% 5.66/6.10 [ =( eq3( var( X ), app( Y, Z, T ) ), bfalse ) ],
% 5.66/6.10 [ =( eq3( var( X ), lam( Y ) ), bfalse ) ],
% 5.66/6.10 [ =( eq( X, X ), btrue ) ],
% 5.66/6.10 [ =( eq2( X, X ), btrue ) ],
% 5.66/6.10 [ =( eq3( X, X ), btrue ) ],
% 5.66/6.10 [ =( eq4( X, X ), btrue ) ],
% 5.66/6.10 [ ~( =( eq4( 'sat_synth_nf_flip'( X ), bfalse ), btrue ) ) ]
% 5.66/6.10 ] .
% 5.66/6.10
% 5.66/6.10
% 5.66/6.10 percentage equality = 1.000000, percentage horn = 1.000000
% 5.66/6.10 This is a pure equality problem
% 5.66/6.10
% 5.66/6.10
% 5.66/6.10
% 5.66/6.10 Options Used:
% 5.66/6.10
% 5.66/6.10 useres = 1
% 5.66/6.10 useparamod = 1
% 5.66/6.10 useeqrefl = 1
% 5.66/6.10 useeqfact = 1
% 5.66/6.10 usefactor = 1
% 5.66/6.10 usesimpsplitting = 0
% 5.66/6.10 usesimpdemod = 5
% 5.66/6.10 usesimpres = 3
% 5.66/6.10
% 5.66/6.10 resimpinuse = 1000
% 5.66/6.10 resimpclauses = 20000
% 5.66/6.10 substype = eqrewr
% 5.66/6.10 backwardsubs = 1
% 5.66/6.10 selectoldest = 5
% 5.66/6.10
% 5.66/6.10 litorderings [0] = split
% 5.66/6.10 litorderings [1] = extend the termordering, first sorting on arguments
% 5.66/6.10
% 5.66/6.10 termordering = kbo
% 5.66/6.10
% 5.66/6.10 litapriori = 0
% 5.66/6.10 termapriori = 1
% 5.66/6.10 litaposteriori = 0
% 5.66/6.10 termaposteriori = 0
% 5.66/6.10 demodaposteriori = 0
% 5.66/6.10 ordereqreflfact = 0
% 5.66/6.10
% 5.66/6.10 litselect = negord
% 5.66/6.10
% 5.66/6.10 maxweight = 15
% 5.66/6.10 maxdepth = 30000
% 5.66/6.10 maxlength = 115
% 5.66/6.10 maxnrvars = 195
% 5.66/6.10 excuselevel = 1
% 5.66/6.10 increasemaxweight = 1
% 5.66/6.10
% 5.66/6.10 maxselected = 10000000
% 5.66/6.10 maxnrclauses = 10000000
% 5.66/6.10
% 5.66/6.10 showgenerated = 0
% 5.66/6.10 showkept = 0
% 5.66/6.10 showselected = 0
% 47.23/47.62 showdeleted = 0
% 47.23/47.62 showresimp = 1
% 47.23/47.62 showstatus = 2000
% 47.23/47.62
% 47.23/47.62 prologoutput = 1
% 47.23/47.62 nrgoals = 5000000
% 47.23/47.62 totalproof = 1
% 47.23/47.62
% 47.23/47.62 Symbols occurring in the translation:
% 47.23/47.62
% 47.23/47.62 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 47.23/47.62 . [1, 2] (w:1, o:44, a:1, s:1, b:0),
% 47.23/47.62 ! [4, 1] (w:0, o:32, a:1, s:1, b:0),
% 47.23/47.62 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 47.23/47.62 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 47.23/47.62 nothing [42, 0] (w:1, o:16, a:1, s:1, b:0),
% 47.23/47.62 aux [43, 4] (w:1, o:79, a:1, s:1, b:0),
% 47.23/47.62 bfalse [44, 0] (w:1, o:18, a:1, s:1, b:0),
% 47.23/47.62 just [46, 1] (w:1, o:37, a:1, s:1, b:0),
% 47.23/47.62 eq [47, 2] (w:1, o:69, a:1, s:1, b:0),
% 47.23/47.62 btrue [48, 0] (w:1, o:21, a:1, s:1, b:0),
% 47.23/47.62 notb [49, 1] (w:1, o:38, a:1, s:1, b:0),
% 47.23/47.62 nil [50, 0] (w:1, o:22, a:1, s:1, b:0),
% 47.23/47.62 index [52, 2] (w:1, o:70, a:1, s:1, b:0),
% 47.23/47.62 cons [54, 2] (w:1, o:71, a:1, s:1, b:0),
% 47.23/47.62 zero [55, 0] (w:1, o:23, a:1, s:1, b:0),
% 47.23/47.62 suc [57, 1] (w:1, o:39, a:1, s:1, b:0),
% 47.23/47.62 andb [59, 2] (w:1, o:72, a:1, s:1, b:0),
% 47.23/47.62 lam [60, 1] (w:1, o:40, a:1, s:1, b:0),
% 47.23/47.62 app [62, 3] (w:1, o:77, a:1, s:1, b:0),
% 47.23/47.62 nf [63, 1] (w:1, o:41, a:1, s:1, b:0),
% 47.23/47.62 var [65, 1] (w:1, o:42, a:1, s:1, b:0),
% 47.23/47.62 tc [69, 3] (w:1, o:78, a:1, s:1, b:0),
% 47.23/47.62 arr [70, 2] (w:1, o:73, a:1, s:1, b:0),
% 47.23/47.62 a [73, 0] (w:1, o:17, a:1, s:1, b:0),
% 47.23/47.62 b [74, 0] (w:1, o:30, a:1, s:1, b:0),
% 47.23/47.62 c [75, 0] (w:1, o:31, a:1, s:1, b:0),
% 47.23/47.62 'sat_synth_nf_flip' [76, 1] (w:1, o:43, a:1, s:1, b:0),
% 47.23/47.62 eq4 [77, 2] (w:1, o:75, a:1, s:1, b:0),
% 47.23/47.62 eq2 [78, 2] (w:1, o:76, a:1, s:1, b:0),
% 47.23/47.62 eq3 [79, 2] (w:1, o:74, a:1, s:1, b:0).
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 15
% 47.23/47.62 maxnrclauses = 10000000
% 47.23/47.62 Generated: 8035
% 47.23/47.62 Kept: 207
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 The strategy used was not complete!
% 47.23/47.62
% 47.23/47.62 Increased maxweight to 16
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 16
% 47.23/47.62 maxnrclauses = 10000000
% 47.23/47.62 Generated: 8314
% 47.23/47.62 Kept: 229
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 The strategy used was not complete!
% 47.23/47.62
% 47.23/47.62 Increased maxweight to 17
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 17
% 47.23/47.62 maxnrclauses = 10000000
% 47.23/47.62 Generated: 10954
% 47.23/47.62 Kept: 290
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 The strategy used was not complete!
% 47.23/47.62
% 47.23/47.62 Increased maxweight to 18
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 18
% 47.23/47.62 maxnrclauses = 10000000
% 47.23/47.62 Generated: 18265
% 47.23/47.62 Kept: 488
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 The strategy used was not complete!
% 47.23/47.62
% 47.23/47.62 Increased maxweight to 19
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 19
% 47.23/47.62 maxnrclauses = 10000000
% 47.23/47.62 Generated: 26919
% 47.23/47.62 Kept: 736
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 The strategy used was not complete!
% 47.23/47.62
% 47.23/47.62 Increased maxweight to 20
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 20
% 47.23/47.62 maxnrclauses = 10000000
% 47.23/47.62 Generated: 48279
% 47.23/47.62 Kept: 1079
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 The strategy used was not complete!
% 47.23/47.62
% 47.23/47.62 Increased maxweight to 21
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 21
% 47.23/47.62 maxnrclauses = 10000000
% 47.23/47.62 Generated: 85217
% 47.23/47.62 Kept: 1780
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 The strategy used was not complete!
% 47.23/47.62
% 47.23/47.62 Increased maxweight to 22
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 Intermediate Status:
% 47.23/47.62 Generated: 50768
% 47.23/47.62 Kept: 2001
% 47.23/47.62 Inuse: 772
% 47.23/47.62 Deleted: 215
% 47.23/47.62 Deletedinuse: 4
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 22
% 47.23/47.62 maxnrclauses = 10000000
% 47.23/47.62 Generated: 182867
% 47.23/47.62 Kept: 3114
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 The strategy used was not complete!
% 47.23/47.62
% 47.23/47.62 Increased maxweight to 23
% 47.23/47.62
% 47.23/47.62 Starting Search:
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 Intermediate Status:
% 47.23/47.62 Generated: 22459
% 47.23/47.62 Kept: 2002
% 47.23/47.62 Inuse: 455
% 47.23/47.62 Deleted: 110
% 47.23/47.62 Deletedinuse: 3
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 Intermediate Status:
% 47.23/47.62 Generated: 77806
% 47.23/47.62 Kept: 4003
% 47.23/47.62 Inuse: 1076
% 47.23/47.62 Deleted: 490
% 47.23/47.62 Deletedinuse: 4
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62
% 47.23/47.62 Intermediate Status:
% 47.23/47.62 Generated: 307993
% 47.23/47.62 Kept: 6006
% 47.23/47.62 Inuse: 3231
% 47.23/47.62 Deleted: 1307
% 47.23/47.62 Deletedinuse: 4
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Resimplifying inuse:
% 47.23/47.62 Done
% 47.23/47.62
% 47.23/47.62 Failed to find proof!
% 47.23/47.62 maxweight = 23
% 90.02/90.49 maxnrclauses = 10000000
% 90.02/90.49 Generated: 461671
% 90.02/90.49 Kept: 6871
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 The strategy used was not complete!
% 90.02/90.49
% 90.02/90.49 Increased maxweight to 24
% 90.02/90.49
% 90.02/90.49 Starting Search:
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 21738
% 90.02/90.49 Kept: 2006
% 90.02/90.49 Inuse: 426
% 90.02/90.49 Deleted: 82
% 90.02/90.49 Deletedinuse: 3
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 42819
% 90.02/90.49 Kept: 4006
% 90.02/90.49 Inuse: 733
% 90.02/90.49 Deleted: 256
% 90.02/90.49 Deletedinuse: 4
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 99250
% 90.02/90.49 Kept: 6011
% 90.02/90.49 Inuse: 1208
% 90.02/90.49 Deleted: 534
% 90.02/90.49 Deletedinuse: 4
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 248987
% 90.02/90.49 Kept: 8013
% 90.02/90.49 Inuse: 2253
% 90.02/90.49 Deleted: 1139
% 90.02/90.49 Deletedinuse: 4
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 371838
% 90.02/90.49 Kept: 10014
% 90.02/90.49 Inuse: 3257
% 90.02/90.49 Deleted: 1574
% 90.02/90.49 Deletedinuse: 4
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 667230
% 90.02/90.49 Kept: 12305
% 90.02/90.49 Inuse: 6093
% 90.02/90.49 Deleted: 2977
% 90.02/90.49 Deletedinuse: 4
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Failed to find proof!
% 90.02/90.49 maxweight = 24
% 90.02/90.49 maxnrclauses = 10000000
% 90.02/90.49 Generated: 1033236
% 90.02/90.49 Kept: 13917
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 The strategy used was not complete!
% 90.02/90.49
% 90.02/90.49 Increased maxweight to 25
% 90.02/90.49
% 90.02/90.49 Starting Search:
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 19468
% 90.02/90.49 Kept: 2005
% 90.02/90.49 Inuse: 388
% 90.02/90.49 Deleted: 69
% 90.02/90.49 Deletedinuse: 3
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 34989
% 90.02/90.49 Kept: 4005
% 90.02/90.49 Inuse: 618
% 90.02/90.49 Deleted: 253
% 90.02/90.49 Deletedinuse: 4
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 56829
% 90.02/90.49 Kept: 6011
% 90.02/90.49 Inuse: 841
% 90.02/90.49 Deleted: 312
% 90.02/90.49 Deletedinuse: 4
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 105185
% 90.02/90.49 Kept: 8012
% 90.02/90.49 Inuse: 1174
% 90.02/90.49 Deleted: 553
% 90.02/90.49 Deletedinuse: 5
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 140276
% 90.02/90.49 Kept: 10012
% 90.02/90.49 Inuse: 1450
% 90.02/90.49 Deleted: 718
% 90.02/90.49 Deletedinuse: 5
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 242637
% 90.02/90.49 Kept: 12045
% 90.02/90.49 Inuse: 1880
% 90.02/90.49 Deleted: 994
% 90.02/90.49 Deletedinuse: 5
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 289057
% 90.02/90.49 Kept: 14046
% 90.02/90.49 Inuse: 2265
% 90.02/90.49 Deleted: 1140
% 90.02/90.49 Deletedinuse: 5
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 406014
% 90.02/90.49 Kept: 16048
% 90.02/90.49 Inuse: 2856
% 90.02/90.49 Deleted: 1577
% 90.02/90.49 Deletedinuse: 5
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 472420
% 90.02/90.49 Kept: 18055
% 90.02/90.49 Inuse: 3336
% 90.02/90.49 Deleted: 1838
% 90.02/90.49 Deletedinuse: 6
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying clauses:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 552772
% 90.02/90.49 Kept: 20095
% 90.02/90.49 Inuse: 3627
% 90.02/90.49 Deleted: 9767
% 90.02/90.49 Deletedinuse: 6
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 706403
% 90.02/90.49 Kept: 22099
% 90.02/90.49 Inuse: 4533
% 90.02/90.49 Deleted: 9782
% 90.02/90.49 Deletedinuse: 19
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 914463
% 90.02/90.49 Kept: 24099
% 90.02/90.49 Inuse: 5860
% 90.02/90.49 Deleted: 9813
% 90.02/90.49 Deletedinuse: 44
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 1299507
% 90.02/90.49 Kept: 26779
% 90.02/90.49 Inuse: 7740
% 90.02/90.49 Deleted: 9951
% 90.02/90.49 Deletedinuse: 44
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 1925961
% 90.02/90.49 Kept: 28779
% 90.02/90.49 Inuse: 11973
% 90.02/90.49 Deleted: 11256
% 90.02/90.49 Deletedinuse: 53
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49
% 90.02/90.49 Intermediate Status:
% 90.02/90.49 Generated: 2671586
% 90.02/90.49 Kept: 30779
% 90.02/90.49 Inuse: 16887
% 90.02/90.49 Deleted: 13237
% 90.02/90.49 Deletedinuse: 122
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Resimplifying inuse:
% 90.02/90.49 Done
% 90.02/90.49
% 90.02/90.49 Failed to find proof!
% 90.02/90.49 maxweight = 25
% 90.02/90.49 maxnrclauses = 10000000
% 90.02/90.49 Generated: 2788981
% 148.75/149.19 Kept: 31721
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 The strategy used was not complete!
% 148.75/149.19
% 148.75/149.19 Increased maxweight to 26
% 148.75/149.19
% 148.75/149.19 Starting Search:
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 19042
% 148.75/149.19 Kept: 2082
% 148.75/149.19 Inuse: 386
% 148.75/149.19 Deleted: 63
% 148.75/149.19 Deletedinuse: 3
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 31766
% 148.75/149.19 Kept: 4124
% 148.75/149.19 Inuse: 571
% 148.75/149.19 Deleted: 189
% 148.75/149.19 Deletedinuse: 4
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 48973
% 148.75/149.19 Kept: 6136
% 148.75/149.19 Inuse: 754
% 148.75/149.19 Deleted: 289
% 148.75/149.19 Deletedinuse: 4
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 76071
% 148.75/149.19 Kept: 8140
% 148.75/149.19 Inuse: 944
% 148.75/149.19 Deleted: 366
% 148.75/149.19 Deletedinuse: 4
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 117374
% 148.75/149.19 Kept: 10143
% 148.75/149.19 Inuse: 1214
% 148.75/149.19 Deleted: 654
% 148.75/149.19 Deletedinuse: 5
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 152232
% 148.75/149.19 Kept: 12150
% 148.75/149.19 Inuse: 1447
% 148.75/149.19 Deleted: 740
% 148.75/149.19 Deletedinuse: 5
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 232385
% 148.75/149.19 Kept: 14153
% 148.75/149.19 Inuse: 1822
% 148.75/149.19 Deleted: 1036
% 148.75/149.19 Deletedinuse: 5
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 299957
% 148.75/149.19 Kept: 16158
% 148.75/149.19 Inuse: 2101
% 148.75/149.19 Deleted: 1084
% 148.75/149.19 Deletedinuse: 5
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 348567
% 148.75/149.19 Kept: 18166
% 148.75/149.19 Inuse: 2448
% 148.75/149.19 Deleted: 1147
% 148.75/149.19 Deletedinuse: 5
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying clauses:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 445984
% 148.75/149.19 Kept: 20167
% 148.75/149.19 Inuse: 2846
% 148.75/149.19 Deleted: 8720
% 148.75/149.19 Deletedinuse: 6
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 516572
% 148.75/149.19 Kept: 22167
% 148.75/149.19 Inuse: 3226
% 148.75/149.19 Deleted: 8720
% 148.75/149.19 Deletedinuse: 6
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 584986
% 148.75/149.19 Kept: 24168
% 148.75/149.19 Inuse: 3611
% 148.75/149.19 Deleted: 8720
% 148.75/149.19 Deletedinuse: 6
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 675872
% 148.75/149.19 Kept: 26175
% 148.75/149.19 Inuse: 4030
% 148.75/149.19 Deleted: 8790
% 148.75/149.19 Deletedinuse: 6
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 932850
% 148.75/149.19 Kept: 28177
% 148.75/149.19 Inuse: 4803
% 148.75/149.19 Deleted: 9210
% 148.75/149.19 Deletedinuse: 10
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 1040869
% 148.75/149.19 Kept: 30177
% 148.75/149.19 Inuse: 5631
% 148.75/149.19 Deleted: 9304
% 148.75/149.19 Deletedinuse: 95
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 1181041
% 148.75/149.19 Kept: 32177
% 148.75/149.19 Inuse: 6681
% 148.75/149.19 Deleted: 9382
% 148.75/149.19 Deletedinuse: 153
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 1539817
% 148.75/149.19 Kept: 34177
% 148.75/149.19 Inuse: 8050
% 148.75/149.19 Deleted: 9765
% 148.75/149.19 Deletedinuse: 222
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 1629967
% 148.75/149.19 Kept: 36178
% 148.75/149.19 Inuse: 8851
% 148.75/149.19 Deleted: 10343
% 148.75/149.19 Deletedinuse: 316
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 2037244
% 148.75/149.19 Kept: 38178
% 148.75/149.19 Inuse: 10066
% 148.75/149.19 Deleted: 10657
% 148.75/149.19 Deletedinuse: 384
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying clauses:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 2327856
% 148.75/149.19 Kept: 40178
% 148.75/149.19 Inuse: 11731
% 148.75/149.19 Deleted: 16661
% 148.75/149.19 Deletedinuse: 384
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 2751917
% 148.75/149.19 Kept: 42179
% 148.75/149.19 Inuse: 13473
% 148.75/149.19 Deleted: 16709
% 148.75/149.19 Deletedinuse: 398
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 3426152
% 148.75/149.19 Kept: 44179
% 148.75/149.19 Inuse: 17130
% 148.75/149.19 Deleted: 16880
% 148.75/149.19 Deletedinuse: 455
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19 Resimplifying inuse:
% 148.75/149.19 Done
% 148.75/149.19
% 148.75/149.19
% 148.75/149.19 Intermediate Status:
% 148.75/149.19 Generated: 3872172
% 148.75/149.19 Kept: 46180
% 148.75/149.19 Inuse: 19002
% 148.75/149.19 Deleted: 17664
% 148.75/149.19 Deletedinuse: 455
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 4711110
% 214.82/215.23 Kept: 48181
% 214.82/215.23 Inuse: 24038
% 214.82/215.23 Deleted: 17967
% 214.82/215.23 Deletedinuse: 455
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 5248510
% 214.82/215.23 Kept: 50181
% 214.82/215.23 Inuse: 28122
% 214.82/215.23 Deleted: 18147
% 214.82/215.23 Deletedinuse: 455
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 5844668
% 214.82/215.23 Kept: 52181
% 214.82/215.23 Inuse: 32807
% 214.82/215.23 Deleted: 18147
% 214.82/215.23 Deletedinuse: 455
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Failed to find proof!
% 214.82/215.23 maxweight = 26
% 214.82/215.23 maxnrclauses = 10000000
% 214.82/215.23 Generated: 6215860
% 214.82/215.23 Kept: 54039
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 The strategy used was not complete!
% 214.82/215.23
% 214.82/215.23 Increased maxweight to 27
% 214.82/215.23
% 214.82/215.23 Starting Search:
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 17479
% 214.82/215.23 Kept: 2006
% 214.82/215.23 Inuse: 362
% 214.82/215.23 Deleted: 41
% 214.82/215.23 Deletedinuse: 3
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 29697
% 214.82/215.23 Kept: 4006
% 214.82/215.23 Inuse: 511
% 214.82/215.23 Deleted: 145
% 214.82/215.23 Deletedinuse: 4
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 42464
% 214.82/215.23 Kept: 6008
% 214.82/215.23 Inuse: 646
% 214.82/215.23 Deleted: 237
% 214.82/215.23 Deletedinuse: 4
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 58611
% 214.82/215.23 Kept: 8013
% 214.82/215.23 Inuse: 788
% 214.82/215.23 Deleted: 301
% 214.82/215.23 Deletedinuse: 4
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 85359
% 214.82/215.23 Kept: 10095
% 214.82/215.23 Inuse: 942
% 214.82/215.23 Deleted: 378
% 214.82/215.23 Deletedinuse: 4
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 109711
% 214.82/215.23 Kept: 12101
% 214.82/215.23 Inuse: 1090
% 214.82/215.23 Deleted: 430
% 214.82/215.23 Deletedinuse: 5
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 148813
% 214.82/215.23 Kept: 14112
% 214.82/215.23 Inuse: 1283
% 214.82/215.23 Deleted: 696
% 214.82/215.23 Deletedinuse: 5
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 176517
% 214.82/215.23 Kept: 16115
% 214.82/215.23 Inuse: 1453
% 214.82/215.23 Deleted: 782
% 214.82/215.23 Deletedinuse: 5
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 236478
% 214.82/215.23 Kept: 18116
% 214.82/215.23 Inuse: 1738
% 214.82/215.23 Deleted: 934
% 214.82/215.23 Deletedinuse: 5
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying clauses:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 291364
% 214.82/215.23 Kept: 20119
% 214.82/215.23 Inuse: 1936
% 214.82/215.23 Deleted: 9470
% 214.82/215.23 Deletedinuse: 5
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 345745
% 214.82/215.23 Kept: 22126
% 214.82/215.23 Inuse: 2179
% 214.82/215.23 Deleted: 9470
% 214.82/215.23 Deletedinuse: 5
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 441787
% 214.82/215.23 Kept: 24127
% 214.82/215.23 Inuse: 2529
% 214.82/215.23 Deleted: 9470
% 214.82/215.23 Deletedinuse: 5
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 604826
% 214.82/215.23 Kept: 26130
% 214.82/215.23 Inuse: 2885
% 214.82/215.23 Deleted: 9470
% 214.82/215.23 Deletedinuse: 5
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 673454
% 214.82/215.23 Kept: 28134
% 214.82/215.23 Inuse: 3124
% 214.82/215.23 Deleted: 9471
% 214.82/215.23 Deletedinuse: 6
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 718377
% 214.82/215.23 Kept: 30146
% 214.82/215.23 Inuse: 3322
% 214.82/215.23 Deleted: 9471
% 214.82/215.23 Deletedinuse: 6
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 803597
% 214.82/215.23 Kept: 32154
% 214.82/215.23 Inuse: 3617
% 214.82/215.23 Deleted: 9471
% 214.82/215.23 Deletedinuse: 6
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 845202
% 214.82/215.23 Kept: 34155
% 214.82/215.23 Inuse: 3823
% 214.82/215.23 Deleted: 9471
% 214.82/215.23 Deletedinuse: 6
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 917522
% 214.82/215.23 Kept: 36155
% 214.82/215.23 Inuse: 4018
% 214.82/215.23 Deleted: 9651
% 214.82/215.23 Deletedinuse: 6
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23
% 214.82/215.23 Intermediate Status:
% 214.82/215.23 Generated: 972105
% 214.82/215.23 Kept: 38156
% 214.82/215.23 Inuse: 4245
% 214.82/215.23 Deleted: 9787
% 214.82/215.23 Deletedinuse: 6
% 214.82/215.23
% 214.82/215.23 Resimplifying inuse:
% 214.82/215.23 Done
% 214.82/215.23
% 214.82/215.23 Resimplifying iTerminated
% 299.64/300.03 Bliksem ended
%------------------------------------------------------------------------------