%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN606-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n014.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:19 EDT 2022
% Result : Unsatisfiable 250.09s 250.59s
% Output : Refutation 250.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN606-1 : TPTP v8.1.0. Released v2.5.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n014.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Mon Jul 11 16:00:19 EDT 2022
% 0.13/0.34 % CPUTime :
% 2.02/2.38 *** allocated 10000 integers for termspace/termends
% 2.02/2.38 *** allocated 10000 integers for clauses
% 2.02/2.38 *** allocated 10000 integers for justifications
% 2.02/2.38 Bliksem 1.12
% 2.02/2.38
% 2.02/2.38
% 2.02/2.38 Automatic Strategy Selection
% 2.02/2.38
% 2.02/2.38 Clauses:
% 2.02/2.38 [
% 2.02/2.38 [ ~( p16( c21 ) ) ],
% 2.02/2.38 [ p2( X, X ) ],
% 2.02/2.38 [ p5( X, X ) ],
% 2.02/2.38 [ p3( X, X ) ],
% 2.02/2.38 [ ~( p5( c21, f7( c20 ) ) ) ],
% 2.02/2.38 [ p3( f12( c22, c21 ), f15( c22 ) ) ],
% 2.02/2.38 [ p3( f12( f15( c22 ), c21 ), c22 ) ],
% 2.02/2.38 [ ~( p3( c19, f4( f6( f7( c20 ) ) ) ) ) ],
% 2.02/2.38 [ p16( X ), ~( p16( Y ) ), ~( p5( Y, X ) ) ],
% 2.02/2.38 [ p5( f8( X ), f8( Y ) ), ~( p5( X, Y ) ) ],
% 2.02/2.38 [ p2( f6( X ), f6( Y ) ), ~( p5( X, Y ) ) ],
% 2.02/2.38 [ p2( f9( X ), f9( Y ) ), ~( p3( X, Y ) ) ],
% 2.02/2.38 [ p3( f13( X ), f13( Y ) ), ~( p5( X, Y ) ) ],
% 2.02/2.38 [ p3( f15( X ), f15( Y ) ), ~( p3( X, Y ) ) ],
% 2.02/2.38 [ p3( f4( X ), f4( Y ) ), ~( p2( X, Y ) ) ],
% 2.02/2.38 [ p5( f7( X ), f7( Y ) ), ~( p5( X, Y ) ) ],
% 2.02/2.38 [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ],
% 2.02/2.38 [ p5( X, Y ), ~( p5( Z, X ) ), ~( p5( Z, Y ) ) ],
% 2.02/2.38 [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ],
% 2.02/2.38 [ p17( X, Y ), ~( p2( Z, X ) ), ~( p2( T, Y ) ), ~( p17( Z, T ) ) ],
% 2.02/2.38 [ p18( X, Y ), ~( p5( Z, X ) ), ~( p5( T, Y ) ), ~( p18( Z, T ) ) ],
% 2.02/2.38 [ p3( f12( f4( f6( f7( f8( c20 ) ) ) ), c21 ), f4( f6( f7( f8( c20 ) ) )
% 2.02/2.38 ) ) ],
% 2.02/2.38 [ p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), c22 ) ), f6( f7( f8( c20 )
% 2.02/2.38 ) ) ) ],
% 2.02/2.38 [ p3( f14( X, Y ), f14( Z, T ) ), ~( p3( X, Z ) ), ~( p3( Y, T ) ) ]
% 2.02/2.38 ,
% 2.02/2.38 [ p3( f10( X, Y ), f10( Z, T ) ), ~( p3( X, Z ) ), ~( p3( Y, T ) ) ]
% 2.02/2.38 ,
% 2.02/2.38 [ p3( f11( X, Y ), f11( Z, T ) ), ~( p3( X, Z ) ), ~( p3( Y, T ) ) ]
% 2.02/2.38 ,
% 2.02/2.38 [ p3( f12( X, Y ), f12( Z, T ) ), ~( p3( X, Z ) ), ~( p5( Y, T ) ) ]
% 2.02/2.38 ,
% 2.02/2.38 [ p3( f12( f15( f4( f6( f7( f8( c20 ) ) ) ) ), c21 ), f15( f4( f6( f7(
% 2.02/2.38 f8( c20 ) ) ) ) ) ) ],
% 2.02/2.38 [ ~( p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), f12( X, c21 ) ) ), f6(
% 2.02/2.38 f7( f8( c20 ) ) ) ) ) ],
% 2.02/2.38 [ p5( X, f7( c20 ) ), p3( c19, f4( f6( f7( c20 ) ) ) ), p17( f9( f10( f4(
% 2.02/2.38 f6( f7( f8( c20 ) ) ) ), f11( c19, f12( f13( X ), X ) ) ) ), f6( f7( f8(
% 2.02/2.38 c20 ) ) ) ), ~( p18( X, c21 ) ) ]
% 2.02/2.38 ] .
% 2.02/2.38
% 2.02/2.38
% 2.02/2.38 percentage equality = 0.000000, percentage horn = 0.966667
% 2.02/2.38 This is a near-Horn, non-equality problem
% 2.02/2.38
% 2.02/2.38
% 2.02/2.38 Options Used:
% 2.02/2.38
% 2.02/2.38 useres = 1
% 2.02/2.38 useparamod = 0
% 2.02/2.38 useeqrefl = 0
% 2.02/2.38 useeqfact = 0
% 2.02/2.38 usefactor = 1
% 2.02/2.38 usesimpsplitting = 0
% 2.02/2.38 usesimpdemod = 0
% 2.02/2.38 usesimpres = 4
% 2.02/2.38
% 2.02/2.38 resimpinuse = 1000
% 2.02/2.38 resimpclauses = 20000
% 2.02/2.38 substype = standard
% 2.02/2.38 backwardsubs = 1
% 2.02/2.38 selectoldest = 5
% 2.02/2.38
% 2.02/2.38 litorderings [0] = split
% 2.02/2.38 litorderings [1] = liftord
% 2.02/2.38
% 2.02/2.38 termordering = none
% 2.02/2.38
% 2.02/2.38 litapriori = 1
% 2.02/2.38 termapriori = 0
% 2.02/2.38 litaposteriori = 0
% 2.02/2.38 termaposteriori = 0
% 2.02/2.38 demodaposteriori = 0
% 2.02/2.38 ordereqreflfact = 0
% 2.02/2.38
% 2.02/2.38 litselect = negative
% 2.02/2.38
% 2.02/2.38 maxweight = 30000
% 2.02/2.38 maxdepth = 30000
% 2.02/2.38 maxlength = 115
% 2.02/2.38 maxnrvars = 195
% 2.02/2.38 excuselevel = 0
% 2.02/2.38 increasemaxweight = 0
% 2.02/2.38
% 2.02/2.38 maxselected = 10000000
% 2.02/2.38 maxnrclauses = 10000000
% 2.02/2.38
% 2.02/2.38 showgenerated = 0
% 2.02/2.38 showkept = 0
% 2.02/2.38 showselected = 0
% 2.02/2.38 showdeleted = 0
% 2.02/2.38 showresimp = 1
% 2.02/2.38 showstatus = 2000
% 2.02/2.38
% 2.02/2.38 prologoutput = 1
% 2.02/2.38 nrgoals = 5000000
% 2.02/2.38 totalproof = 1
% 2.02/2.38
% 2.02/2.38 Symbols occurring in the translation:
% 2.02/2.38
% 2.02/2.38 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.02/2.38 . [1, 2] (w:1, o:77, a:1, s:1, b:0),
% 2.02/2.38 ! [4, 1] (w:1, o:64, a:1, s:1, b:0),
% 2.02/2.38 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.02/2.38 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.02/2.38 c21 [39, 0] (w:1, o:11, a:1, s:1, b:0),
% 2.02/2.38 p16 [40, 1] (w:1, o:69, a:1, s:1, b:0),
% 2.02/2.38 p2 [42, 2] (w:1, o:104, a:1, s:1, b:0),
% 2.02/2.38 p5 [44, 2] (w:1, o:105, a:1, s:1, b:0),
% 2.02/2.38 p3 [46, 2] (w:1, o:106, a:1, s:1, b:0),
% 2.02/2.38 c20 [47, 0] (w:1, o:10, a:1, s:1, b:0),
% 2.02/2.38 f7 [48, 1] (w:1, o:71, a:1, s:1, b:0),
% 2.02/2.38 c22 [49, 0] (w:1, o:41, a:1, s:1, b:0),
% 2.02/2.38 f12 [50, 2] (w:1, o:108, a:1, s:1, b:0),
% 2.02/2.38 f15 [51, 1] (w:1, o:72, a:1, s:1, b:0),
% 2.02/2.38 c19 [52, 0] (w:1, o:9, a:1, s:1, b:0),
% 2.02/2.38 f6 [53, 1] (w:1, o:70, a:1, s:1, b:0),
% 2.02/2.38 f4 [54, 1] (w:1, o:73, a:1, s:1, b:0),
% 2.02/2.38 f8 [58, 1] (w:1, o:74, a:1, s:1, b:0),
% 2.02/2.38 f9 [63, 1] (w:1, o:75, a:1, s:1, b:0),
% 2.02/2.38 f13 [66, 1] (w:1, o:76, a:1, s:1, b:0),
% 2.02/2.38 p17 [82, 2] (w:1, o:102, a:1, s:1, b:0),
% 4.22/4.66 p18 [87, 2] (w:1, o:103, a:1, s:1, b:0),
% 4.22/4.66 f14 [90, 2] (w:1, o:109, a:1, s:1, b:0),
% 4.22/4.66 f10 [91, 2] (w:1, o:110, a:1, s:1, b:0),
% 4.22/4.66 f11 [102, 2] (w:1, o:107, a:1, s:1, b:0).
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Starting Search:
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 2264
% 4.22/4.66 Kept: 2009
% 4.22/4.66 Inuse: 231
% 4.22/4.66 Deleted: 0
% 4.22/4.66 Deletedinuse: 0
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 4409
% 4.22/4.66 Kept: 4015
% 4.22/4.66 Inuse: 324
% 4.22/4.66 Deleted: 0
% 4.22/4.66 Deletedinuse: 0
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 6480
% 4.22/4.66 Kept: 6045
% 4.22/4.66 Inuse: 361
% 4.22/4.66 Deleted: 0
% 4.22/4.66 Deletedinuse: 0
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 8560
% 4.22/4.66 Kept: 8069
% 4.22/4.66 Inuse: 407
% 4.22/4.66 Deleted: 0
% 4.22/4.66 Deletedinuse: 0
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 10864
% 4.22/4.66 Kept: 10138
% 4.22/4.66 Inuse: 475
% 4.22/4.66 Deleted: 4
% 4.22/4.66 Deletedinuse: 4
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 12980
% 4.22/4.66 Kept: 12142
% 4.22/4.66 Inuse: 508
% 4.22/4.66 Deleted: 8
% 4.22/4.66 Deletedinuse: 8
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 15201
% 4.22/4.66 Kept: 14314
% 4.22/4.66 Inuse: 531
% 4.22/4.66 Deleted: 8
% 4.22/4.66 Deletedinuse: 8
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 17248
% 4.22/4.66 Kept: 16315
% 4.22/4.66 Inuse: 552
% 4.22/4.66 Deleted: 8
% 4.22/4.66 Deletedinuse: 8
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 19330
% 4.22/4.66 Kept: 18360
% 4.22/4.66 Inuse: 573
% 4.22/4.66 Deleted: 8
% 4.22/4.66 Deletedinuse: 8
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying clauses:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 21401
% 4.22/4.66 Kept: 20387
% 4.22/4.66 Inuse: 595
% 4.22/4.66 Deleted: 288
% 4.22/4.66 Deletedinuse: 8
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 23455
% 4.22/4.66 Kept: 22406
% 4.22/4.66 Inuse: 615
% 4.22/4.66 Deleted: 288
% 4.22/4.66 Deletedinuse: 8
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 25819
% 4.22/4.66 Kept: 24449
% 4.22/4.66 Inuse: 642
% 4.22/4.66 Deleted: 288
% 4.22/4.66 Deletedinuse: 8
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 28181
% 4.22/4.66 Kept: 26769
% 4.22/4.66 Inuse: 661
% 4.22/4.66 Deleted: 294
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 30605
% 4.22/4.66 Kept: 29061
% 4.22/4.66 Inuse: 679
% 4.22/4.66 Deleted: 296
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 32703
% 4.22/4.66 Kept: 31104
% 4.22/4.66 Inuse: 694
% 4.22/4.66 Deleted: 296
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 34875
% 4.22/4.66 Kept: 33224
% 4.22/4.66 Inuse: 709
% 4.22/4.66 Deleted: 296
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 37113
% 4.22/4.66 Kept: 35416
% 4.22/4.66 Inuse: 724
% 4.22/4.66 Deleted: 296
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 39259
% 4.22/4.66 Kept: 37478
% 4.22/4.66 Inuse: 741
% 4.22/4.66 Deleted: 296
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 41361
% 4.22/4.66 Kept: 39485
% 4.22/4.66 Inuse: 768
% 4.22/4.66 Deleted: 304
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying clauses:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 43741
% 4.22/4.66 Kept: 41821
% 4.22/4.66 Inuse: 791
% 4.22/4.66 Deleted: 580
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 46104
% 4.22/4.66 Kept: 44148
% 4.22/4.66 Inuse: 806
% 4.22/4.66 Deleted: 580
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 48365
% 4.22/4.66 Kept: 46381
% 4.22/4.66 Inuse: 821
% 4.22/4.66 Deleted: 580
% 4.22/4.66 Deletedinuse: 14
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66 Resimplifying inuse:
% 4.22/4.66 Done
% 4.22/4.66
% 4.22/4.66
% 4.22/4.66 Intermediate Status:
% 4.22/4.66 Generated: 50754
% 4.22/4.66 Kept: 48742
% 4.22/4.66 Inuse: 836
% 4.22/4.66 Deleted: 580
% 4.22/4.66 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 52798
% 12.11/12.46 Kept: 50755
% 12.11/12.46 Inuse: 860
% 12.11/12.46 Deleted: 580
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 54894
% 12.11/12.46 Kept: 52803
% 12.11/12.46 Inuse: 886
% 12.11/12.46 Deleted: 580
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 57008
% 12.11/12.46 Kept: 54890
% 12.11/12.46 Inuse: 900
% 12.11/12.46 Deleted: 580
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 59304
% 12.11/12.46 Kept: 57168
% 12.11/12.46 Inuse: 911
% 12.11/12.46 Deleted: 580
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 61434
% 12.11/12.46 Kept: 59254
% 12.11/12.46 Inuse: 929
% 12.11/12.46 Deleted: 580
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying clauses:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 63517
% 12.11/12.46 Kept: 61312
% 12.11/12.46 Inuse: 940
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 65585
% 12.11/12.46 Kept: 63327
% 12.11/12.46 Inuse: 955
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 67815
% 12.11/12.46 Kept: 65487
% 12.11/12.46 Inuse: 976
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 70313
% 12.11/12.46 Kept: 67946
% 12.11/12.46 Inuse: 996
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 72455
% 12.11/12.46 Kept: 70072
% 12.11/12.46 Inuse: 1006
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 74493
% 12.11/12.46 Kept: 72082
% 12.11/12.46 Inuse: 1024
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 76592
% 12.11/12.46 Kept: 74148
% 12.11/12.46 Inuse: 1035
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 79251
% 12.11/12.46 Kept: 76774
% 12.11/12.46 Inuse: 1046
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 81517
% 12.11/12.46 Kept: 79015
% 12.11/12.46 Inuse: 1056
% 12.11/12.46 Deleted: 597
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying clauses:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 83819
% 12.11/12.46 Kept: 81297
% 12.11/12.46 Inuse: 1066
% 12.11/12.46 Deleted: 605
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 86147
% 12.11/12.46 Kept: 83579
% 12.11/12.46 Inuse: 1076
% 12.11/12.46 Deleted: 605
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 88507
% 12.11/12.46 Kept: 85889
% 12.11/12.46 Inuse: 1086
% 12.11/12.46 Deleted: 605
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 90555
% 12.11/12.46 Kept: 87917
% 12.11/12.46 Inuse: 1097
% 12.11/12.46 Deleted: 605
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 92607
% 12.11/12.46 Kept: 89951
% 12.11/12.46 Inuse: 1107
% 12.11/12.46 Deleted: 605
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 94700
% 12.11/12.46 Kept: 92018
% 12.11/12.46 Inuse: 1118
% 12.11/12.46 Deleted: 605
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 96793
% 12.11/12.46 Kept: 94090
% 12.11/12.46 Inuse: 1128
% 12.11/12.46 Deleted: 605
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 98893
% 12.11/12.46 Kept: 96167
% 12.11/12.46 Inuse: 1137
% 12.11/12.46 Deleted: 605
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 100989
% 12.11/12.46 Kept: 98223
% 12.11/12.46 Inuse: 1156
% 12.11/12.46 Deleted: 606
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46 Resimplifying inuse:
% 12.11/12.46 Done
% 12.11/12.46
% 12.11/12.46
% 12.11/12.46 Intermediate Status:
% 12.11/12.46 Generated: 103103
% 12.11/12.46 Kept: 100308
% 12.11/12.46 Inuse: 1177
% 12.11/12.46 Deleted: 606
% 12.11/12.46 Deletedinuse: 14
% 12.11/12.46
% 12.11/12.46 Resimplifying clauses:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 105239
% 31.46/31.84 Kept: 102416
% 31.46/31.84 Inuse: 1199
% 31.46/31.84 Deleted: 611
% 31.46/31.84 Deletedinuse: 14
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 107347
% 31.46/31.84 Kept: 104501
% 31.46/31.84 Inuse: 1220
% 31.46/31.84 Deleted: 611
% 31.46/31.84 Deletedinuse: 14
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 109388
% 31.46/31.84 Kept: 106511
% 31.46/31.84 Inuse: 1236
% 31.46/31.84 Deleted: 611
% 31.46/31.84 Deletedinuse: 14
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 111545
% 31.46/31.84 Kept: 108639
% 31.46/31.84 Inuse: 1252
% 31.46/31.84 Deleted: 611
% 31.46/31.84 Deletedinuse: 14
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 113706
% 31.46/31.84 Kept: 110767
% 31.46/31.84 Inuse: 1268
% 31.46/31.84 Deleted: 611
% 31.46/31.84 Deletedinuse: 14
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 115807
% 31.46/31.84 Kept: 112847
% 31.46/31.84 Inuse: 1282
% 31.46/31.84 Deleted: 611
% 31.46/31.84 Deletedinuse: 14
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 118277
% 31.46/31.84 Kept: 115304
% 31.46/31.84 Inuse: 1290
% 31.46/31.84 Deleted: 611
% 31.46/31.84 Deletedinuse: 14
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 120386
% 31.46/31.84 Kept: 117390
% 31.46/31.84 Inuse: 1302
% 31.46/31.84 Deleted: 612
% 31.46/31.84 Deletedinuse: 15
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 122896
% 31.46/31.84 Kept: 119878
% 31.46/31.84 Inuse: 1310
% 31.46/31.84 Deleted: 612
% 31.46/31.84 Deletedinuse: 15
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying clauses:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 124919
% 31.46/31.84 Kept: 121885
% 31.46/31.84 Inuse: 1322
% 31.46/31.84 Deleted: 617
% 31.46/31.84 Deletedinuse: 16
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 127221
% 31.46/31.84 Kept: 124178
% 31.46/31.84 Inuse: 1330
% 31.46/31.84 Deleted: 617
% 31.46/31.84 Deletedinuse: 16
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 130081
% 31.46/31.84 Kept: 126192
% 31.46/31.84 Inuse: 1359
% 31.46/31.84 Deleted: 619
% 31.46/31.84 Deletedinuse: 17
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 132282
% 31.46/31.84 Kept: 128322
% 31.46/31.84 Inuse: 1374
% 31.46/31.84 Deleted: 619
% 31.46/31.84 Deletedinuse: 17
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 134481
% 31.46/31.84 Kept: 130452
% 31.46/31.84 Inuse: 1389
% 31.46/31.84 Deleted: 619
% 31.46/31.84 Deletedinuse: 17
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 136680
% 31.46/31.84 Kept: 132582
% 31.46/31.84 Inuse: 1404
% 31.46/31.84 Deleted: 619
% 31.46/31.84 Deletedinuse: 17
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 138888
% 31.46/31.84 Kept: 134712
% 31.46/31.84 Inuse: 1419
% 31.46/31.84 Deleted: 619
% 31.46/31.84 Deletedinuse: 17
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 141073
% 31.46/31.84 Kept: 136842
% 31.46/31.84 Inuse: 1434
% 31.46/31.84 Deleted: 619
% 31.46/31.84 Deletedinuse: 17
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 143167
% 31.46/31.84 Kept: 138905
% 31.46/31.84 Inuse: 1453
% 31.46/31.84 Deleted: 619
% 31.46/31.84 Deletedinuse: 17
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying clauses:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 146122
% 31.46/31.84 Kept: 141831
% 31.46/31.84 Inuse: 1464
% 31.46/31.84 Deleted: 623
% 31.46/31.84 Deletedinuse: 17
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 148186
% 31.46/31.84 Kept: 143871
% 31.46/31.84 Inuse: 1477
% 31.46/31.84 Deleted: 625
% 31.46/31.84 Deletedinuse: 19
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 150280
% 31.46/31.84 Kept: 145931
% 31.46/31.84 Inuse: 1493
% 31.46/31.84 Deleted: 625
% 31.46/31.84 Deletedinuse: 19
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 152428
% 31.46/31.84 Kept: 148051
% 31.46/31.84 Inuse: 1513
% 31.46/31.84 Deleted: 625
% 31.46/31.84 Deletedinuse: 19
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 154545
% 31.46/31.84 Kept: 150141
% 31.46/31.84 Inuse: 1531
% 31.46/31.84 Deleted: 625
% 31.46/31.84 Deletedinuse: 19
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84 Resimplifying inuse:
% 31.46/31.84 Done
% 31.46/31.84
% 31.46/31.84
% 31.46/31.84 Intermediate Status:
% 31.46/31.84 Generated: 156692
% 31.46/31.84 Kept: 152261
% 31.46/31.84 Inuse: 1551
% 51.42/51.84 Deleted: 625
% 51.42/51.84 Deletedinuse: 19
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 158803
% 51.42/51.84 Kept: 154336
% 51.42/51.84 Inuse: 1568
% 51.42/51.84 Deleted: 625
% 51.42/51.84 Deletedinuse: 19
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 161914
% 51.42/51.84 Kept: 157379
% 51.42/51.84 Inuse: 1599
% 51.42/51.84 Deleted: 625
% 51.42/51.84 Deletedinuse: 19
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 164641
% 51.42/51.84 Kept: 160078
% 51.42/51.84 Inuse: 1609
% 51.42/51.84 Deleted: 627
% 51.42/51.84 Deletedinuse: 21
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying clauses:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 166983
% 51.42/51.84 Kept: 162370
% 51.42/51.84 Inuse: 1629
% 51.42/51.84 Deleted: 628
% 51.42/51.84 Deletedinuse: 22
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 169762
% 51.42/51.84 Kept: 165127
% 51.42/51.84 Inuse: 1639
% 51.42/51.84 Deleted: 630
% 51.42/51.84 Deletedinuse: 24
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 172772
% 51.42/51.84 Kept: 168118
% 51.42/51.84 Inuse: 1659
% 51.42/51.84 Deleted: 631
% 51.42/51.84 Deletedinuse: 25
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 174802
% 51.42/51.84 Kept: 170139
% 51.42/51.84 Inuse: 1666
% 51.42/51.84 Deleted: 633
% 51.42/51.84 Deletedinuse: 27
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 176843
% 51.42/51.84 Kept: 172162
% 51.42/51.84 Inuse: 1673
% 51.42/51.84 Deleted: 634
% 51.42/51.84 Deletedinuse: 28
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 179700
% 51.42/51.84 Kept: 174996
% 51.42/51.84 Inuse: 1689
% 51.42/51.84 Deleted: 634
% 51.42/51.84 Deletedinuse: 28
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 181764
% 51.42/51.84 Kept: 177016
% 51.42/51.84 Inuse: 1696
% 51.42/51.84 Deleted: 634
% 51.42/51.84 Deletedinuse: 28
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 183842
% 51.42/51.84 Kept: 179059
% 51.42/51.84 Inuse: 1704
% 51.42/51.84 Deleted: 634
% 51.42/51.84 Deletedinuse: 28
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 186314
% 51.42/51.84 Kept: 181505
% 51.42/51.84 Inuse: 1719
% 51.42/51.84 Deleted: 634
% 51.42/51.84 Deletedinuse: 28
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying clauses:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 189238
% 51.42/51.84 Kept: 184405
% 51.42/51.84 Inuse: 1729
% 51.42/51.84 Deleted: 637
% 51.42/51.84 Deletedinuse: 28
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 192266
% 51.42/51.84 Kept: 187408
% 51.42/51.84 Inuse: 1749
% 51.42/51.84 Deleted: 637
% 51.42/51.84 Deletedinuse: 28
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 194422
% 51.42/51.84 Kept: 189546
% 51.42/51.84 Inuse: 1758
% 51.42/51.84 Deleted: 639
% 51.42/51.84 Deletedinuse: 30
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 196596
% 51.42/51.84 Kept: 191703
% 51.42/51.84 Inuse: 1768
% 51.42/51.84 Deleted: 640
% 51.42/51.84 Deletedinuse: 31
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 198782
% 51.42/51.84 Kept: 193879
% 51.42/51.84 Inuse: 1779
% 51.42/51.84 Deleted: 640
% 51.42/51.84 Deletedinuse: 31
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 200805
% 51.42/51.84 Kept: 195885
% 51.42/51.84 Inuse: 1787
% 51.42/51.84 Deleted: 642
% 51.42/51.84 Deletedinuse: 33
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 202976
% 51.42/51.84 Kept: 198044
% 51.42/51.84 Inuse: 1795
% 51.42/51.84 Deleted: 643
% 51.42/51.84 Deletedinuse: 34
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 205701
% 51.42/51.84 Kept: 200746
% 51.42/51.84 Inuse: 1809
% 51.42/51.84 Deleted: 643
% 51.42/51.84 Deletedinuse: 34
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying clauses:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 207732
% 51.42/51.84 Kept: 202763
% 51.42/51.84 Inuse: 1817
% 51.42/51.84 Deleted: 656
% 51.42/51.84 Deletedinuse: 36
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 209762
% 51.42/51.84 Kept: 204774
% 51.42/51.84 Inuse: 1824
% 51.42/51.84 Deleted: 657
% 51.42/51.84 Deletedinuse: 37
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 211850
% 51.42/51.84 Kept: 206802
% 51.42/51.84 Inuse: 1836
% 51.42/51.84 Deleted: 657
% 51.42/51.84 Deletedinuse: 37
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84 Resimplifying inuse:
% 51.42/51.84 Done
% 51.42/51.84
% 51.42/51.84
% 51.42/51.84 Intermediate Status:
% 51.42/51.84 Generated: 213903
% 51.42/51.84 Kept: 208819
% 51.42/51.84 Inuse: 1842
% 51.42/51.84 Deleted: 658
% 89.95/90.38 Deletedinuse: 38
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 215959
% 89.95/90.38 Kept: 210845
% 89.95/90.38 Inuse: 1848
% 89.95/90.38 Deleted: 659
% 89.95/90.38 Deletedinuse: 39
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 218024
% 89.95/90.38 Kept: 212880
% 89.95/90.38 Inuse: 1854
% 89.95/90.38 Deleted: 660
% 89.95/90.38 Deletedinuse: 40
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 220134
% 89.95/90.38 Kept: 214942
% 89.95/90.38 Inuse: 1866
% 89.95/90.38 Deleted: 660
% 89.95/90.38 Deletedinuse: 40
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 222560
% 89.95/90.38 Kept: 217334
% 89.95/90.38 Inuse: 1874
% 89.95/90.38 Deleted: 661
% 89.95/90.38 Deletedinuse: 41
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 224716
% 89.95/90.38 Kept: 219473
% 89.95/90.38 Inuse: 1886
% 89.95/90.38 Deleted: 663
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 226842
% 89.95/90.38 Kept: 221556
% 89.95/90.38 Inuse: 1901
% 89.95/90.38 Deleted: 663
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying clauses:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 228988
% 89.95/90.38 Kept: 223687
% 89.95/90.38 Inuse: 1909
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 231118
% 89.95/90.38 Kept: 225800
% 89.95/90.38 Inuse: 1915
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 233283
% 89.95/90.38 Kept: 227938
% 89.95/90.38 Inuse: 1922
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 235312
% 89.95/90.38 Kept: 229947
% 89.95/90.38 Inuse: 1940
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 237500
% 89.95/90.38 Kept: 232119
% 89.95/90.38 Inuse: 1949
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 239680
% 89.95/90.38 Kept: 234284
% 89.95/90.38 Inuse: 1957
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 241706
% 89.95/90.38 Kept: 236295
% 89.95/90.38 Inuse: 1966
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 243726
% 89.95/90.38 Kept: 238301
% 89.95/90.38 Inuse: 1981
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 245776
% 89.95/90.38 Kept: 240339
% 89.95/90.38 Inuse: 1989
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 247812
% 89.95/90.38 Kept: 242363
% 89.95/90.38 Inuse: 1995
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying clauses:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 249856
% 89.95/90.38 Kept: 244388
% 89.95/90.38 Inuse: 2001
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 251944
% 89.95/90.38 Kept: 246454
% 89.95/90.38 Inuse: 2018
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 253998
% 89.95/90.38 Kept: 248478
% 89.95/90.38 Inuse: 2030
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 256784
% 89.95/90.38 Kept: 251246
% 89.95/90.38 Inuse: 2039
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 258844
% 89.95/90.38 Kept: 253293
% 89.95/90.38 Inuse: 2044
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 260912
% 89.95/90.38 Kept: 255348
% 89.95/90.38 Inuse: 2049
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 263159
% 89.95/90.38 Kept: 257375
% 89.95/90.38 Inuse: 2063
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 265767
% 89.95/90.38 Kept: 259681
% 89.95/90.38 Inuse: 2079
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38
% 89.95/90.38 Intermediate Status:
% 89.95/90.38 Generated: 268561
% 89.95/90.38 Kept: 262351
% 89.95/90.38 Inuse: 2089
% 89.95/90.38 Deleted: 664
% 89.95/90.38 Deletedinuse: 43
% 89.95/90.38
% 89.95/90.38 Resimplifying inuse:
% 89.95/90.38 Done
% 89.95/90.38
% 89.95/90.38 Resimplifying clauses:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 271468
% 136.58/137.03 Kept: 264678
% 136.58/137.03 Inuse: 2109
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 274220
% 136.58/137.03 Kept: 267332
% 136.58/137.03 Inuse: 2119
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 276561
% 136.58/137.03 Kept: 269386
% 136.58/137.03 Inuse: 2149
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 278578
% 136.58/137.03 Kept: 271395
% 136.58/137.03 Inuse: 2157
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 280759
% 136.58/137.03 Kept: 273561
% 136.58/137.03 Inuse: 2164
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 282766
% 136.58/137.03 Kept: 275561
% 136.58/137.03 Inuse: 2171
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 284826
% 136.58/137.03 Kept: 277586
% 136.58/137.03 Inuse: 2188
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 286886
% 136.58/137.03 Kept: 279596
% 136.58/137.03 Inuse: 2200
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 288920
% 136.58/137.03 Kept: 281614
% 136.58/137.03 Inuse: 2207
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying clauses:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 292126
% 136.58/137.03 Kept: 284795
% 136.58/137.03 Inuse: 2214
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 294236
% 136.58/137.03 Kept: 286890
% 136.58/137.03 Inuse: 2231
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 297137
% 136.58/137.03 Kept: 289768
% 136.58/137.03 Inuse: 2244
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 299204
% 136.58/137.03 Kept: 291816
% 136.58/137.03 Inuse: 2251
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 301233
% 136.58/137.03 Kept: 293822
% 136.58/137.03 Inuse: 2256
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 303310
% 136.58/137.03 Kept: 295848
% 136.58/137.03 Inuse: 2269
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 305336
% 136.58/137.03 Kept: 297855
% 136.58/137.03 Inuse: 2286
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 307562
% 136.58/137.03 Kept: 300056
% 136.58/137.03 Inuse: 2303
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 309649
% 136.58/137.03 Kept: 302129
% 136.58/137.03 Inuse: 2309
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying clauses:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 311766
% 136.58/137.03 Kept: 304239
% 136.58/137.03 Inuse: 2316
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 314099
% 136.58/137.03 Kept: 306556
% 136.58/137.03 Inuse: 2324
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 316124
% 136.58/137.03 Kept: 308564
% 136.58/137.03 Inuse: 2342
% 136.58/137.03 Deleted: 664
% 136.58/137.03 Deletedinuse: 43
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 318156
% 136.58/137.03 Kept: 310573
% 136.58/137.03 Inuse: 2357
% 136.58/137.03 Deleted: 665
% 136.58/137.03 Deletedinuse: 44
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 320310
% 136.58/137.03 Kept: 312675
% 136.58/137.03 Inuse: 2369
% 136.58/137.03 Deleted: 665
% 136.58/137.03 Deletedinuse: 44
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 322613
% 136.58/137.03 Kept: 314950
% 136.58/137.03 Inuse: 2374
% 136.58/137.03 Deleted: 665
% 136.58/137.03 Deletedinuse: 44
% 136.58/137.03
% 136.58/137.03 Resimplifying inuse:
% 136.58/137.03 Done
% 136.58/137.03
% 136.58/137.03
% 136.58/137.03 Intermediate Status:
% 136.58/137.03 Generated: 324923
% 136.58/137.03 Kept: 317241
% 136.58/137.03 Inuse: 2379
% 136.58/137.03 Deleted: 666
% 199.81/200.27 Deletedinuse: 45
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 328325
% 199.81/200.27 Kept: 320579
% 199.81/200.27 Inuse: 2389
% 199.81/200.27 Deleted: 667
% 199.81/200.27 Deletedinuse: 46
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 330445
% 199.81/200.27 Kept: 322652
% 199.81/200.27 Inuse: 2399
% 199.81/200.27 Deleted: 668
% 199.81/200.27 Deletedinuse: 47
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying clauses:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 332583
% 199.81/200.27 Kept: 324732
% 199.81/200.27 Inuse: 2410
% 199.81/200.27 Deleted: 669
% 199.81/200.27 Deletedinuse: 48
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 334729
% 199.81/200.27 Kept: 326812
% 199.81/200.27 Inuse: 2420
% 199.81/200.27 Deleted: 669
% 199.81/200.27 Deletedinuse: 48
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 336875
% 199.81/200.27 Kept: 328892
% 199.81/200.27 Inuse: 2430
% 199.81/200.27 Deleted: 669
% 199.81/200.27 Deletedinuse: 48
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 339024
% 199.81/200.27 Kept: 331013
% 199.81/200.27 Inuse: 2434
% 199.81/200.27 Deleted: 669
% 199.81/200.27 Deletedinuse: 48
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 341397
% 199.81/200.27 Kept: 333349
% 199.81/200.27 Inuse: 2439
% 199.81/200.27 Deleted: 670
% 199.81/200.27 Deletedinuse: 49
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 344869
% 199.81/200.27 Kept: 336747
% 199.81/200.27 Inuse: 2449
% 199.81/200.27 Deleted: 671
% 199.81/200.27 Deletedinuse: 50
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 347037
% 199.81/200.27 Kept: 338857
% 199.81/200.27 Inuse: 2459
% 199.81/200.27 Deleted: 672
% 199.81/200.27 Deletedinuse: 51
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 349215
% 199.81/200.27 Kept: 340967
% 199.81/200.27 Inuse: 2469
% 199.81/200.27 Deleted: 672
% 199.81/200.27 Deletedinuse: 51
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 352724
% 199.81/200.27 Kept: 344411
% 199.81/200.27 Inuse: 2479
% 199.81/200.27 Deleted: 672
% 199.81/200.27 Deletedinuse: 51
% 199.81/200.27
% 199.81/200.27 Resimplifying inuse:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27 Resimplifying clauses:
% 199.81/200.27 Done
% 199.81/200.27
% 199.81/200.27
% 199.81/200.27 Intermediate Status:
% 199.81/200.27 Generated: 355149
% 199.81/200.27 Kept: 346816
% 199.81/200.27 Inuse: 2484
% 199.81/200.28 Deleted: 675
% 199.81/200.28 Deletedinuse: 52
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 357588
% 199.81/200.28 Kept: 349228
% 199.81/200.28 Inuse: 2489
% 199.81/200.28 Deleted: 676
% 199.81/200.28 Deletedinuse: 53
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 359782
% 199.81/200.28 Kept: 351377
% 199.81/200.28 Inuse: 2499
% 199.81/200.28 Deleted: 677
% 199.81/200.28 Deletedinuse: 54
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 363300
% 199.81/200.28 Kept: 354855
% 199.81/200.28 Inuse: 2509
% 199.81/200.28 Deleted: 677
% 199.81/200.28 Deletedinuse: 54
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 365743
% 199.81/200.28 Kept: 357274
% 199.81/200.28 Inuse: 2514
% 199.81/200.28 Deleted: 678
% 199.81/200.28 Deletedinuse: 55
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 368193
% 199.81/200.28 Kept: 359700
% 199.81/200.28 Inuse: 2519
% 199.81/200.28 Deleted: 679
% 199.81/200.28 Deletedinuse: 56
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 370351
% 199.81/200.28 Kept: 361828
% 199.81/200.28 Inuse: 2529
% 199.81/200.28 Deleted: 680
% 199.81/200.28 Deletedinuse: 57
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 372545
% 199.81/200.28 Kept: 363990
% 199.81/200.28 Inuse: 2540
% 199.81/200.28 Deleted: 681
% 199.81/200.28 Deletedinuse: 58
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying clauses:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 375902
% 199.81/200.28 Kept: 367318
% 199.81/200.28 Inuse: 2549
% 199.81/200.28 Deleted: 683
% 199.81/200.28 Deletedinuse: 58
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 378399
% 199.81/200.28 Kept: 369800
% 199.81/200.28 Inuse: 2554
% 199.81/200.28 Deleted: 684
% 199.81/200.28 Deletedinuse: 59
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 380905
% 199.81/200.28 Kept: 372289
% 199.81/200.28 Inuse: 2559
% 199.81/200.28 Deleted: 685
% 199.81/200.28 Deletedinuse: 60
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 383145
% 199.81/200.28 Kept: 374494
% 199.81/200.28 Inuse: 2569
% 199.81/200.28 Deleted: 686
% 199.81/200.28 Deletedinuse: 61
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28
% 199.81/200.28 Intermediate Status:
% 199.81/200.28 Generated: 385261
% 199.81/200.28 Kept: 376578
% 199.81/200.28 Inuse: 2582
% 199.81/200.28 Deleted: 686
% 199.81/200.28 Deletedinuse: 61
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 199.81/200.28 Done
% 199.81/200.28
% 199.81/200.28 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 388365
% 250.09/250.59 Kept: 379657
% 250.09/250.59 Inuse: 2594
% 250.09/250.59 Deleted: 686
% 250.09/250.59 Deletedinuse: 61
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 390498
% 250.09/250.59 Kept: 381782
% 250.09/250.59 Inuse: 2599
% 250.09/250.59 Deleted: 686
% 250.09/250.59 Deletedinuse: 61
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 393370
% 250.09/250.59 Kept: 384632
% 250.09/250.59 Inuse: 2609
% 250.09/250.59 Deleted: 686
% 250.09/250.59 Deletedinuse: 61
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying clauses:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 395530
% 250.09/250.59 Kept: 386770
% 250.09/250.59 Inuse: 2626
% 250.09/250.59 Deleted: 686
% 250.09/250.59 Deletedinuse: 61
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 397638
% 250.09/250.59 Kept: 388858
% 250.09/250.59 Inuse: 2638
% 250.09/250.59 Deleted: 687
% 250.09/250.59 Deletedinuse: 62
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 400422
% 250.09/250.59 Kept: 391622
% 250.09/250.59 Inuse: 2644
% 250.09/250.59 Deleted: 687
% 250.09/250.59 Deletedinuse: 62
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 402991
% 250.09/250.59 Kept: 394170
% 250.09/250.59 Inuse: 2649
% 250.09/250.59 Deleted: 688
% 250.09/250.59 Deletedinuse: 63
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 405566
% 250.09/250.59 Kept: 396719
% 250.09/250.59 Inuse: 2654
% 250.09/250.59 Deleted: 689
% 250.09/250.59 Deletedinuse: 64
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 407622
% 250.09/250.59 Kept: 398751
% 250.09/250.59 Inuse: 2663
% 250.09/250.59 Deleted: 690
% 250.09/250.59 Deletedinuse: 65
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 410774
% 250.09/250.59 Kept: 401893
% 250.09/250.59 Inuse: 2674
% 250.09/250.59 Deleted: 690
% 250.09/250.59 Deletedinuse: 65
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 413388
% 250.09/250.59 Kept: 404491
% 250.09/250.59 Inuse: 2679
% 250.09/250.59 Deleted: 691
% 250.09/250.59 Deletedinuse: 66
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying clauses:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 416009
% 250.09/250.59 Kept: 407096
% 250.09/250.59 Inuse: 2684
% 250.09/250.59 Deleted: 692
% 250.09/250.59 Deletedinuse: 67
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 418186
% 250.09/250.59 Kept: 409247
% 250.09/250.59 Inuse: 2696
% 250.09/250.59 Deleted: 693
% 250.09/250.59 Deletedinuse: 68
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 420890
% 250.09/250.59 Kept: 411931
% 250.09/250.59 Inuse: 2704
% 250.09/250.59 Deleted: 693
% 250.09/250.59 Deletedinuse: 68
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 423105
% 250.09/250.59 Kept: 414133
% 250.09/250.59 Inuse: 2709
% 250.09/250.59 Deleted: 694
% 250.09/250.59 Deletedinuse: 69
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 425327
% 250.09/250.59 Kept: 416338
% 250.09/250.59 Inuse: 2714
% 250.09/250.59 Deleted: 695
% 250.09/250.59 Deletedinuse: 70
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 427582
% 250.09/250.59 Kept: 418568
% 250.09/250.59 Inuse: 2730
% 250.09/250.59 Deleted: 696
% 250.09/250.59 Deletedinuse: 71
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 431102
% 250.09/250.59 Kept: 422071
% 250.09/250.59 Inuse: 2744
% 250.09/250.59 Deleted: 697
% 250.09/250.59 Deletedinuse: 72
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 433770
% 250.09/250.59 Kept: 424726
% 250.09/250.59 Inuse: 2749
% 250.09/250.59 Deleted: 698
% 250.09/250.59 Deletedinuse: 73
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying clauses:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 436445
% 250.09/250.59 Kept: 427388
% 250.09/250.59 Inuse: 2754
% 250.09/250.59 Deleted: 699
% 250.09/250.59 Deletedinuse: 74
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 438810
% 250.09/250.59 Kept: 429727
% 250.09/250.59 Inuse: 2764
% 250.09/250.59 Deleted: 700
% 250.09/250.59 Deletedinuse: 75
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 440951
% 250.09/250.59 Kept: 431842
% 250.09/250.59 Inuse: 2774
% 250.09/250.59 Deleted: 701
% 250.09/250.59 Deletedinuse: 76
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 443089
% 250.09/250.59 Kept: 433949
% 250.09/250.59 Inuse: 2783
% 250.09/250.59 Deleted: 701
% 250.09/250.59 Deletedinuse: 76
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 445308
% 250.09/250.59 Kept: 436150
% 250.09/250.59 Inuse: 2786
% 250.09/250.59 Deleted: 702
% 250.09/250.59 Deletedinuse: 77
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 447530
% 250.09/250.59 Kept: 438354
% 250.09/250.59 Inuse: 2789
% 250.09/250.59 Deleted: 702
% 250.09/250.59 Deletedinuse: 77
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 450236
% 250.09/250.59 Kept: 441033
% 250.09/250.59 Inuse: 2794
% 250.09/250.59 Deleted: 703
% 250.09/250.59 Deletedinuse: 78
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 452399
% 250.09/250.59 Kept: 443159
% 250.09/250.59 Inuse: 2803
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying clauses:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 454569
% 250.09/250.59 Kept: 445287
% 250.09/250.59 Inuse: 2812
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 456730
% 250.09/250.59 Kept: 447415
% 250.09/250.59 Inuse: 2821
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 460201
% 250.09/250.59 Kept: 450861
% 250.09/250.59 Inuse: 2829
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 462952
% 250.09/250.59 Kept: 453597
% 250.09/250.59 Inuse: 2834
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 465145
% 250.09/250.59 Kept: 455749
% 250.09/250.59 Inuse: 2843
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 467184
% 250.09/250.59 Kept: 457783
% 250.09/250.59 Inuse: 2845
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 469382
% 250.09/250.59 Kept: 459948
% 250.09/250.59 Inuse: 2855
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 473345
% 250.09/250.59 Kept: 463515
% 250.09/250.59 Inuse: 2869
% 250.09/250.59 Deleted: 704
% 250.09/250.59 Deletedinuse: 79
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Intermediate Status:
% 250.09/250.59 Generated: 475700
% 250.09/250.59 Kept: 465836
% 250.09/250.59 Inuse: 2874
% 250.09/250.59 Deleted: 705
% 250.09/250.59 Deletedinuse: 80
% 250.09/250.59
% 250.09/250.59 Resimplifying inuse:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59 Resimplifying clauses:
% 250.09/250.59 Done
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 Bliksems!, er is een bewijs:
% 250.09/250.59 % SZS status Unsatisfiable
% 250.09/250.59 % SZS output start Refutation
% 250.09/250.59
% 250.09/250.59 clause( 1, [ p2( X, X ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 3, [ p3( X, X ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 6, [ p3( f12( f15( c22 ), c21 ), c22 ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 11, [ p2( f9( X ), f9( Y ) ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 18, [ ~( p3( Z, X ) ), p3( X, Y ), ~( p3( Z, Y ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 19, [ p17( X, Y ), ~( p17( Z, T ) ), ~( p2( Z, X ) ), ~( p2( T, Y )
% 250.09/250.59 ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 22, [ p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), c22 ) ), f6( f7(
% 250.09/250.59 f8( c20 ) ) ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 24, [ ~( p3( X, Z ) ), p3( f10( X, Y ), f10( Z, T ) ), ~( p3( Y, T
% 250.09/250.59 ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 28, [ ~( p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), f12( X, c21 ) )
% 250.09/250.59 ), f6( f7( f8( c20 ) ) ) ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 70, [ p3( Y, X ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 73, [ p3( c22, f12( f15( c22 ), c21 ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 85, [ p17( X, Y ), ~( p17( Z, Y ) ), ~( p2( Z, X ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 192, [ p3( f10( X, c22 ), f10( Y, f12( f15( c22 ), c21 ) ) ), ~( p3(
% 250.09/250.59 X, Y ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 16263, [ p3( f10( X, c22 ), f10( X, f12( f15( c22 ), c21 ) ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 16313, [ p2( f9( f10( X, c22 ) ), f9( f10( X, f12( f15( c22 ), c21
% 250.09/250.59 ) ) ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 16746, [ p17( f9( f10( X, f12( f15( c22 ), c21 ) ) ), Y ), ~( p17(
% 250.09/250.59 f9( f10( X, c22 ) ), Y ) ) ] )
% 250.09/250.59 .
% 250.09/250.59 clause( 466349, [] )
% 250.09/250.59 .
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 % SZS output end Refutation
% 250.09/250.59 found a proof!
% 250.09/250.59
% 250.09/250.59 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 250.09/250.59
% 250.09/250.59 initialclauses(
% 250.09/250.59 [ clause( 466351, [ ~( p16( c21 ) ) ] )
% 250.09/250.59 , clause( 466352, [ p2( X, X ) ] )
% 250.09/250.59 , clause( 466353, [ p5( X, X ) ] )
% 250.09/250.59 , clause( 466354, [ p3( X, X ) ] )
% 250.09/250.59 , clause( 466355, [ ~( p5( c21, f7( c20 ) ) ) ] )
% 250.09/250.59 , clause( 466356, [ p3( f12( c22, c21 ), f15( c22 ) ) ] )
% 250.09/250.59 , clause( 466357, [ p3( f12( f15( c22 ), c21 ), c22 ) ] )
% 250.09/250.59 , clause( 466358, [ ~( p3( c19, f4( f6( f7( c20 ) ) ) ) ) ] )
% 250.09/250.59 , clause( 466359, [ p16( X ), ~( p16( Y ) ), ~( p5( Y, X ) ) ] )
% 250.09/250.59 , clause( 466360, [ p5( f8( X ), f8( Y ) ), ~( p5( X, Y ) ) ] )
% 250.09/250.59 , clause( 466361, [ p2( f6( X ), f6( Y ) ), ~( p5( X, Y ) ) ] )
% 250.09/250.59 , clause( 466362, [ p2( f9( X ), f9( Y ) ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 , clause( 466363, [ p3( f13( X ), f13( Y ) ), ~( p5( X, Y ) ) ] )
% 250.09/250.59 , clause( 466364, [ p3( f15( X ), f15( Y ) ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 , clause( 466365, [ p3( f4( X ), f4( Y ) ), ~( p2( X, Y ) ) ] )
% 250.09/250.59 , clause( 466366, [ p5( f7( X ), f7( Y ) ), ~( p5( X, Y ) ) ] )
% 250.09/250.59 , clause( 466367, [ p2( X, Y ), ~( p2( Z, X ) ), ~( p2( Z, Y ) ) ] )
% 250.09/250.59 , clause( 466368, [ p5( X, Y ), ~( p5( Z, X ) ), ~( p5( Z, Y ) ) ] )
% 250.09/250.59 , clause( 466369, [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ] )
% 250.09/250.59 , clause( 466370, [ p17( X, Y ), ~( p2( Z, X ) ), ~( p2( T, Y ) ), ~( p17(
% 250.09/250.59 Z, T ) ) ] )
% 250.09/250.59 , clause( 466371, [ p18( X, Y ), ~( p5( Z, X ) ), ~( p5( T, Y ) ), ~( p18(
% 250.09/250.59 Z, T ) ) ] )
% 250.09/250.59 , clause( 466372, [ p3( f12( f4( f6( f7( f8( c20 ) ) ) ), c21 ), f4( f6( f7(
% 250.09/250.59 f8( c20 ) ) ) ) ) ] )
% 250.09/250.59 , clause( 466373, [ p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), c22 ) ), f6(
% 250.09/250.59 f7( f8( c20 ) ) ) ) ] )
% 250.09/250.59 , clause( 466374, [ p3( f14( X, Y ), f14( Z, T ) ), ~( p3( X, Z ) ), ~( p3(
% 250.09/250.59 Y, T ) ) ] )
% 250.09/250.59 , clause( 466375, [ p3( f10( X, Y ), f10( Z, T ) ), ~( p3( X, Z ) ), ~( p3(
% 250.09/250.59 Y, T ) ) ] )
% 250.09/250.59 , clause( 466376, [ p3( f11( X, Y ), f11( Z, T ) ), ~( p3( X, Z ) ), ~( p3(
% 250.09/250.59 Y, T ) ) ] )
% 250.09/250.59 , clause( 466377, [ p3( f12( X, Y ), f12( Z, T ) ), ~( p3( X, Z ) ), ~( p5(
% 250.09/250.59 Y, T ) ) ] )
% 250.09/250.59 , clause( 466378, [ p3( f12( f15( f4( f6( f7( f8( c20 ) ) ) ) ), c21 ), f15(
% 250.09/250.59 f4( f6( f7( f8( c20 ) ) ) ) ) ) ] )
% 250.09/250.59 , clause( 466379, [ ~( p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), f12( X,
% 250.09/250.59 c21 ) ) ), f6( f7( f8( c20 ) ) ) ) ) ] )
% 250.09/250.59 , clause( 466380, [ p5( X, f7( c20 ) ), p3( c19, f4( f6( f7( c20 ) ) ) ),
% 250.09/250.59 p17( f9( f10( f4( f6( f7( f8( c20 ) ) ) ), f11( c19, f12( f13( X ), X ) )
% 250.09/250.59 ) ), f6( f7( f8( c20 ) ) ) ), ~( p18( X, c21 ) ) ] )
% 250.09/250.59 ] ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 1, [ p2( X, X ) ] )
% 250.09/250.59 , clause( 466352, [ p2( X, X ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 3, [ p3( X, X ) ] )
% 250.09/250.59 , clause( 466354, [ p3( X, X ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 6, [ p3( f12( f15( c22 ), c21 ), c22 ) ] )
% 250.09/250.59 , clause( 466357, [ p3( f12( f15( c22 ), c21 ), c22 ) ] )
% 250.09/250.59 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 11, [ p2( f9( X ), f9( Y ) ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 , clause( 466362, [ p2( f9( X ), f9( Y ) ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 250.09/250.59 ), ==>( 1, 1 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 18, [ ~( p3( Z, X ) ), p3( X, Y ), ~( p3( Z, Y ) ) ] )
% 250.09/250.59 , clause( 466369, [ p3( X, Y ), ~( p3( Z, X ) ), ~( p3( Z, Y ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 250.09/250.59 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2, 2 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 19, [ p17( X, Y ), ~( p17( Z, T ) ), ~( p2( Z, X ) ), ~( p2( T, Y )
% 250.09/250.59 ) ] )
% 250.09/250.59 , clause( 466370, [ p17( X, Y ), ~( p2( Z, X ) ), ~( p2( T, Y ) ), ~( p17(
% 250.09/250.59 Z, T ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 250.09/250.59 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 2 ), ==>( 2, 3 ), ==>( 3, 1 )] )
% 250.09/250.59 ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 22, [ p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), c22 ) ), f6( f7(
% 250.09/250.59 f8( c20 ) ) ) ) ] )
% 250.09/250.59 , clause( 466373, [ p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), c22 ) ), f6(
% 250.09/250.59 f7( f8( c20 ) ) ) ) ] )
% 250.09/250.59 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 24, [ ~( p3( X, Z ) ), p3( f10( X, Y ), f10( Z, T ) ), ~( p3( Y, T
% 250.09/250.59 ) ) ] )
% 250.09/250.59 , clause( 466375, [ p3( f10( X, Y ), f10( Z, T ) ), ~( p3( X, Z ) ), ~( p3(
% 250.09/250.59 Y, T ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 250.09/250.59 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2, 2 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 28, [ ~( p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), f12( X, c21 ) )
% 250.09/250.59 ), f6( f7( f8( c20 ) ) ) ) ) ] )
% 250.09/250.59 , clause( 466379, [ ~( p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), f12( X,
% 250.09/250.59 c21 ) ) ), f6( f7( f8( c20 ) ) ) ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 resolution(
% 250.09/250.59 clause( 466409, [ ~( p3( X, Y ) ), p3( Y, X ) ] )
% 250.09/250.59 , clause( 18, [ ~( p3( Z, X ) ), p3( X, Y ), ~( p3( Z, Y ) ) ] )
% 250.09/250.59 , 2, clause( 3, [ p3( X, X ) ] )
% 250.09/250.59 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, X )] ),
% 250.09/250.59 substitution( 1, [ :=( X, X )] )).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 70, [ p3( Y, X ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 , clause( 466409, [ ~( p3( X, Y ) ), p3( Y, X ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 250.09/250.59 ), ==>( 1, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 resolution(
% 250.09/250.59 clause( 466410, [ p3( c22, f12( f15( c22 ), c21 ) ) ] )
% 250.09/250.59 , clause( 70, [ p3( Y, X ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 , 1, clause( 6, [ p3( f12( f15( c22 ), c21 ), c22 ) ] )
% 250.09/250.59 , 0, substitution( 0, [ :=( X, f12( f15( c22 ), c21 ) ), :=( Y, c22 )] ),
% 250.09/250.59 substitution( 1, [] )).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 73, [ p3( c22, f12( f15( c22 ), c21 ) ) ] )
% 250.09/250.59 , clause( 466410, [ p3( c22, f12( f15( c22 ), c21 ) ) ] )
% 250.09/250.59 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 resolution(
% 250.09/250.59 clause( 466412, [ p17( X, Y ), ~( p17( Z, Y ) ), ~( p2( Z, X ) ) ] )
% 250.09/250.59 , clause( 19, [ p17( X, Y ), ~( p17( Z, T ) ), ~( p2( Z, X ) ), ~( p2( T, Y
% 250.09/250.59 ) ) ] )
% 250.09/250.59 , 3, clause( 1, [ p2( X, X ) ] )
% 250.09/250.59 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, Y )] ),
% 250.09/250.59 substitution( 1, [ :=( X, Y )] )).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 85, [ p17( X, Y ), ~( p17( Z, Y ) ), ~( p2( Z, X ) ) ] )
% 250.09/250.59 , clause( 466412, [ p17( X, Y ), ~( p17( Z, Y ) ), ~( p2( Z, X ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 250.09/250.59 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 resolution(
% 250.09/250.59 clause( 466414, [ ~( p3( X, Y ) ), p3( f10( X, c22 ), f10( Y, f12( f15( c22
% 250.09/250.59 ), c21 ) ) ) ] )
% 250.09/250.59 , clause( 24, [ ~( p3( X, Z ) ), p3( f10( X, Y ), f10( Z, T ) ), ~( p3( Y,
% 250.09/250.59 T ) ) ] )
% 250.09/250.59 , 2, clause( 73, [ p3( c22, f12( f15( c22 ), c21 ) ) ] )
% 250.09/250.59 , 0, substitution( 0, [ :=( X, X ), :=( Y, c22 ), :=( Z, Y ), :=( T, f12(
% 250.09/250.59 f15( c22 ), c21 ) )] ), substitution( 1, [] )).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 192, [ p3( f10( X, c22 ), f10( Y, f12( f15( c22 ), c21 ) ) ), ~( p3(
% 250.09/250.59 X, Y ) ) ] )
% 250.09/250.59 , clause( 466414, [ ~( p3( X, Y ) ), p3( f10( X, c22 ), f10( Y, f12( f15(
% 250.09/250.59 c22 ), c21 ) ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 250.09/250.59 ), ==>( 1, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 resolution(
% 250.09/250.59 clause( 466415, [ p3( f10( X, c22 ), f10( X, f12( f15( c22 ), c21 ) ) ) ]
% 250.09/250.59 )
% 250.09/250.59 , clause( 192, [ p3( f10( X, c22 ), f10( Y, f12( f15( c22 ), c21 ) ) ), ~(
% 250.09/250.59 p3( X, Y ) ) ] )
% 250.09/250.59 , 1, clause( 3, [ p3( X, X ) ] )
% 250.09/250.59 , 0, substitution( 0, [ :=( X, X ), :=( Y, X )] ), substitution( 1, [ :=( X
% 250.09/250.59 , X )] )).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 16263, [ p3( f10( X, c22 ), f10( X, f12( f15( c22 ), c21 ) ) ) ] )
% 250.09/250.59 , clause( 466415, [ p3( f10( X, c22 ), f10( X, f12( f15( c22 ), c21 ) ) ) ]
% 250.09/250.59 )
% 250.09/250.59 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 resolution(
% 250.09/250.59 clause( 466416, [ p2( f9( f10( X, c22 ) ), f9( f10( X, f12( f15( c22 ), c21
% 250.09/250.59 ) ) ) ) ] )
% 250.09/250.59 , clause( 11, [ p2( f9( X ), f9( Y ) ), ~( p3( X, Y ) ) ] )
% 250.09/250.59 , 1, clause( 16263, [ p3( f10( X, c22 ), f10( X, f12( f15( c22 ), c21 ) ) )
% 250.09/250.59 ] )
% 250.09/250.59 , 0, substitution( 0, [ :=( X, f10( X, c22 ) ), :=( Y, f10( X, f12( f15(
% 250.09/250.59 c22 ), c21 ) ) )] ), substitution( 1, [ :=( X, X )] )).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 16313, [ p2( f9( f10( X, c22 ) ), f9( f10( X, f12( f15( c22 ), c21
% 250.09/250.59 ) ) ) ) ] )
% 250.09/250.59 , clause( 466416, [ p2( f9( f10( X, c22 ) ), f9( f10( X, f12( f15( c22 ),
% 250.09/250.59 c21 ) ) ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 resolution(
% 250.09/250.59 clause( 466417, [ p17( f9( f10( X, f12( f15( c22 ), c21 ) ) ), Y ), ~( p17(
% 250.09/250.59 f9( f10( X, c22 ) ), Y ) ) ] )
% 250.09/250.59 , clause( 85, [ p17( X, Y ), ~( p17( Z, Y ) ), ~( p2( Z, X ) ) ] )
% 250.09/250.59 , 2, clause( 16313, [ p2( f9( f10( X, c22 ) ), f9( f10( X, f12( f15( c22 )
% 250.09/250.59 , c21 ) ) ) ) ] )
% 250.09/250.59 , 0, substitution( 0, [ :=( X, f9( f10( X, f12( f15( c22 ), c21 ) ) ) ),
% 250.09/250.59 :=( Y, Y ), :=( Z, f9( f10( X, c22 ) ) )] ), substitution( 1, [ :=( X, X
% 250.09/250.59 )] )).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 subsumption(
% 250.09/250.59 clause( 16746, [ p17( f9( f10( X, f12( f15( c22 ), c21 ) ) ), Y ), ~( p17(
% 250.09/250.59 f9( f10( X, c22 ) ), Y ) ) ] )
% 250.09/250.59 , clause( 466417, [ p17( f9( f10( X, f12( f15( c22 ), c21 ) ) ), Y ), ~(
% 250.09/250.59 p17( f9( f10( X, c22 ) ), Y ) ) ] )
% 250.09/250.59 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 250.09/250.59 ), ==>( 1, 1 )] ) ).
% 250.09/250.59
% 250.09/250.59
% 250.09/250.59 resolution(
% 250.09/250.59 clause( 466418, [ p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), f12( f15( c22
% 250.09/250.59 ), c21 ) ) ), f6( f7( f8( c20 ) ) ) ) ] )
% 250.09/250.59 , clause( 16746, [ p17( f9( f10( X, f12( f15( c22 ), c21 ) ) ), Y ), ~( p17(
% 250.09/250.59 f9( f10( X, c22 ) ), Y ) ) ] )
% 250.09/250.59 , 1, clause( 22, [ p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), c22 ) ), f6(
% 250.09/250.59 f7( f8( c20 ) ) ) ) ] )
% 250.09/250.59 , 0, substitution( 0, [ :=( X, f14( f4( f9( c19 ) ), c19 ) ), :=( Y, f6( f7(
% 250.09/250.59 f8( c20 ) ) ) )] ), substitution( 1, [] )).
% 250.21/250.62
% 250.21/250.62
% 250.21/250.62 resolution(
% 250.21/250.62 clause( 466419, [] )
% 250.21/250.62 , clause( 28, [ ~( p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), f12( X, c21 )
% 250.21/250.62 ) ), f6( f7( f8( c20 ) ) ) ) ) ] )
% 250.21/250.62 , 0, clause( 466418, [ p17( f9( f10( f14( f4( f9( c19 ) ), c19 ), f12( f15(
% 250.21/250.62 c22 ), c21 ) ) ), f6( f7( f8( c20 ) ) ) ) ] )
% 250.21/250.62 , 0, substitution( 0, [ :=( X, f15( c22 ) )] ), substitution( 1, [] )).
% 250.21/250.62
% 250.21/250.62
% 250.21/250.62 subsumption(
% 250.21/250.62 clause( 466349, [] )
% 250.21/250.62 , clause( 466419, [] )
% 250.21/250.62 , substitution( 0, [] ), permutation( 0, [] ) ).
% 250.21/250.62
% 250.21/250.62
% 250.21/250.62 end.
% 250.21/250.62
% 250.21/250.62 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 250.21/250.62
% 250.21/250.62 Memory use:
% 250.21/250.62
% 250.21/250.62 space for terms: 12168139
% 250.21/250.62 space for clauses: 56515043
% 250.21/250.62
% 250.21/250.62
% 250.21/250.62 clauses generated: 476250
% 250.21/250.62 clauses kept: 466350
% 250.21/250.62 clauses selected: 2878
% 250.21/250.62 clauses deleted: 706
% 250.21/250.62 clauses inuse deleted: 81
% 250.21/250.62
% 250.21/250.62 subsentry: 1034624
% 250.21/250.62 literals s-matched: 613447
% 250.21/250.62 literals matched: 613447
% 250.21/250.62 full subsumption: 6938
% 250.21/250.62
% 250.21/250.62 checksum: 347474930
% 250.21/250.62
% 250.21/250.62
% 250.21/250.62 Bliksem ended
%------------------------------------------------------------------------------