%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX197+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Tue May 5 06:56:46 PM UTC 2026
% Result : Timeout 299.58s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX197+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.16/0.34 % Computer : n001.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % DateTime : Tue May 5 11:03:48 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.74/1.42 *** allocated 10000 integers for termspace/termends
% 0.74/1.42 *** allocated 10000 integers for clauses
% 0.74/1.42 *** allocated 10000 integers for justifications
% 0.74/1.42 Bliksem 1.12
% 0.74/1.42
% 0.74/1.42
% 0.74/1.42 Automatic Strategy Selection
% 0.74/1.42
% 0.74/1.42
% 0.74/1.42 Clauses:
% 0.74/1.42
% 0.74/1.42 { proj1Suc( suc( X ) ) = X }.
% 0.74/1.42 { ! zero = suc( X ) }.
% 0.74/1.42 { proj1N( n( X ) ) = X }.
% 0.74/1.42 { proj1Add( add( X, Y ) ) = X }.
% 0.74/1.42 { proj2Add( add( X, Y ) ) = Y }.
% 0.74/1.42 { proj1Mul( mul( X, Y ) ) = X }.
% 0.74/1.42 { proj2Mul( mul( X, Y ) ) = Y }.
% 0.74/1.42 { proj1Eq( eq( X, Y ) ) = X }.
% 0.74/1.42 { proj2Eq( eq( X, Y ) ) = Y }.
% 0.74/1.42 { proj1V( v( X ) ) = X }.
% 0.74/1.42 { ! n( X ) = add( Y, Z ) }.
% 0.74/1.42 { ! n( X ) = mul( Y, Z ) }.
% 0.74/1.42 { ! n( X ) = eq( Y, Z ) }.
% 0.74/1.42 { ! n( X ) = v( Y ) }.
% 0.74/1.42 { ! add( X, Y ) = mul( Z, T ) }.
% 0.74/1.42 { ! add( X, Y ) = eq( Z, T ) }.
% 0.74/1.42 { ! add( X, Y ) = v( Z ) }.
% 0.74/1.42 { ! mul( X, Y ) = eq( Z, T ) }.
% 0.74/1.42 { ! mul( X, Y ) = v( Z ) }.
% 0.74/1.42 { ! eq( X, Y ) = v( Z ) }.
% 0.74/1.42 { proj1Print( print( X ) ) = X }.
% 0.74/1.42 { proj1( x( X, Y ) ) = X }.
% 0.74/1.42 { proj2( x( X, Y ) ) = Y }.
% 0.74/1.42 { proj1While( while( X, Y ) ) = X }.
% 0.74/1.42 { proj2While( while( X, Y ) ) = Y }.
% 0.74/1.42 { proj1If( if( X, Y, Z ) ) = X }.
% 0.74/1.42 { proj2If( if( X, Y, Z ) ) = Y }.
% 0.74/1.42 { proj3If( if( X, Y, Z ) ) = Z }.
% 0.74/1.42 { ! print( X ) = x( Y, Z ) }.
% 0.74/1.42 { ! print( X ) = while( Y, Z ) }.
% 0.74/1.42 { ! print( X ) = if( Y, Z, T ) }.
% 0.74/1.42 { ! x( X, Y ) = while( Z, T ) }.
% 0.74/1.42 { ! x( X, Y ) = if( Z, T, U ) }.
% 0.74/1.42 { ! while( X, Y ) = if( Z, T, U ) }.
% 0.74/1.42 { head( cons( X, Y ) ) = X }.
% 0.74/1.42 { tail( cons( X, Y ) ) = Y }.
% 0.74/1.42 { ! nil = cons( X, Y ) }.
% 0.74/1.42 { head2( cons2( X, Y ) ) = X }.
% 0.74/1.42 { tail2( cons2( X, Y ) ) = Y }.
% 0.74/1.42 { ! nil2 = cons2( X, Y ) }.
% 0.74/1.42 { store( nil, zero, X ) = cons( X, nil ) }.
% 0.74/1.42 { store( nil, suc( Y ), X ) = cons( zero, store( nil, Y, X ) ) }.
% 0.74/1.42 { store( cons( Y, Z ), zero, X ) = cons( X, Z ) }.
% 0.74/1.42 { store( cons( Y, Z ), suc( T ), X ) = cons( Y, store( Z, T, X ) ) }.
% 0.74/1.42 { X = while( proj1While( X ), proj2While( X ) ), X = if( proj1If( X ),
% 0.74/1.42 proj2If( X ), proj3If( X ) ), opti2( X ) = X }.
% 0.74/1.42 { opti2( while( X, Y ) ) = while( X, map( lam, Y ) ) }.
% 0.74/1.42 { opti2( if( X, Y, Z ) ) = if( add( n( suc( zero ) ), X ), Z, Y ) }.
% 0.74/1.42 { fetch( nil, X ) = zero }.
% 0.74/1.42 { fetch( cons( X, Y ), zero ) = X }.
% 0.74/1.42 { fetch( cons( X, Y ), suc( Z ) ) = fetch( Y, Z ) }.
% 0.74/1.42 { addNat( zero, X ) = X }.
% 0.74/1.42 { addNat( suc( X ), zero ) = suc( X ) }.
% 0.74/1.42 { addNat( suc( X ), suc( Y ) ) = suc( addNat( X, suc( Y ) ) ) }.
% 0.74/1.42 { mulNat( zero, X ) = zero }.
% 0.74/1.42 { mulNat( suc( X ), zero ) = zero }.
% 0.74/1.42 { mulNat( suc( X ), suc( Y ) ) = addNat( mulNat( X, suc( Y ) ), suc( Y ) )
% 0.74/1.42 }.
% 0.74/1.42 { eval( X, n( Y ) ) = Y }.
% 0.74/1.42 { eval( X, add( Y, Z ) ) = addNat( eval( X, Y ), eval( X, Z ) ) }.
% 0.74/1.42 { eval( X, mul( Y, Z ) ) = mulNat( eval( X, Y ), eval( X, Z ) ) }.
% 0.74/1.42 { ! eval( X, Y ) = eval( X, Z ), eval( X, eq( Y, Z ) ) = suc( zero ) }.
% 0.74/1.42 { eval( X, Y ) = eval( X, Z ), eval( X, eq( Y, Z ) ) = zero }.
% 0.74/1.42 { eval( X, v( Y ) ) = fetch( X, Y ) }.
% 0.74/1.42 { run( X, nil2 ) = nil }.
% 0.74/1.42 { run( X, cons2( print( Z ), Y ) ) = cons( eval( X, Z ), run( X, Y ) ) }.
% 0.74/1.42 { run( X, cons2( x( Z, T ), Y ) ) = run( store( X, Z, eval( X, T ) ), Y ) }
% 0.74/1.42 .
% 0.74/1.42 { run( X, cons2( while( Z, T ), Y ) ) = run( X, cons2( if( Z, append( T,
% 0.74/1.42 cons2( while( Z, T ), nil2 ) ), nil2 ), Y ) ) }.
% 0.74/1.42 { ! eval( X, Y ) = zero, run( X, cons2( if( Y, T, U ), Z ) ) = run( X,
% 0.74/1.42 append( U, Z ) ) }.
% 0.74/1.42 { ! eval( X, Y ) = suc( Z ), run( X, cons2( if( Y, U, W ), T ) ) = run( X,
% 0.74/1.42 append( U, T ) ) }.
% 0.74/1.42 { map( X, nil2 ) = nil2 }.
% 0.74/1.42 { map( X, cons2( Y, Z ) ) = cons2( apply1( X, Y ), map( X, Z ) ) }.
% 0.74/1.42 { append( nil2, X ) = X }.
% 0.74/1.42 { append( cons2( Y, Z ), X ) = cons2( Y, append( Z, X ) ) }.
% 0.74/1.42 { apply1( lam, X ) = opti2( X ) }.
% 0.74/1.42 { run( nil, cons2( X, nil2 ) ) = run( nil, cons2( opti2( X ), nil2 ) ) }.
% 0.74/1.42
% 0.74/1.42 percentage equality = 1.000000, percentage horn = 0.972973
% 0.74/1.42 This is a pure equality problem
% 0.74/1.42
% 0.74/1.42
% 0.74/1.42
% 0.74/1.42 Options Used:
% 0.74/1.42
% 0.74/1.42 useres = 1
% 0.74/1.42 useparamod = 1
% 0.74/1.42 useeqrefl = 1
% 0.74/1.42 useeqfact = 1
% 0.74/1.42 usefactor = 1
% 0.74/1.42 usesimpsplitting = 0
% 0.74/1.42 usesimpdemod = 5
% 0.74/1.42 usesimpres = 3
% 0.74/1.42
% 0.74/1.42 resimpinuse = 1000
% 0.74/1.42 resimpclauses = 20000
% 0.74/1.42 substype = eqrewr
% 0.74/1.42 backwardsubs = 1
% 0.74/1.42 selectoldest = 5
% 0.74/1.42
% 0.74/1.42 litorderings [0] = split
% 0.74/1.42 litorderings [1] = extend the termordering, first sorting on arguments
% 0.74/1.42
% 0.74/1.42 termordering = kbo
% 0.74/1.42
% 0.74/1.42 litapriori = 0
% 0.74/1.42 termapriori = 1
% 0.74/1.42 litaposteriori = 0
% 0.74/1.42 termaposteriori = 0
% 0.74/1.42 demodaposteriori = 0
% 0.74/1.42 ordereqreflfact = 0
% 0.74/1.42
% 0.74/1.42 litselect = negord
% 3.83/4.27
% 3.83/4.27 maxweight = 15
% 3.83/4.27 maxdepth = 30000
% 3.83/4.27 maxlength = 115
% 3.83/4.27 maxnrvars = 195
% 3.83/4.27 excuselevel = 1
% 3.83/4.27 increasemaxweight = 1
% 3.83/4.27
% 3.83/4.27 maxselected = 10000000
% 3.83/4.27 maxnrclauses = 10000000
% 3.83/4.27
% 3.83/4.27 showgenerated = 0
% 3.83/4.27 showkept = 0
% 3.83/4.27 showselected = 0
% 3.83/4.27 showdeleted = 0
% 3.83/4.27 showresimp = 1
% 3.83/4.27 showstatus = 2000
% 3.83/4.27
% 3.83/4.27 prologoutput = 0
% 3.83/4.27 nrgoals = 5000000
% 3.83/4.27 totalproof = 1
% 3.83/4.27
% 3.83/4.27 Symbols occurring in the translation:
% 3.83/4.27
% 3.83/4.27 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.83/4.27 . [1, 2] (w:1, o:66, a:1, s:1, b:0),
% 3.83/4.27 ! [4, 1] (w:0, o:35, a:1, s:1, b:0),
% 3.83/4.27 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.83/4.27 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.83/4.27 suc [36, 1] (w:1, o:40, a:1, s:1, b:0),
% 3.83/4.27 proj1Suc [37, 1] (w:1, o:42, a:1, s:1, b:0),
% 3.83/4.27 zero [38, 0] (w:1, o:7, a:1, s:1, b:0),
% 3.83/4.27 n [39, 1] (w:1, o:43, a:1, s:1, b:0),
% 3.83/4.27 proj1N [40, 1] (w:1, o:45, a:1, s:1, b:0),
% 3.83/4.27 add [42, 2] (w:1, o:90, a:1, s:1, b:0),
% 3.83/4.27 proj1Add [43, 1] (w:1, o:46, a:1, s:1, b:0),
% 3.83/4.27 proj2Add [44, 1] (w:1, o:53, a:1, s:1, b:0),
% 3.83/4.27 mul [45, 2] (w:1, o:91, a:1, s:1, b:0),
% 3.83/4.27 proj1Mul [46, 1] (w:1, o:44, a:1, s:1, b:0),
% 3.83/4.27 proj2Mul [47, 1] (w:1, o:54, a:1, s:1, b:0),
% 3.83/4.27 eq [48, 2] (w:1, o:92, a:1, s:1, b:0),
% 3.83/4.27 proj1Eq [49, 1] (w:1, o:47, a:1, s:1, b:0),
% 3.83/4.27 proj2Eq [50, 1] (w:1, o:55, a:1, s:1, b:0),
% 3.83/4.27 v [51, 1] (w:1, o:56, a:1, s:1, b:0),
% 3.83/4.27 proj1V [52, 1] (w:1, o:48, a:1, s:1, b:0),
% 3.83/4.27 print [55, 1] (w:1, o:57, a:1, s:1, b:0),
% 3.83/4.27 proj1Print [56, 1] (w:1, o:49, a:1, s:1, b:0),
% 3.83/4.27 x [57, 2] (w:1, o:94, a:1, s:1, b:0),
% 3.83/4.27 proj1 [58, 1] (w:1, o:50, a:1, s:1, b:0),
% 3.83/4.27 proj2 [59, 1] (w:1, o:58, a:1, s:1, b:0),
% 3.83/4.27 while [60, 2] (w:1, o:93, a:1, s:1, b:0),
% 3.83/4.27 proj1While [61, 1] (w:1, o:51, a:1, s:1, b:0),
% 3.83/4.27 proj2While [62, 1] (w:1, o:59, a:1, s:1, b:0),
% 3.83/4.27 if [63, 3] (w:1, o:105, a:1, s:1, b:0),
% 3.83/4.27 proj1If [64, 1] (w:1, o:52, a:1, s:1, b:0),
% 3.83/4.27 proj2If [65, 1] (w:1, o:60, a:1, s:1, b:0),
% 3.83/4.27 proj3If [66, 1] (w:1, o:61, a:1, s:1, b:0),
% 3.83/4.27 cons [68, 2] (w:1, o:95, a:1, s:1, b:0),
% 3.83/4.27 head [69, 1] (w:1, o:62, a:1, s:1, b:0),
% 3.83/4.27 tail [70, 1] (w:1, o:63, a:1, s:1, b:0),
% 3.83/4.27 nil [71, 0] (w:1, o:12, a:1, s:1, b:0),
% 3.83/4.27 cons2 [72, 2] (w:1, o:96, a:1, s:1, b:0),
% 3.83/4.27 head2 [73, 1] (w:1, o:64, a:1, s:1, b:0),
% 3.83/4.27 tail2 [74, 1] (w:1, o:65, a:1, s:1, b:0),
% 3.83/4.27 nil2 [75, 0] (w:1, o:13, a:1, s:1, b:0),
% 3.83/4.27 store [77, 3] (w:1, o:106, a:1, s:1, b:0),
% 3.83/4.27 opti2 [80, 1] (w:1, o:41, a:1, s:1, b:0),
% 3.83/4.27 lam [83, 0] (w:1, o:24, a:1, s:1, b:0),
% 3.83/4.27 map [84, 2] (w:1, o:97, a:1, s:1, b:0),
% 3.83/4.27 fetch [89, 2] (w:1, o:99, a:1, s:1, b:0),
% 3.83/4.27 addNat [90, 2] (w:1, o:100, a:1, s:1, b:0),
% 3.83/4.27 mulNat [91, 2] (w:1, o:101, a:1, s:1, b:0),
% 3.83/4.27 eval [92, 2] (w:1, o:98, a:1, s:1, b:0),
% 3.83/4.27 run [98, 2] (w:1, o:102, a:1, s:1, b:0),
% 3.83/4.27 append [101, 2] (w:1, o:103, a:1, s:1, b:0),
% 3.83/4.27 apply1 [106, 2] (w:1, o:104, a:1, s:1, b:0).
% 3.83/4.27
% 3.83/4.27
% 3.83/4.27 Starting Search:
% 3.83/4.27
% 3.83/4.27 *** allocated 15000 integers for clauses
% 3.83/4.27 *** allocated 22500 integers for clauses
% 3.83/4.27 *** allocated 33750 integers for clauses
% 3.83/4.27 *** allocated 50625 integers for clauses
% 3.83/4.27 *** allocated 15000 integers for termspace/termends
% 3.83/4.27 *** allocated 75937 integers for clauses
% 3.83/4.27 *** allocated 22500 integers for termspace/termends
% 3.83/4.27 *** allocated 113905 integers for clauses
% 3.83/4.27 Resimplifying inuse:
% 3.83/4.27 Done
% 3.83/4.27
% 3.83/4.27 *** allocated 33750 integers for termspace/termends
% 3.83/4.27 *** allocated 170857 integers for clauses
% 3.83/4.27
% 3.83/4.27 Intermediate Status:
% 3.83/4.27 Generated: 12938
% 3.83/4.27 Kept: 2172
% 3.83/4.27 Inuse: 206
% 3.83/4.27 Deleted: 9
% 3.83/4.27 Deletedinuse: 3
% 3.83/4.27
% 3.83/4.27 Resimplifying inuse:
% 3.83/4.27 Done
% 3.83/4.27
% 3.83/4.27 *** allocated 50625 integers for termspace/termends
% 3.83/4.27 *** allocated 256285 integers for clauses
% 3.83/4.27 Resimplifying inuse:
% 3.83/4.27 Done
% 3.83/4.27
% 3.83/4.27 *** allocated 75937 integers for termspace/termends
% 3.83/4.27
% 3.83/4.27 Intermediate Status:
% 3.83/4.27 Generated: 23085
% 3.83/4.27 Kept: 4186
% 3.83/4.27 Inuse: 245
% 3.83/4.27 Deleted: 10
% 3.83/4.27 Deletedinuse: 3
% 3.83/4.27
% 3.83/4.27 Resimplifying inuse:
% 3.83/4.27 Done
% 3.83/4.27
% 3.83/4.27 *** allocated 384427 integers for clauses
% 3.83/4.27 *** allocated 113905 integers for termspace/termends
% 3.83/4.27 Resimplifying inuse:
% 3.83/4.27 Done
% 3.83/4.27
% 3.83/4.27
% 3.83/4.27 Intermediate Status:
% 3.83/4.27 Generated: 37191
% 18.12/18.55 Kept: 6652
% 18.12/18.55 Inuse: 310
% 18.12/18.55 Deleted: 11
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 *** allocated 576640 integers for clauses
% 18.12/18.55 *** allocated 170857 integers for termspace/termends
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 46802
% 18.12/18.55 Kept: 9097
% 18.12/18.55 Inuse: 316
% 18.12/18.55 Deleted: 11
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 54878
% 18.12/18.55 Kept: 11116
% 18.12/18.55 Inuse: 321
% 18.12/18.55 Deleted: 11
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 *** allocated 256285 integers for termspace/termends
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 *** allocated 864960 integers for clauses
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 63411
% 18.12/18.55 Kept: 13198
% 18.12/18.55 Inuse: 326
% 18.12/18.55 Deleted: 11
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 73279
% 18.12/18.55 Kept: 15235
% 18.12/18.55 Inuse: 350
% 18.12/18.55 Deleted: 11
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 *** allocated 384427 integers for termspace/termends
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 82636
% 18.12/18.55 Kept: 17243
% 18.12/18.55 Inuse: 379
% 18.12/18.55 Deleted: 11
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 *** allocated 1297440 integers for clauses
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 93075
% 18.12/18.55 Kept: 19257
% 18.12/18.55 Inuse: 402
% 18.12/18.55 Deleted: 11
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying clauses:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 101235
% 18.12/18.55 Kept: 21377
% 18.12/18.55 Inuse: 429
% 18.12/18.55 Deleted: 321
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 107047
% 18.12/18.55 Kept: 23382
% 18.12/18.55 Inuse: 455
% 18.12/18.55 Deleted: 321
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 *** allocated 576640 integers for termspace/termends
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 119617
% 18.12/18.55 Kept: 25644
% 18.12/18.55 Inuse: 484
% 18.12/18.55 Deleted: 321
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 *** allocated 1946160 integers for clauses
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 128965
% 18.12/18.55 Kept: 27652
% 18.12/18.55 Inuse: 506
% 18.12/18.55 Deleted: 321
% 18.12/18.55 Deletedinuse: 3
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 142543
% 18.12/18.55 Kept: 29682
% 18.12/18.55 Inuse: 520
% 18.12/18.55 Deleted: 322
% 18.12/18.55 Deletedinuse: 4
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 153814
% 18.12/18.55 Kept: 31713
% 18.12/18.55 Inuse: 541
% 18.12/18.55 Deleted: 323
% 18.12/18.55 Deletedinuse: 5
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 168371
% 18.12/18.55 Kept: 33766
% 18.12/18.55 Inuse: 554
% 18.12/18.55 Deleted: 324
% 18.12/18.55 Deletedinuse: 6
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 179785
% 18.12/18.55 Kept: 35843
% 18.12/18.55 Inuse: 572
% 18.12/18.55 Deleted: 325
% 18.12/18.55 Deletedinuse: 7
% 18.12/18.55
% 18.12/18.55 *** allocated 864960 integers for termspace/termends
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 196844
% 18.12/18.55 Kept: 38358
% 18.12/18.55 Inuse: 590
% 18.12/18.55 Deleted: 325
% 18.12/18.55 Deletedinuse: 7
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying clauses:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 208573
% 18.12/18.55 Kept: 40412
% 18.12/18.55 Inuse: 606
% 18.12/18.55 Deleted: 657
% 18.12/18.55 Deletedinuse: 7
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 *** allocated 2919240 integers for clauses
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 220392
% 18.12/18.55 Kept: 42450
% 18.12/18.55 Inuse: 625
% 18.12/18.55 Deleted: 657
% 18.12/18.55 Deletedinuse: 7
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 238560
% 18.12/18.55 Kept: 45083
% 18.12/18.55 Inuse: 640
% 18.12/18.55 Deleted: 657
% 18.12/18.55 Deletedinuse: 7
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 251305
% 18.12/18.55 Kept: 47123
% 18.12/18.55 Inuse: 656
% 18.12/18.55 Deleted: 657
% 18.12/18.55 Deletedinuse: 7
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 267419
% 18.12/18.55 Kept: 49127
% 18.12/18.55 Inuse: 692
% 18.12/18.55 Deleted: 657
% 18.12/18.55 Deletedinuse: 7
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 18.12/18.55 Generated: 287627
% 18.12/18.55 Kept: 51167
% 18.12/18.55 Inuse: 732
% 18.12/18.55 Deleted: 657
% 18.12/18.55 Deletedinuse: 7
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55 Resimplifying inuse:
% 18.12/18.55 Done
% 18.12/18.55
% 18.12/18.55
% 18.12/18.55 Intermediate Status:
% 86.39/86.84 Generated: 311646
% 86.39/86.84 Kept: 53167
% 86.39/86.84 Inuse: 788
% 86.39/86.84 Deleted: 657
% 86.39/86.84 Deletedinuse: 7
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 *** allocated 1297440 integers for termspace/termends
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 330977
% 86.39/86.84 Kept: 55195
% 86.39/86.84 Inuse: 842
% 86.39/86.84 Deleted: 657
% 86.39/86.84 Deletedinuse: 7
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 375177
% 86.39/86.84 Kept: 57234
% 86.39/86.84 Inuse: 889
% 86.39/86.84 Deleted: 657
% 86.39/86.84 Deletedinuse: 7
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 *** allocated 4378860 integers for clauses
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 404294
% 86.39/86.84 Kept: 59247
% 86.39/86.84 Inuse: 937
% 86.39/86.84 Deleted: 657
% 86.39/86.84 Deletedinuse: 7
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying clauses:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 431515
% 86.39/86.84 Kept: 61269
% 86.39/86.84 Inuse: 952
% 86.39/86.84 Deleted: 851
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 482229
% 86.39/86.84 Kept: 63299
% 86.39/86.84 Inuse: 995
% 86.39/86.84 Deleted: 851
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 517325
% 86.39/86.84 Kept: 65523
% 86.39/86.84 Inuse: 1011
% 86.39/86.84 Deleted: 851
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 541278
% 86.39/86.84 Kept: 67533
% 86.39/86.84 Inuse: 1021
% 86.39/86.84 Deleted: 851
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 580813
% 86.39/86.84 Kept: 70787
% 86.39/86.84 Inuse: 1036
% 86.39/86.84 Deleted: 851
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 630895
% 86.39/86.84 Kept: 74390
% 86.39/86.84 Inuse: 1060
% 86.39/86.84 Deleted: 851
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 665390
% 86.39/86.84 Kept: 78026
% 86.39/86.84 Inuse: 1084
% 86.39/86.84 Deleted: 851
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 *** allocated 1946160 integers for termspace/termends
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 699480
% 86.39/86.84 Kept: 81695
% 86.39/86.84 Inuse: 1107
% 86.39/86.84 Deleted: 851
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying clauses:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 735306
% 86.39/86.84 Kept: 85412
% 86.39/86.84 Inuse: 1131
% 86.39/86.84 Deleted: 1268
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 *** allocated 6568290 integers for clauses
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 772436
% 86.39/86.84 Kept: 89190
% 86.39/86.84 Inuse: 1156
% 86.39/86.84 Deleted: 1268
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 804853
% 86.39/86.84 Kept: 91770
% 86.39/86.84 Inuse: 1180
% 86.39/86.84 Deleted: 1268
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 836885
% 86.39/86.84 Kept: 94665
% 86.39/86.84 Inuse: 1184
% 86.39/86.84 Deleted: 1268
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 867935
% 86.39/86.84 Kept: 97573
% 86.39/86.84 Inuse: 1187
% 86.39/86.84 Deleted: 1268
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 900159
% 86.39/86.84 Kept: 100486
% 86.39/86.84 Inuse: 1191
% 86.39/86.84 Deleted: 1268
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying clauses:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 929246
% 86.39/86.84 Kept: 102974
% 86.39/86.84 Inuse: 1199
% 86.39/86.84 Deleted: 1513
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 952071
% 86.39/86.84 Kept: 105004
% 86.39/86.84 Inuse: 1206
% 86.39/86.84 Deleted: 1513
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 984898
% 86.39/86.84 Kept: 107945
% 86.39/86.84 Inuse: 1210
% 86.39/86.84 Deleted: 1513
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 1017993
% 86.39/86.84 Kept: 110891
% 86.39/86.84 Inuse: 1214
% 86.39/86.84 Deleted: 1513
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 86.39/86.84
% 86.39/86.84
% 86.39/86.84 Intermediate Status:
% 86.39/86.84 Generated: 1046159
% 86.39/86.84 Kept: 113304
% 86.39/86.84 Inuse: 1220
% 86.39/86.84 Deleted: 1513
% 86.39/86.84 Deletedinuse: 8
% 86.39/86.84
% 86.39/86.84 Resimplifying inuse:
% 86.39/86.84 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1078273
% 263.26/263.74 Kept: 115996
% 263.26/263.74 Inuse: 1230
% 263.26/263.74 Deleted: 1513
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1112066
% 263.26/263.74 Kept: 118978
% 263.26/263.74 Inuse: 1234
% 263.26/263.74 Deleted: 1513
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1141078
% 263.26/263.74 Kept: 121396
% 263.26/263.74 Inuse: 1240
% 263.26/263.74 Deleted: 1513
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying clauses:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 *** allocated 2919240 integers for termspace/termends
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1166756
% 263.26/263.74 Kept: 123438
% 263.26/263.74 Inuse: 1249
% 263.26/263.74 Deleted: 1751
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1196945
% 263.26/263.74 Kept: 125950
% 263.26/263.74 Inuse: 1255
% 263.26/263.74 Deleted: 1751
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1225818
% 263.26/263.74 Kept: 128372
% 263.26/263.74 Inuse: 1261
% 263.26/263.74 Deleted: 1751
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1257632
% 263.26/263.74 Kept: 130486
% 263.26/263.74 Inuse: 1270
% 263.26/263.74 Deleted: 1751
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1302686
% 263.26/263.74 Kept: 132515
% 263.26/263.74 Inuse: 1308
% 263.26/263.74 Deleted: 1752
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 *** allocated 9852435 integers for clauses
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1343941
% 263.26/263.74 Kept: 134580
% 263.26/263.74 Inuse: 1339
% 263.26/263.74 Deleted: 1752
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1379957
% 263.26/263.74 Kept: 136604
% 263.26/263.74 Inuse: 1369
% 263.26/263.74 Deleted: 1752
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1419355
% 263.26/263.74 Kept: 138679
% 263.26/263.74 Inuse: 1399
% 263.26/263.74 Deleted: 1752
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1456995
% 263.26/263.74 Kept: 140723
% 263.26/263.74 Inuse: 1428
% 263.26/263.74 Deleted: 1752
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying clauses:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1493966
% 263.26/263.74 Kept: 142756
% 263.26/263.74 Inuse: 1456
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1532074
% 263.26/263.74 Kept: 144775
% 263.26/263.74 Inuse: 1485
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1570612
% 263.26/263.74 Kept: 146788
% 263.26/263.74 Inuse: 1514
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1622615
% 263.26/263.74 Kept: 148842
% 263.26/263.74 Inuse: 1544
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1668237
% 263.26/263.74 Kept: 150903
% 263.26/263.74 Inuse: 1578
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1710729
% 263.26/263.74 Kept: 152959
% 263.26/263.74 Inuse: 1611
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1754394
% 263.26/263.74 Kept: 155016
% 263.26/263.74 Inuse: 1645
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1797636
% 263.26/263.74 Kept: 157035
% 263.26/263.74 Inuse: 1679
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1853044
% 263.26/263.74 Kept: 159040
% 263.26/263.74 Inuse: 1745
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1921926
% 263.26/263.74 Kept: 161057
% 263.26/263.74 Inuse: 1793
% 263.26/263.74 Deleted: 2295
% 263.26/263.74 Deletedinuse: 8
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying clauses:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74 Resimplifying inuse:
% 263.26/263.74 Done
% 263.26/263.74
% 263.26/263.74
% 263.26/263.74 Intermediate Status:
% 263.26/263.74 Generated: 1967871
% 263.26/263.74 Kept: 163143
% 263.26/263.74 Inuse: 1835
% 263.26/263.74 Deleted: 2976
% 263.26/263.74 DeleteTerminated
% 299.58/300.03 Bliksem ended
%------------------------------------------------------------------------------