%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX241-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n026.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:53 PM UTC 2026
% Result : Timeout 299.49s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX241-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n026.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 13:24:38 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.72/1.11 *** allocated 10000 integers for termspace/termends
% 0.72/1.11 *** allocated 10000 integers for clauses
% 0.72/1.11 *** allocated 10000 integers for justifications
% 0.72/1.11 Bliksem 1.12
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Automatic Strategy Selection
% 0.72/1.11
% 0.72/1.11 Clauses:
% 0.72/1.11 [
% 0.72/1.11 [ =( aux( X, Y, Z, btrue ), del( X, Z ) ) ],
% 0.72/1.11 [ =( aux( X, Y, Z, bfalse ), cons( Y, del( X, Z ) ) ) ],
% 0.72/1.11 [ =( aux2( X, Y, Z, btrue ), cons( Y, X ) ) ],
% 0.72/1.11 [ =( aux2( X, Y, Z, bfalse ), del( Y, X ) ) ],
% 0.72/1.11 [ =( aux3( X, Y, Z, T, btrue ), run( X, Z ) ) ],
% 0.72/1.11 [ =( aux3( X, Y, Z, T, bfalse ), run( X, T ) ) ],
% 0.72/1.11 [ =( orb( btrue, X ), btrue ) ],
% 0.72/1.11 [ =( orb( bfalse, X ), X ) ],
% 0.72/1.11 [ =( secret( nand( X, Y ) ), orb( secret( X ), secret( Y ) ) ) ],
% 0.72/1.11 [ =( secret( var( high( X ) ) ), btrue ) ],
% 0.72/1.11 [ =( secret( var( low( X ) ) ), bfalse ) ],
% 0.72/1.11 [ =( secret( tT ), bfalse ) ],
% 0.72/1.11 [ =( secret( fF ), bfalse ) ],
% 0.72/1.11 [ =( notb( btrue ), bfalse ) ],
% 0.72/1.11 [ =( notb( bfalse ), btrue ) ],
% 0.72/1.11 [ =( l, low( zero ) ) ],
% 0.72/1.11 [ =( impl( btrue, X ), X ) ],
% 0.72/1.11 [ =( impl( bfalse, X ), btrue ) ],
% 0.72/1.11 [ =( h, high( zero ) ) ],
% 0.72/1.11 [ =( elem( X, nil ), bfalse ) ],
% 0.72/1.11 [ =( elem( X, cons( Y, Z ) ), orb( eq2( Y, X ), elem( X, Z ) ) ) ],
% 0.72/1.11 [ =( del( X, nil ), nil ) ],
% 0.72/1.11 [ =( del( X, cons( Y, Z ) ), aux( X, Y, Z, eq2( X, Y ) ) ) ],
% 0.72/1.11 [ =( andb( btrue, X ), X ) ],
% 0.72/1.11 [ =( andb( bfalse, X ), bfalse ) ],
% 0.72/1.11 [ =( eval( X, nand( Y, Z ) ), notb( andb( eval( X, Y ), eval( X, Z ) ) )
% 0.72/1.11 ) ],
% 0.72/1.11 [ =( eval( X, tT ), btrue ) ],
% 0.72/1.11 [ =( eval( X, fF ), bfalse ) ],
% 0.72/1.11 [ =( eval( X, var( Y ) ), elem( Y, X ) ) ],
% 0.72/1.11 [ =( run( X, skip ), X ) ],
% 0.72/1.11 [ =( run( X, assign( Y, Z ) ), aux2( X, Y, Z, eval( X, Z ) ) ) ],
% 0.72/1.11 [ =( run( X, seq( Y, Z ) ), run( run( X, Y ), Z ) ) ],
% 0.72/1.11 [ =( run( X, ifThenElse( Y, Z, T ) ), aux3( X, Y, Z, T, eval( X, Y ) ) )
% 0.72/1.11 ],
% 0.72/1.11 [ =( run( X, while( Y, Z ) ), run( X, ifThenElse( Y, seq( Z, while( Y, Z
% 0.72/1.11 ) ), skip ) ) ) ],
% 0.72/1.11 [ =( typeCorrect( skip ), btrue ) ],
% 0.72/1.11 [ =( typeCorrect( assign( high( X ), Y ) ), btrue ) ],
% 0.72/1.11 [ =( typeCorrect( assign( low( X ), Y ) ), notb( secret( Y ) ) ) ],
% 0.72/1.11 [ =( typeCorrect( seq( X, Y ) ), andb( typeCorrect( X ), typeCorrect( Y
% 0.72/1.11 ) ) ) ],
% 0.72/1.11 [ =( typeCorrect( ifThenElse( X, Y, Z ) ), andb( typeCorrect( Y ),
% 0.72/1.11 typeCorrect( Z ) ) ) ],
% 0.72/1.11 [ =( typeCorrect( while( X, Y ) ), typeCorrect( Y ) ) ],
% 0.72/1.11 [ =( prop( X, Y ), impl( typeCorrect( X ), eq5( elem( l, run( Y, X ) ),
% 0.72/1.11 elem( l, run( cons( h, Y ), X ) ) ) ) ) ],
% 0.72/1.11 [ =( eq3( tT, fF ), bfalse ) ],
% 0.72/1.11 [ =( eq3( fF, tT ), bfalse ) ],
% 0.72/1.11 [ =( eq5( bfalse, btrue ), bfalse ) ],
% 0.72/1.11 [ =( eq5( btrue, bfalse ), bfalse ) ],
% 0.72/1.11 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( nand( X, Z ), nand( Y, T ) ),
% 0.72/1.11 bfalse ) ],
% 0.72/1.11 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( nand( X, Z ), nand( Y, T ) ),
% 0.72/1.11 eq3( Z, T ) ) ],
% 0.72/1.11 [ =( eq3( var( X ), var( Y ) ), eq2( X, Y ) ) ],
% 0.72/1.11 [ =( eq3( nand( X, Y ), tT ), bfalse ) ],
% 0.72/1.11 [ =( eq3( nand( X, Y ), fF ), bfalse ) ],
% 0.72/1.11 [ =( eq3( nand( X, Y ), var( Z ) ), bfalse ) ],
% 0.72/1.11 [ =( eq3( tT, nand( X, Y ) ), bfalse ) ],
% 0.72/1.11 [ =( eq3( tT, var( X ) ), bfalse ) ],
% 0.72/1.11 [ =( eq3( fF, nand( X, Y ) ), bfalse ) ],
% 0.72/1.11 [ =( eq3( fF, var( X ) ), bfalse ) ],
% 0.72/1.11 [ =( eq3( var( X ), nand( Y, Z ) ), bfalse ) ],
% 0.72/1.11 [ =( eq3( var( X ), tT ), bfalse ) ],
% 0.72/1.11 [ =( eq3( var( X ), fF ), bfalse ) ],
% 0.72/1.11 [ =( eq2( high( X ), high( Y ) ), eq( X, Y ) ) ],
% 0.72/1.11 [ =( eq2( low( X ), low( Y ) ), eq( X, Y ) ) ],
% 0.72/1.11 [ =( eq2( high( X ), low( Y ) ), bfalse ) ],
% 0.72/1.11 [ =( eq2( low( X ), high( Y ) ), bfalse ) ],
% 0.72/1.11 [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ],
% 0.72/1.11 [ =( eq( zero, suc( X ) ), bfalse ) ],
% 0.72/1.11 [ =( eq( suc( X ), zero ), bfalse ) ],
% 0.72/1.11 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq4( assign( X, Z ), assign( Y, T )
% 0.72/1.11 ), bfalse ) ],
% 0.72/1.11 [ ~( =( eq2( X, Y ), btrue ) ), =( eq4( assign( X, Z ), assign( Y, T ) )
% 0.72/1.11 , eq3( Z, T ) ) ],
% 0.72/1.11 [ ~( =( eq4( X, Y ), bfalse ) ), =( eq4( seq( X, Z ), seq( Y, T ) ),
% 0.72/1.11 bfalse ) ],
% 0.72/1.11 [ ~( =( eq4( X, Y ), btrue ) ), =( eq4( seq( X, Z ), seq( Y, T ) ), eq4(
% 0.72/1.11 Z, T ) ) ],
% 0.72/1.11 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq4( ifThenElse( X, Z, T ),
% 0.72/1.11 ifThenElse( Y, U, W ) ), bfalse ) ],
% 0.72/1.11 [ ~( =( eq3( X, Y ), btrue ) ), ~( =( eq4( Z, T ), bfalse ) ), =( eq4(
% 0.72/1.11 ifThenElse( X, Z, U ), ifThenElse( Y, T, W ) ), bfalse ) ],
% 21.14/21.58 [ ~( =( eq3( X, Y ), btrue ) ), ~( =( eq4( Z, T ), btrue ) ), =( eq4(
% 21.14/21.58 ifThenElse( X, Z, U ), ifThenElse( Y, T, W ) ), eq4( U, W ) ) ],
% 21.14/21.58 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq4( while( X, Z ), while( Y, T ) )
% 21.14/21.58 , bfalse ) ],
% 21.14/21.58 [ ~( =( eq3( X, Y ), btrue ) ), =( eq4( while( X, Z ), while( Y, T ) ),
% 21.14/21.58 eq4( Z, T ) ) ],
% 21.14/21.58 [ =( eq4( skip, assign( X, Y ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( skip, seq( X, Y ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( skip, ifThenElse( X, Y, Z ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( skip, while( X, Y ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( assign( X, Y ), skip ), bfalse ) ],
% 21.14/21.58 [ =( eq4( assign( X, Y ), seq( Z, T ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( assign( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( assign( X, Y ), while( Z, T ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( seq( X, Y ), skip ), bfalse ) ],
% 21.14/21.58 [ =( eq4( seq( X, Y ), assign( Z, T ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( seq( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( seq( X, Y ), while( Z, T ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( ifThenElse( X, Y, Z ), skip ), bfalse ) ],
% 21.14/21.58 [ =( eq4( ifThenElse( X, Y, Z ), assign( T, U ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( ifThenElse( X, Y, Z ), seq( T, U ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( ifThenElse( X, Y, Z ), while( T, U ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( while( X, Y ), skip ), bfalse ) ],
% 21.14/21.58 [ =( eq4( while( X, Y ), assign( Z, T ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( while( X, Y ), seq( Z, T ) ), bfalse ) ],
% 21.14/21.58 [ =( eq4( while( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 21.14/21.58 [ =( eq( X, X ), btrue ) ],
% 21.14/21.58 [ =( eq2( X, X ), btrue ) ],
% 21.14/21.58 [ =( eq3( X, X ), btrue ) ],
% 21.14/21.58 [ =( eq4( X, X ), btrue ) ],
% 21.14/21.58 [ =( eq5( X, X ), btrue ) ],
% 21.14/21.58 [ ~( =( eq5( prop( X, Y ), bfalse ), btrue ) ) ]
% 21.14/21.58 ] .
% 21.14/21.58
% 21.14/21.58
% 21.14/21.58 percentage equality = 1.000000, percentage horn = 1.000000
% 21.14/21.58 This is a pure equality problem
% 21.14/21.58
% 21.14/21.58
% 21.14/21.58
% 21.14/21.58 Options Used:
% 21.14/21.58
% 21.14/21.58 useres = 1
% 21.14/21.58 useparamod = 1
% 21.14/21.58 useeqrefl = 1
% 21.14/21.58 useeqfact = 1
% 21.14/21.58 usefactor = 1
% 21.14/21.58 usesimpsplitting = 0
% 21.14/21.58 usesimpdemod = 5
% 21.14/21.58 usesimpres = 3
% 21.14/21.58
% 21.14/21.58 resimpinuse = 1000
% 21.14/21.58 resimpclauses = 20000
% 21.14/21.58 substype = eqrewr
% 21.14/21.58 backwardsubs = 1
% 21.14/21.58 selectoldest = 5
% 21.14/21.58
% 21.14/21.58 litorderings [0] = split
% 21.14/21.58 litorderings [1] = extend the termordering, first sorting on arguments
% 21.14/21.58
% 21.14/21.58 termordering = kbo
% 21.14/21.58
% 21.14/21.58 litapriori = 0
% 21.14/21.58 termapriori = 1
% 21.14/21.58 litaposteriori = 0
% 21.14/21.58 termaposteriori = 0
% 21.14/21.58 demodaposteriori = 0
% 21.14/21.58 ordereqreflfact = 0
% 21.14/21.58
% 21.14/21.58 litselect = negord
% 21.14/21.58
% 21.14/21.58 maxweight = 15
% 21.14/21.58 maxdepth = 30000
% 21.14/21.58 maxlength = 115
% 21.14/21.58 maxnrvars = 195
% 21.14/21.58 excuselevel = 1
% 21.14/21.58 increasemaxweight = 1
% 21.14/21.58
% 21.14/21.58 maxselected = 10000000
% 21.14/21.58 maxnrclauses = 10000000
% 21.14/21.58
% 21.14/21.58 showgenerated = 0
% 21.14/21.58 showkept = 0
% 21.14/21.58 showselected = 0
% 21.14/21.58 showdeleted = 0
% 21.14/21.58 showresimp = 1
% 21.14/21.58 showstatus = 2000
% 21.14/21.58
% 21.14/21.58 prologoutput = 1
% 21.14/21.58 nrgoals = 5000000
% 21.14/21.58 totalproof = 1
% 21.14/21.58
% 21.14/21.58 Symbols occurring in the translation:
% 21.14/21.58
% 21.14/21.58 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 21.14/21.58 . [1, 2] (w:1, o:49, a:1, s:1, b:0),
% 21.14/21.58 ! [4, 1] (w:0, o:37, a:1, s:1, b:0),
% 21.14/21.58 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 21.14/21.58 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 21.14/21.58 btrue [42, 0] (w:1, o:18, a:1, s:1, b:0),
% 21.14/21.58 aux [43, 4] (w:1, o:93, a:1, s:1, b:0),
% 21.14/21.58 del [44, 2] (w:1, o:75, a:1, s:1, b:0),
% 21.14/21.58 bfalse [45, 0] (w:1, o:19, a:1, s:1, b:0),
% 21.14/21.58 cons [46, 2] (w:1, o:74, a:1, s:1, b:0),
% 21.14/21.58 aux2 [48, 4] (w:1, o:94, a:1, s:1, b:0),
% 21.14/21.58 aux3 [52, 5] (w:1, o:95, a:1, s:1, b:0),
% 21.14/21.58 run [53, 2] (w:1, o:76, a:1, s:1, b:0),
% 21.14/21.58 orb [55, 2] (w:1, o:78, a:1, s:1, b:0),
% 21.14/21.58 nand [58, 2] (w:1, o:77, a:1, s:1, b:0),
% 21.14/21.58 secret [59, 1] (w:1, o:42, a:1, s:1, b:0),
% 21.14/21.58 high [60, 1] (w:1, o:43, a:1, s:1, b:0),
% 21.14/21.58 var [61, 1] (w:1, o:44, a:1, s:1, b:0),
% 21.14/21.58 low [63, 1] (w:1, o:45, a:1, s:1, b:0),
% 21.14/21.58 tT [64, 0] (w:1, o:29, a:1, s:1, b:0),
% 21.14/21.58 fF [65, 0] (w:1, o:30, a:1, s:1, b:0),
% 21.14/21.58 notb [66, 1] (w:1, o:46, a:1, s:1, b:0),
% 21.14/21.58 l [67, 0] (w:1, o:31, a:1, s:1, b:0),
% 21.14/21.58 zero [68, 0] (w:1, o:32, a:1, s:1, b:0),
% 21.14/21.58 impl [69, 2] (w:1, o:79, a:1, s:1, b:0),
% 21.14/21.58 h [70, 0] (w:1, o:33, a:1, s:1, b:0),
% 21.14/21.58 nil [71, 0] (w:1, o:34, a:1, s:1, b:0),
% 92.84/93.27 elem [72, 2] (w:1, o:80, a:1, s:1, b:0),
% 92.84/93.27 eq2 [74, 2] (w:1, o:81, a:1, s:1, b:0),
% 92.84/93.27 andb [75, 2] (w:1, o:82, a:1, s:1, b:0),
% 92.84/93.27 eval [76, 2] (w:1, o:83, a:1, s:1, b:0),
% 92.84/93.27 skip [77, 0] (w:1, o:5, a:1, s:1, b:0),
% 92.84/93.27 assign [78, 2] (w:1, o:84, a:1, s:1, b:0),
% 92.84/93.27 seq [80, 2] (w:1, o:85, a:1, s:1, b:0),
% 92.84/93.27 ifThenElse [81, 3] (w:1, o:92, a:1, s:1, b:0),
% 92.84/93.27 while [84, 2] (w:1, o:86, a:1, s:1, b:0),
% 92.84/93.27 typeCorrect [85, 1] (w:1, o:48, a:1, s:1, b:0),
% 92.84/93.27 prop [88, 2] (w:1, o:87, a:1, s:1, b:0),
% 92.84/93.27 eq5 [89, 2] (w:1, o:89, a:1, s:1, b:0),
% 92.84/93.27 eq3 [90, 2] (w:1, o:90, a:1, s:1, b:0),
% 92.84/93.27 eq [91, 2] (w:1, o:91, a:1, s:1, b:0),
% 92.84/93.27 suc [92, 1] (w:1, o:47, a:1, s:1, b:0),
% 92.84/93.27 eq4 [93, 2] (w:1, o:88, a:1, s:1, b:0).
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Starting Search:
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Failed to find proof!
% 92.84/93.27 maxweight = 15
% 92.84/93.27 maxnrclauses = 10000000
% 92.84/93.27 Generated: 32655
% 92.84/93.27 Kept: 701
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 The strategy used was not complete!
% 92.84/93.27
% 92.84/93.27 Increased maxweight to 16
% 92.84/93.27
% 92.84/93.27 Starting Search:
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Failed to find proof!
% 92.84/93.27 maxweight = 16
% 92.84/93.27 maxnrclauses = 10000000
% 92.84/93.27 Generated: 40734
% 92.84/93.27 Kept: 819
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 The strategy used was not complete!
% 92.84/93.27
% 92.84/93.27 Increased maxweight to 17
% 92.84/93.27
% 92.84/93.27 Starting Search:
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Failed to find proof!
% 92.84/93.27 maxweight = 17
% 92.84/93.27 maxnrclauses = 10000000
% 92.84/93.27 Generated: 71277
% 92.84/93.27 Kept: 1163
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 The strategy used was not complete!
% 92.84/93.27
% 92.84/93.27 Increased maxweight to 18
% 92.84/93.27
% 92.84/93.27 Starting Search:
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Failed to find proof!
% 92.84/93.27 maxweight = 18
% 92.84/93.27 maxnrclauses = 10000000
% 92.84/93.27 Generated: 131312
% 92.84/93.27 Kept: 1713
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 The strategy used was not complete!
% 92.84/93.27
% 92.84/93.27 Increased maxweight to 19
% 92.84/93.27
% 92.84/93.27 Starting Search:
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 69916
% 92.84/93.27 Kept: 2000
% 92.84/93.27 Inuse: 1085
% 92.84/93.27 Deleted: 113
% 92.84/93.27 Deletedinuse: 1
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Failed to find proof!
% 92.84/93.27 maxweight = 19
% 92.84/93.27 maxnrclauses = 10000000
% 92.84/93.27 Generated: 261677
% 92.84/93.27 Kept: 2455
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 The strategy used was not complete!
% 92.84/93.27
% 92.84/93.27 Increased maxweight to 20
% 92.84/93.27
% 92.84/93.27 Starting Search:
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 45288
% 92.84/93.27 Kept: 2006
% 92.84/93.27 Inuse: 809
% 92.84/93.27 Deleted: 63
% 92.84/93.27 Deletedinuse: 1
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 362081
% 92.84/93.27 Kept: 4007
% 92.84/93.27 Inuse: 2795
% 92.84/93.27 Deleted: 328
% 92.84/93.27 Deletedinuse: 3
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Failed to find proof!
% 92.84/93.27 maxweight = 20
% 92.84/93.27 maxnrclauses = 10000000
% 92.84/93.27 Generated: 585694
% 92.84/93.27 Kept: 4146
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 The strategy used was not complete!
% 92.84/93.27
% 92.84/93.27 Increased maxweight to 21
% 92.84/93.27
% 92.84/93.27 Starting Search:
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 42283
% 92.84/93.27 Kept: 2000
% 92.84/93.27 Inuse: 785
% 92.84/93.27 Deleted: 68
% 92.84/93.27 Deletedinuse: 1
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 131903
% 92.84/93.27 Kept: 4000
% 92.84/93.27 Inuse: 1600
% 92.84/93.27 Deleted: 177
% 92.84/93.27 Deletedinuse: 3
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 369378
% 92.84/93.27 Kept: 6007
% 92.84/93.27 Inuse: 2902
% 92.84/93.27 Deleted: 379
% 92.84/93.27 Deletedinuse: 6
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 787811
% 92.84/93.27 Kept: 8008
% 92.84/93.27 Inuse: 5114
% 92.84/93.27 Deleted: 813
% 92.84/93.27 Deletedinuse: 7
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Failed to find proof!
% 92.84/93.27 maxweight = 21
% 92.84/93.27 maxnrclauses = 10000000
% 92.84/93.27 Generated: 1487217
% 92.84/93.27 Kept: 9004
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 The strategy used was not complete!
% 92.84/93.27
% 92.84/93.27 Increased maxweight to 22
% 92.84/93.27
% 92.84/93.27 Starting Search:
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 28736
% 92.84/93.27 Kept: 2011
% 92.84/93.27 Inuse: 680
% 92.84/93.27 Deleted: 58
% 92.84/93.27 Deletedinuse: 1
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 86705
% 92.84/93.27 Kept: 4036
% 92.84/93.27 Inuse: 1239
% 92.84/93.27 Deleted: 120
% 92.84/93.27 Deletedinuse: 3
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 336488
% 92.84/93.27 Kept: 6039
% 92.84/93.27 Inuse: 2463
% 92.84/93.27 Deleted: 300
% 92.84/93.27 Deletedinuse: 10
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27 Resimplifying inuse:
% 92.84/93.27 Done
% 92.84/93.27
% 92.84/93.27
% 92.84/93.27 Intermediate Status:
% 92.84/93.27 Generated: 427961
% 92.84/93.27 Kept: 8041
% 92.84/93.27 Inuse: 3054
% 269.24/269.74 Deleted: 395
% 269.24/269.74 Deletedinuse: 12
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 494746
% 269.24/269.74 Kept: 10046
% 269.24/269.74 Inuse: 3643
% 269.24/269.74 Deleted: 458
% 269.24/269.74 Deletedinuse: 12
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 670502
% 269.24/269.74 Kept: 12046
% 269.24/269.74 Inuse: 4603
% 269.24/269.74 Deleted: 636
% 269.24/269.74 Deletedinuse: 12
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 996379
% 269.24/269.74 Kept: 14046
% 269.24/269.74 Inuse: 6028
% 269.24/269.74 Deleted: 861
% 269.24/269.74 Deletedinuse: 12
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 1363013
% 269.24/269.74 Kept: 16052
% 269.24/269.74 Inuse: 6868
% 269.24/269.74 Deleted: 953
% 269.24/269.74 Deletedinuse: 12
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 2158472
% 269.24/269.74 Kept: 18056
% 269.24/269.74 Inuse: 8873
% 269.24/269.74 Deleted: 1497
% 269.24/269.74 Deletedinuse: 12
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Failed to find proof!
% 269.24/269.74 maxweight = 22
% 269.24/269.74 maxnrclauses = 10000000
% 269.24/269.74 Generated: 5062870
% 269.24/269.74 Kept: 19566
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 The strategy used was not complete!
% 269.24/269.74
% 269.24/269.74 Increased maxweight to 23
% 269.24/269.74
% 269.24/269.74 Starting Search:
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 21444
% 269.24/269.74 Kept: 2028
% 269.24/269.74 Inuse: 612
% 269.24/269.74 Deleted: 49
% 269.24/269.74 Deletedinuse: 0
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 71707
% 269.24/269.74 Kept: 4030
% 269.24/269.74 Inuse: 1110
% 269.24/269.74 Deleted: 111
% 269.24/269.74 Deletedinuse: 3
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 134100
% 269.24/269.74 Kept: 6032
% 269.24/269.74 Inuse: 1685
% 269.24/269.74 Deleted: 196
% 269.24/269.74 Deletedinuse: 3
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 282385
% 269.24/269.74 Kept: 8032
% 269.24/269.74 Inuse: 2410
% 269.24/269.74 Deleted: 315
% 269.24/269.74 Deletedinuse: 7
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 433534
% 269.24/269.74 Kept: 10037
% 269.24/269.74 Inuse: 3017
% 269.24/269.74 Deleted: 436
% 269.24/269.74 Deletedinuse: 10
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 493396
% 269.24/269.74 Kept: 12097
% 269.24/269.74 Inuse: 3405
% 269.24/269.74 Deleted: 502
% 269.24/269.74 Deletedinuse: 11
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 636008
% 269.24/269.74 Kept: 14098
% 269.24/269.74 Inuse: 4056
% 269.24/269.74 Deleted: 637
% 269.24/269.74 Deletedinuse: 11
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 695037
% 269.24/269.74 Kept: 16100
% 269.24/269.74 Inuse: 4424
% 269.24/269.74 Deleted: 717
% 269.24/269.74 Deletedinuse: 11
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 745733
% 269.24/269.74 Kept: 18101
% 269.24/269.74 Inuse: 4822
% 269.24/269.74 Deleted: 781
% 269.24/269.74 Deletedinuse: 11
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying clauses:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 967064
% 269.24/269.74 Kept: 20103
% 269.24/269.74 Inuse: 5737
% 269.24/269.74 Deleted: 3511
% 269.24/269.74 Deletedinuse: 11
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 1248386
% 269.24/269.74 Kept: 22104
% 269.24/269.74 Inuse: 7174
% 269.24/269.74 Deleted: 3511
% 269.24/269.74 Deletedinuse: 11
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 1472430
% 269.24/269.74 Kept: 24111
% 269.24/269.74 Inuse: 8018
% 269.24/269.74 Deleted: 3896
% 269.24/269.74 Deletedinuse: 327
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 1733414
% 269.24/269.74 Kept: 26130
% 269.24/269.74 Inuse: 8435
% 269.24/269.74 Deleted: 3972
% 269.24/269.74 Deletedinuse: 403
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 2102643
% 269.24/269.74 Kept: 28132
% 269.24/269.74 Inuse: 9030
% 269.24/269.74 Deleted: 4050
% 269.24/269.74 Deletedinuse: 403
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 2894601
% 269.24/269.74 Kept: 30132
% 269.24/269.74 Inuse: 10232
% 269.24/269.74 Deleted: 4062
% 269.24/269.74 Deletedinuse: 403
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 3102602
% 269.24/269.74 Kept: 32134
% 269.24/269.74 Inuse: 10975
% 269.24/269.74 Deleted: 4244
% 269.24/269.74 Deletedinuse: 404
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74 Resimplifying inuse:
% 269.24/269.74 Done
% 269.24/269.74
% 269.24/269.74
% 269.24/269.74 Intermediate Status:
% 269.24/269.74 Generated: 3348217
% 269.24/269.74 Kept: 34134
% 269.24/269.74 Inuse: 11753
% 269.24/269.74 Deleted: 4507
% 269.24/269.74 Deletedinuse:Terminated
% 299.49/300.03 Bliksem ended
% 299.49/300.03 Terminated
%------------------------------------------------------------------------------