%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX216-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n006.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:49 PM UTC 2026
% Result : Timeout 299.67s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX216-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.18/0.33 % Computer : n006.cluster.edu
% 0.18/0.33 % Model : x86_64 x86_64
% 0.18/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.33 % Memory : 8042.1875MB
% 0.18/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.33 % CPULimit : 300
% 0.18/0.33 % DateTime : Tue May 5 12:12:45 EDT 2026
% 0.18/0.33 % CPUTime :
% 0.70/1.10 *** allocated 10000 integers for termspace/termends
% 0.70/1.10 *** allocated 10000 integers for clauses
% 0.70/1.10 *** allocated 10000 integers for justifications
% 0.70/1.10 Bliksem 1.12
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10 Automatic Strategy Selection
% 0.70/1.10
% 0.70/1.10 Clauses:
% 0.70/1.10 [
% 0.70/1.10 [ =( aux( X, Y, Z, btrue ), del( X, Z ) ) ],
% 0.70/1.10 [ =( aux( X, Y, Z, bfalse ), cons( Y, del( X, Z ) ) ) ],
% 0.70/1.10 [ =( aux2( X, Y, Z, btrue ), pair2( cons( Y, X ), bfalse ) ) ],
% 0.70/1.10 [ =( aux2( X, Y, Z, bfalse ), pair2( del( Y, X ), bfalse ) ) ],
% 0.70/1.10 [ =( aux3( X, Y, Z, pair2( T, btrue ) ), pair2( T, btrue ) ) ],
% 0.70/1.10 [ =( aux3( X, Y, Z, pair2( T, bfalse ) ), run( T, Z ) ) ],
% 0.70/1.10 [ =( aux4( X, Y, Z, T, btrue ), run( X, Z ) ) ],
% 0.70/1.10 [ =( aux4( X, Y, Z, T, bfalse ), run( X, T ) ) ],
% 0.70/1.10 [ =( aux5( X, Y, Z, pair2( T, btrue ) ), run( T, Z ) ) ],
% 0.70/1.10 [ =( aux5( X, Y, Z, pair2( T, bfalse ) ), pair2( T, bfalse ) ) ],
% 0.70/1.10 [ =( aux6( X, Y, Z, pair2( T, U ) ), impl( typeCorrect( bfalse, X ), eq5(
% 0.70/1.10 elem( l, Z ), elem( l, T ) ) ) ) ],
% 0.70/1.10 [ =( aux7( X, Y, pair2( Z, T ) ), aux6( X, Y, Z, run( cons( h, Y ), X )
% 0.70/1.10 ) ) ],
% 0.70/1.10 [ =( orb( btrue, X ), btrue ) ],
% 0.70/1.10 [ =( orb( bfalse, X ), X ) ],
% 0.70/1.10 [ =( secret( nand( X, Y ) ), orb( secret( X ), secret( Y ) ) ) ],
% 0.70/1.10 [ =( secret( var( high( X ) ) ), btrue ) ],
% 0.70/1.10 [ =( secret( var( low( X ) ) ), bfalse ) ],
% 0.70/1.10 [ =( secret( tT ), bfalse ) ],
% 0.70/1.10 [ =( secret( fF ), bfalse ) ],
% 0.70/1.10 [ =( notb( btrue ), bfalse ) ],
% 0.70/1.10 [ =( notb( bfalse ), btrue ) ],
% 0.70/1.10 [ =( l, low( zero ) ) ],
% 0.70/1.10 [ =( impl( btrue, X ), X ) ],
% 0.70/1.10 [ =( impl( bfalse, X ), btrue ) ],
% 0.70/1.10 [ =( h, high( zero ) ) ],
% 0.70/1.10 [ =( elem( X, nil ), bfalse ) ],
% 0.70/1.10 [ =( elem( X, cons( Y, Z ) ), orb( eq2( Y, X ), elem( X, Z ) ) ) ],
% 0.70/1.10 [ =( del( X, nil ), nil ) ],
% 0.70/1.10 [ =( del( X, cons( Y, Z ) ), aux( X, Y, Z, eq2( X, Y ) ) ) ],
% 0.70/1.10 [ =( andb( btrue, X ), X ) ],
% 0.70/1.10 [ =( andb( bfalse, X ), bfalse ) ],
% 0.70/1.10 [ =( eval( X, nand( Y, Z ) ), notb( andb( eval( X, Y ), eval( X, Z ) ) )
% 0.70/1.10 ) ],
% 0.70/1.10 [ =( eval( X, tT ), btrue ) ],
% 0.70/1.10 [ =( eval( X, fF ), bfalse ) ],
% 0.70/1.10 [ =( eval( X, var( Y ) ), elem( Y, X ) ) ],
% 0.70/1.10 [ =( run( X, skip ), pair2( X, bfalse ) ) ],
% 0.70/1.10 [ =( run( X, assign( Y, Z ) ), aux2( X, Y, Z, eval( X, Z ) ) ) ],
% 0.70/1.10 [ =( run( X, seq( Y, Z ) ), aux3( X, Y, Z, run( X, Y ) ) ) ],
% 0.70/1.10 [ =( run( X, ifThenElse( Y, Z, T ) ), aux4( X, Y, Z, T, eval( X, Y ) ) )
% 0.70/1.10 ],
% 0.70/1.10 [ =( run( X, catch( Y, Z ) ), aux5( X, Y, Z, run( X, Y ) ) ) ],
% 0.70/1.10 [ =( run( X, throw ), pair2( X, btrue ) ) ],
% 0.70/1.10 [ =( run( X, while( Y, Z ) ), run( X, ifThenElse( Y, seq( Z, while( Y, Z
% 0.70/1.10 ) ), skip ) ) ) ],
% 0.70/1.10 [ =( typeCorrect( X, assign( high( Y ), Z ) ), btrue ) ],
% 0.70/1.10 [ =( typeCorrect( X, assign( low( Y ), Z ) ), andb( notb( X ), notb(
% 0.70/1.10 secret( Z ) ) ) ) ],
% 0.70/1.10 [ =( typeCorrect( X, seq( Y, Z ) ), andb( typeCorrect( X, Y ),
% 0.70/1.10 typeCorrect( X, Z ) ) ) ],
% 0.70/1.10 [ =( typeCorrect( X, ifThenElse( Y, Z, T ) ), andb( typeCorrect( orb(
% 0.70/1.10 secret( Y ), X ), Z ), typeCorrect( orb( secret( Y ), X ), T ) ) ) ],
% 0.70/1.10 [ =( typeCorrect( X, catch( Y, Z ) ), andb( typeCorrect( X, Y ),
% 0.70/1.10 typeCorrect( X, Z ) ) ) ],
% 0.70/1.10 [ =( typeCorrect( X, while( Y, Z ) ), typeCorrect( orb( secret( Y ), X )
% 0.70/1.10 , Z ) ) ],
% 0.70/1.10 [ =( typeCorrect( X, skip ), btrue ) ],
% 0.70/1.10 [ =( typeCorrect( X, throw ), btrue ) ],
% 0.70/1.10 [ =( prop( X, Y ), aux7( X, Y, run( Y, X ) ) ) ],
% 0.70/1.10 [ =( eq3( tT, fF ), bfalse ) ],
% 0.70/1.10 [ =( eq3( fF, tT ), bfalse ) ],
% 0.70/1.10 [ =( eq4( skip, throw ), bfalse ) ],
% 0.70/1.10 [ =( eq4( throw, skip ), bfalse ) ],
% 0.70/1.10 [ =( eq5( bfalse, btrue ), bfalse ) ],
% 0.70/1.10 [ =( eq5( btrue, bfalse ), bfalse ) ],
% 0.70/1.10 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( nand( X, Z ), nand( Y, T ) ),
% 0.70/1.10 bfalse ) ],
% 0.70/1.10 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( nand( X, Z ), nand( Y, T ) ),
% 0.70/1.10 eq3( Z, T ) ) ],
% 0.70/1.10 [ =( eq3( var( X ), var( Y ) ), eq2( X, Y ) ) ],
% 0.70/1.10 [ =( eq3( nand( X, Y ), tT ), bfalse ) ],
% 0.70/1.10 [ =( eq3( nand( X, Y ), fF ), bfalse ) ],
% 0.70/1.10 [ =( eq3( nand( X, Y ), var( Z ) ), bfalse ) ],
% 0.70/1.10 [ =( eq3( tT, nand( X, Y ) ), bfalse ) ],
% 0.70/1.10 [ =( eq3( tT, var( X ) ), bfalse ) ],
% 0.70/1.10 [ =( eq3( fF, nand( X, Y ) ), bfalse ) ],
% 0.70/1.10 [ =( eq3( fF, var( X ) ), bfalse ) ],
% 0.70/1.10 [ =( eq3( var( X ), nand( Y, Z ) ), bfalse ) ],
% 0.70/1.10 [ =( eq3( var( X ), tT ), bfalse ) ],
% 0.70/1.10 [ =( eq3( var( X ), fF ), bfalse ) ],
% 0.70/1.10 [ =( eq2( high( X ), high( Y ) ), eq( X, Y ) ) ],
% 2.93/3.40 [ =( eq2( low( X ), low( Y ) ), eq( X, Y ) ) ],
% 2.93/3.40 [ =( eq2( high( X ), low( Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq2( low( X ), high( Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ],
% 2.93/3.40 [ =( eq( zero, suc( X ) ), bfalse ) ],
% 2.93/3.40 [ =( eq( suc( X ), zero ), bfalse ) ],
% 2.93/3.40 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq4( assign( X, Z ), assign( Y, T )
% 2.93/3.40 ), bfalse ) ],
% 2.93/3.40 [ ~( =( eq2( X, Y ), btrue ) ), =( eq4( assign( X, Z ), assign( Y, T ) )
% 2.93/3.40 , eq3( Z, T ) ) ],
% 2.93/3.40 [ ~( =( eq4( X, Y ), bfalse ) ), =( eq4( seq( X, Z ), seq( Y, T ) ),
% 2.93/3.40 bfalse ) ],
% 2.93/3.40 [ ~( =( eq4( X, Y ), btrue ) ), =( eq4( seq( X, Z ), seq( Y, T ) ), eq4(
% 2.93/3.40 Z, T ) ) ],
% 2.93/3.40 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq4( ifThenElse( X, Z, T ),
% 2.93/3.40 ifThenElse( Y, U, W ) ), bfalse ) ],
% 2.93/3.40 [ ~( =( eq3( X, Y ), btrue ) ), ~( =( eq4( Z, T ), bfalse ) ), =( eq4(
% 2.93/3.40 ifThenElse( X, Z, U ), ifThenElse( Y, T, W ) ), bfalse ) ],
% 2.93/3.40 [ ~( =( eq3( X, Y ), btrue ) ), ~( =( eq4( Z, T ), btrue ) ), =( eq4(
% 2.93/3.40 ifThenElse( X, Z, U ), ifThenElse( Y, T, W ) ), eq4( U, W ) ) ],
% 2.93/3.40 [ ~( =( eq4( X, Y ), bfalse ) ), =( eq4( catch( X, Z ), catch( Y, T ) )
% 2.93/3.40 , bfalse ) ],
% 2.93/3.40 [ ~( =( eq4( X, Y ), btrue ) ), =( eq4( catch( X, Z ), catch( Y, T ) ),
% 2.93/3.40 eq4( Z, T ) ) ],
% 2.93/3.40 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq4( while( X, Z ), while( Y, T ) )
% 2.93/3.40 , bfalse ) ],
% 2.93/3.40 [ ~( =( eq3( X, Y ), btrue ) ), =( eq4( while( X, Z ), while( Y, T ) ),
% 2.93/3.40 eq4( Z, T ) ) ],
% 2.93/3.40 [ =( eq4( skip, assign( X, Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( skip, seq( X, Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( skip, ifThenElse( X, Y, Z ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( skip, catch( X, Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( skip, while( X, Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( assign( X, Y ), skip ), bfalse ) ],
% 2.93/3.40 [ =( eq4( assign( X, Y ), seq( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( assign( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( assign( X, Y ), catch( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( assign( X, Y ), throw ), bfalse ) ],
% 2.93/3.40 [ =( eq4( assign( X, Y ), while( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( seq( X, Y ), skip ), bfalse ) ],
% 2.93/3.40 [ =( eq4( seq( X, Y ), assign( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( seq( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( seq( X, Y ), catch( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( seq( X, Y ), throw ), bfalse ) ],
% 2.93/3.40 [ =( eq4( seq( X, Y ), while( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( ifThenElse( X, Y, Z ), skip ), bfalse ) ],
% 2.93/3.40 [ =( eq4( ifThenElse( X, Y, Z ), assign( T, U ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( ifThenElse( X, Y, Z ), seq( T, U ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( ifThenElse( X, Y, Z ), catch( T, U ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( ifThenElse( X, Y, Z ), throw ), bfalse ) ],
% 2.93/3.40 [ =( eq4( ifThenElse( X, Y, Z ), while( T, U ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( catch( X, Y ), skip ), bfalse ) ],
% 2.93/3.40 [ =( eq4( catch( X, Y ), assign( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( catch( X, Y ), seq( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( catch( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( catch( X, Y ), throw ), bfalse ) ],
% 2.93/3.40 [ =( eq4( catch( X, Y ), while( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( throw, assign( X, Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( throw, seq( X, Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( throw, ifThenElse( X, Y, Z ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( throw, catch( X, Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( throw, while( X, Y ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( while( X, Y ), skip ), bfalse ) ],
% 2.93/3.40 [ =( eq4( while( X, Y ), assign( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( while( X, Y ), seq( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( while( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( while( X, Y ), catch( Z, T ) ), bfalse ) ],
% 2.93/3.40 [ =( eq4( while( X, Y ), throw ), bfalse ) ],
% 2.93/3.40 [ =( eq( X, X ), btrue ) ],
% 2.93/3.40 [ =( eq2( X, X ), btrue ) ],
% 2.93/3.40 [ =( eq3( X, X ), btrue ) ],
% 2.93/3.40 [ =( eq4( X, X ), btrue ) ],
% 2.93/3.40 [ =( eq5( X, X ), btrue ) ],
% 2.93/3.40 [ ~( =( eq5( prop( X, Y ), bfalse ), btrue ) ) ]
% 2.93/3.40 ] .
% 2.93/3.40
% 2.93/3.40
% 2.93/3.40 percentage equality = 1.000000, percentage horn = 1.000000
% 2.93/3.40 This is a pure equality problem
% 2.93/3.40
% 2.93/3.40
% 2.93/3.40
% 2.93/3.40 Options Used:
% 2.93/3.40
% 2.93/3.40 useres = 1
% 2.93/3.40 useparamod = 1
% 2.93/3.40 useeqrefl = 1
% 2.93/3.40 useeqfact = 1
% 2.93/3.40 usefactor = 1
% 2.93/3.40 usesimpsplitting = 0
% 50.43/50.80 usesimpdemod = 5
% 50.43/50.80 usesimpres = 3
% 50.43/50.80
% 50.43/50.80 resimpinuse = 1000
% 50.43/50.80 resimpclauses = 20000
% 50.43/50.80 substype = eqrewr
% 50.43/50.80 backwardsubs = 1
% 50.43/50.80 selectoldest = 5
% 50.43/50.80
% 50.43/50.80 litorderings [0] = split
% 50.43/50.80 litorderings [1] = extend the termordering, first sorting on arguments
% 50.43/50.80
% 50.43/50.80 termordering = kbo
% 50.43/50.80
% 50.43/50.80 litapriori = 0
% 50.43/50.80 termapriori = 1
% 50.43/50.80 litaposteriori = 0
% 50.43/50.80 termaposteriori = 0
% 50.43/50.80 demodaposteriori = 0
% 50.43/50.80 ordereqreflfact = 0
% 50.43/50.80
% 50.43/50.80 litselect = negord
% 50.43/50.80
% 50.43/50.80 maxweight = 15
% 50.43/50.80 maxdepth = 30000
% 50.43/50.80 maxlength = 115
% 50.43/50.80 maxnrvars = 195
% 50.43/50.80 excuselevel = 1
% 50.43/50.80 increasemaxweight = 1
% 50.43/50.80
% 50.43/50.80 maxselected = 10000000
% 50.43/50.80 maxnrclauses = 10000000
% 50.43/50.80
% 50.43/50.80 showgenerated = 0
% 50.43/50.80 showkept = 0
% 50.43/50.80 showselected = 0
% 50.43/50.80 showdeleted = 0
% 50.43/50.80 showresimp = 1
% 50.43/50.80 showstatus = 2000
% 50.43/50.80
% 50.43/50.80 prologoutput = 1
% 50.43/50.80 nrgoals = 5000000
% 50.43/50.80 totalproof = 1
% 50.43/50.80
% 50.43/50.80 Symbols occurring in the translation:
% 50.43/50.80
% 50.43/50.80 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 50.43/50.80 . [1, 2] (w:1, o:55, a:1, s:1, b:0),
% 50.43/50.80 ! [4, 1] (w:0, o:44, a:1, s:1, b:0),
% 50.43/50.80 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 50.43/50.80 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 50.43/50.80 btrue [42, 0] (w:1, o:20, a:1, s:1, b:0),
% 50.43/50.80 aux [43, 4] (w:1, o:103, a:1, s:1, b:0),
% 50.43/50.80 del [44, 2] (w:1, o:82, a:1, s:1, b:0),
% 50.43/50.80 bfalse [45, 0] (w:1, o:21, a:1, s:1, b:0),
% 50.43/50.80 cons [46, 2] (w:1, o:80, a:1, s:1, b:0),
% 50.43/50.80 aux2 [48, 4] (w:1, o:104, a:1, s:1, b:0),
% 50.43/50.80 pair2 [49, 2] (w:1, o:85, a:1, s:1, b:0),
% 50.43/50.80 aux3 [53, 4] (w:1, o:105, a:1, s:1, b:0),
% 50.43/50.80 run [54, 2] (w:1, o:86, a:1, s:1, b:0),
% 50.43/50.80 aux4 [58, 5] (w:1, o:108, a:1, s:1, b:0),
% 50.43/50.80 aux5 [62, 4] (w:1, o:106, a:1, s:1, b:0),
% 50.43/50.80 aux6 [66, 4] (w:1, o:107, a:1, s:1, b:0),
% 50.43/50.80 typeCorrect [67, 2] (w:1, o:88, a:1, s:1, b:0),
% 50.43/50.80 l [68, 0] (w:1, o:33, a:1, s:1, b:0),
% 50.43/50.80 elem [69, 2] (w:1, o:89, a:1, s:1, b:0),
% 50.43/50.80 eq5 [70, 2] (w:1, o:91, a:1, s:1, b:0),
% 50.43/50.80 impl [71, 2] (w:1, o:92, a:1, s:1, b:0),
% 50.43/50.80 aux7 [73, 3] (w:1, o:101, a:1, s:1, b:0),
% 50.43/50.80 h [74, 0] (w:1, o:34, a:1, s:1, b:0),
% 50.43/50.80 orb [75, 2] (w:1, o:84, a:1, s:1, b:0),
% 50.43/50.80 nand [78, 2] (w:1, o:83, a:1, s:1, b:0),
% 50.43/50.80 secret [79, 1] (w:1, o:49, a:1, s:1, b:0),
% 50.43/50.80 high [80, 1] (w:1, o:50, a:1, s:1, b:0),
% 50.43/50.80 var [81, 1] (w:1, o:51, a:1, s:1, b:0),
% 50.43/50.80 low [82, 1] (w:1, o:52, a:1, s:1, b:0),
% 50.43/50.80 tT [83, 0] (w:1, o:37, a:1, s:1, b:0),
% 50.43/50.80 fF [84, 0] (w:1, o:38, a:1, s:1, b:0),
% 50.43/50.80 notb [85, 1] (w:1, o:53, a:1, s:1, b:0),
% 50.43/50.80 zero [86, 0] (w:1, o:39, a:1, s:1, b:0),
% 50.43/50.80 nil [87, 0] (w:1, o:40, a:1, s:1, b:0),
% 50.43/50.80 eq2 [89, 2] (w:1, o:93, a:1, s:1, b:0),
% 50.43/50.80 andb [90, 2] (w:1, o:94, a:1, s:1, b:0),
% 50.43/50.80 eval [91, 2] (w:1, o:95, a:1, s:1, b:0),
% 50.43/50.80 skip [92, 0] (w:1, o:5, a:1, s:1, b:0),
% 50.43/50.80 assign [93, 2] (w:1, o:96, a:1, s:1, b:0),
% 50.43/50.80 seq [94, 2] (w:1, o:87, a:1, s:1, b:0),
% 50.43/50.80 ifThenElse [95, 3] (w:1, o:102, a:1, s:1, b:0),
% 50.43/50.80 catch [96, 2] (w:1, o:81, a:1, s:1, b:0),
% 50.43/50.80 throw [97, 0] (w:1, o:41, a:1, s:1, b:0),
% 50.43/50.80 while [100, 2] (w:1, o:97, a:1, s:1, b:0),
% 50.43/50.80 prop [103, 2] (w:1, o:98, a:1, s:1, b:0),
% 50.43/50.80 eq3 [104, 2] (w:1, o:99, a:1, s:1, b:0),
% 50.43/50.80 eq4 [105, 2] (w:1, o:90, a:1, s:1, b:0),
% 50.43/50.80 eq [106, 2] (w:1, o:100, a:1, s:1, b:0),
% 50.43/50.80 suc [107, 1] (w:1, o:54, a:1, s:1, b:0).
% 50.43/50.80
% 50.43/50.80
% 50.43/50.80 Starting Search:
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80 Failed to find proof!
% 50.43/50.80 maxweight = 15
% 50.43/50.80 maxnrclauses = 10000000
% 50.43/50.80 Generated: 83506
% 50.43/50.80 Kept: 1417
% 50.43/50.80
% 50.43/50.80
% 50.43/50.80 The strategy used was not complete!
% 50.43/50.80
% 50.43/50.80 Increased maxweight to 16
% 50.43/50.80
% 50.43/50.80 Starting Search:
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80 Failed to find proof!
% 50.43/50.80 maxweight = 16
% 50.43/50.80 maxnrclauses = 10000000
% 50.43/50.80 Generated: 99183
% 50.43/50.80 Kept: 1663
% 50.43/50.80
% 50.43/50.80
% 50.43/50.80 The strategy used was not complete!
% 50.43/50.80
% 50.43/50.80 Increased maxweight to 17
% 50.43/50.80
% 50.43/50.80 Starting Search:
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80
% 50.43/50.80 Intermediate Status:
% 50.43/50.80 Generated: 18822
% 50.43/50.80 Kept: 2002
% 50.43/50.80 Inuse: 762
% 50.43/50.80 Deleted: 117
% 50.43/50.80 Deletedinuse: 8
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80 Resimplifying inuse:
% 50.43/50.80 Done
% 50.43/50.80
% 50.43/50.80
% 50.43/50.80 Intermediate Status:
% 50.43/50.80 Generated: 168663
% 50.43/50.80 Kept: 4002
% 50.43/50.80 Inuse: 2506
% 222.83/223.29 Deleted: 399
% 222.83/223.29 Deletedinuse: 42
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Failed to find proof!
% 222.83/223.29 maxweight = 17
% 222.83/223.29 maxnrclauses = 10000000
% 222.83/223.29 Generated: 303189
% 222.83/223.29 Kept: 4542
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 The strategy used was not complete!
% 222.83/223.29
% 222.83/223.29 Increased maxweight to 18
% 222.83/223.29
% 222.83/223.29 Starting Search:
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 10639
% 222.83/223.29 Kept: 2014
% 222.83/223.29 Inuse: 610
% 222.83/223.29 Deleted: 97
% 222.83/223.29 Deletedinuse: 7
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 139276
% 222.83/223.29 Kept: 4015
% 222.83/223.29 Inuse: 1896
% 222.83/223.29 Deleted: 298
% 222.83/223.29 Deletedinuse: 25
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Failed to find proof!
% 222.83/223.29 maxweight = 18
% 222.83/223.29 maxnrclauses = 10000000
% 222.83/223.29 Generated: 498960
% 222.83/223.29 Kept: 5872
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 The strategy used was not complete!
% 222.83/223.29
% 222.83/223.29 Increased maxweight to 19
% 222.83/223.29
% 222.83/223.29 Starting Search:
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 10171
% 222.83/223.29 Kept: 2005
% 222.83/223.29 Inuse: 585
% 222.83/223.29 Deleted: 86
% 222.83/223.29 Deletedinuse: 7
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 74173
% 222.83/223.29 Kept: 4013
% 222.83/223.29 Inuse: 1200
% 222.83/223.29 Deleted: 196
% 222.83/223.29 Deletedinuse: 23
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 117184
% 222.83/223.29 Kept: 6016
% 222.83/223.29 Inuse: 1609
% 222.83/223.29 Deleted: 220
% 222.83/223.29 Deletedinuse: 26
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 179091
% 222.83/223.29 Kept: 8017
% 222.83/223.29 Inuse: 2456
% 222.83/223.29 Deleted: 382
% 222.83/223.29 Deletedinuse: 53
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 282989
% 222.83/223.29 Kept: 10020
% 222.83/223.29 Inuse: 3400
% 222.83/223.29 Deleted: 574
% 222.83/223.29 Deletedinuse: 60
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 370604
% 222.83/223.29 Kept: 12020
% 222.83/223.29 Inuse: 4537
% 222.83/223.29 Deleted: 694
% 222.83/223.29 Deletedinuse: 88
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 929484
% 222.83/223.29 Kept: 14020
% 222.83/223.29 Inuse: 8304
% 222.83/223.29 Deleted: 1142
% 222.83/223.29 Deletedinuse: 124
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 1251141
% 222.83/223.29 Kept: 16021
% 222.83/223.29 Inuse: 10043
% 222.83/223.29 Deleted: 2045
% 222.83/223.29 Deletedinuse: 496
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Failed to find proof!
% 222.83/223.29 maxweight = 19
% 222.83/223.29 maxnrclauses = 10000000
% 222.83/223.29 Generated: 2307326
% 222.83/223.29 Kept: 17373
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 The strategy used was not complete!
% 222.83/223.29
% 222.83/223.29 Increased maxweight to 20
% 222.83/223.29
% 222.83/223.29 Starting Search:
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 9830
% 222.83/223.29 Kept: 2004
% 222.83/223.29 Inuse: 566
% 222.83/223.29 Deleted: 81
% 222.83/223.29 Deletedinuse: 7
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 69604
% 222.83/223.29 Kept: 4005
% 222.83/223.29 Inuse: 1170
% 222.83/223.29 Deleted: 200
% 222.83/223.29 Deletedinuse: 25
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 96398
% 222.83/223.29 Kept: 6050
% 222.83/223.29 Inuse: 1428
% 222.83/223.29 Deleted: 219
% 222.83/223.29 Deletedinuse: 26
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 158503
% 222.83/223.29 Kept: 8051
% 222.83/223.29 Inuse: 1988
% 222.83/223.29 Deleted: 285
% 222.83/223.29 Deletedinuse: 29
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 187144
% 222.83/223.29 Kept: 10054
% 222.83/223.29 Inuse: 2425
% 222.83/223.29 Deleted: 369
% 222.83/223.29 Deletedinuse: 50
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 239492
% 222.83/223.29 Kept: 12275
% 222.83/223.29 Inuse: 2946
% 222.83/223.29 Deleted: 485
% 222.83/223.29 Deletedinuse: 66
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 330728
% 222.83/223.29 Kept: 14282
% 222.83/223.29 Inuse: 3789
% 222.83/223.29 Deleted: 686
% 222.83/223.29 Deletedinuse: 100
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 400323
% 222.83/223.29 Kept: 16288
% 222.83/223.29 Inuse: 4593
% 222.83/223.29 Deleted: 767
% 222.83/223.29 Deletedinuse: 121
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 527495
% 222.83/223.29 Kept: 18289
% 222.83/223.29 Inuse: 5507
% 222.83/223.29 Deleted: 907
% 222.83/223.29 Deletedinuse: 126
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying inuse:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29 Resimplifying clauses:
% 222.83/223.29 Done
% 222.83/223.29
% 222.83/223.29
% 222.83/223.29 Intermediate Status:
% 222.83/223.29 Generated: 747524
% 222.83/223.29 Kept: 20290
% 250.44/250.82 Inuse: 6839
% 250.44/250.82 Deleted: 2220
% 250.44/250.82 Deletedinuse: 205
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 854010
% 250.44/250.82 Kept: 22293
% 250.44/250.82 Inuse: 7482
% 250.44/250.82 Deleted: 2272
% 250.44/250.82 Deletedinuse: 215
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 922038
% 250.44/250.82 Kept: 24293
% 250.44/250.82 Inuse: 8186
% 250.44/250.82 Deleted: 2285
% 250.44/250.82 Deletedinuse: 228
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 1036219
% 250.44/250.82 Kept: 26298
% 250.44/250.82 Inuse: 8802
% 250.44/250.82 Deleted: 2285
% 250.44/250.82 Deletedinuse: 228
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 1590120
% 250.44/250.82 Kept: 28298
% 250.44/250.82 Inuse: 10079
% 250.44/250.82 Deleted: 2405
% 250.44/250.82 Deletedinuse: 231
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 1808013
% 250.44/250.82 Kept: 30318
% 250.44/250.82 Inuse: 11437
% 250.44/250.82 Deleted: 3160
% 250.44/250.82 Deletedinuse: 554
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 2585534
% 250.44/250.82 Kept: 32318
% 250.44/250.82 Inuse: 14840
% 250.44/250.82 Deleted: 3701
% 250.44/250.82 Deletedinuse: 597
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 3397007
% 250.44/250.82 Kept: 34325
% 250.44/250.82 Inuse: 19021
% 250.44/250.82 Deleted: 4015
% 250.44/250.82 Deletedinuse: 658
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 4530114
% 250.44/250.82 Kept: 36327
% 250.44/250.82 Inuse: 22100
% 250.44/250.82 Deleted: 4487
% 250.44/250.82 Deletedinuse: 734
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 4707851
% 250.44/250.82 Kept: 38340
% 250.44/250.82 Inuse: 22559
% 250.44/250.82 Deleted: 5603
% 250.44/250.82 Deletedinuse: 1767
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying clauses:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 4833646
% 250.44/250.82 Kept: 40340
% 250.44/250.82 Inuse: 22978
% 250.44/250.82 Deleted: 9215
% 250.44/250.82 Deletedinuse: 2729
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 5523135
% 250.44/250.82 Kept: 42342
% 250.44/250.82 Inuse: 24655
% 250.44/250.82 Deleted: 9754
% 250.44/250.82 Deletedinuse: 3264
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 6188394
% 250.44/250.82 Kept: 44357
% 250.44/250.82 Inuse: 26470
% 250.44/250.82 Deleted: 10301
% 250.44/250.82 Deletedinuse: 3646
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 8839428
% 250.44/250.82 Kept: 46363
% 250.44/250.82 Inuse: 36245
% 250.44/250.82 Deleted: 13993
% 250.44/250.82 Deletedinuse: 3921
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Failed to find proof!
% 250.44/250.82 maxweight = 20
% 250.44/250.82 maxnrclauses = 10000000
% 250.44/250.82 Generated: 8843733
% 250.44/250.82 Kept: 46379
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 The strategy used was not complete!
% 250.44/250.82
% 250.44/250.82 Increased maxweight to 21
% 250.44/250.82
% 250.44/250.82 Starting Search:
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 9216
% 250.44/250.82 Kept: 2002
% 250.44/250.82 Inuse: 529
% 250.44/250.82 Deleted: 83
% 250.44/250.82 Deletedinuse: 7
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 36681
% 250.44/250.82 Kept: 4005
% 250.44/250.82 Inuse: 1014
% 250.44/250.82 Deleted: 175
% 250.44/250.82 Deletedinuse: 23
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 85348
% 250.44/250.82 Kept: 6010
% 250.44/250.82 Inuse: 1327
% 250.44/250.82 Deleted: 213
% 250.44/250.82 Deletedinuse: 23
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 113736
% 250.44/250.82 Kept: 8011
% 250.44/250.82 Inuse: 1524
% 250.44/250.82 Deleted: 235
% 250.44/250.82 Deletedinuse: 27
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 151063
% 250.44/250.82 Kept: 10122
% 250.44/250.82 Inuse: 1977
% 250.44/250.82 Deleted: 284
% 250.44/250.82 Deletedinuse: 30
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 162564
% 250.44/250.82 Kept: 12131
% 250.44/250.82 Inuse: 2148
% 250.44/250.82 Deleted: 307
% 250.44/250.82 Deletedinuse: 37
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 199403
% 250.44/250.82 Kept: 14131
% 250.44/250.82 Inuse: 2524
% 250.44/250.82 Deleted: 375
% 250.44/250.82 Deletedinuse: 47
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 215787
% 250.44/250.82 Kept: 16134
% 250.44/250.82 Inuse: 2750
% 250.44/250.82 Deleted: 388
% 250.44/250.82 Deletedinuse: 49
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82 Resimplifying inuse:
% 250.44/250.82 Done
% 250.44/250.82
% 250.44/250.82
% 250.44/250.82 Intermediate Status:
% 250.44/250.82 Generated: 252597
% 250.44/250.82 Kept: 18137
% 250.44/250.82 Inuse: 3134
% 250.44/250.82 Deleted: 516
% 250.44/250.82 DeletediTerminated
% 299.67/300.03 Bliksem ended
% 299.67/300.03 Terminated
%------------------------------------------------------------------------------