%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX208+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n024.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:48 PM UTC 2026
% Result : Timeout 299.58s 300.01s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SWX208+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.07 % Command : bliksem %s
% 0.07/0.25 % Computer : n024.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % DateTime : Tue May 5 06:36:26 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.39/0.82 *** allocated 10000 integers for termspace/termends
% 0.39/0.82 *** allocated 10000 integers for clauses
% 0.39/0.82 *** allocated 10000 integers for justifications
% 0.39/0.82 Bliksem 1.12
% 0.39/0.82
% 0.39/0.82
% 0.39/0.82 Automatic Strategy Selection
% 0.39/0.82
% 0.39/0.82
% 0.39/0.82 Clauses:
% 0.39/0.82
% 0.39/0.82 { proj1pair( pair2( X, Y ) ) = X }.
% 0.39/0.82 { proj2pair( pair2( X, Y ) ) = Y }.
% 0.39/0.82 { head( cons( X, Y ) ) = X }.
% 0.39/0.82 { tail( cons( X, Y ) ) = Y }.
% 0.39/0.82 { ! nil = cons( X, Y ) }.
% 0.39/0.82 { proj1S( s( X ) ) = X }.
% 0.39/0.82 { ! z = s( X ) }.
% 0.39/0.82 { proj1Add( add( X, Y ) ) = X }.
% 0.39/0.82 { proj2Add( add( X, Y ) ) = Y }.
% 0.39/0.82 { proj1Mul( mul( X, Y ) ) = X }.
% 0.39/0.82 { proj2Mul( mul( X, Y ) ) = Y }.
% 0.39/0.82 { proj1Num( num( X ) ) = X }.
% 0.39/0.82 { ! x = add( X, Y ) }.
% 0.39/0.82 { ! x = mul( X, Y ) }.
% 0.39/0.82 { ! x = num( X ) }.
% 0.39/0.82 { ! add( X, Y ) = mul( Z, T ) }.
% 0.39/0.82 { ! add( X, Y ) = num( Z ) }.
% 0.39/0.82 { ! mul( X, Y ) = num( Z ) }.
% 0.39/0.82 { proj1Left( left( X ) ) = X }.
% 0.39/0.82 { proj1Right( right( X ) ) = X }.
% 0.39/0.82 { ! left( X ) = right( Y ) }.
% 0.39/0.82 { ! pAR1 = pAR2 }.
% 0.39/0.82 { ! pAR1 = pLUS }.
% 0.39/0.82 { ! pAR1 = mULT }.
% 0.39/0.82 { ! pAR1 = cHARX }.
% 0.39/0.82 { ! pAR1 = dIG0 }.
% 0.39/0.82 { ! pAR1 = dIG1 }.
% 0.39/0.82 { ! pAR1 = dIG2 }.
% 0.39/0.82 { ! pAR1 = dIG3 }.
% 0.39/0.82 { ! pAR1 = dIG4 }.
% 0.39/0.82 { ! pAR1 = dIG5 }.
% 0.39/0.82 { ! pAR1 = dIG6 }.
% 0.39/0.82 { ! pAR1 = dIG7 }.
% 0.39/0.82 { ! pAR1 = dIG8 }.
% 0.39/0.82 { ! pAR1 = dIG9 }.
% 0.39/0.82 { ! pAR2 = pLUS }.
% 0.39/0.82 { ! pAR2 = mULT }.
% 0.39/0.82 { ! pAR2 = cHARX }.
% 0.39/0.82 { ! pAR2 = dIG0 }.
% 0.39/0.82 { ! pAR2 = dIG1 }.
% 0.39/0.82 { ! pAR2 = dIG2 }.
% 0.39/0.82 { ! pAR2 = dIG3 }.
% 0.39/0.82 { ! pAR2 = dIG4 }.
% 0.39/0.82 { ! pAR2 = dIG5 }.
% 0.39/0.82 { ! pAR2 = dIG6 }.
% 0.39/0.82 { ! pAR2 = dIG7 }.
% 0.39/0.82 { ! pAR2 = dIG8 }.
% 0.39/0.82 { ! pAR2 = dIG9 }.
% 0.39/0.82 { ! pLUS = mULT }.
% 0.39/0.82 { ! pLUS = cHARX }.
% 0.39/0.82 { ! pLUS = dIG0 }.
% 0.39/0.82 { ! pLUS = dIG1 }.
% 0.39/0.82 { ! pLUS = dIG2 }.
% 0.39/0.82 { ! pLUS = dIG3 }.
% 0.39/0.82 { ! pLUS = dIG4 }.
% 0.39/0.82 { ! pLUS = dIG5 }.
% 0.39/0.82 { ! pLUS = dIG6 }.
% 0.39/0.82 { ! pLUS = dIG7 }.
% 0.39/0.82 { ! pLUS = dIG8 }.
% 0.39/0.82 { ! pLUS = dIG9 }.
% 0.39/0.82 { ! mULT = cHARX }.
% 0.39/0.82 { ! mULT = dIG0 }.
% 0.39/0.82 { ! mULT = dIG1 }.
% 0.39/0.82 { ! mULT = dIG2 }.
% 0.39/0.82 { ! mULT = dIG3 }.
% 0.39/0.82 { ! mULT = dIG4 }.
% 0.39/0.82 { ! mULT = dIG5 }.
% 0.39/0.82 { ! mULT = dIG6 }.
% 0.39/0.82 { ! mULT = dIG7 }.
% 0.39/0.82 { ! mULT = dIG8 }.
% 0.39/0.82 { ! mULT = dIG9 }.
% 0.39/0.82 { ! cHARX = dIG0 }.
% 0.39/0.82 { ! cHARX = dIG1 }.
% 0.39/0.82 { ! cHARX = dIG2 }.
% 0.39/0.82 { ! cHARX = dIG3 }.
% 0.39/0.82 { ! cHARX = dIG4 }.
% 0.39/0.82 { ! cHARX = dIG5 }.
% 0.39/0.82 { ! cHARX = dIG6 }.
% 0.39/0.82 { ! cHARX = dIG7 }.
% 0.39/0.82 { ! cHARX = dIG8 }.
% 0.39/0.82 { ! cHARX = dIG9 }.
% 0.39/0.82 { ! dIG0 = dIG1 }.
% 0.39/0.82 { ! dIG0 = dIG2 }.
% 0.39/0.82 { ! dIG0 = dIG3 }.
% 0.39/0.82 { ! dIG0 = dIG4 }.
% 0.39/0.82 { ! dIG0 = dIG5 }.
% 0.39/0.82 { ! dIG0 = dIG6 }.
% 0.39/0.82 { ! dIG0 = dIG7 }.
% 0.39/0.82 { ! dIG0 = dIG8 }.
% 0.39/0.82 { ! dIG0 = dIG9 }.
% 0.39/0.82 { ! dIG1 = dIG2 }.
% 0.39/0.82 { ! dIG1 = dIG3 }.
% 0.39/0.82 { ! dIG1 = dIG4 }.
% 0.39/0.82 { ! dIG1 = dIG5 }.
% 0.39/0.82 { ! dIG1 = dIG6 }.
% 0.39/0.82 { ! dIG1 = dIG7 }.
% 0.39/0.82 { ! dIG1 = dIG8 }.
% 0.39/0.82 { ! dIG1 = dIG9 }.
% 0.39/0.82 { ! dIG2 = dIG3 }.
% 0.39/0.82 { ! dIG2 = dIG4 }.
% 0.39/0.82 { ! dIG2 = dIG5 }.
% 0.39/0.82 { ! dIG2 = dIG6 }.
% 0.39/0.82 { ! dIG2 = dIG7 }.
% 0.39/0.82 { ! dIG2 = dIG8 }.
% 0.39/0.82 { ! dIG2 = dIG9 }.
% 0.39/0.82 { ! dIG3 = dIG4 }.
% 0.39/0.82 { ! dIG3 = dIG5 }.
% 0.39/0.82 { ! dIG3 = dIG6 }.
% 0.39/0.82 { ! dIG3 = dIG7 }.
% 0.39/0.82 { ! dIG3 = dIG8 }.
% 0.39/0.82 { ! dIG3 = dIG9 }.
% 0.39/0.82 { ! dIG4 = dIG5 }.
% 0.39/0.82 { ! dIG4 = dIG6 }.
% 0.39/0.82 { ! dIG4 = dIG7 }.
% 0.39/0.82 { ! dIG4 = dIG8 }.
% 0.39/0.82 { ! dIG4 = dIG9 }.
% 0.39/0.82 { ! dIG5 = dIG6 }.
% 0.39/0.82 { ! dIG5 = dIG7 }.
% 0.39/0.82 { ! dIG5 = dIG8 }.
% 0.39/0.82 { ! dIG5 = dIG9 }.
% 0.39/0.82 { ! dIG6 = dIG7 }.
% 0.39/0.82 { ! dIG6 = dIG8 }.
% 0.39/0.82 { ! dIG6 = dIG9 }.
% 0.39/0.82 { ! dIG7 = dIG8 }.
% 0.39/0.82 { ! dIG7 = dIG9 }.
% 0.39/0.82 { ! dIG8 = dIG9 }.
% 0.39/0.82 { append( nil, X ) = X }.
% 0.39/0.82 { append( cons( Y, Z ), X ) = cons( Y, append( Z, X ) ) }.
% 0.39/0.82 { x2( z, z ) = z }.
% 0.39/0.82 { x2( z, s( X ) ) = z }.
% 0.39/0.82 { x2( s( X ), z ) = s( X ) }.
% 0.39/0.82 { x2( s( X ), s( Y ) ) = x2( X, Y ) }.
% 0.39/0.82 { min10( z ) = left( dIG0 ) }.
% 0.39/0.82 { min10( s( z ) ) = left( dIG1 ) }.
% 0.39/0.82 { min10( s( s( z ) ) ) = left( dIG2 ) }.
% 0.39/0.82 { min10( s( s( s( z ) ) ) ) = left( dIG3 ) }.
% 0.39/0.82 { min10( s( s( s( s( z ) ) ) ) ) = left( dIG4 ) }.
% 0.39/0.82 { min10( s( s( s( s( s( z ) ) ) ) ) ) = left( dIG5 ) }.
% 0.39/0.82 { min10( s( s( s( s( s( s( z ) ) ) ) ) ) ) = left( dIG6 ) }.
% 0.39/0.82 { min10( s( s( s( s( s( s( s( z ) ) ) ) ) ) ) ) = left( dIG7 ) }.
% 0.39/0.82 { min10( s( s( s( s( s( s( s( s( z ) ) ) ) ) ) ) ) ) = left( dIG8 ) }.
% 0.39/0.82 { min10( s( s( s( s( s( s( s( s( s( z ) ) ) ) ) ) ) ) ) ) = left( dIG9 ) }
% 0.39/0.82 .
% 0.39/0.82 { min10( s( s( s( s( s( s( s( s( s( s( X ) ) ) ) ) ) ) ) ) ) ) = right( x2
% 0.39/0.82 ( s( s( s( s( s( s( s( s( s( s( X ) ) ) ) ) ) ) ) ) ), s( s( s( s( s( s(
% 0.39/0.82 s( s( s( s( z ) ) ) ) ) ) ) ) ) ) ) ) }.
% 0.39/0.82 { ! min10( X ) = left( Y ), mod10( X ) = pair2( Y, z ) }.
% 0.39/0.82 { ! min10( X ) = right( Y ), ! mod10( Y ) = pair2( Z, T ), mod10( X ) =
% 0.39/0.82 pair2( Z, s( T ) ) }.
% 0.39/0.82 { showNumnum( X, z ) = X }.
% 0.39/0.82 { ! mod10( s( X ) ) = pair2( Y, Z ), showNumnum( T, s( X ) ) = showNumnum(
% 0.39/0.82 cons( Y, T ), Z ) }.
% 0.39/0.82 { showNum( z ) = cons( dIG0, nil ) }.
% 0.39/0.82 { showNum( s( X ) ) = showNumnum( nil, s( X ) ) }.
% 3.61/4.10 { show( x ) = cons( cHARX, nil ) }.
% 3.61/4.10 { show( add( X, Y ) ) = append( show( X ), append( cons( pLUS, nil ), show
% 3.61/4.10 ( Y ) ) ) }.
% 3.61/4.10 { show( mul( X, Y ) ) = append( showF( X ), append( cons( mULT, nil ),
% 3.61/4.10 showF( Y ) ) ) }.
% 3.61/4.10 { show( num( X ) ) = showNum( X ) }.
% 3.61/4.10 { X = add( proj1Add( X ), proj2Add( X ) ), showF( X ) = show( X ) }.
% 3.61/4.10 { showF( add( X, Y ) ) = cons( pAR1, append( show( add( X, Y ) ), cons(
% 3.61/4.10 pAR2, nil ) ) ) }.
% 3.61/4.10 { ! show( X ) = cons( pAR1, cons( pAR1, cons( cHARX, cons( pLUS, cons( dIG5
% 3.61/4.10 , cons( pAR2, cons( pLUS, cons( dIG7, cons( pAR2, cons( mULT, cons( cHARX
% 3.61/4.10 , nil ) ) ) ) ) ) ) ) ) ) ) }.
% 3.61/4.10
% 3.61/4.10 percentage equality = 1.000000, percentage horn = 0.993590
% 3.61/4.10 This is a pure equality problem
% 3.61/4.10
% 3.61/4.10
% 3.61/4.10
% 3.61/4.10 Options Used:
% 3.61/4.10
% 3.61/4.10 useres = 1
% 3.61/4.10 useparamod = 1
% 3.61/4.10 useeqrefl = 1
% 3.61/4.10 useeqfact = 1
% 3.61/4.10 usefactor = 1
% 3.61/4.10 usesimpsplitting = 0
% 3.61/4.10 usesimpdemod = 5
% 3.61/4.10 usesimpres = 3
% 3.61/4.10
% 3.61/4.10 resimpinuse = 1000
% 3.61/4.10 resimpclauses = 20000
% 3.61/4.10 substype = eqrewr
% 3.61/4.10 backwardsubs = 1
% 3.61/4.10 selectoldest = 5
% 3.61/4.10
% 3.61/4.10 litorderings [0] = split
% 3.61/4.10 litorderings [1] = extend the termordering, first sorting on arguments
% 3.61/4.10
% 3.61/4.10 termordering = kbo
% 3.61/4.10
% 3.61/4.10 litapriori = 0
% 3.61/4.10 termapriori = 1
% 3.61/4.10 litaposteriori = 0
% 3.61/4.10 termaposteriori = 0
% 3.61/4.10 demodaposteriori = 0
% 3.61/4.10 ordereqreflfact = 0
% 3.61/4.10
% 3.61/4.10 litselect = negord
% 3.61/4.10
% 3.61/4.10 maxweight = 15
% 3.61/4.10 maxdepth = 30000
% 3.61/4.10 maxlength = 115
% 3.61/4.10 maxnrvars = 195
% 3.61/4.10 excuselevel = 1
% 3.61/4.10 increasemaxweight = 1
% 3.61/4.10
% 3.61/4.10 maxselected = 10000000
% 3.61/4.10 maxnrclauses = 10000000
% 3.61/4.10
% 3.61/4.10 showgenerated = 0
% 3.61/4.10 showkept = 0
% 3.61/4.10 showselected = 0
% 3.61/4.10 showdeleted = 0
% 3.61/4.10 showresimp = 1
% 3.61/4.10 showstatus = 2000
% 3.61/4.10
% 3.61/4.10 prologoutput = 0
% 3.61/4.10 nrgoals = 5000000
% 3.61/4.10 totalproof = 1
% 3.61/4.10
% 3.61/4.10 Symbols occurring in the translation:
% 3.61/4.10
% 3.61/4.10 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.61/4.10 . [1, 2] (w:1, o:69, a:1, s:1, b:0),
% 3.61/4.10 ! [4, 1] (w:0, o:43, a:1, s:1, b:0),
% 3.61/4.10 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.61/4.10 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.61/4.10 pair2 [37, 2] (w:1, o:93, a:1, s:1, b:0),
% 3.61/4.10 proj1pair [38, 1] (w:1, o:48, a:1, s:1, b:0),
% 3.61/4.10 proj2pair [39, 1] (w:1, o:55, a:1, s:1, b:0),
% 3.61/4.10 cons [40, 2] (w:1, o:94, a:1, s:1, b:0),
% 3.61/4.10 head [41, 1] (w:1, o:56, a:1, s:1, b:0),
% 3.61/4.10 tail [42, 1] (w:1, o:62, a:1, s:1, b:0),
% 3.61/4.10 nil [43, 0] (w:1, o:9, a:1, s:1, b:0),
% 3.61/4.10 s [44, 1] (w:1, o:58, a:1, s:1, b:0),
% 3.61/4.10 proj1S [45, 1] (w:1, o:50, a:1, s:1, b:0),
% 3.61/4.10 z [46, 0] (w:1, o:10, a:1, s:1, b:0),
% 3.61/4.10 add [47, 2] (w:1, o:95, a:1, s:1, b:0),
% 3.61/4.10 proj1Add [48, 1] (w:1, o:51, a:1, s:1, b:0),
% 3.61/4.10 proj2Add [49, 1] (w:1, o:63, a:1, s:1, b:0),
% 3.61/4.10 mul [50, 2] (w:1, o:96, a:1, s:1, b:0),
% 3.61/4.10 proj1Mul [51, 1] (w:1, o:53, a:1, s:1, b:0),
% 3.61/4.10 proj2Mul [52, 1] (w:1, o:64, a:1, s:1, b:0),
% 3.61/4.10 num [53, 1] (w:1, o:67, a:1, s:1, b:0),
% 3.61/4.10 proj1Num [54, 1] (w:1, o:54, a:1, s:1, b:0),
% 3.61/4.10 x [55, 0] (w:1, o:11, a:1, s:1, b:0),
% 3.61/4.10 left [58, 1] (w:1, o:68, a:1, s:1, b:0),
% 3.61/4.10 proj1Left [59, 1] (w:1, o:52, a:1, s:1, b:0),
% 3.61/4.10 right [60, 1] (w:1, o:57, a:1, s:1, b:0),
% 3.61/4.10 proj1Right [61, 1] (w:1, o:49, a:1, s:1, b:0),
% 3.61/4.10 pAR1 [62, 0] (w:1, o:14, a:1, s:1, b:0),
% 3.61/4.10 pAR2 [63, 0] (w:1, o:15, a:1, s:1, b:0),
% 3.61/4.10 pLUS [64, 0] (w:1, o:16, a:1, s:1, b:0),
% 3.61/4.10 mULT [65, 0] (w:1, o:8, a:1, s:1, b:0),
% 3.61/4.10 cHARX [66, 0] (w:1, o:17, a:1, s:1, b:0),
% 3.61/4.10 dIG0 [67, 0] (w:1, o:18, a:1, s:1, b:0),
% 3.61/4.10 dIG1 [68, 0] (w:1, o:19, a:1, s:1, b:0),
% 3.61/4.10 dIG2 [69, 0] (w:1, o:20, a:1, s:1, b:0),
% 3.61/4.10 dIG3 [70, 0] (w:1, o:21, a:1, s:1, b:0),
% 3.61/4.10 dIG4 [71, 0] (w:1, o:22, a:1, s:1, b:0),
% 3.61/4.10 dIG5 [72, 0] (w:1, o:23, a:1, s:1, b:0),
% 3.61/4.10 dIG6 [73, 0] (w:1, o:24, a:1, s:1, b:0),
% 3.61/4.10 dIG7 [74, 0] (w:1, o:25, a:1, s:1, b:0),
% 3.61/4.10 dIG8 [75, 0] (w:1, o:26, a:1, s:1, b:0),
% 3.61/4.10 dIG9 [76, 0] (w:1, o:27, a:1, s:1, b:0),
% 3.61/4.10 append [78, 2] (w:1, o:97, a:1, s:1, b:0),
% 3.61/4.10 x2 [81, 2] (w:1, o:98, a:1, s:1, b:0),
% 3.61/4.10 min10 [84, 1] (w:1, o:65, a:1, s:1, b:0),
% 3.61/4.10 mod10 [87, 1] (w:1, o:66, a:1, s:1, b:0),
% 3.61/4.10 showNumnum [90, 2] (w:1, o:99, a:1, s:1, b:0),
% 3.61/4.10 showNum [92, 1] (w:1, o:59, a:1, s:1, b:0),
% 18.29/18.79 show [93, 1] (w:1, o:60, a:1, s:1, b:0),
% 18.29/18.79 showF [98, 1] (w:1, o:61, a:1, s:1, b:0).
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Starting Search:
% 18.29/18.79
% 18.29/18.79 *** allocated 15000 integers for clauses
% 18.29/18.79 *** allocated 22500 integers for clauses
% 18.29/18.79 *** allocated 33750 integers for clauses
% 18.29/18.79 *** allocated 50625 integers for clauses
% 18.29/18.79 *** allocated 15000 integers for termspace/termends
% 18.29/18.79 *** allocated 75937 integers for clauses
% 18.29/18.79 *** allocated 22500 integers for termspace/termends
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 113905 integers for clauses
% 18.29/18.79 *** allocated 33750 integers for termspace/termends
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 5601
% 18.29/18.79 Kept: 2156
% 18.29/18.79 Inuse: 284
% 18.29/18.79 Deleted: 7
% 18.29/18.79 Deletedinuse: 1
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 170857 integers for clauses
% 18.29/18.79 *** allocated 50625 integers for termspace/termends
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 75937 integers for termspace/termends
% 18.29/18.79 *** allocated 256285 integers for clauses
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 14845
% 18.29/18.79 Kept: 4218
% 18.29/18.79 Inuse: 347
% 18.29/18.79 Deleted: 8
% 18.29/18.79 Deletedinuse: 1
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 113905 integers for termspace/termends
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 384427 integers for clauses
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 23150
% 18.29/18.79 Kept: 6608
% 18.29/18.79 Inuse: 416
% 18.29/18.79 Deleted: 8
% 18.29/18.79 Deletedinuse: 1
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 170857 integers for termspace/termends
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 576640 integers for clauses
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 30636
% 18.29/18.79 Kept: 8628
% 18.29/18.79 Inuse: 479
% 18.29/18.79 Deleted: 8
% 18.29/18.79 Deletedinuse: 1
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 37782
% 18.29/18.79 Kept: 10638
% 18.29/18.79 Inuse: 540
% 18.29/18.79 Deleted: 11
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 256285 integers for termspace/termends
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 47166
% 18.29/18.79 Kept: 12640
% 18.29/18.79 Inuse: 635
% 18.29/18.79 Deleted: 11
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 *** allocated 864960 integers for clauses
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 54508
% 18.29/18.79 Kept: 15390
% 18.29/18.79 Inuse: 644
% 18.29/18.79 Deleted: 11
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 384427 integers for termspace/termends
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 63173
% 18.29/18.79 Kept: 17715
% 18.29/18.79 Inuse: 689
% 18.29/18.79 Deleted: 11
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 1297440 integers for clauses
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 76439
% 18.29/18.79 Kept: 20050
% 18.29/18.79 Inuse: 709
% 18.29/18.79 Deleted: 11
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying clauses:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 84406
% 18.29/18.79 Kept: 22101
% 18.29/18.79 Inuse: 724
% 18.29/18.79 Deleted: 347
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 97164
% 18.29/18.79 Kept: 24118
% 18.29/18.79 Inuse: 760
% 18.29/18.79 Deleted: 347
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 576640 integers for termspace/termends
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 119561
% 18.29/18.79 Kept: 26125
% 18.29/18.79 Inuse: 883
% 18.29/18.79 Deleted: 347
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 142002
% 18.29/18.79 Kept: 29118
% 18.29/18.79 Inuse: 997
% 18.29/18.79 Deleted: 347
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 1946160 integers for clauses
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 152081
% 18.29/18.79 Kept: 31684
% 18.29/18.79 Inuse: 1000
% 18.29/18.79 Deleted: 347
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 168875
% 18.29/18.79 Kept: 34892
% 18.29/18.79 Inuse: 1027
% 18.29/18.79 Deleted: 347
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 *** allocated 864960 integers for termspace/termends
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 179529
% 18.29/18.79 Kept: 37460
% 18.29/18.79 Inuse: 1030
% 18.29/18.79 Deleted: 347
% 18.29/18.79 Deletedinuse: 4
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79 Resimplifying inuse:
% 18.29/18.79 Done
% 18.29/18.79
% 18.29/18.79
% 18.29/18.79 Intermediate Status:
% 18.29/18.79 Generated: 196924
% 18.29/18.79 Kept: 40739
% 18.29/18.79 Inuse: 1060
% 18.29/18.79 Deleted: 347
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying clauses:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 207652
% 96.60/97.06 Kept: 43306
% 96.60/97.06 Inuse: 1062
% 96.60/97.06 Deleted: 442
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 226818
% 96.60/97.06 Kept: 45313
% 96.60/97.06 Inuse: 1081
% 96.60/97.06 Deleted: 442
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 *** allocated 2919240 integers for clauses
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 245933
% 96.60/97.06 Kept: 48214
% 96.60/97.06 Inuse: 1096
% 96.60/97.06 Deleted: 442
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 257036
% 96.60/97.06 Kept: 50813
% 96.60/97.06 Inuse: 1098
% 96.60/97.06 Deleted: 442
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 272889
% 96.60/97.06 Kept: 52915
% 96.60/97.06 Inuse: 1132
% 96.60/97.06 Deleted: 442
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 *** allocated 1297440 integers for termspace/termends
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 284699
% 96.60/97.06 Kept: 55479
% 96.60/97.06 Inuse: 1135
% 96.60/97.06 Deleted: 442
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 299129
% 96.60/97.06 Kept: 57489
% 96.60/97.06 Inuse: 1162
% 96.60/97.06 Deleted: 442
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 313739
% 96.60/97.06 Kept: 60248
% 96.60/97.06 Inuse: 1173
% 96.60/97.06 Deleted: 442
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying clauses:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 326101
% 96.60/97.06 Kept: 62860
% 96.60/97.06 Inuse: 1176
% 96.60/97.06 Deleted: 573
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 344259
% 96.60/97.06 Kept: 65863
% 96.60/97.06 Inuse: 1196
% 96.60/97.06 Deleted: 573
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 356506
% 96.60/97.06 Kept: 68462
% 96.60/97.06 Inuse: 1198
% 96.60/97.06 Deleted: 573
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 *** allocated 4378860 integers for clauses
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 376399
% 96.60/97.06 Kept: 71548
% 96.60/97.06 Inuse: 1221
% 96.60/97.06 Deleted: 573
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 388930
% 96.60/97.06 Kept: 74147
% 96.60/97.06 Inuse: 1223
% 96.60/97.06 Deleted: 573
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 438758
% 96.60/97.06 Kept: 76171
% 96.60/97.06 Inuse: 1278
% 96.60/97.06 Deleted: 573
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 472163
% 96.60/97.06 Kept: 78195
% 96.60/97.06 Inuse: 1345
% 96.60/97.06 Deleted: 573
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 506306
% 96.60/97.06 Kept: 81005
% 96.60/97.06 Inuse: 1402
% 96.60/97.06 Deleted: 573
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 *** allocated 1946160 integers for termspace/termends
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying clauses:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 521310
% 96.60/97.06 Kept: 83564
% 96.60/97.06 Inuse: 1405
% 96.60/97.06 Deleted: 648
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 548497
% 96.60/97.06 Kept: 85568
% 96.60/97.06 Inuse: 1451
% 96.60/97.06 Deleted: 648
% 96.60/97.06 Deletedinuse: 4
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 598702
% 96.60/97.06 Kept: 87759
% 96.60/97.06 Inuse: 1569
% 96.60/97.06 Deleted: 651
% 96.60/97.06 Deletedinuse: 7
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 634329
% 96.60/97.06 Kept: 89923
% 96.60/97.06 Inuse: 1589
% 96.60/97.06 Deleted: 651
% 96.60/97.06 Deletedinuse: 7
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 671922
% 96.60/97.06 Kept: 91924
% 96.60/97.06 Inuse: 1629
% 96.60/97.06 Deleted: 651
% 96.60/97.06 Deletedinuse: 7
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 713877
% 96.60/97.06 Kept: 93929
% 96.60/97.06 Inuse: 1731
% 96.60/97.06 Deleted: 651
% 96.60/97.06 Deletedinuse: 7
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06 Resimplifying inuse:
% 96.60/97.06 Done
% 96.60/97.06
% 96.60/97.06
% 96.60/97.06 Intermediate Status:
% 96.60/97.06 Generated: 758492
% 200.08/200.60 Kept: 95943
% 200.08/200.60 Inuse: 1839
% 200.08/200.60 Deleted: 652
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 820077
% 200.08/200.60 Kept: 97943
% 200.08/200.60 Inuse: 1983
% 200.08/200.60 Deleted: 652
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 890786
% 200.08/200.60 Kept: 99955
% 200.08/200.60 Inuse: 2098
% 200.08/200.60 Deleted: 652
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 957144
% 200.08/200.60 Kept: 101959
% 200.08/200.60 Inuse: 2247
% 200.08/200.60 Deleted: 657
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 *** allocated 6568290 integers for clauses
% 200.08/200.60 Resimplifying clauses:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 1033272
% 200.08/200.60 Kept: 103970
% 200.08/200.60 Inuse: 2416
% 200.08/200.60 Deleted: 873
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 1117203
% 200.08/200.60 Kept: 105971
% 200.08/200.60 Inuse: 2604
% 200.08/200.60 Deleted: 873
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 1196652
% 200.08/200.60 Kept: 108212
% 200.08/200.60 Inuse: 2728
% 200.08/200.60 Deleted: 873
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 1305565
% 200.08/200.60 Kept: 110218
% 200.08/200.60 Inuse: 2920
% 200.08/200.60 Deleted: 873
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 1411601
% 200.08/200.60 Kept: 112224
% 200.08/200.60 Inuse: 3074
% 200.08/200.60 Deleted: 873
% 200.08/200.60 Deletedinuse: 8
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 1509806
% 200.08/200.60 Kept: 114224
% 200.08/200.60 Inuse: 3265
% 200.08/200.60 Deleted: 877
% 200.08/200.60 Deletedinuse: 12
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 1724893
% 200.08/200.60 Kept: 116229
% 200.08/200.60 Inuse: 3455
% 200.08/200.60 Deleted: 877
% 200.08/200.60 Deletedinuse: 12
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.08/200.60 Done
% 200.08/200.60
% 200.08/200.60
% 200.08/200.60 Intermediate Status:
% 200.08/200.60 Generated: 1825943
% 200.08/200.60 Kept: 118234
% 200.08/200.60 Inuse: 3644
% 200.08/200.60 Deleted: 877
% 200.08/200.60 Deletedinuse: 12
% 200.08/200.60
% 200.08/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 *** allocated 2919240 integers for termspace/termends
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 2044238
% 200.18/200.60 Kept: 120244
% 200.18/200.60 Inuse: 3827
% 200.18/200.60 Deleted: 877
% 200.18/200.60 Deletedinuse: 12
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 2157449
% 200.18/200.60 Kept: 122380
% 200.18/200.60 Inuse: 3988
% 200.18/200.60 Deleted: 881
% 200.18/200.60 Deletedinuse: 16
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying clauses:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 2273548
% 200.18/200.60 Kept: 124801
% 200.18/200.60 Inuse: 4053
% 200.18/200.60 Deleted: 949
% 200.18/200.60 Deletedinuse: 17
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 2371294
% 200.18/200.60 Kept: 126837
% 200.18/200.60 Inuse: 4083
% 200.18/200.60 Deleted: 949
% 200.18/200.60 Deletedinuse: 17
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 2471801
% 200.18/200.60 Kept: 128855
% 200.18/200.60 Inuse: 4149
% 200.18/200.60 Deleted: 949
% 200.18/200.60 Deletedinuse: 17
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 2746040
% 200.18/200.60 Kept: 130858
% 200.18/200.60 Inuse: 4244
% 200.18/200.60 Deleted: 949
% 200.18/200.60 Deletedinuse: 17
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 2889394
% 200.18/200.60 Kept: 132867
% 200.18/200.60 Inuse: 4436
% 200.18/200.60 Deleted: 949
% 200.18/200.60 Deletedinuse: 17
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 3008568
% 200.18/200.60 Kept: 134878
% 200.18/200.60 Inuse: 4619
% 200.18/200.60 Deleted: 949
% 200.18/200.60 Deletedinuse: 17
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 3118294
% 200.18/200.60 Kept: 136883
% 200.18/200.60 Inuse: 4792
% 200.18/200.60 Deleted: 953
% 200.18/200.60 Deletedinuse: 21
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 3180130
% 200.18/200.60 Kept: 138889
% 200.18/200.60 Inuse: 4811
% 200.18/200.60 Deleted: 953
% 200.18/200.60 Deletedinuse: 21
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 Intermediate Status:
% 200.18/200.60 Generated: 3313020
% 200.18/200.60 Kept: 140892
% 200.18/200.60 Inuse: 4897
% 200.18/200.60 Deleted: 953
% 200.18/200.60 Deletedinuse: 21
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying inuse:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60 Resimplifying clauses:
% 200.18/200.60 Done
% 200.18/200.60
% 200.18/200.60
% 200.18/200.60 InTerminated
% 299.58/300.01 Bliksem ended
%------------------------------------------------------------------------------