%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN598-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n012.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 : Thu Jul 21 02:53:15 EDT 2022
% Result : Unsatisfiable 280.20s 280.62s
% Output : Refutation 280.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYN598-1 : TPTP v8.1.0. Released v2.5.0.
% 0.12/0.14 % Command : bliksem %s
% 0.14/0.35 % Computer : n012.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % DateTime : Mon Jul 11 17:03:28 EDT 2022
% 0.14/0.35 % CPUTime :
% 1.93/2.34 *** allocated 10000 integers for termspace/termends
% 1.93/2.34 *** allocated 10000 integers for clauses
% 1.93/2.34 *** allocated 10000 integers for justifications
% 1.93/2.34 Bliksem 1.12
% 1.93/2.34
% 1.93/2.34
% 1.93/2.34 Automatic Strategy Selection
% 1.93/2.34
% 1.93/2.34 Clauses:
% 1.93/2.34 [
% 1.93/2.34 [ p17( c21 ) ],
% 1.93/2.34 [ p18( c21 ) ],
% 1.93/2.34 [ p7( X, X ) ],
% 1.93/2.34 [ p2( X, X ) ],
% 1.93/2.34 [ p3( X, X ) ],
% 1.93/2.34 [ p5( X, X ) ],
% 1.93/2.34 [ p3( f4( f6( c21 ) ), c22 ) ],
% 1.93/2.34 [ p17( X ), ~( p17( Y ) ), ~( p5( Y, X ) ) ],
% 1.93/2.34 [ p18( X ), ~( p18( Y ) ), ~( p5( Y, X ) ) ],
% 1.93/2.34 [ p7( f9( X ), f9( Y ) ), ~( p5( X, Y ) ) ],
% 1.93/2.34 [ p2( f6( X ), f6( Y ) ), ~( p5( X, Y ) ) ],
% 1.93/2.34 [ p3( f12( X ), f12( Y ) ), ~( p3( X, Y ) ) ],
% 1.93/2.34 [ p3( f13( X ), f13( Y ) ), ~( p3( X, Y ) ) ],
% 1.93/2.34 [ p3( f15( X ), f15( Y ) ), ~( p3( X, Y ) ) ],
% 1.93/2.34 [ p3( f16( X ), f16( Y ) ), ~( p3( X, Y ) ) ],
% 1.93/2.34 [ p3( f4( X ), f4( Y ) ), ~( p2( X, Y ) ) ],
% 1.93/2.34 [ p7( f14( X ), f14( Y ) ), ~( p3( X, Y ) ) ],
% 1.93/2.34 [ p7( f8( X ), f8( Y ) ), ~( p7( X, Y ) ) ],
% 1.93/2.34 [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ],
% 1.93/2.34 [ p7( X, Y ), ~( p7( Z, X ) ), ~( p7( Z, Y ) ) ],
% 1.93/2.34 [ p5( X, Y ), ~( p5( Z, X ) ), ~( p5( Z, Y ) ) ],
% 1.93/2.34 [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ],
% 1.93/2.34 [ p19( X, Y ), ~( p7( Z, X ) ), ~( p7( T, Y ) ), ~( p19( Z, T ) ) ],
% 1.93/2.34 [ p20( X, Y ), ~( p7( Z, X ) ), ~( p7( T, Y ) ), ~( p20( Z, T ) ) ],
% 1.93/2.34 [ p7( f11( X, Y ), f11( Z, T ) ), ~( p3( Y, T ) ), ~( p7( X, Z ) ) ]
% 1.93/2.34 ,
% 1.93/2.34 [ p7( f10( X, Y ), f10( Z, T ) ), ~( p7( Y, T ) ), ~( p7( X, Z ) ) ]
% 1.93/2.34 ,
% 1.93/2.34 [ ~( p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), c22 ), f11( f14(
% 1.93/2.34 f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13( f13( f13( c23 )
% 1.93/2.34 ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ) ],
% 1.93/2.34 [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6( X ) ) ), f11(
% 1.93/2.34 f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13( f13( f13(
% 1.93/2.34 c23 ) ) ) ) ) ) ) ) ) ), f8( f9( X ) ) ), ~( p18( X ) ) ],
% 1.93/2.34 [ p20( f8( f9( X ) ), f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f16( f4(
% 1.93/2.34 f6( X ) ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13(
% 1.93/2.34 f13( f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ) ), ~( p18( X ) ) ]
% 1.93/2.34 ] .
% 1.93/2.34
% 1.93/2.34
% 1.93/2.34 percentage equality = 0.000000, percentage horn = 1.000000
% 1.93/2.34 This is a near-Horn, non-equality problem
% 1.93/2.34
% 1.93/2.34
% 1.93/2.34 Options Used:
% 1.93/2.34
% 1.93/2.34 useres = 1
% 1.93/2.34 useparamod = 0
% 1.93/2.34 useeqrefl = 0
% 1.93/2.34 useeqfact = 0
% 1.93/2.34 usefactor = 1
% 1.93/2.34 usesimpsplitting = 0
% 1.93/2.34 usesimpdemod = 0
% 1.93/2.34 usesimpres = 4
% 1.93/2.34
% 1.93/2.34 resimpinuse = 1000
% 1.93/2.34 resimpclauses = 20000
% 1.93/2.34 substype = standard
% 1.93/2.34 backwardsubs = 1
% 1.93/2.34 selectoldest = 5
% 1.93/2.34
% 1.93/2.34 litorderings [0] = split
% 1.93/2.34 litorderings [1] = liftord
% 1.93/2.34
% 1.93/2.34 termordering = none
% 1.93/2.34
% 1.93/2.34 litapriori = 1
% 1.93/2.34 termapriori = 0
% 1.93/2.34 litaposteriori = 0
% 1.93/2.34 termaposteriori = 0
% 1.93/2.34 demodaposteriori = 0
% 1.93/2.34 ordereqreflfact = 0
% 1.93/2.34
% 1.93/2.34 litselect = negative
% 1.93/2.34
% 1.93/2.34 maxweight = 30000
% 1.93/2.34 maxdepth = 30000
% 1.93/2.34 maxlength = 115
% 1.93/2.34 maxnrvars = 195
% 1.93/2.34 excuselevel = 0
% 1.93/2.34 increasemaxweight = 0
% 1.93/2.34
% 1.93/2.34 maxselected = 10000000
% 1.93/2.34 maxnrclauses = 10000000
% 1.93/2.34
% 1.93/2.34 showgenerated = 0
% 1.93/2.34 showkept = 0
% 1.93/2.34 showselected = 0
% 1.93/2.34 showdeleted = 0
% 1.93/2.34 showresimp = 1
% 1.93/2.34 showstatus = 2000
% 1.93/2.34
% 1.93/2.34 prologoutput = 1
% 1.93/2.34 nrgoals = 5000000
% 1.93/2.34 totalproof = 1
% 1.93/2.34
% 1.93/2.34 Symbols occurring in the translation:
% 1.93/2.34
% 1.93/2.34 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.93/2.34 . [1, 2] (w:1, o:79, a:1, s:1, b:0),
% 1.93/2.34 ! [4, 1] (w:1, o:63, a:1, s:1, b:0),
% 1.93/2.34 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.93/2.34 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.93/2.34 c21 [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 1.93/2.34 p17 [40, 1] (w:1, o:68, a:1, s:1, b:0),
% 1.93/2.34 p18 [41, 1] (w:1, o:69, a:1, s:1, b:0),
% 1.93/2.34 p7 [43, 2] (w:1, o:104, a:1, s:1, b:0),
% 1.93/2.34 p2 [45, 2] (w:1, o:106, a:1, s:1, b:0),
% 1.93/2.34 p3 [47, 2] (w:1, o:108, a:1, s:1, b:0),
% 1.93/2.34 p5 [49, 2] (w:1, o:109, a:1, s:1, b:0),
% 1.93/2.34 f6 [50, 1] (w:1, o:70, a:1, s:1, b:0),
% 1.93/2.34 f4 [51, 1] (w:1, o:71, a:1, s:1, b:0),
% 1.93/2.34 c22 [52, 0] (w:1, o:38, a:1, s:1, b:0),
% 1.93/2.34 f9 [58, 1] (w:1, o:73, a:1, s:1, b:0),
% 1.93/2.34 f12 [63, 1] (w:1, o:74, a:1, s:1, b:0),
% 1.93/2.34 f13 [66, 1] (w:1, o:75, a:1, s:1, b:0),
% 1.93/2.34 f15 [69, 1] (w:1, o:77, a:1, s:1, b:0),
% 1.93/2.34 f16 [72, 1] (w:1, o:78, a:1, s:1, b:0),
% 1.93/2.34 f14 [77, 1] (w:1, o:76, a:1, s:1, b:0),
% 5.12/5.48 f8 [80, 1] (w:1, o:72, a:1, s:1, b:0),
% 5.12/5.48 p19 [92, 2] (w:1, o:105, a:1, s:1, b:0),
% 5.12/5.48 p20 [97, 2] (w:1, o:107, a:1, s:1, b:0),
% 5.12/5.48 f11 [102, 2] (w:1, o:111, a:1, s:1, b:0),
% 5.12/5.48 f10 [107, 2] (w:1, o:110, a:1, s:1, b:0),
% 5.12/5.48 c23 [110, 0] (w:1, o:62, a:1, s:1, b:0).
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Starting Search:
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 2289
% 5.12/5.48 Kept: 2005
% 5.12/5.48 Inuse: 284
% 5.12/5.48 Deleted: 0
% 5.12/5.48 Deletedinuse: 0
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 4367
% 5.12/5.48 Kept: 4009
% 5.12/5.48 Inuse: 376
% 5.12/5.48 Deleted: 0
% 5.12/5.48 Deletedinuse: 0
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 6479
% 5.12/5.48 Kept: 6028
% 5.12/5.48 Inuse: 446
% 5.12/5.48 Deleted: 0
% 5.12/5.48 Deletedinuse: 0
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 8549
% 5.12/5.48 Kept: 8055
% 5.12/5.48 Inuse: 499
% 5.12/5.48 Deleted: 0
% 5.12/5.48 Deletedinuse: 0
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 10627
% 5.12/5.48 Kept: 10065
% 5.12/5.48 Inuse: 578
% 5.12/5.48 Deleted: 0
% 5.12/5.48 Deletedinuse: 0
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 12687
% 5.12/5.48 Kept: 12066
% 5.12/5.48 Inuse: 641
% 5.12/5.48 Deleted: 0
% 5.12/5.48 Deletedinuse: 0
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 14848
% 5.12/5.48 Kept: 14166
% 5.12/5.48 Inuse: 701
% 5.12/5.48 Deleted: 0
% 5.12/5.48 Deletedinuse: 0
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 16897
% 5.12/5.48 Kept: 16171
% 5.12/5.48 Inuse: 747
% 5.12/5.48 Deleted: 0
% 5.12/5.48 Deletedinuse: 0
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 18988
% 5.12/5.48 Kept: 18213
% 5.12/5.48 Inuse: 802
% 5.12/5.48 Deleted: 1
% 5.12/5.48 Deletedinuse: 1
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying clauses:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 21202
% 5.12/5.48 Kept: 20391
% 5.12/5.48 Inuse: 841
% 5.12/5.48 Deleted: 4
% 5.12/5.48 Deletedinuse: 4
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 23281
% 5.12/5.48 Kept: 22405
% 5.12/5.48 Inuse: 907
% 5.12/5.48 Deleted: 6
% 5.12/5.48 Deletedinuse: 6
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 25362
% 5.12/5.48 Kept: 24418
% 5.12/5.48 Inuse: 977
% 5.12/5.48 Deleted: 6
% 5.12/5.48 Deletedinuse: 6
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 27411
% 5.12/5.48 Kept: 26441
% 5.12/5.48 Inuse: 1005
% 5.12/5.48 Deleted: 6
% 5.12/5.48 Deletedinuse: 6
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 29488
% 5.12/5.48 Kept: 28477
% 5.12/5.48 Inuse: 1051
% 5.12/5.48 Deleted: 6
% 5.12/5.48 Deletedinuse: 6
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 31785
% 5.12/5.48 Kept: 30728
% 5.12/5.48 Inuse: 1101
% 5.12/5.48 Deleted: 9
% 5.12/5.48 Deletedinuse: 9
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 33819
% 5.12/5.48 Kept: 32733
% 5.12/5.48 Inuse: 1130
% 5.12/5.48 Deleted: 11
% 5.12/5.48 Deletedinuse: 11
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 36142
% 5.12/5.48 Kept: 34999
% 5.12/5.48 Inuse: 1191
% 5.12/5.48 Deleted: 12
% 5.12/5.48 Deletedinuse: 12
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 38183
% 5.12/5.48 Kept: 37003
% 5.12/5.48 Inuse: 1216
% 5.12/5.48 Deleted: 14
% 5.12/5.48 Deletedinuse: 14
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 40227
% 5.12/5.48 Kept: 39018
% 5.12/5.48 Inuse: 1251
% 5.12/5.48 Deleted: 16
% 5.12/5.48 Deletedinuse: 16
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying clauses:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 42286
% 5.12/5.48 Kept: 41026
% 5.12/5.48 Inuse: 1292
% 5.12/5.48 Deleted: 18
% 5.12/5.48 Deletedinuse: 18
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 44321
% 5.12/5.48 Kept: 43044
% 5.12/5.48 Inuse: 1313
% 5.12/5.48 Deleted: 20
% 5.12/5.48 Deletedinuse: 20
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 46531
% 5.12/5.48 Kept: 45202
% 5.12/5.48 Inuse: 1356
% 5.12/5.48 Deleted: 21
% 5.12/5.48 Deletedinuse: 21
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48 Resimplifying inuse:
% 5.12/5.48 Done
% 5.12/5.48
% 5.12/5.48
% 5.12/5.48 Intermediate Status:
% 5.12/5.48 Generated: 48851
% 5.12/5.48 Kept: 47505
% 11.47/11.85 Inuse: 1371
% 11.47/11.85 Deleted: 22
% 11.47/11.85 Deletedinuse: 22
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 51448
% 11.47/11.85 Kept: 49778
% 11.47/11.85 Inuse: 1431
% 11.47/11.85 Deleted: 25
% 11.47/11.85 Deletedinuse: 25
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 53601
% 11.47/11.85 Kept: 51840
% 11.47/11.85 Inuse: 1457
% 11.47/11.85 Deleted: 27
% 11.47/11.85 Deletedinuse: 27
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 55994
% 11.47/11.85 Kept: 54194
% 11.47/11.85 Inuse: 1471
% 11.47/11.85 Deleted: 28
% 11.47/11.85 Deletedinuse: 28
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 58417
% 11.47/11.85 Kept: 56575
% 11.47/11.85 Inuse: 1496
% 11.47/11.85 Deleted: 30
% 11.47/11.85 Deletedinuse: 30
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 60650
% 11.47/11.85 Kept: 58781
% 11.47/11.85 Inuse: 1511
% 11.47/11.85 Deleted: 31
% 11.47/11.85 Deletedinuse: 31
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying clauses:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 62774
% 11.47/11.85 Kept: 60852
% 11.47/11.85 Inuse: 1546
% 11.47/11.85 Deleted: 35
% 11.47/11.85 Deletedinuse: 35
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 64936
% 11.47/11.85 Kept: 62960
% 11.47/11.85 Inuse: 1586
% 11.47/11.85 Deleted: 37
% 11.47/11.85 Deletedinuse: 37
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 67077
% 11.47/11.85 Kept: 65052
% 11.47/11.85 Inuse: 1621
% 11.47/11.85 Deleted: 40
% 11.47/11.85 Deletedinuse: 40
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 69338
% 11.47/11.85 Kept: 67255
% 11.47/11.85 Inuse: 1671
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 71619
% 11.47/11.85 Kept: 69469
% 11.47/11.85 Inuse: 1726
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 73768
% 11.47/11.85 Kept: 71480
% 11.47/11.85 Inuse: 1822
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 75886
% 11.47/11.85 Kept: 73566
% 11.47/11.85 Inuse: 1834
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 77915
% 11.47/11.85 Kept: 75566
% 11.47/11.85 Inuse: 1852
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 80229
% 11.47/11.85 Kept: 77867
% 11.47/11.85 Inuse: 1866
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 82297
% 11.47/11.85 Kept: 79914
% 11.47/11.85 Inuse: 1880
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying clauses:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 84429
% 11.47/11.85 Kept: 82014
% 11.47/11.85 Inuse: 1900
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 86557
% 11.47/11.85 Kept: 84114
% 11.47/11.85 Inuse: 1922
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 88654
% 11.47/11.85 Kept: 86202
% 11.47/11.85 Inuse: 1932
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 90757
% 11.47/11.85 Kept: 88276
% 11.47/11.85 Inuse: 1945
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 92860
% 11.47/11.85 Kept: 90328
% 11.47/11.85 Inuse: 1964
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 94967
% 11.47/11.85 Kept: 92380
% 11.47/11.85 Inuse: 1984
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 97257
% 11.47/11.85 Kept: 94645
% 11.47/11.85 Inuse: 1996
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 99287
% 11.47/11.85 Kept: 96647
% 11.47/11.85 Inuse: 2006
% 11.47/11.85 Deleted: 42
% 11.47/11.85 Deletedinuse: 42
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85 Resimplifying inuse:
% 11.47/11.85 Done
% 11.47/11.85
% 11.47/11.85
% 11.47/11.85 Intermediate Status:
% 11.47/11.85 Generated: 101451
% 11.47/11.85 Kept: 98756
% 22.28/22.71 Inuse: 2028
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying clauses:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 103581
% 22.28/22.71 Kept: 100870
% 22.28/22.71 Inuse: 2037
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 105690
% 22.28/22.71 Kept: 102948
% 22.28/22.71 Inuse: 2048
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 107796
% 22.28/22.71 Kept: 105000
% 22.28/22.71 Inuse: 2066
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 109902
% 22.28/22.71 Kept: 107052
% 22.28/22.71 Inuse: 2084
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 112236
% 22.28/22.71 Kept: 109345
% 22.28/22.71 Inuse: 2101
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 114585
% 22.28/22.71 Kept: 111667
% 22.28/22.71 Inuse: 2111
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 116731
% 22.28/22.71 Kept: 113776
% 22.28/22.71 Inuse: 2126
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 118790
% 22.28/22.71 Kept: 115792
% 22.28/22.71 Inuse: 2150
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 120924
% 22.28/22.71 Kept: 117916
% 22.28/22.71 Inuse: 2162
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 122945
% 22.28/22.71 Kept: 119918
% 22.28/22.71 Inuse: 2173
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying clauses:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 124992
% 22.28/22.71 Kept: 121944
% 22.28/22.71 Inuse: 2195
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 127008
% 22.28/22.71 Kept: 123945
% 22.28/22.71 Inuse: 2203
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 129041
% 22.28/22.71 Kept: 125959
% 22.28/22.71 Inuse: 2225
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 131139
% 22.28/22.71 Kept: 128040
% 22.28/22.71 Inuse: 2233
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 133187
% 22.28/22.71 Kept: 130078
% 22.28/22.71 Inuse: 2245
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 135226
% 22.28/22.71 Kept: 132098
% 22.28/22.71 Inuse: 2265
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 137322
% 22.28/22.71 Kept: 134179
% 22.28/22.71 Inuse: 2273
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 140046
% 22.28/22.71 Kept: 136880
% 22.28/22.71 Inuse: 2296
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 142134
% 22.28/22.71 Kept: 138948
% 22.28/22.71 Inuse: 2306
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 144152
% 22.28/22.71 Kept: 140948
% 22.28/22.71 Inuse: 2328
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying clauses:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 146266
% 22.28/22.71 Kept: 143054
% 22.28/22.71 Inuse: 2336
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 148460
% 22.28/22.71 Kept: 145230
% 22.28/22.71 Inuse: 2346
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 22.28/22.71 Generated: 150648
% 22.28/22.71 Kept: 147401
% 22.28/22.71 Inuse: 2366
% 22.28/22.71 Deleted: 42
% 22.28/22.71 Deletedinuse: 42
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71 Resimplifying inuse:
% 22.28/22.71 Done
% 22.28/22.71
% 22.28/22.71
% 22.28/22.71 Intermediate Status:
% 35.26/35.67 Generated: 153014
% 35.26/35.67 Kept: 149748
% 35.26/35.67 Inuse: 2376
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 155108
% 35.26/35.67 Kept: 151824
% 35.26/35.67 Inuse: 2398
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 157300
% 35.26/35.67 Kept: 154008
% 35.26/35.67 Inuse: 2406
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 159564
% 35.26/35.67 Kept: 156254
% 35.26/35.67 Inuse: 2416
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 161650
% 35.26/35.67 Kept: 158323
% 35.26/35.67 Inuse: 2436
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 164194
% 35.26/35.67 Kept: 160848
% 35.26/35.67 Inuse: 2446
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying clauses:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 166311
% 35.26/35.67 Kept: 162948
% 35.26/35.67 Inuse: 2467
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 168633
% 35.26/35.67 Kept: 165261
% 35.26/35.67 Inuse: 2476
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 170965
% 35.26/35.67 Kept: 167575
% 35.26/35.67 Inuse: 2486
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 173028
% 35.26/35.67 Kept: 169621
% 35.26/35.67 Inuse: 2506
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 175662
% 35.26/35.67 Kept: 172236
% 35.26/35.67 Inuse: 2516
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 177743
% 35.26/35.67 Kept: 174302
% 35.26/35.67 Inuse: 2534
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 180350
% 35.26/35.67 Kept: 176898
% 35.26/35.67 Inuse: 2546
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 182750
% 35.26/35.67 Kept: 179280
% 35.26/35.67 Inuse: 2556
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 184982
% 35.26/35.67 Kept: 181492
% 35.26/35.67 Inuse: 2576
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying clauses:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 187282
% 35.26/35.67 Kept: 183772
% 35.26/35.67 Inuse: 2586
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 189429
% 35.26/35.67 Kept: 185904
% 35.26/35.67 Inuse: 2604
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 191817
% 35.26/35.67 Kept: 188268
% 35.26/35.67 Inuse: 2616
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 194253
% 35.26/35.67 Kept: 190695
% 35.26/35.67 Inuse: 2626
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 196448
% 35.26/35.67 Kept: 192870
% 35.26/35.67 Inuse: 2646
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 198926
% 35.26/35.67 Kept: 195328
% 35.26/35.67 Inuse: 2656
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 201031
% 35.26/35.67 Kept: 197418
% 35.26/35.67 Inuse: 2674
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 203810
% 35.26/35.67 Kept: 200173
% 35.26/35.67 Inuse: 2686
% 35.26/35.67 Deleted: 42
% 35.26/35.67 Deletedinuse: 42
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying inuse:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67 Resimplifying clauses:
% 35.26/35.67 Done
% 35.26/35.67
% 35.26/35.67
% 35.26/35.67 Intermediate Status:
% 35.26/35.67 Generated: 206092
% 35.26/35.67 Kept: 202446
% 61.58/61.95 Inuse: 2696
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 208458
% 61.58/61.95 Kept: 204792
% 61.58/61.95 Inuse: 2716
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 211014
% 61.58/61.95 Kept: 207328
% 61.58/61.95 Inuse: 2726
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 213059
% 61.58/61.95 Kept: 209360
% 61.58/61.95 Inuse: 2742
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 215941
% 61.58/61.95 Kept: 212229
% 61.58/61.95 Inuse: 2756
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 218513
% 61.58/61.95 Kept: 214783
% 61.58/61.95 Inuse: 2766
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 220948
% 61.58/61.95 Kept: 217198
% 61.58/61.95 Inuse: 2786
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 223582
% 61.58/61.95 Kept: 219812
% 61.58/61.95 Inuse: 2796
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying clauses:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 225622
% 61.58/61.95 Kept: 221840
% 61.58/61.95 Inuse: 2810
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 228537
% 61.58/61.95 Kept: 224728
% 61.58/61.95 Inuse: 2826
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 231032
% 61.58/61.95 Kept: 227214
% 61.58/61.95 Inuse: 2836
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 233418
% 61.58/61.95 Kept: 229580
% 61.58/61.95 Inuse: 2856
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 236246
% 61.58/61.95 Kept: 232388
% 61.58/61.95 Inuse: 2866
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 238403
% 61.58/61.95 Kept: 234532
% 61.58/61.95 Inuse: 2882
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 241457
% 61.58/61.95 Kept: 237560
% 61.58/61.95 Inuse: 2896
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 243887
% 61.58/61.95 Kept: 239981
% 61.58/61.95 Inuse: 2906
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying clauses:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 246456
% 61.58/61.95 Kept: 242530
% 61.58/61.95 Inuse: 2926
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 249126
% 61.58/61.95 Kept: 245180
% 61.58/61.95 Inuse: 2936
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 251260
% 61.58/61.95 Kept: 247304
% 61.58/61.95 Inuse: 2948
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 253302
% 61.58/61.95 Kept: 249329
% 61.58/61.95 Inuse: 2964
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 255811
% 61.58/61.95 Kept: 251821
% 61.58/61.95 Inuse: 2971
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 257849
% 61.58/61.95 Kept: 253849
% 61.58/61.95 Inuse: 2983
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 259905
% 61.58/61.95 Kept: 255890
% 61.58/61.95 Inuse: 2997
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 262706
% 61.58/61.95 Kept: 258672
% 61.58/61.95 Inuse: 3006
% 61.58/61.95 Deleted: 42
% 61.58/61.95 Deletedinuse: 42
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95 Resimplifying inuse:
% 61.58/61.95 Done
% 61.58/61.95
% 61.58/61.95
% 61.58/61.95 Intermediate Status:
% 61.58/61.95 Generated: 264906
% 99.83/100.22 Kept: 260860
% 99.83/100.22 Inuse: 3020
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying clauses:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 266988
% 99.83/100.22 Kept: 262927
% 99.83/100.22 Inuse: 3034
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 269565
% 99.83/100.22 Kept: 265487
% 99.83/100.22 Inuse: 3041
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 271607
% 99.83/100.22 Kept: 267516
% 99.83/100.22 Inuse: 3058
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 273691
% 99.83/100.22 Kept: 269579
% 99.83/100.22 Inuse: 3084
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 275833
% 99.83/100.22 Kept: 271701
% 99.83/100.22 Inuse: 3109
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 277917
% 99.83/100.22 Kept: 273764
% 99.83/100.22 Inuse: 3135
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 280001
% 99.83/100.22 Kept: 275827
% 99.83/100.22 Inuse: 3162
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 282085
% 99.83/100.22 Kept: 277890
% 99.83/100.22 Inuse: 3188
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 284169
% 99.83/100.22 Kept: 279953
% 99.83/100.22 Inuse: 3214
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 286253
% 99.83/100.22 Kept: 282016
% 99.83/100.22 Inuse: 3240
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying clauses:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 288326
% 99.83/100.22 Kept: 284070
% 99.83/100.22 Inuse: 3264
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 290410
% 99.83/100.22 Kept: 286133
% 99.83/100.22 Inuse: 3290
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 292494
% 99.83/100.22 Kept: 288196
% 99.83/100.22 Inuse: 3317
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 294578
% 99.83/100.22 Kept: 290259
% 99.83/100.22 Inuse: 3343
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 296789
% 99.83/100.22 Kept: 292449
% 99.83/100.22 Inuse: 3368
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 299708
% 99.83/100.22 Kept: 295347
% 99.83/100.22 Inuse: 3376
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 302637
% 99.83/100.22 Kept: 298267
% 99.83/100.22 Inuse: 3386
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 304682
% 99.83/100.22 Kept: 300292
% 99.83/100.22 Inuse: 3412
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 306797
% 99.83/100.22 Kept: 302386
% 99.83/100.22 Inuse: 3438
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying clauses:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 308912
% 99.83/100.22 Kept: 304480
% 99.83/100.22 Inuse: 3464
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 311027
% 99.83/100.22 Kept: 306574
% 99.83/100.22 Inuse: 3490
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 313142
% 99.83/100.22 Kept: 308668
% 99.83/100.22 Inuse: 3517
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 99.83/100.22 Done
% 99.83/100.22
% 99.83/100.22
% 99.83/100.22 Intermediate Status:
% 99.83/100.22 Generated: 315257
% 99.83/100.22 Kept: 310762
% 99.83/100.22 Inuse: 3543
% 99.83/100.22 Deleted: 42
% 99.83/100.22 Deletedinuse: 42
% 99.83/100.22
% 99.83/100.22 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 317372
% 138.85/139.23 Kept: 312856
% 138.85/139.23 Inuse: 3569
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 319487
% 138.85/139.23 Kept: 314950
% 138.85/139.23 Inuse: 3595
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 321602
% 138.85/139.23 Kept: 317044
% 138.85/139.23 Inuse: 3622
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 323647
% 138.85/139.23 Kept: 319069
% 138.85/139.23 Inuse: 3647
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 325681
% 138.85/139.23 Kept: 321085
% 138.85/139.23 Inuse: 3669
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying clauses:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 327726
% 138.85/139.23 Kept: 323110
% 138.85/139.23 Inuse: 3694
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 329900
% 138.85/139.23 Kept: 325264
% 138.85/139.23 Inuse: 3718
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 333106
% 138.85/139.23 Kept: 328449
% 138.85/139.23 Inuse: 3726
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 336059
% 138.85/139.23 Kept: 331393
% 138.85/139.23 Inuse: 3736
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 338265
% 138.85/139.23 Kept: 333579
% 138.85/139.23 Inuse: 3760
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 341787
% 138.85/139.23 Kept: 337078
% 138.85/139.23 Inuse: 3771
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 344638
% 138.85/139.23 Kept: 339920
% 138.85/139.23 Inuse: 3781
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 346671
% 138.85/139.23 Kept: 341934
% 138.85/139.23 Inuse: 3805
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying clauses:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 348704
% 138.85/139.23 Kept: 343948
% 138.85/139.23 Inuse: 3829
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 350737
% 138.85/139.23 Kept: 345962
% 138.85/139.23 Inuse: 3853
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 352759
% 138.85/139.23 Kept: 347967
% 138.85/139.23 Inuse: 3874
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 354803
% 138.85/139.23 Kept: 349990
% 138.85/139.23 Inuse: 3900
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 356836
% 138.85/139.23 Kept: 352004
% 138.85/139.23 Inuse: 3924
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 359013
% 138.85/139.23 Kept: 354160
% 138.85/139.23 Inuse: 3950
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 361190
% 138.85/139.23 Kept: 356316
% 138.85/139.23 Inuse: 3977
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 363367
% 138.85/139.23 Kept: 358472
% 138.85/139.23 Inuse: 4003
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 365544
% 138.85/139.23 Kept: 360628
% 138.85/139.23 Inuse: 4029
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 367638
% 138.85/139.23 Kept: 362704
% 138.85/139.23 Inuse: 4052
% 138.85/139.23 Deleted: 42
% 138.85/139.23 Deletedinuse: 42
% 138.85/139.23
% 138.85/139.23 Resimplifying clauses:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23 Resimplifying inuse:
% 138.85/139.23 Done
% 138.85/139.23
% 138.85/139.23
% 138.85/139.23 Intermediate Status:
% 138.85/139.23 Generated: 369815
% 201.23/201.65 Kept: 364860
% 201.23/201.65 Inuse: 4078
% 201.23/201.65 Deleted: 42
% 201.23/201.65 Deletedinuse: 42
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65
% 201.23/201.65 Intermediate Status:
% 201.23/201.65 Generated: 371992
% 201.23/201.65 Kept: 367016
% 201.23/201.65 Inuse: 4104
% 201.23/201.65 Deleted: 42
% 201.23/201.65 Deletedinuse: 42
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65
% 201.23/201.65 Intermediate Status:
% 201.23/201.65 Generated: 374169
% 201.23/201.65 Kept: 369172
% 201.23/201.65 Inuse: 4130
% 201.23/201.65 Deleted: 42
% 201.23/201.65 Deletedinuse: 42
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65
% 201.23/201.65 Intermediate Status:
% 201.23/201.65 Generated: 376346
% 201.23/201.65 Kept: 371328
% 201.23/201.65 Inuse: 4157
% 201.23/201.65 Deleted: 42
% 201.23/201.65 Deletedinuse: 42
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65
% 201.23/201.65 Intermediate Status:
% 201.23/201.65 Generated: 378523
% 201.23/201.65 Kept: 373484
% 201.23/201.65 Inuse: 4183
% 201.23/201.65 Deleted: 42
% 201.23/201.65 Deletedinuse: 42
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65
% 201.23/201.65 Intermediate Status:
% 201.23/201.65 Generated: 380556
% 201.23/201.65 Kept: 375498
% 201.23/201.65 Inuse: 4207
% 201.23/201.65 Deleted: 42
% 201.23/201.65 Deletedinuse: 42
% 201.23/201.65
% 201.23/201.65 Resimplifying inuse:
% 201.23/201.65 Done
% 201.23/201.65
% 201.23/201.65
% 201.23/201.65 Intermediate Status:
% 201.23/201.65 Generated: 382589
% 201.23/201.65 Kept: 377512
% 201.23/201.66 Inuse: 4230
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 384766
% 201.23/201.66 Kept: 379668
% 201.23/201.66 Inuse: 4257
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 386810
% 201.23/201.66 Kept: 381691
% 201.23/201.66 Inuse: 4283
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying clauses:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 388915
% 201.23/201.66 Kept: 383776
% 201.23/201.66 Inuse: 4308
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 390948
% 201.23/201.66 Kept: 385790
% 201.23/201.66 Inuse: 4332
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 392981
% 201.23/201.66 Kept: 387804
% 201.23/201.66 Inuse: 4355
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 395158
% 201.23/201.66 Kept: 389960
% 201.23/201.66 Inuse: 4382
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 397335
% 201.23/201.66 Kept: 392116
% 201.23/201.66 Inuse: 4408
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 399368
% 201.23/201.66 Kept: 394130
% 201.23/201.66 Inuse: 4431
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 401738
% 201.23/201.66 Kept: 396484
% 201.23/201.66 Inuse: 4446
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 404154
% 201.23/201.66 Kept: 398885
% 201.23/201.66 Inuse: 4451
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 406296
% 201.23/201.66 Kept: 401021
% 201.23/201.66 Inuse: 4458
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying clauses:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 408333
% 201.23/201.66 Kept: 403048
% 201.23/201.66 Inuse: 4470
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 410395
% 201.23/201.66 Kept: 405091
% 201.23/201.66 Inuse: 4494
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 412457
% 201.23/201.66 Kept: 407134
% 201.23/201.66 Inuse: 4518
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 414665
% 201.23/201.66 Kept: 409321
% 201.23/201.66 Inuse: 4544
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 416873
% 201.23/201.66 Kept: 411508
% 201.23/201.66 Inuse: 4570
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 418997
% 201.23/201.66 Kept: 413614
% 201.23/201.66 Inuse: 4593
% 201.23/201.66 Deleted: 42
% 201.23/201.66 Deletedinuse: 42
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66 Resimplifying inuse:
% 201.23/201.66 Done
% 201.23/201.66
% 201.23/201.66
% 201.23/201.66 Intermediate Status:
% 201.23/201.66 Generated: 421205
% 201.23/201.66 Kept: 415801
% 257.05/257.49 Inuse: 4619
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 423413
% 257.05/257.49 Kept: 417988
% 257.05/257.49 Inuse: 4645
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 425621
% 257.05/257.49 Kept: 420175
% 257.05/257.49 Inuse: 4672
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 427829
% 257.05/257.49 Kept: 422362
% 257.05/257.49 Inuse: 4698
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying clauses:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 429891
% 257.05/257.49 Kept: 424405
% 257.05/257.49 Inuse: 4722
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 431964
% 257.05/257.49 Kept: 426457
% 257.05/257.49 Inuse: 4748
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 434026
% 257.05/257.49 Kept: 428500
% 257.05/257.49 Inuse: 4772
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 436161
% 257.05/257.49 Kept: 430615
% 257.05/257.49 Inuse: 4797
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 438223
% 257.05/257.49 Kept: 432658
% 257.05/257.49 Inuse: 4819
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 442257
% 257.05/257.49 Kept: 436672
% 257.05/257.49 Inuse: 4826
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 444352
% 257.05/257.49 Kept: 438761
% 257.05/257.49 Inuse: 4833
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 446390
% 257.05/257.49 Kept: 440792
% 257.05/257.49 Inuse: 4842
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 448418
% 257.05/257.49 Kept: 442800
% 257.05/257.49 Inuse: 4867
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying clauses:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 450509
% 257.05/257.49 Kept: 444872
% 257.05/257.49 Inuse: 4890
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 452600
% 257.05/257.49 Kept: 446944
% 257.05/257.49 Inuse: 4914
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 454628
% 257.05/257.49 Kept: 448952
% 257.05/257.49 Inuse: 4939
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 456719
% 257.05/257.49 Kept: 451024
% 257.05/257.49 Inuse: 4963
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 458810
% 257.05/257.49 Kept: 453096
% 257.05/257.49 Inuse: 4987
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 460838
% 257.05/257.49 Kept: 455104
% 257.05/257.49 Inuse: 5012
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 462929
% 257.05/257.49 Kept: 457176
% 257.05/257.49 Inuse: 5035
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 465020
% 257.05/257.49 Kept: 459248
% 257.05/257.49 Inuse: 5059
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 467111
% 257.05/257.49 Kept: 461320
% 257.05/257.49 Inuse: 5083
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying clauses:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 469202
% 257.05/257.49 Kept: 463392
% 257.05/257.49 Inuse: 5107
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 257.05/257.49 Generated: 471230
% 257.05/257.49 Kept: 465400
% 257.05/257.49 Inuse: 5132
% 257.05/257.49 Deleted: 42
% 257.05/257.49 Deletedinuse: 42
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49 Resimplifying inuse:
% 257.05/257.49 Done
% 257.05/257.49
% 257.05/257.49
% 257.05/257.49 Intermediate Status:
% 280.20/280.61 Generated: 473384
% 280.20/280.61 Kept: 467536
% 280.20/280.61 Inuse: 5154
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 475412
% 280.20/280.61 Kept: 469544
% 280.20/280.61 Inuse: 5179
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 477440
% 280.20/280.61 Kept: 471552
% 280.20/280.61 Inuse: 5204
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 479531
% 280.20/280.61 Kept: 473624
% 280.20/280.61 Inuse: 5228
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 481622
% 280.20/280.61 Kept: 475696
% 280.20/280.61 Inuse: 5252
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 483776
% 280.20/280.61 Kept: 477832
% 280.20/280.61 Inuse: 5274
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 485804
% 280.20/280.61 Kept: 479840
% 280.20/280.61 Inuse: 5299
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 487895
% 280.20/280.61 Kept: 481912
% 280.20/280.61 Inuse: 5323
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying clauses:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 489986
% 280.20/280.61 Kept: 483984
% 280.20/280.61 Inuse: 5347
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 492077
% 280.20/280.61 Kept: 486056
% 280.20/280.61 Inuse: 5370
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 494168
% 280.20/280.61 Kept: 488128
% 280.20/280.61 Inuse: 5394
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 496196
% 280.20/280.61 Kept: 490136
% 280.20/280.61 Inuse: 5419
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 498224
% 280.20/280.61 Kept: 492144
% 280.20/280.61 Inuse: 5444
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 500315
% 280.20/280.61 Kept: 494216
% 280.20/280.61 Inuse: 5468
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 502406
% 280.20/280.61 Kept: 496288
% 280.20/280.61 Inuse: 5492
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 504497
% 280.20/280.61 Kept: 498360
% 280.20/280.61 Inuse: 5515
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 506588
% 280.20/280.61 Kept: 500432
% 280.20/280.61 Inuse: 5538
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61 Resimplifying inuse:
% 280.20/280.61 Done
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 508768
% 280.20/280.61 Kept: 502602
% 280.20/280.61 Inuse: 5545
% 280.20/280.61 Deleted: 42
% 280.20/280.61 Deletedinuse: 42
% 280.20/280.61
% 280.20/280.61
% 280.20/280.61 Intermediate Status:
% 280.20/280.61 Generated: 511415
% 280.20/280.61 Kept: 505238
% 280.20/280.62 Inuse: 5546
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying clauses:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 513603
% 280.20/280.62 Kept: 507419
% 280.20/280.62 Inuse: 5554
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 515656
% 280.20/280.62 Kept: 509465
% 280.20/280.62 Inuse: 5563
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 517701
% 280.20/280.62 Kept: 511492
% 280.20/280.62 Inuse: 5585
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 519821
% 280.20/280.62 Kept: 513593
% 280.20/280.62 Inuse: 5609
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 521877
% 280.20/280.62 Kept: 515629
% 280.20/280.62 Inuse: 5634
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 523933
% 280.20/280.62 Kept: 517665
% 280.20/280.62 Inuse: 5659
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 525978
% 280.20/280.62 Kept: 519692
% 280.20/280.62 Inuse: 5682
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 528136
% 280.20/280.62 Kept: 521831
% 280.20/280.62 Inuse: 5712
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Intermediate Status:
% 280.20/280.62 Generated: 530286
% 280.20/280.62 Kept: 523961
% 280.20/280.62 Inuse: 5724
% 280.20/280.62 Deleted: 42
% 280.20/280.62 Deletedinuse: 42
% 280.20/280.62
% 280.20/280.62 Resimplifying inuse:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62 Resimplifying clauses:
% 280.20/280.62 Done
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 Bliksems!, er is een bewijs:
% 280.20/280.62 % SZS status Unsatisfiable
% 280.20/280.62 % SZS output start Refutation
% 280.20/280.62
% 280.20/280.62 clause( 1, [ p18( c21 ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 2, [ p7( X, X ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 6, [ p3( f4( f6( c21 ) ), c22 ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 22, [ ~( p7( Z, X ) ), p19( X, Y ), ~( p19( Z, T ) ), ~( p7( T, Y )
% 280.20/280.62 ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 24, [ p7( f11( X, Y ), f11( Z, T ) ), ~( p3( Y, T ) ), ~( p7( X, Z
% 280.20/280.62 ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 25, [ p7( f10( X, Y ), f10( Z, T ) ), ~( p7( X, Z ) ), ~( p7( Y, T
% 280.20/280.62 ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 26, [ ~( p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), c22 ), f11(
% 280.20/280.62 f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13( f13( f13(
% 280.20/280.62 c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 27, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6( X ) )
% 280.20/280.62 ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( X ) ) ), ~( p18( X ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 132, [ p19( Y, Z ), ~( p19( X, Z ) ), ~( p7( X, Y ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 180, [ p7( f11( X, Y ), f11( X, Z ) ), ~( p3( Y, Z ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 210, [ p7( f10( X, Y ), f10( Z, Y ) ), ~( p7( X, Z ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 259, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6( c21
% 280.20/280.62 ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 489, [ p7( f11( X, f4( f6( c21 ) ) ), f11( X, c22 ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 502, [ p7( f10( f11( X, f4( f6( c21 ) ) ), Y ), f10( f11( X, c22 )
% 280.20/280.62 , Y ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 2742, [ p19( f10( f11( X, c22 ), Y ), Z ), ~( p19( f10( f11( X, f4(
% 280.20/280.62 f6( c21 ) ) ), Y ), Z ) ) ] )
% 280.20/280.62 .
% 280.20/280.62 clause( 525453, [] )
% 280.20/280.62 .
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 % SZS output end Refutation
% 280.20/280.62 found a proof!
% 280.20/280.62
% 280.20/280.62 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 280.20/280.62
% 280.20/280.62 initialclauses(
% 280.20/280.62 [ clause( 525455, [ p17( c21 ) ] )
% 280.20/280.62 , clause( 525456, [ p18( c21 ) ] )
% 280.20/280.62 , clause( 525457, [ p7( X, X ) ] )
% 280.20/280.62 , clause( 525458, [ p2( X, X ) ] )
% 280.20/280.62 , clause( 525459, [ p3( X, X ) ] )
% 280.20/280.62 , clause( 525460, [ p5( X, X ) ] )
% 280.20/280.62 , clause( 525461, [ p3( f4( f6( c21 ) ), c22 ) ] )
% 280.20/280.62 , clause( 525462, [ p17( X ), ~( p17( Y ) ), ~( p5( Y, X ) ) ] )
% 280.20/280.62 , clause( 525463, [ p18( X ), ~( p18( Y ) ), ~( p5( Y, X ) ) ] )
% 280.20/280.62 , clause( 525464, [ p7( f9( X ), f9( Y ) ), ~( p5( X, Y ) ) ] )
% 280.20/280.62 , clause( 525465, [ p2( f6( X ), f6( Y ) ), ~( p5( X, Y ) ) ] )
% 280.20/280.62 , clause( 525466, [ p3( f12( X ), f12( Y ) ), ~( p3( X, Y ) ) ] )
% 280.20/280.62 , clause( 525467, [ p3( f13( X ), f13( Y ) ), ~( p3( X, Y ) ) ] )
% 280.20/280.62 , clause( 525468, [ p3( f15( X ), f15( Y ) ), ~( p3( X, Y ) ) ] )
% 280.20/280.62 , clause( 525469, [ p3( f16( X ), f16( Y ) ), ~( p3( X, Y ) ) ] )
% 280.20/280.62 , clause( 525470, [ p3( f4( X ), f4( Y ) ), ~( p2( X, Y ) ) ] )
% 280.20/280.62 , clause( 525471, [ p7( f14( X ), f14( Y ) ), ~( p3( X, Y ) ) ] )
% 280.20/280.62 , clause( 525472, [ p7( f8( X ), f8( Y ) ), ~( p7( X, Y ) ) ] )
% 280.20/280.62 , clause( 525473, [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ] )
% 280.20/280.62 , clause( 525474, [ p7( X, Y ), ~( p7( Z, X ) ), ~( p7( Z, Y ) ) ] )
% 280.20/280.62 , clause( 525475, [ p5( X, Y ), ~( p5( Z, X ) ), ~( p5( Z, Y ) ) ] )
% 280.20/280.62 , clause( 525476, [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ] )
% 280.20/280.62 , clause( 525477, [ p19( X, Y ), ~( p7( Z, X ) ), ~( p7( T, Y ) ), ~( p19(
% 280.20/280.62 Z, T ) ) ] )
% 280.20/280.62 , clause( 525478, [ p20( X, Y ), ~( p7( Z, X ) ), ~( p7( T, Y ) ), ~( p20(
% 280.20/280.62 Z, T ) ) ] )
% 280.20/280.62 , clause( 525479, [ p7( f11( X, Y ), f11( Z, T ) ), ~( p3( Y, T ) ), ~( p7(
% 280.20/280.62 X, Z ) ) ] )
% 280.20/280.62 , clause( 525480, [ p7( f10( X, Y ), f10( Z, T ) ), ~( p7( Y, T ) ), ~( p7(
% 280.20/280.62 X, Z ) ) ] )
% 280.20/280.62 , clause( 525481, [ ~( p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), c22
% 280.20/280.62 ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ) ] )
% 280.20/280.62 , clause( 525482, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6(
% 280.20/280.62 X ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( X ) ) ), ~( p18( X ) ) ]
% 280.20/280.62 )
% 280.20/280.62 , clause( 525483, [ p20( f8( f9( X ) ), f10( f11( f14( f12( f15( f13( c23 )
% 280.20/280.62 ) ) ), f16( f4( f6( X ) ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12(
% 280.20/280.62 f13( f13( f13( f13( f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ) ), ~( p18( X )
% 280.20/280.62 ) ] )
% 280.20/280.62 ] ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 1, [ p18( c21 ) ] )
% 280.20/280.62 , clause( 525456, [ p18( c21 ) ] )
% 280.20/280.62 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 2, [ p7( X, X ) ] )
% 280.20/280.62 , clause( 525457, [ p7( X, X ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 6, [ p3( f4( f6( c21 ) ), c22 ) ] )
% 280.20/280.62 , clause( 525461, [ p3( f4( f6( c21 ) ), c22 ) ] )
% 280.20/280.62 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 22, [ ~( p7( Z, X ) ), p19( X, Y ), ~( p19( Z, T ) ), ~( p7( T, Y )
% 280.20/280.62 ) ] )
% 280.20/280.62 , clause( 525477, [ p19( X, Y ), ~( p7( Z, X ) ), ~( p7( T, Y ) ), ~( p19(
% 280.20/280.62 Z, T ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 280.20/280.62 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2, 3 ), ==>( 3, 2 )] )
% 280.20/280.62 ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 24, [ p7( f11( X, Y ), f11( Z, T ) ), ~( p3( Y, T ) ), ~( p7( X, Z
% 280.20/280.62 ) ) ] )
% 280.20/280.62 , clause( 525479, [ p7( f11( X, Y ), f11( Z, T ) ), ~( p3( Y, T ) ), ~( p7(
% 280.20/280.62 X, Z ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 280.20/280.62 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 25, [ p7( f10( X, Y ), f10( Z, T ) ), ~( p7( X, Z ) ), ~( p7( Y, T
% 280.20/280.62 ) ) ] )
% 280.20/280.62 , clause( 525480, [ p7( f10( X, Y ), f10( Z, T ) ), ~( p7( Y, T ) ), ~( p7(
% 280.20/280.62 X, Z ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 280.20/280.62 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 2 ), ==>( 2, 1 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 26, [ ~( p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), c22 ), f11(
% 280.20/280.62 f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13( f13( f13(
% 280.20/280.62 c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ) ] )
% 280.20/280.62 , clause( 525481, [ ~( p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), c22
% 280.20/280.62 ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ) ] )
% 280.20/280.62 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 27, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6( X ) )
% 280.20/280.62 ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( X ) ) ), ~( p18( X ) ) ] )
% 280.20/280.62 , clause( 525482, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6(
% 280.20/280.62 X ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( X ) ) ), ~( p18( X ) ) ]
% 280.20/280.62 )
% 280.20/280.62 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 280.20/280.62 1 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 resolution(
% 280.20/280.62 clause( 525517, [ ~( p7( X, Y ) ), p19( Y, Z ), ~( p19( X, Z ) ) ] )
% 280.20/280.62 , clause( 22, [ ~( p7( Z, X ) ), p19( X, Y ), ~( p19( Z, T ) ), ~( p7( T, Y
% 280.20/280.62 ) ) ] )
% 280.20/280.62 , 3, clause( 2, [ p7( X, X ) ] )
% 280.20/280.62 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X ), :=( T, Z )] ),
% 280.20/280.62 substitution( 1, [ :=( X, Z )] )).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 132, [ p19( Y, Z ), ~( p19( X, Z ) ), ~( p7( X, Y ) ) ] )
% 280.20/280.62 , clause( 525517, [ ~( p7( X, Y ) ), p19( Y, Z ), ~( p19( X, Z ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 280.20/280.62 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2, 1 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 resolution(
% 280.20/280.62 clause( 525518, [ p7( f11( X, Y ), f11( X, Z ) ), ~( p3( Y, Z ) ) ] )
% 280.20/280.62 , clause( 24, [ p7( f11( X, Y ), f11( Z, T ) ), ~( p3( Y, T ) ), ~( p7( X,
% 280.20/280.62 Z ) ) ] )
% 280.20/280.62 , 2, clause( 2, [ p7( X, X ) ] )
% 280.20/280.62 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, X ), :=( T, Z )] ),
% 280.20/280.62 substitution( 1, [ :=( X, X )] )).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 180, [ p7( f11( X, Y ), f11( X, Z ) ), ~( p3( Y, Z ) ) ] )
% 280.20/280.62 , clause( 525518, [ p7( f11( X, Y ), f11( X, Z ) ), ~( p3( Y, Z ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 280.20/280.62 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 resolution(
% 280.20/280.62 clause( 525520, [ p7( f10( X, Y ), f10( Z, Y ) ), ~( p7( X, Z ) ) ] )
% 280.20/280.62 , clause( 25, [ p7( f10( X, Y ), f10( Z, T ) ), ~( p7( X, Z ) ), ~( p7( Y,
% 280.20/280.62 T ) ) ] )
% 280.20/280.62 , 2, clause( 2, [ p7( X, X ) ] )
% 280.20/280.62 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, Y )] ),
% 280.20/280.62 substitution( 1, [ :=( X, Y )] )).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 210, [ p7( f10( X, Y ), f10( Z, Y ) ), ~( p7( X, Z ) ) ] )
% 280.20/280.62 , clause( 525520, [ p7( f10( X, Y ), f10( Z, Y ) ), ~( p7( X, Z ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 280.20/280.62 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 resolution(
% 280.20/280.62 clause( 525521, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6(
% 280.20/280.62 c21 ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ] )
% 280.20/280.62 , clause( 27, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6( X )
% 280.20/280.62 ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( X ) ) ), ~( p18( X ) ) ] )
% 280.20/280.62 , 1, clause( 1, [ p18( c21 ) ] )
% 280.20/280.62 , 0, substitution( 0, [ :=( X, c21 )] ), substitution( 1, [] )).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 259, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6( c21
% 280.20/280.62 ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ] )
% 280.20/280.62 , clause( 525521, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6(
% 280.20/280.62 c21 ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13(
% 280.20/280.62 f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ] )
% 280.20/280.62 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 resolution(
% 280.20/280.62 clause( 525522, [ p7( f11( X, f4( f6( c21 ) ) ), f11( X, c22 ) ) ] )
% 280.20/280.62 , clause( 180, [ p7( f11( X, Y ), f11( X, Z ) ), ~( p3( Y, Z ) ) ] )
% 280.20/280.62 , 1, clause( 6, [ p3( f4( f6( c21 ) ), c22 ) ] )
% 280.20/280.62 , 0, substitution( 0, [ :=( X, X ), :=( Y, f4( f6( c21 ) ) ), :=( Z, c22 )] )
% 280.20/280.62 , substitution( 1, [] )).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 489, [ p7( f11( X, f4( f6( c21 ) ) ), f11( X, c22 ) ) ] )
% 280.20/280.62 , clause( 525522, [ p7( f11( X, f4( f6( c21 ) ) ), f11( X, c22 ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 resolution(
% 280.20/280.62 clause( 525523, [ p7( f10( f11( X, f4( f6( c21 ) ) ), Y ), f10( f11( X, c22
% 280.20/280.62 ), Y ) ) ] )
% 280.20/280.62 , clause( 210, [ p7( f10( X, Y ), f10( Z, Y ) ), ~( p7( X, Z ) ) ] )
% 280.20/280.62 , 1, clause( 489, [ p7( f11( X, f4( f6( c21 ) ) ), f11( X, c22 ) ) ] )
% 280.20/280.62 , 0, substitution( 0, [ :=( X, f11( X, f4( f6( c21 ) ) ) ), :=( Y, Y ),
% 280.20/280.62 :=( Z, f11( X, c22 ) )] ), substitution( 1, [ :=( X, X )] )).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 502, [ p7( f10( f11( X, f4( f6( c21 ) ) ), Y ), f10( f11( X, c22 )
% 280.20/280.62 , Y ) ) ] )
% 280.20/280.62 , clause( 525523, [ p7( f10( f11( X, f4( f6( c21 ) ) ), Y ), f10( f11( X,
% 280.20/280.62 c22 ), Y ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 280.20/280.62 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 resolution(
% 280.20/280.62 clause( 525524, [ p19( f10( f11( X, c22 ), Y ), Z ), ~( p19( f10( f11( X,
% 280.20/280.62 f4( f6( c21 ) ) ), Y ), Z ) ) ] )
% 280.20/280.62 , clause( 132, [ p19( Y, Z ), ~( p19( X, Z ) ), ~( p7( X, Y ) ) ] )
% 280.20/280.62 , 2, clause( 502, [ p7( f10( f11( X, f4( f6( c21 ) ) ), Y ), f10( f11( X,
% 280.20/280.62 c22 ), Y ) ) ] )
% 280.20/280.62 , 0, substitution( 0, [ :=( X, f10( f11( X, f4( f6( c21 ) ) ), Y ) ), :=( Y
% 280.20/280.62 , f10( f11( X, c22 ), Y ) ), :=( Z, Z )] ), substitution( 1, [ :=( X, X )
% 280.20/280.62 , :=( Y, Y )] )).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 subsumption(
% 280.20/280.62 clause( 2742, [ p19( f10( f11( X, c22 ), Y ), Z ), ~( p19( f10( f11( X, f4(
% 280.20/280.62 f6( c21 ) ) ), Y ), Z ) ) ] )
% 280.20/280.62 , clause( 525524, [ p19( f10( f11( X, c22 ), Y ), Z ), ~( p19( f10( f11( X
% 280.20/280.62 , f4( f6( c21 ) ) ), Y ), Z ) ) ] )
% 280.20/280.62 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 280.20/280.62 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 280.20/280.62
% 280.20/280.62
% 280.20/280.62 resolution(
% 280.20/280.62 clause( 525525, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), c22 ),
% 280.20/280.62 f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13( f13(
% 280.20/280.62 f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ] )
% 280.20/280.62 , clause( 2742, [ p19( f10( f11( X, c22 ), Y ), Z ), ~( p19( f10( f11( X,
% 280.20/280.64 f4( f6( c21 ) ) ), Y ), Z ) ) ] )
% 280.20/280.64 , 1, clause( 259, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), f4( f6(
% 280.20/280.64 c21 ) ) ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13(
% 280.20/280.64 f13( f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ] )
% 280.20/280.64 , 0, substitution( 0, [ :=( X, f14( f12( f15( f13( c23 ) ) ) ) ), :=( Y,
% 280.20/280.64 f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13( f13(
% 280.20/280.64 f13( c23 ) ) ) ) ) ) ) ) ) ), :=( Z, f8( f9( c21 ) ) )] ), substitution(
% 280.20/280.64 1, [] )).
% 280.20/280.64
% 280.20/280.64
% 280.20/280.64 resolution(
% 280.20/280.64 clause( 525526, [] )
% 280.20/280.64 , clause( 26, [ ~( p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), c22 ),
% 280.20/280.64 f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13( f13(
% 280.20/280.64 f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ) ] )
% 280.20/280.64 , 0, clause( 525525, [ p19( f10( f11( f14( f12( f15( f13( c23 ) ) ) ), c22
% 280.20/280.64 ), f11( f14( f12( f15( f13( c23 ) ) ) ), f12( f13( f13( f13( f13( f13(
% 280.20/280.64 f13( f13( c23 ) ) ) ) ) ) ) ) ) ), f8( f9( c21 ) ) ) ] )
% 280.20/280.64 , 0, substitution( 0, [] ), substitution( 1, [] )).
% 280.20/280.64
% 280.20/280.64
% 280.20/280.64 subsumption(
% 280.20/280.64 clause( 525453, [] )
% 280.20/280.64 , clause( 525526, [] )
% 280.20/280.64 , substitution( 0, [] ), permutation( 0, [] ) ).
% 280.20/280.64
% 280.20/280.64
% 280.20/280.64 end.
% 280.20/280.64
% 280.20/280.64 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 280.20/280.64
% 280.20/280.64 Memory use:
% 280.20/280.64
% 280.20/280.64 space for terms: 13483367
% 280.20/280.64 space for clauses: 63217019
% 280.20/280.64
% 280.20/280.64
% 280.20/280.64 clauses generated: 532382
% 280.20/280.64 clauses kept: 525454
% 280.20/280.64 clauses selected: 5753
% 280.20/280.64 clauses deleted: 42
% 280.20/280.64 clauses inuse deleted: 42
% 280.20/280.64
% 280.20/280.64 subsentry: 8570439
% 280.20/280.64 literals s-matched: 7779671
% 280.20/280.64 literals matched: 7779670
% 280.20/280.64 full subsumption: 6418
% 280.20/280.64
% 280.20/280.64 checksum: 837648534
% 280.20/280.64
% 280.20/280.64
% 280.20/280.64 Bliksem ended
%------------------------------------------------------------------------------