%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX197-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n027.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.64s 300.02s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX197-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n027.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % DateTime : Tue May 5 11:05:34 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.67/1.08 *** allocated 10000 integers for termspace/termends
% 0.67/1.08 *** allocated 10000 integers for clauses
% 0.67/1.08 *** allocated 10000 integers for justifications
% 0.67/1.08 Bliksem 1.12
% 0.67/1.08
% 0.67/1.08
% 0.67/1.08 Automatic Strategy Selection
% 0.67/1.08
% 0.67/1.08 Clauses:
% 0.67/1.08 [
% 0.67/1.08 [ =( aux( X, Y, Z, btrue ), suc( zero ) ) ],
% 0.67/1.08 [ =( aux( X, Y, Z, bfalse ), zero ) ],
% 0.67/1.08 [ =( aux2( X, Y, Z, T, U, btrue ), run( X, append( U, Y ) ) ) ],
% 0.67/1.08 [ =( aux2( X, Y, Z, T, U, bfalse ), run( X, append( T, Y ) ) ) ],
% 0.67/1.08 [ =( store( nil, zero, X ), cons( X, nil ) ) ],
% 0.67/1.08 [ =( store( nil, suc( X ), Y ), cons( zero, store( nil, X, Y ) ) ) ]
% 0.67/1.08 ,
% 0.67/1.08 [ =( store( cons( X, Y ), zero, Z ), cons( Z, Y ) ) ],
% 0.67/1.08 [ =( store( cons( X, Y ), suc( Z ), T ), cons( X, store( Y, Z, T ) ) ) ]
% 0.67/1.08 ,
% 0.67/1.08 [ =( opti2( while( X, Y ) ), while( X, map( lam, Y ) ) ) ],
% 0.67/1.08 [ =( opti2( if( X, Y, Z ) ), if( add( n( suc( zero ) ), X ), Z, Y ) ) ]
% 0.67/1.08 ,
% 0.67/1.08 [ =( opti2( print( X ) ), print( X ) ) ],
% 0.67/1.08 [ =( opti2( x( X, Y ) ), x( X, Y ) ) ],
% 0.67/1.08 [ =( fetch( nil, X ), zero ) ],
% 0.67/1.08 [ =( fetch( cons( X, Y ), zero ), X ) ],
% 0.67/1.08 [ =( fetch( cons( X, Y ), suc( Z ) ), fetch( Y, Z ) ) ],
% 0.67/1.08 [ =( addNat( zero, X ), X ) ],
% 0.67/1.08 [ =( addNat( suc( X ), zero ), suc( X ) ) ],
% 0.67/1.08 [ =( addNat( suc( X ), suc( Y ) ), suc( addNat( X, suc( Y ) ) ) ) ],
% 0.67/1.08 [ =( mulNat( zero, X ), zero ) ],
% 0.67/1.08 [ =( mulNat( suc( X ), zero ), zero ) ],
% 0.67/1.08 [ =( mulNat( suc( X ), suc( Y ) ), addNat( mulNat( X, suc( Y ) ), suc( Y
% 0.67/1.08 ) ) ) ],
% 0.67/1.08 [ =( eval( X, n( Y ) ), Y ) ],
% 0.67/1.08 [ =( eval( X, add( Y, Z ) ), addNat( eval( X, Y ), eval( X, Z ) ) ) ]
% 0.67/1.08 ,
% 0.67/1.08 [ =( eval( X, mul( Y, Z ) ), mulNat( eval( X, Y ), eval( X, Z ) ) ) ]
% 0.67/1.08 ,
% 0.67/1.08 [ =( eval( X, eq( Y, Z ) ), aux( X, Y, Z, eq4( eval( X, Y ), eval( X, Z
% 0.67/1.08 ) ) ) ) ],
% 0.67/1.08 [ =( eval( X, v( Y ) ), fetch( X, Y ) ) ],
% 0.67/1.08 [ =( run( X, nil2 ), nil ) ],
% 0.67/1.08 [ =( run( X, cons2( print( Y ), Z ) ), cons( eval( X, Y ), run( X, Z ) )
% 0.67/1.08 ) ],
% 0.67/1.08 [ =( run( X, cons2( x( Y, Z ), T ) ), run( store( X, Y, eval( X, Z ) ),
% 0.67/1.08 T ) ) ],
% 0.67/1.08 [ =( run( X, cons2( while( Y, Z ), T ) ), run( X, cons2( if( Y, append(
% 0.67/1.08 Z, cons2( while( Y, Z ), nil2 ) ), nil2 ), T ) ) ) ],
% 0.67/1.08 [ =( run( X, cons2( if( Y, Z, T ), U ) ), aux2( X, U, Y, Z, T, eq4( eval(
% 0.67/1.08 X, Y ), zero ) ) ) ],
% 0.67/1.08 [ =( 'prop_Opti2'( X ), eq2( run( nil, cons2( X, nil2 ) ), run( nil,
% 0.67/1.08 cons2( opti2( X ), nil2 ) ) ) ) ],
% 0.67/1.08 [ =( map( X, nil2 ), nil2 ) ],
% 0.67/1.08 [ =( map( X, cons2( Y, Z ) ), cons2( apply1( X, Y ), map( X, Z ) ) ) ]
% 0.67/1.08 ,
% 0.67/1.08 [ =( append( nil2, X ), X ) ],
% 0.67/1.08 [ =( append( cons2( X, Y ), Z ), cons2( X, append( Y, Z ) ) ) ],
% 0.67/1.08 [ =( eq7( bfalse, btrue ), bfalse ) ],
% 0.67/1.08 [ =( eq7( btrue, bfalse ), bfalse ) ],
% 0.67/1.08 [ =( eq4( X, X ), btrue ) ],
% 0.67/1.08 [ =( eq5( X, X ), btrue ) ],
% 0.67/1.08 [ =( eq6( X, X ), btrue ) ],
% 0.67/1.08 [ =( eq7( X, X ), btrue ) ],
% 0.67/1.08 [ =( eq2( X, X ), btrue ) ],
% 0.67/1.08 [ =( eq3( X, X ), btrue ) ],
% 0.67/1.08 [ ~( =( eq4( X, Y ), bfalse ) ), =( eq2( cons( X, Z ), cons( Y, T ) ),
% 0.67/1.08 bfalse ) ],
% 0.67/1.08 [ ~( =( eq6( X, Y ), bfalse ) ), =( eq3( cons2( X, Z ), cons2( Y, T ) )
% 0.67/1.08 , bfalse ) ],
% 0.67/1.08 [ ~( =( eq4( X, Y ), btrue ) ), =( eq2( cons( X, Z ), cons( Y, T ) ),
% 0.67/1.08 eq2( Z, T ) ) ],
% 0.67/1.08 [ ~( =( eq6( X, Y ), btrue ) ), =( eq3( cons2( X, Z ), cons2( Y, T ) ),
% 0.67/1.08 eq3( Z, T ) ) ],
% 0.67/1.08 [ =( eq2( nil, cons( X, Y ) ), bfalse ) ],
% 0.67/1.08 [ =( eq3( nil2, cons2( X, Y ) ), bfalse ) ],
% 0.67/1.08 [ =( eq2( cons( X, Y ), nil ), bfalse ) ],
% 0.67/1.08 [ =( eq3( cons2( X, Y ), nil2 ), bfalse ) ],
% 0.67/1.08 [ =( eq5( n( X ), n( Y ) ), eq4( X, Y ) ) ],
% 0.67/1.08 [ ~( =( eq5( X, Y ), bfalse ) ), =( eq5( add( X, Z ), add( Y, T ) ),
% 0.67/1.08 bfalse ) ],
% 0.67/1.08 [ ~( =( eq5( X, Y ), btrue ) ), =( eq5( add( X, Z ), add( Y, T ) ), eq5(
% 0.67/1.08 Z, T ) ) ],
% 0.67/1.08 [ ~( =( eq5( X, Y ), bfalse ) ), =( eq5( mul( X, Z ), mul( Y, T ) ),
% 0.67/1.08 bfalse ) ],
% 0.67/1.08 [ ~( =( eq5( X, Y ), btrue ) ), =( eq5( mul( X, Z ), mul( Y, T ) ), eq5(
% 0.67/1.08 Z, T ) ) ],
% 0.67/1.08 [ ~( =( eq5( X, Y ), bfalse ) ), =( eq5( eq( X, Z ), eq( Y, T ) ),
% 0.67/1.08 bfalse ) ],
% 0.67/1.08 [ ~( =( eq5( X, Y ), btrue ) ), =( eq5( eq( X, Z ), eq( Y, T ) ), eq5( Z
% 0.67/1.08 , T ) ) ],
% 0.67/1.08 [ =( eq5( v( X ), v( Y ) ), eq4( X, Y ) ) ],
% 0.67/1.08 [ =( eq5( n( X ), add( Y, Z ) ), bfalse ) ],
% 0.67/1.08 [ =( eq5( n( X ), mul( Y, Z ) ), bfalse ) ],
% 0.67/1.08 [ =( eq5( n( X ), eq( Y, Z ) ), bfalse ) ],
% 0.67/1.08 [ =( eq5( n( X ), v( Y ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( add( X, Y ), n( Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( add( X, Y ), mul( Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( add( X, Y ), eq( Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( add( X, Y ), v( Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( mul( X, Y ), n( Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( mul( X, Y ), add( Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( mul( X, Y ), eq( Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( mul( X, Y ), v( Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( eq( X, Y ), n( Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( eq( X, Y ), add( Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( eq( X, Y ), mul( Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( eq( X, Y ), v( Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( v( X ), n( Y ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( v( X ), add( Y, Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( v( X ), mul( Y, Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq5( v( X ), eq( Y, Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq4( suc( X ), suc( Y ) ), eq4( X, Y ) ) ],
% 18.42/18.82 [ =( eq4( zero, suc( X ) ), bfalse ) ],
% 18.42/18.82 [ =( eq4( suc( X ), zero ), bfalse ) ],
% 18.42/18.82 [ =( eq6( print( X ), print( Y ) ), eq5( X, Y ) ) ],
% 18.42/18.82 [ ~( =( eq4( X, Y ), bfalse ) ), =( eq6( x( X, Z ), x( Y, T ) ), bfalse
% 18.42/18.82 ) ],
% 18.42/18.82 [ ~( =( eq4( X, Y ), btrue ) ), =( eq6( x( X, Z ), x( Y, T ) ), eq5( Z,
% 18.42/18.82 T ) ) ],
% 18.42/18.82 [ ~( =( eq5( X, Y ), bfalse ) ), =( eq6( while( X, Z ), while( Y, T ) )
% 18.42/18.82 , bfalse ) ],
% 18.42/18.82 [ ~( =( eq5( X, Y ), btrue ) ), =( eq6( while( X, Z ), while( Y, T ) ),
% 18.42/18.82 eq3( Z, T ) ) ],
% 18.42/18.82 [ ~( =( eq5( X, Y ), bfalse ) ), =( eq6( if( X, Z, T ), if( Y, U, W ) )
% 18.42/18.82 , bfalse ) ],
% 18.42/18.82 [ ~( =( eq5( X, Y ), btrue ) ), ~( =( eq3( Z, T ), bfalse ) ), =( eq6(
% 18.42/18.82 if( X, Z, U ), if( Y, T, W ) ), bfalse ) ],
% 18.42/18.82 [ ~( =( eq5( X, Y ), btrue ) ), ~( =( eq3( Z, T ), btrue ) ), =( eq6( if(
% 18.42/18.82 X, Z, U ), if( Y, T, W ) ), eq3( U, W ) ) ],
% 18.42/18.82 [ =( eq6( print( X ), x( Y, Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( print( X ), while( Y, Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( print( X ), if( Y, Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( x( X, Y ), print( Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( x( X, Y ), while( Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( x( X, Y ), if( Z, T, U ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( while( X, Y ), print( Z ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( while( X, Y ), x( Z, T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( while( X, Y ), if( Z, T, U ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( if( X, Y, Z ), print( T ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( if( X, Y, Z ), x( T, U ) ), bfalse ) ],
% 18.42/18.82 [ =( eq6( if( X, Y, Z ), while( T, U ) ), bfalse ) ],
% 18.42/18.82 [ =( apply1( lam, X ), opti2( X ) ) ],
% 18.42/18.82 [ ~( =( eq7( 'prop_Opti2'( X ), bfalse ), btrue ) ) ]
% 18.42/18.82 ] .
% 18.42/18.82
% 18.42/18.82
% 18.42/18.82 percentage equality = 1.000000, percentage horn = 1.000000
% 18.42/18.82 This is a pure equality problem
% 18.42/18.82
% 18.42/18.82
% 18.42/18.82
% 18.42/18.82 Options Used:
% 18.42/18.82
% 18.42/18.82 useres = 1
% 18.42/18.82 useparamod = 1
% 18.42/18.82 useeqrefl = 1
% 18.42/18.82 useeqfact = 1
% 18.42/18.82 usefactor = 1
% 18.42/18.82 usesimpsplitting = 0
% 18.42/18.82 usesimpdemod = 5
% 18.42/18.82 usesimpres = 3
% 18.42/18.82
% 18.42/18.82 resimpinuse = 1000
% 18.42/18.82 resimpclauses = 20000
% 18.42/18.82 substype = eqrewr
% 18.42/18.82 backwardsubs = 1
% 18.42/18.82 selectoldest = 5
% 18.42/18.82
% 18.42/18.82 litorderings [0] = split
% 18.42/18.82 litorderings [1] = extend the termordering, first sorting on arguments
% 18.42/18.82
% 18.42/18.82 termordering = kbo
% 18.42/18.82
% 18.42/18.82 litapriori = 0
% 18.42/18.82 termapriori = 1
% 18.42/18.82 litaposteriori = 0
% 18.42/18.82 termaposteriori = 0
% 18.42/18.82 demodaposteriori = 0
% 18.42/18.82 ordereqreflfact = 0
% 18.42/18.82
% 18.42/18.82 litselect = negord
% 18.42/18.82
% 18.42/18.82 maxweight = 15
% 18.42/18.82 maxdepth = 30000
% 18.42/18.82 maxlength = 115
% 18.42/18.82 maxnrvars = 195
% 18.42/18.82 excuselevel = 1
% 18.42/18.82 increasemaxweight = 1
% 18.42/18.82
% 18.42/18.82 maxselected = 10000000
% 18.42/18.82 maxnrclauses = 10000000
% 18.42/18.82
% 18.42/18.82 showgenerated = 0
% 18.42/18.82 showkept = 0
% 18.42/18.82 showselected = 0
% 18.42/18.82 showdeleted = 0
% 18.42/18.82 showresimp = 1
% 18.42/18.82 showstatus = 2000
% 18.42/18.82
% 18.42/18.82 prologoutput = 1
% 18.42/18.82 nrgoals = 5000000
% 18.42/18.82 totalproof = 1
% 18.42/18.82
% 18.42/18.82 Symbols occurring in the translation:
% 18.42/18.82
% 18.42/18.82 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 18.42/18.82 . [1, 2] (w:1, o:50, a:1, s:1, b:0),
% 18.42/18.82 ! [4, 1] (w:0, o:39, a:1, s:1, b:0),
% 18.42/18.82 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 18.42/18.82 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 18.42/18.82 btrue [42, 0] (w:1, o:14, a:1, s:1, b:0),
% 18.42/18.82 aux [43, 4] (w:1, o:98, a:1, s:1, b:0),
% 18.42/18.82 zero [44, 0] (w:1, o:15, a:1, s:1, b:0),
% 18.42/18.82 suc [45, 1] (w:1, o:44, a:1, s:1, b:0),
% 18.42/18.82 bfalse [46, 0] (w:1, o:16, a:1, s:1, b:0),
% 18.42/18.82 aux2 [51, 6] (w:1, o:99, a:1, s:1, b:0),
% 18.42/18.82 append [52, 2] (w:1, o:75, a:1, s:1, b:0),
% 259.64/260.07 run [53, 2] (w:1, o:76, a:1, s:1, b:0),
% 259.64/260.07 nil [54, 0] (w:1, o:23, a:1, s:1, b:0),
% 259.64/260.07 store [56, 3] (w:1, o:96, a:1, s:1, b:0),
% 259.64/260.07 cons [57, 2] (w:1, o:77, a:1, s:1, b:0),
% 259.64/260.07 while [64, 2] (w:1, o:78, a:1, s:1, b:0),
% 259.64/260.07 opti2 [65, 1] (w:1, o:46, a:1, s:1, b:0),
% 259.64/260.07 lam [66, 0] (w:1, o:33, a:1, s:1, b:0),
% 259.64/260.07 map [67, 2] (w:1, o:79, a:1, s:1, b:0),
% 259.64/260.07 if [69, 3] (w:1, o:97, a:1, s:1, b:0),
% 259.64/260.07 n [70, 1] (w:1, o:45, a:1, s:1, b:0),
% 259.64/260.07 add [71, 2] (w:1, o:80, a:1, s:1, b:0),
% 259.64/260.07 print [72, 1] (w:1, o:47, a:1, s:1, b:0),
% 259.64/260.07 x [73, 2] (w:1, o:81, a:1, s:1, b:0),
% 259.64/260.07 fetch [75, 2] (w:1, o:90, a:1, s:1, b:0),
% 259.64/260.07 addNat [76, 2] (w:1, o:91, a:1, s:1, b:0),
% 259.64/260.07 mulNat [77, 2] (w:1, o:92, a:1, s:1, b:0),
% 259.64/260.07 eval [78, 2] (w:1, o:82, a:1, s:1, b:0),
% 259.64/260.07 mul [82, 2] (w:1, o:93, a:1, s:1, b:0),
% 259.64/260.07 eq [83, 2] (w:1, o:83, a:1, s:1, b:0),
% 259.64/260.07 eq4 [84, 2] (w:1, o:85, a:1, s:1, b:0),
% 259.64/260.07 v [85, 1] (w:1, o:48, a:1, s:1, b:0),
% 259.64/260.07 nil2 [86, 0] (w:1, o:36, a:1, s:1, b:0),
% 259.64/260.07 cons2 [87, 2] (w:1, o:94, a:1, s:1, b:0),
% 259.64/260.07 'prop_Opti2' [90, 1] (w:1, o:49, a:1, s:1, b:0),
% 259.64/260.07 eq2 [91, 2] (w:1, o:86, a:1, s:1, b:0),
% 259.64/260.07 apply1 [94, 2] (w:1, o:95, a:1, s:1, b:0),
% 259.64/260.07 eq7 [95, 2] (w:1, o:88, a:1, s:1, b:0),
% 259.64/260.07 eq5 [96, 2] (w:1, o:89, a:1, s:1, b:0),
% 259.64/260.07 eq6 [97, 2] (w:1, o:87, a:1, s:1, b:0),
% 259.64/260.07 eq3 [98, 2] (w:1, o:84, a:1, s:1, b:0).
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Starting Search:
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Failed to find proof!
% 259.64/260.07 maxweight = 15
% 259.64/260.07 maxnrclauses = 10000000
% 259.64/260.07 Generated: 56124
% 259.64/260.07 Kept: 1182
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 The strategy used was not complete!
% 259.64/260.07
% 259.64/260.07 Increased maxweight to 16
% 259.64/260.07
% 259.64/260.07 Starting Search:
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 41095
% 259.64/260.07 Kept: 2000
% 259.64/260.07 Inuse: 1109
% 259.64/260.07 Deleted: 63
% 259.64/260.07 Deletedinuse: 0
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Failed to find proof!
% 259.64/260.07 maxweight = 16
% 259.64/260.07 maxnrclauses = 10000000
% 259.64/260.07 Generated: 119280
% 259.64/260.07 Kept: 2140
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 The strategy used was not complete!
% 259.64/260.07
% 259.64/260.07 Increased maxweight to 17
% 259.64/260.07
% 259.64/260.07 Starting Search:
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 16356
% 259.64/260.07 Kept: 2018
% 259.64/260.07 Inuse: 709
% 259.64/260.07 Deleted: 13
% 259.64/260.07 Deletedinuse: 0
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Failed to find proof!
% 259.64/260.07 maxweight = 17
% 259.64/260.07 maxnrclauses = 10000000
% 259.64/260.07 Generated: 260710
% 259.64/260.07 Kept: 3843
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 The strategy used was not complete!
% 259.64/260.07
% 259.64/260.07 Increased maxweight to 18
% 259.64/260.07
% 259.64/260.07 Starting Search:
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 8553
% 259.64/260.07 Kept: 2001
% 259.64/260.07 Inuse: 543
% 259.64/260.07 Deleted: 6
% 259.64/260.07 Deletedinuse: 0
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 49876
% 259.64/260.07 Kept: 4003
% 259.64/260.07 Inuse: 1167
% 259.64/260.07 Deleted: 68
% 259.64/260.07 Deletedinuse: 2
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 170669
% 259.64/260.07 Kept: 6004
% 259.64/260.07 Inuse: 2057
% 259.64/260.07 Deleted: 141
% 259.64/260.07 Deletedinuse: 4
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Failed to find proof!
% 259.64/260.07 maxweight = 18
% 259.64/260.07 maxnrclauses = 10000000
% 259.64/260.07 Generated: 1027209
% 259.64/260.07 Kept: 7995
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 The strategy used was not complete!
% 259.64/260.07
% 259.64/260.07 Increased maxweight to 19
% 259.64/260.07
% 259.64/260.07 Starting Search:
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 7661
% 259.64/260.07 Kept: 2016
% 259.64/260.07 Inuse: 525
% 259.64/260.07 Deleted: 6
% 259.64/260.07 Deletedinuse: 0
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 31467
% 259.64/260.07 Kept: 4018
% 259.64/260.07 Inuse: 933
% 259.64/260.07 Deleted: 31
% 259.64/260.07 Deletedinuse: 2
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 128195
% 259.64/260.07 Kept: 6020
% 259.64/260.07 Inuse: 1697
% 259.64/260.07 Deleted: 85
% 259.64/260.07 Deletedinuse: 4
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 179364
% 259.64/260.07 Kept: 8022
% 259.64/260.07 Inuse: 2102
% 259.64/260.07 Deleted: 190
% 259.64/260.07 Deletedinuse: 12
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 Intermediate Status:
% 259.64/260.07 Generated: 316408
% 259.64/260.07 Kept: 10023
% 259.64/260.07 Inuse: 3010
% 259.64/260.07 Deleted: 302
% 259.64/260.07 Deletedinuse: 17
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07 Resimplifying inuse:
% 259.64/260.07 Done
% 259.64/260.07
% 259.64/260.07
% 259.64/260.07 IntermTerminated
% 299.64/300.02 Bliksem ended
%------------------------------------------------------------------------------