%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX223-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n016.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.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX223-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n016.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:37:36 EDT 2026
% 0.15/0.33 % CPUTime :
% 5.52/6.02 *** allocated 10000 integers for termspace/termends
% 5.52/6.02 *** allocated 10000 integers for clauses
% 5.52/6.02 *** allocated 10000 integers for justifications
% 5.52/6.02 Bliksem 1.12
% 5.52/6.02
% 5.52/6.02
% 5.52/6.02 Automatic Strategy Selection
% 5.52/6.02
% 5.52/6.02 Clauses:
% 5.52/6.02 [
% 5.52/6.02 [ =( aux( X, Y, Z, nothing ), bfalse ) ],
% 5.52/6.02 [ =( aux( X, Y, Z, just( T ) ), eq( T, Y ) ) ],
% 5.52/6.02 [ =( notb( btrue ), bfalse ) ],
% 5.52/6.02 [ =( notb( bfalse ), btrue ) ],
% 5.52/6.02 [ =( index( nil, X ), nothing ) ],
% 5.52/6.02 [ =( index( cons( X, Y ), zero ), just( X ) ) ],
% 5.52/6.02 [ =( index( cons( X, Y ), suc( Z ) ), index( Y, Z ) ) ],
% 5.52/6.02 [ =( andb( btrue, X ), X ) ],
% 5.52/6.02 [ =( andb( bfalse, X ), bfalse ) ],
% 5.52/6.02 [ =( nf( app( lam( X ), Y, Z ) ), bfalse ) ],
% 5.52/6.02 [ =( nf( app( app( X, Y, Z ), T, U ) ), andb( nf( app( X, Y, Z ) ), nf(
% 5.52/6.02 T ) ) ) ],
% 5.52/6.02 [ =( nf( app( var( X ), Y, Z ) ), andb( nf( var( X ) ), nf( Y ) ) ) ]
% 5.52/6.02 ,
% 5.52/6.02 [ =( nf( lam( X ) ), nf( X ) ) ],
% 5.52/6.02 [ =( nf( var( X ) ), btrue ) ],
% 5.52/6.02 [ =( tc( X, app( Y, Z, T ), U ), andb( tc( X, Y, arr( T, U ) ), tc( X, Z
% 5.52/6.02 , T ) ) ) ],
% 5.52/6.02 [ =( tc( X, lam( Y ), arr( Z, T ) ), tc( cons( Z, X ), Y, T ) ) ],
% 5.52/6.02 [ =( tc( X, lam( Y ), a ), bfalse ) ],
% 5.52/6.02 [ =( tc( X, lam( Y ), b ), bfalse ) ],
% 5.52/6.02 [ =( tc( X, lam( Y ), c ), bfalse ) ],
% 5.52/6.02 [ =( tc( X, var( Y ), Z ), aux( X, Z, Y, index( X, Y ) ) ) ],
% 5.52/6.02 [ =( 'sat_synth_nf_w'( X ), notb( andb( nf( X ), tc( nil, X, arr( arr( a
% 5.52/6.02 , arr( a, b ) ), arr( a, b ) ) ) ) ) ) ],
% 5.52/6.02 [ =( eq( a, b ), bfalse ) ],
% 5.52/6.02 [ =( eq( a, c ), bfalse ) ],
% 5.52/6.02 [ =( eq( b, a ), bfalse ) ],
% 5.52/6.02 [ =( eq( b, c ), bfalse ) ],
% 5.52/6.02 [ =( eq( c, a ), bfalse ) ],
% 5.52/6.02 [ =( eq( c, b ), bfalse ) ],
% 5.52/6.02 [ =( eq4( bfalse, btrue ), bfalse ) ],
% 5.52/6.02 [ =( eq4( btrue, bfalse ), bfalse ) ],
% 5.52/6.02 [ =( eq2( suc( X ), suc( Y ) ), eq2( X, Y ) ) ],
% 5.52/6.02 [ =( eq2( zero, suc( X ) ), bfalse ) ],
% 5.52/6.02 [ =( eq2( suc( X ), zero ), bfalse ) ],
% 5.52/6.02 [ ~( =( eq( X, Y ), bfalse ) ), =( eq( arr( X, Z ), arr( Y, T ) ),
% 5.52/6.02 bfalse ) ],
% 5.52/6.02 [ ~( =( eq( X, Y ), btrue ) ), =( eq( arr( X, Z ), arr( Y, T ) ), eq( Z
% 5.52/6.02 , T ) ) ],
% 5.52/6.02 [ =( eq( arr( X, Y ), a ), bfalse ) ],
% 5.52/6.02 [ =( eq( arr( X, Y ), b ), bfalse ) ],
% 5.52/6.02 [ =( eq( arr( X, Y ), c ), bfalse ) ],
% 5.52/6.02 [ =( eq( a, arr( X, Y ) ), bfalse ) ],
% 5.52/6.02 [ =( eq( b, arr( X, Y ) ), bfalse ) ],
% 5.52/6.02 [ =( eq( c, arr( X, Y ) ), bfalse ) ],
% 5.52/6.02 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( app( X, Z, T ), app( Y, U, W )
% 5.52/6.02 ), bfalse ) ],
% 5.52/6.02 [ ~( =( eq3( X, Y ), bfalse ) ), ~( =( eq3( Z, T ), btrue ) ), =( eq3(
% 5.52/6.02 app( Z, X, U ), app( T, Y, W ) ), bfalse ) ],
% 5.52/6.02 [ ~( =( eq3( X, Y ), btrue ) ), ~( =( eq3( Z, T ), btrue ) ), =( eq3(
% 5.52/6.02 app( X, Z, U ), app( Y, T, W ) ), eq( U, W ) ) ],
% 5.52/6.02 [ =( eq3( lam( X ), lam( Y ) ), eq3( X, Y ) ) ],
% 5.52/6.02 [ =( eq3( var( X ), var( Y ) ), eq2( X, Y ) ) ],
% 5.52/6.02 [ =( eq3( app( X, Y, Z ), lam( T ) ), bfalse ) ],
% 5.52/6.02 [ =( eq3( app( X, Y, Z ), var( T ) ), bfalse ) ],
% 5.52/6.02 [ =( eq3( lam( X ), app( Y, Z, T ) ), bfalse ) ],
% 5.52/6.02 [ =( eq3( lam( X ), var( Y ) ), bfalse ) ],
% 5.52/6.02 [ =( eq3( var( X ), app( Y, Z, T ) ), bfalse ) ],
% 5.52/6.02 [ =( eq3( var( X ), lam( Y ) ), bfalse ) ],
% 5.52/6.02 [ =( eq( X, X ), btrue ) ],
% 5.52/6.02 [ =( eq2( X, X ), btrue ) ],
% 5.52/6.02 [ =( eq3( X, X ), btrue ) ],
% 5.52/6.02 [ =( eq4( X, X ), btrue ) ],
% 5.52/6.02 [ ~( =( eq4( 'sat_synth_nf_w'( X ), bfalse ), btrue ) ) ]
% 5.52/6.02 ] .
% 5.52/6.02
% 5.52/6.02
% 5.52/6.02 percentage equality = 1.000000, percentage horn = 1.000000
% 5.52/6.02 This is a pure equality problem
% 5.52/6.02
% 5.52/6.02
% 5.52/6.02
% 5.52/6.02 Options Used:
% 5.52/6.02
% 5.52/6.02 useres = 1
% 5.52/6.02 useparamod = 1
% 5.52/6.02 useeqrefl = 1
% 5.52/6.02 useeqfact = 1
% 5.52/6.02 usefactor = 1
% 5.52/6.02 usesimpsplitting = 0
% 5.52/6.02 usesimpdemod = 5
% 5.52/6.02 usesimpres = 3
% 5.52/6.02
% 5.52/6.02 resimpinuse = 1000
% 5.52/6.02 resimpclauses = 20000
% 5.52/6.02 substype = eqrewr
% 5.52/6.02 backwardsubs = 1
% 5.52/6.02 selectoldest = 5
% 5.52/6.02
% 5.52/6.02 litorderings [0] = split
% 5.52/6.02 litorderings [1] = extend the termordering, first sorting on arguments
% 5.52/6.02
% 5.52/6.02 termordering = kbo
% 5.52/6.02
% 5.52/6.02 litapriori = 0
% 5.52/6.02 termapriori = 1
% 5.52/6.02 litaposteriori = 0
% 5.52/6.02 termaposteriori = 0
% 5.52/6.02 demodaposteriori = 0
% 5.52/6.02 ordereqreflfact = 0
% 5.52/6.02
% 5.52/6.02 litselect = negord
% 5.52/6.02
% 5.52/6.02 maxweight = 15
% 5.52/6.02 maxdepth = 30000
% 5.52/6.02 maxlength = 115
% 5.52/6.02 maxnrvars = 195
% 5.52/6.02 excuselevel = 1
% 5.52/6.02 increasemaxweight = 1
% 5.52/6.02
% 5.52/6.02 maxselected = 10000000
% 5.52/6.02 maxnrclauses = 10000000
% 5.52/6.02
% 5.52/6.02 showgenerated = 0
% 5.52/6.02 showkept = 0
% 5.52/6.02 showselected = 0
% 5.52/6.02 showdeleted = 0
% 46.32/46.77 showresimp = 1
% 46.32/46.77 showstatus = 2000
% 46.32/46.77
% 46.32/46.77 prologoutput = 1
% 46.32/46.77 nrgoals = 5000000
% 46.32/46.77 totalproof = 1
% 46.32/46.77
% 46.32/46.77 Symbols occurring in the translation:
% 46.32/46.77
% 46.32/46.77 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 46.32/46.77 . [1, 2] (w:1, o:44, a:1, s:1, b:0),
% 46.32/46.77 ! [4, 1] (w:0, o:32, a:1, s:1, b:0),
% 46.32/46.77 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 46.32/46.77 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 46.32/46.77 nothing [42, 0] (w:1, o:16, a:1, s:1, b:0),
% 46.32/46.77 aux [43, 4] (w:1, o:79, a:1, s:1, b:0),
% 46.32/46.77 bfalse [44, 0] (w:1, o:18, a:1, s:1, b:0),
% 46.32/46.77 just [46, 1] (w:1, o:37, a:1, s:1, b:0),
% 46.32/46.77 eq [47, 2] (w:1, o:69, a:1, s:1, b:0),
% 46.32/46.77 btrue [48, 0] (w:1, o:21, a:1, s:1, b:0),
% 46.32/46.77 notb [49, 1] (w:1, o:38, a:1, s:1, b:0),
% 46.32/46.77 nil [50, 0] (w:1, o:22, a:1, s:1, b:0),
% 46.32/46.77 index [52, 2] (w:1, o:70, a:1, s:1, b:0),
% 46.32/46.77 cons [54, 2] (w:1, o:71, a:1, s:1, b:0),
% 46.32/46.77 zero [55, 0] (w:1, o:23, a:1, s:1, b:0),
% 46.32/46.77 suc [57, 1] (w:1, o:39, a:1, s:1, b:0),
% 46.32/46.77 andb [59, 2] (w:1, o:72, a:1, s:1, b:0),
% 46.32/46.77 lam [60, 1] (w:1, o:40, a:1, s:1, b:0),
% 46.32/46.77 app [62, 3] (w:1, o:77, a:1, s:1, b:0),
% 46.32/46.77 nf [63, 1] (w:1, o:41, a:1, s:1, b:0),
% 46.32/46.77 var [65, 1] (w:1, o:42, a:1, s:1, b:0),
% 46.32/46.77 tc [69, 3] (w:1, o:78, a:1, s:1, b:0),
% 46.32/46.77 arr [70, 2] (w:1, o:73, a:1, s:1, b:0),
% 46.32/46.77 a [73, 0] (w:1, o:17, a:1, s:1, b:0),
% 46.32/46.77 b [74, 0] (w:1, o:30, a:1, s:1, b:0),
% 46.32/46.77 c [75, 0] (w:1, o:31, a:1, s:1, b:0),
% 46.32/46.77 'sat_synth_nf_w' [76, 1] (w:1, o:43, a:1, s:1, b:0),
% 46.32/46.77 eq4 [77, 2] (w:1, o:75, a:1, s:1, b:0),
% 46.32/46.77 eq2 [78, 2] (w:1, o:76, a:1, s:1, b:0),
% 46.32/46.77 eq3 [79, 2] (w:1, o:74, a:1, s:1, b:0).
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 15
% 46.32/46.77 maxnrclauses = 10000000
% 46.32/46.77 Generated: 8035
% 46.32/46.77 Kept: 207
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 The strategy used was not complete!
% 46.32/46.77
% 46.32/46.77 Increased maxweight to 16
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 16
% 46.32/46.77 maxnrclauses = 10000000
% 46.32/46.77 Generated: 8314
% 46.32/46.77 Kept: 229
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 The strategy used was not complete!
% 46.32/46.77
% 46.32/46.77 Increased maxweight to 17
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 17
% 46.32/46.77 maxnrclauses = 10000000
% 46.32/46.77 Generated: 10954
% 46.32/46.77 Kept: 290
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 The strategy used was not complete!
% 46.32/46.77
% 46.32/46.77 Increased maxweight to 18
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 18
% 46.32/46.77 maxnrclauses = 10000000
% 46.32/46.77 Generated: 18265
% 46.32/46.77 Kept: 488
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 The strategy used was not complete!
% 46.32/46.77
% 46.32/46.77 Increased maxweight to 19
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 19
% 46.32/46.77 maxnrclauses = 10000000
% 46.32/46.77 Generated: 26923
% 46.32/46.77 Kept: 737
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 The strategy used was not complete!
% 46.32/46.77
% 46.32/46.77 Increased maxweight to 20
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 20
% 46.32/46.77 maxnrclauses = 10000000
% 46.32/46.77 Generated: 48283
% 46.32/46.77 Kept: 1080
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 The strategy used was not complete!
% 46.32/46.77
% 46.32/46.77 Increased maxweight to 21
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 21
% 46.32/46.77 maxnrclauses = 10000000
% 46.32/46.77 Generated: 85391
% 46.32/46.77 Kept: 1838
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 The strategy used was not complete!
% 46.32/46.77
% 46.32/46.77 Increased maxweight to 22
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 Intermediate Status:
% 46.32/46.77 Generated: 43187
% 46.32/46.77 Kept: 2000
% 46.32/46.77 Inuse: 711
% 46.32/46.77 Deleted: 223
% 46.32/46.77 Deletedinuse: 4
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 22
% 46.32/46.77 maxnrclauses = 10000000
% 46.32/46.77 Generated: 183104
% 46.32/46.77 Kept: 3180
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 The strategy used was not complete!
% 46.32/46.77
% 46.32/46.77 Increased maxweight to 23
% 46.32/46.77
% 46.32/46.77 Starting Search:
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 Intermediate Status:
% 46.32/46.77 Generated: 22459
% 46.32/46.77 Kept: 2002
% 46.32/46.77 Inuse: 455
% 46.32/46.77 Deleted: 110
% 46.32/46.77 Deletedinuse: 3
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 Intermediate Status:
% 46.32/46.77 Generated: 77810
% 46.32/46.77 Kept: 4004
% 46.32/46.77 Inuse: 1078
% 46.32/46.77 Deleted: 489
% 46.32/46.77 Deletedinuse: 4
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77
% 46.32/46.77 Intermediate Status:
% 46.32/46.77 Generated: 299431
% 46.32/46.77 Kept: 6005
% 46.32/46.77 Inuse: 3070
% 46.32/46.77 Deleted: 1363
% 46.32/46.77 Deletedinuse: 4
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Resimplifying inuse:
% 46.32/46.77 Done
% 46.32/46.77
% 46.32/46.77 Failed to find proof!
% 46.32/46.77 maxweight = 23
% 91.82/92.27 maxnrclauses = 10000000
% 91.82/92.27 Generated: 462334
% 91.82/92.27 Kept: 7051
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 The strategy used was not complete!
% 91.82/92.27
% 91.82/92.27 Increased maxweight to 24
% 91.82/92.27
% 91.82/92.27 Starting Search:
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 21738
% 91.82/92.27 Kept: 2006
% 91.82/92.27 Inuse: 426
% 91.82/92.27 Deleted: 82
% 91.82/92.27 Deletedinuse: 3
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 43211
% 91.82/92.27 Kept: 4006
% 91.82/92.27 Inuse: 735
% 91.82/92.27 Deleted: 256
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 99254
% 91.82/92.27 Kept: 6011
% 91.82/92.27 Inuse: 1210
% 91.82/92.27 Deleted: 534
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 245672
% 91.82/92.27 Kept: 8218
% 91.82/92.27 Inuse: 2225
% 91.82/92.27 Deleted: 1138
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 374538
% 91.82/92.27 Kept: 10219
% 91.82/92.27 Inuse: 3284
% 91.82/92.27 Deleted: 1687
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 758359
% 91.82/92.27 Kept: 12219
% 91.82/92.27 Inuse: 6739
% 91.82/92.27 Deleted: 3804
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Failed to find proof!
% 91.82/92.27 maxweight = 24
% 91.82/92.27 maxnrclauses = 10000000
% 91.82/92.27 Generated: 1033286
% 91.82/92.27 Kept: 13609
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 The strategy used was not complete!
% 91.82/92.27
% 91.82/92.27 Increased maxweight to 25
% 91.82/92.27
% 91.82/92.27 Starting Search:
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 19468
% 91.82/92.27 Kept: 2005
% 91.82/92.27 Inuse: 388
% 91.82/92.27 Deleted: 69
% 91.82/92.27 Deletedinuse: 3
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 35347
% 91.82/92.27 Kept: 4012
% 91.82/92.27 Inuse: 622
% 91.82/92.27 Deleted: 259
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 57015
% 91.82/92.27 Kept: 6020
% 91.82/92.27 Inuse: 844
% 91.82/92.27 Deleted: 312
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 105500
% 91.82/92.27 Kept: 8020
% 91.82/92.27 Inuse: 1177
% 91.82/92.27 Deleted: 547
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 141066
% 91.82/92.27 Kept: 10020
% 91.82/92.27 Inuse: 1459
% 91.82/92.27 Deleted: 714
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 242629
% 91.82/92.27 Kept: 12040
% 91.82/92.27 Inuse: 1881
% 91.82/92.27 Deleted: 988
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 289041
% 91.82/92.27 Kept: 14041
% 91.82/92.27 Inuse: 2266
% 91.82/92.27 Deleted: 1135
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 398396
% 91.82/92.27 Kept: 16066
% 91.82/92.27 Inuse: 2788
% 91.82/92.27 Deleted: 1591
% 91.82/92.27 Deletedinuse: 4
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 463806
% 91.82/92.27 Kept: 18068
% 91.82/92.27 Inuse: 3257
% 91.82/92.27 Deleted: 1945
% 91.82/92.27 Deletedinuse: 5
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying clauses:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 544605
% 91.82/92.27 Kept: 20083
% 91.82/92.27 Inuse: 3613
% 91.82/92.27 Deleted: 9770
% 91.82/92.27 Deletedinuse: 5
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 613039
% 91.82/92.27 Kept: 22084
% 91.82/92.27 Inuse: 4190
% 91.82/92.27 Deleted: 9778
% 91.82/92.27 Deletedinuse: 11
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 888993
% 91.82/92.27 Kept: 24085
% 91.82/92.27 Inuse: 5595
% 91.82/92.27 Deleted: 9810
% 91.82/92.27 Deletedinuse: 43
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 1282700
% 91.82/92.27 Kept: 26086
% 91.82/92.27 Inuse: 7692
% 91.82/92.27 Deleted: 9906
% 91.82/92.27 Deletedinuse: 43
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 1883311
% 91.82/92.27 Kept: 28086
% 91.82/92.27 Inuse: 11731
% 91.82/92.27 Deleted: 10479
% 91.82/92.27 Deletedinuse: 52
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27
% 91.82/92.27 Intermediate Status:
% 91.82/92.27 Generated: 2658349
% 91.82/92.27 Kept: 30086
% 91.82/92.27 Inuse: 16718
% 91.82/92.27 Deleted: 12659
% 91.82/92.27 Deletedinuse: 121
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Resimplifying inuse:
% 91.82/92.27 Done
% 91.82/92.27
% 91.82/92.27 Failed to find proof!
% 91.82/92.27 maxweight = 25
% 150.41/150.87 maxnrclauses = 10000000
% 150.41/150.87 Generated: 2787668
% 150.41/150.87 Kept: 31136
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 The strategy used was not complete!
% 150.41/150.87
% 150.41/150.87 Increased maxweight to 26
% 150.41/150.87
% 150.41/150.87 Starting Search:
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 19042
% 150.41/150.87 Kept: 2082
% 150.41/150.87 Inuse: 386
% 150.41/150.87 Deleted: 63
% 150.41/150.87 Deletedinuse: 3
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 31766
% 150.41/150.87 Kept: 4124
% 150.41/150.87 Inuse: 571
% 150.41/150.87 Deleted: 189
% 150.41/150.87 Deletedinuse: 4
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 48982
% 150.41/150.87 Kept: 6137
% 150.41/150.87 Inuse: 755
% 150.41/150.87 Deleted: 288
% 150.41/150.87 Deletedinuse: 4
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 76786
% 150.41/150.87 Kept: 8147
% 150.41/150.87 Inuse: 949
% 150.41/150.87 Deleted: 366
% 150.41/150.87 Deletedinuse: 4
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 117592
% 150.41/150.87 Kept: 10154
% 150.41/150.87 Inuse: 1217
% 150.41/150.87 Deleted: 646
% 150.41/150.87 Deletedinuse: 4
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 152345
% 150.41/150.87 Kept: 12155
% 150.41/150.87 Inuse: 1449
% 150.41/150.87 Deleted: 732
% 150.41/150.87 Deletedinuse: 4
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 232964
% 150.41/150.87 Kept: 14160
% 150.41/150.87 Inuse: 1825
% 150.41/150.87 Deleted: 1028
% 150.41/150.87 Deletedinuse: 4
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 300000
% 150.41/150.87 Kept: 16163
% 150.41/150.87 Inuse: 2103
% 150.41/150.87 Deleted: 1076
% 150.41/150.87 Deletedinuse: 4
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 348637
% 150.41/150.87 Kept: 18166
% 150.41/150.87 Inuse: 2450
% 150.41/150.87 Deleted: 1139
% 150.41/150.87 Deletedinuse: 4
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying clauses:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 441337
% 150.41/150.87 Kept: 20172
% 150.41/150.87 Inuse: 2810
% 150.41/150.87 Deleted: 8959
% 150.41/150.87 Deletedinuse: 5
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 513842
% 150.41/150.87 Kept: 22178
% 150.41/150.87 Inuse: 3200
% 150.41/150.87 Deleted: 8959
% 150.41/150.87 Deletedinuse: 5
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 581532
% 150.41/150.87 Kept: 24181
% 150.41/150.87 Inuse: 3585
% 150.41/150.87 Deleted: 8959
% 150.41/150.87 Deletedinuse: 5
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 658550
% 150.41/150.87 Kept: 26197
% 150.41/150.87 Inuse: 3993
% 150.41/150.87 Deleted: 8959
% 150.41/150.87 Deletedinuse: 5
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 920016
% 150.41/150.87 Kept: 28200
% 150.41/150.87 Inuse: 4740
% 150.41/150.87 Deleted: 9446
% 150.41/150.87 Deletedinuse: 5
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 1025571
% 150.41/150.87 Kept: 30201
% 150.41/150.87 Inuse: 5509
% 150.41/150.87 Deleted: 9538
% 150.41/150.87 Deletedinuse: 81
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 1169731
% 150.41/150.87 Kept: 32201
% 150.41/150.87 Inuse: 6554
% 150.41/150.87 Deleted: 9621
% 150.41/150.87 Deletedinuse: 140
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 1520130
% 150.41/150.87 Kept: 34201
% 150.41/150.87 Inuse: 7886
% 150.41/150.87 Deleted: 10046
% 150.41/150.87 Deletedinuse: 205
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 1738114
% 150.41/150.87 Kept: 36202
% 150.41/150.87 Inuse: 9257
% 150.41/150.87 Deleted: 10349
% 150.41/150.87 Deletedinuse: 320
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 2030794
% 150.41/150.87 Kept: 38203
% 150.41/150.87 Inuse: 10314
% 150.41/150.87 Deleted: 10414
% 150.41/150.87 Deletedinuse: 385
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying clauses:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 2340567
% 150.41/150.87 Kept: 40203
% 150.41/150.87 Inuse: 11906
% 150.41/150.87 Deleted: 16264
% 150.41/150.87 Deletedinuse: 385
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 3148179
% 150.41/150.87 Kept: 42203
% 150.41/150.87 Inuse: 15133
% 150.41/150.87 Deleted: 16381
% 150.41/150.87 Deletedinuse: 456
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 3638000
% 150.41/150.87 Kept: 44205
% 150.41/150.87 Inuse: 18285
% 150.41/150.87 Deleted: 16509
% 150.41/150.87 Deletedinuse: 456
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87 Resimplifying inuse:
% 150.41/150.87 Done
% 150.41/150.87
% 150.41/150.87
% 150.41/150.87 Intermediate Status:
% 150.41/150.87 Generated: 3984196
% 150.41/150.87 Kept: 46206
% 150.41/150.87 Inuse: 20059
% 225.83/226.26 Deleted: 17328
% 225.83/226.26 Deletedinuse: 456
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 4863443
% 225.83/226.26 Kept: 48207
% 225.83/226.26 Inuse: 25196
% 225.83/226.26 Deleted: 17398
% 225.83/226.26 Deletedinuse: 456
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 5408632
% 225.83/226.26 Kept: 50207
% 225.83/226.26 Inuse: 29372
% 225.83/226.26 Deleted: 17578
% 225.83/226.26 Deletedinuse: 456
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 6046915
% 225.83/226.26 Kept: 52207
% 225.83/226.26 Inuse: 34378
% 225.83/226.26 Deleted: 17581
% 225.83/226.26 Deletedinuse: 456
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Failed to find proof!
% 225.83/226.26 maxweight = 26
% 225.83/226.26 maxnrclauses = 10000000
% 225.83/226.26 Generated: 6217888
% 225.83/226.26 Kept: 53473
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 The strategy used was not complete!
% 225.83/226.26
% 225.83/226.26 Increased maxweight to 27
% 225.83/226.26
% 225.83/226.26 Starting Search:
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 17479
% 225.83/226.26 Kept: 2006
% 225.83/226.26 Inuse: 362
% 225.83/226.26 Deleted: 41
% 225.83/226.26 Deletedinuse: 3
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 29697
% 225.83/226.26 Kept: 4006
% 225.83/226.26 Inuse: 511
% 225.83/226.26 Deleted: 145
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 42468
% 225.83/226.26 Kept: 6009
% 225.83/226.26 Inuse: 647
% 225.83/226.26 Deleted: 237
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 58620
% 225.83/226.26 Kept: 8014
% 225.83/226.26 Inuse: 789
% 225.83/226.26 Deleted: 302
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 85367
% 225.83/226.26 Kept: 10096
% 225.83/226.26 Inuse: 943
% 225.83/226.26 Deleted: 377
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 109714
% 225.83/226.26 Kept: 12102
% 225.83/226.26 Inuse: 1090
% 225.83/226.26 Deleted: 428
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 148813
% 225.83/226.26 Kept: 14106
% 225.83/226.26 Inuse: 1284
% 225.83/226.26 Deleted: 688
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 176516
% 225.83/226.26 Kept: 16109
% 225.83/226.26 Inuse: 1454
% 225.83/226.26 Deleted: 774
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 235977
% 225.83/226.26 Kept: 18110
% 225.83/226.26 Inuse: 1738
% 225.83/226.26 Deleted: 926
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying clauses:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 297472
% 225.83/226.26 Kept: 20117
% 225.83/226.26 Inuse: 1942
% 225.83/226.26 Deleted: 9467
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 347479
% 225.83/226.26 Kept: 22120
% 225.83/226.26 Inuse: 2185
% 225.83/226.26 Deleted: 9467
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 442813
% 225.83/226.26 Kept: 24123
% 225.83/226.26 Inuse: 2533
% 225.83/226.26 Deleted: 9467
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 618100
% 225.83/226.26 Kept: 26132
% 225.83/226.26 Inuse: 2896
% 225.83/226.26 Deleted: 9557
% 225.83/226.26 Deletedinuse: 4
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 689522
% 225.83/226.26 Kept: 28132
% 225.83/226.26 Inuse: 3141
% 225.83/226.26 Deleted: 9582
% 225.83/226.26 Deletedinuse: 5
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 741266
% 225.83/226.26 Kept: 30143
% 225.83/226.26 Inuse: 3341
% 225.83/226.26 Deleted: 9582
% 225.83/226.26 Deletedinuse: 5
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 815589
% 225.83/226.26 Kept: 32152
% 225.83/226.26 Inuse: 3632
% 225.83/226.26 Deleted: 9582
% 225.83/226.26 Deletedinuse: 5
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 890261
% 225.83/226.26 Kept: 34153
% 225.83/226.26 Inuse: 3826
% 225.83/226.26 Deleted: 9687
% 225.83/226.26 Deletedinuse: 5
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 949907
% 225.83/226.26 Kept: 36164
% 225.83/226.26 Inuse: 4009
% 225.83/226.26 Deleted: 9875
% 225.83/226.26 Deletedinuse: 5
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26 Resimplifying inuse:
% 225.83/226.26 Done
% 225.83/226.26
% 225.83/226.26
% 225.83/226.26 Intermediate Status:
% 225.83/226.26 Generated: 969684
% 225.83/226.26 Kept: 38165
% 225.83/226.26 Inuse: 4196
% 225.83/226.26 Deleted: 9943
% 225.83/226.26 Deletedinuse: 5
% 225.83/226.26
% 225.83/226.26 ResimplTerminated
% 299.65/300.03 Bliksem ended
%------------------------------------------------------------------------------