%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX240-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n029.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.11 % Problem : SWX240-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.14/0.33 % Computer : n029.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % DateTime : Tue May 5 13:21:14 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.72/1.25 *** allocated 10000 integers for termspace/termends
% 0.72/1.25 *** allocated 10000 integers for clauses
% 0.72/1.25 *** allocated 10000 integers for justifications
% 0.72/1.25 Bliksem 1.12
% 0.72/1.25
% 0.72/1.25
% 0.72/1.25 Automatic Strategy Selection
% 0.72/1.25
% 0.72/1.25 Clauses:
% 0.72/1.25 [
% 0.72/1.25 [ =( aux( X, Y, Z, btrue ), del( X, Z ) ) ],
% 0.72/1.25 [ =( aux( X, Y, Z, bfalse ), cons( Y, del( X, Z ) ) ) ],
% 0.72/1.25 [ =( aux2( X, Y, Z, btrue ), cons( Y, X ) ) ],
% 0.72/1.25 [ =( aux2( X, Y, Z, bfalse ), del( Y, X ) ) ],
% 0.72/1.25 [ =( aux3( X, Y, Z, T, btrue ), run( X, Z ) ) ],
% 0.72/1.25 [ =( aux3( X, Y, Z, T, bfalse ), run( X, T ) ) ],
% 0.72/1.25 [ =( orb( btrue, X ), btrue ) ],
% 0.72/1.25 [ =( orb( bfalse, X ), X ) ],
% 0.72/1.25 [ =( secret( nand( X, Y ) ), orb( secret( X ), secret( Y ) ) ) ],
% 0.72/1.25 [ =( secret( var( high( X ) ) ), btrue ) ],
% 0.72/1.25 [ =( secret( var( low( X ) ) ), bfalse ) ],
% 0.72/1.25 [ =( secret( tT ), bfalse ) ],
% 0.72/1.25 [ =( secret( fF ), bfalse ) ],
% 0.72/1.25 [ =( notb( btrue ), bfalse ) ],
% 0.72/1.25 [ =( notb( bfalse ), btrue ) ],
% 0.72/1.25 [ =( l, low( zero ) ) ],
% 0.72/1.25 [ =( impl( btrue, X ), X ) ],
% 0.72/1.25 [ =( impl( bfalse, X ), btrue ) ],
% 0.72/1.25 [ =( h, high( zero ) ) ],
% 0.72/1.25 [ =( elem( X, nil ), bfalse ) ],
% 0.72/1.25 [ =( elem( X, cons( Y, Z ) ), orb( eq2( Y, X ), elem( X, Z ) ) ) ],
% 0.72/1.25 [ =( del( X, nil ), nil ) ],
% 0.72/1.25 [ =( del( X, cons( Y, Z ) ), aux( X, Y, Z, eq2( X, Y ) ) ) ],
% 0.72/1.25 [ =( andb( btrue, X ), X ) ],
% 0.72/1.25 [ =( andb( bfalse, X ), bfalse ) ],
% 0.72/1.25 [ =( eval( X, nand( Y, Z ) ), notb( andb( eval( X, Y ), eval( X, Z ) ) )
% 0.72/1.25 ) ],
% 0.72/1.25 [ =( eval( X, tT ), btrue ) ],
% 0.72/1.25 [ =( eval( X, fF ), bfalse ) ],
% 0.72/1.25 [ =( eval( X, var( Y ) ), elem( Y, X ) ) ],
% 0.72/1.25 [ =( run( X, skip ), X ) ],
% 0.72/1.25 [ =( run( X, assign( Y, Z ) ), aux2( X, Y, Z, eval( X, Z ) ) ) ],
% 0.72/1.25 [ =( run( X, seq( Y, Z ) ), run( run( X, Y ), Z ) ) ],
% 0.72/1.25 [ =( run( X, ifThenElse( Y, Z, T ) ), aux3( X, Y, Z, T, eval( X, Y ) ) )
% 0.72/1.25 ],
% 0.72/1.25 [ =( typeCorrect( skip ), btrue ) ],
% 0.72/1.25 [ =( typeCorrect( assign( high( X ), Y ) ), btrue ) ],
% 0.72/1.25 [ =( typeCorrect( assign( low( X ), Y ) ), notb( secret( Y ) ) ) ],
% 0.72/1.25 [ =( typeCorrect( seq( X, Y ) ), andb( typeCorrect( X ), typeCorrect( Y
% 0.72/1.25 ) ) ) ],
% 0.72/1.25 [ =( typeCorrect( ifThenElse( X, Y, Z ) ), andb( typeCorrect( Y ),
% 0.72/1.25 typeCorrect( Z ) ) ) ],
% 0.72/1.25 [ =( prop( X, Y ), impl( typeCorrect( X ), eq5( elem( l, run( Y, X ) ),
% 0.72/1.25 elem( l, run( cons( h, Y ), X ) ) ) ) ) ],
% 0.72/1.25 [ =( eq3( tT, fF ), bfalse ) ],
% 0.72/1.25 [ =( eq3( fF, tT ), bfalse ) ],
% 0.72/1.25 [ =( eq5( bfalse, btrue ), bfalse ) ],
% 0.72/1.25 [ =( eq5( btrue, bfalse ), bfalse ) ],
% 0.72/1.25 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( nand( X, Z ), nand( Y, T ) ),
% 0.72/1.25 bfalse ) ],
% 0.72/1.25 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( nand( X, Z ), nand( Y, T ) ),
% 0.72/1.25 eq3( Z, T ) ) ],
% 0.72/1.25 [ =( eq3( var( X ), var( Y ) ), eq2( X, Y ) ) ],
% 0.72/1.25 [ =( eq3( nand( X, Y ), tT ), bfalse ) ],
% 0.72/1.25 [ =( eq3( nand( X, Y ), fF ), bfalse ) ],
% 0.72/1.25 [ =( eq3( nand( X, Y ), var( Z ) ), bfalse ) ],
% 0.72/1.25 [ =( eq3( tT, nand( X, Y ) ), bfalse ) ],
% 0.72/1.25 [ =( eq3( tT, var( X ) ), bfalse ) ],
% 0.72/1.25 [ =( eq3( fF, nand( X, Y ) ), bfalse ) ],
% 0.72/1.25 [ =( eq3( fF, var( X ) ), bfalse ) ],
% 0.72/1.25 [ =( eq3( var( X ), nand( Y, Z ) ), bfalse ) ],
% 0.72/1.25 [ =( eq3( var( X ), tT ), bfalse ) ],
% 0.72/1.25 [ =( eq3( var( X ), fF ), bfalse ) ],
% 0.72/1.25 [ =( eq2( high( X ), high( Y ) ), eq( X, Y ) ) ],
% 0.72/1.25 [ =( eq2( low( X ), low( Y ) ), eq( X, Y ) ) ],
% 0.72/1.25 [ =( eq2( high( X ), low( Y ) ), bfalse ) ],
% 0.72/1.25 [ =( eq2( low( X ), high( Y ) ), bfalse ) ],
% 0.72/1.25 [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ],
% 0.72/1.25 [ =( eq( zero, suc( X ) ), bfalse ) ],
% 0.72/1.25 [ =( eq( suc( X ), zero ), bfalse ) ],
% 0.72/1.25 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq4( assign( X, Z ), assign( Y, T )
% 0.72/1.25 ), bfalse ) ],
% 0.72/1.25 [ ~( =( eq2( X, Y ), btrue ) ), =( eq4( assign( X, Z ), assign( Y, T ) )
% 0.72/1.25 , eq3( Z, T ) ) ],
% 0.72/1.25 [ ~( =( eq4( X, Y ), bfalse ) ), =( eq4( seq( X, Z ), seq( Y, T ) ),
% 0.72/1.25 bfalse ) ],
% 0.72/1.25 [ ~( =( eq4( X, Y ), btrue ) ), =( eq4( seq( X, Z ), seq( Y, T ) ), eq4(
% 0.72/1.25 Z, T ) ) ],
% 0.72/1.25 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq4( ifThenElse( X, Z, T ),
% 0.72/1.25 ifThenElse( Y, U, W ) ), bfalse ) ],
% 0.72/1.25 [ ~( =( eq3( X, Y ), btrue ) ), ~( =( eq4( Z, T ), bfalse ) ), =( eq4(
% 0.72/1.25 ifThenElse( X, Z, U ), ifThenElse( Y, T, W ) ), bfalse ) ],
% 0.72/1.25 [ ~( =( eq3( X, Y ), btrue ) ), ~( =( eq4( Z, T ), btrue ) ), =( eq4(
% 0.72/1.25 ifThenElse( X, Z, U ), ifThenElse( Y, T, W ) ), eq4( U, W ) ) ],
% 46.93/47.34 [ =( eq4( skip, assign( X, Y ) ), bfalse ) ],
% 46.93/47.34 [ =( eq4( skip, seq( X, Y ) ), bfalse ) ],
% 46.93/47.34 [ =( eq4( skip, ifThenElse( X, Y, Z ) ), bfalse ) ],
% 46.93/47.34 [ =( eq4( assign( X, Y ), skip ), bfalse ) ],
% 46.93/47.34 [ =( eq4( assign( X, Y ), seq( Z, T ) ), bfalse ) ],
% 46.93/47.34 [ =( eq4( assign( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 46.93/47.34 [ =( eq4( seq( X, Y ), skip ), bfalse ) ],
% 46.93/47.34 [ =( eq4( seq( X, Y ), assign( Z, T ) ), bfalse ) ],
% 46.93/47.34 [ =( eq4( seq( X, Y ), ifThenElse( Z, T, U ) ), bfalse ) ],
% 46.93/47.34 [ =( eq4( ifThenElse( X, Y, Z ), skip ), bfalse ) ],
% 46.93/47.34 [ =( eq4( ifThenElse( X, Y, Z ), assign( T, U ) ), bfalse ) ],
% 46.93/47.34 [ =( eq4( ifThenElse( X, Y, Z ), seq( T, U ) ), bfalse ) ],
% 46.93/47.34 [ =( eq( X, X ), btrue ) ],
% 46.93/47.34 [ =( eq2( X, X ), btrue ) ],
% 46.93/47.34 [ =( eq3( X, X ), btrue ) ],
% 46.93/47.34 [ =( eq4( X, X ), btrue ) ],
% 46.93/47.34 [ =( eq5( X, X ), btrue ) ],
% 46.93/47.34 [ ~( =( eq5( prop( X, Y ), bfalse ), btrue ) ) ]
% 46.93/47.34 ] .
% 46.93/47.34
% 46.93/47.34
% 46.93/47.34 percentage equality = 1.000000, percentage horn = 1.000000
% 46.93/47.34 This is a pure equality problem
% 46.93/47.34
% 46.93/47.34
% 46.93/47.34
% 46.93/47.34 Options Used:
% 46.93/47.34
% 46.93/47.34 useres = 1
% 46.93/47.34 useparamod = 1
% 46.93/47.34 useeqrefl = 1
% 46.93/47.34 useeqfact = 1
% 46.93/47.34 usefactor = 1
% 46.93/47.34 usesimpsplitting = 0
% 46.93/47.34 usesimpdemod = 5
% 46.93/47.34 usesimpres = 3
% 46.93/47.34
% 46.93/47.34 resimpinuse = 1000
% 46.93/47.34 resimpclauses = 20000
% 46.93/47.34 substype = eqrewr
% 46.93/47.34 backwardsubs = 1
% 46.93/47.34 selectoldest = 5
% 46.93/47.34
% 46.93/47.34 litorderings [0] = split
% 46.93/47.34 litorderings [1] = extend the termordering, first sorting on arguments
% 46.93/47.34
% 46.93/47.34 termordering = kbo
% 46.93/47.34
% 46.93/47.34 litapriori = 0
% 46.93/47.34 termapriori = 1
% 46.93/47.34 litaposteriori = 0
% 46.93/47.34 termaposteriori = 0
% 46.93/47.34 demodaposteriori = 0
% 46.93/47.34 ordereqreflfact = 0
% 46.93/47.34
% 46.93/47.34 litselect = negord
% 46.93/47.34
% 46.93/47.34 maxweight = 15
% 46.93/47.34 maxdepth = 30000
% 46.93/47.34 maxlength = 115
% 46.93/47.34 maxnrvars = 195
% 46.93/47.34 excuselevel = 1
% 46.93/47.34 increasemaxweight = 1
% 46.93/47.34
% 46.93/47.34 maxselected = 10000000
% 46.93/47.34 maxnrclauses = 10000000
% 46.93/47.34
% 46.93/47.34 showgenerated = 0
% 46.93/47.34 showkept = 0
% 46.93/47.34 showselected = 0
% 46.93/47.34 showdeleted = 0
% 46.93/47.34 showresimp = 1
% 46.93/47.34 showstatus = 2000
% 46.93/47.34
% 46.93/47.34 prologoutput = 1
% 46.93/47.34 nrgoals = 5000000
% 46.93/47.34 totalproof = 1
% 46.93/47.34
% 46.93/47.34 Symbols occurring in the translation:
% 46.93/47.34
% 46.93/47.34 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 46.93/47.34 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 46.93/47.34 ! [4, 1] (w:0, o:35, a:1, s:1, b:0),
% 46.93/47.34 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 46.93/47.34 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 46.93/47.34 btrue [42, 0] (w:1, o:18, a:1, s:1, b:0),
% 46.93/47.34 aux [43, 4] (w:1, o:90, a:1, s:1, b:0),
% 46.93/47.34 del [44, 2] (w:1, o:73, a:1, s:1, b:0),
% 46.93/47.34 bfalse [45, 0] (w:1, o:19, a:1, s:1, b:0),
% 46.93/47.34 cons [46, 2] (w:1, o:72, a:1, s:1, b:0),
% 46.93/47.34 aux2 [48, 4] (w:1, o:91, a:1, s:1, b:0),
% 46.93/47.34 aux3 [52, 5] (w:1, o:92, a:1, s:1, b:0),
% 46.93/47.34 run [53, 2] (w:1, o:74, a:1, s:1, b:0),
% 46.93/47.34 orb [55, 2] (w:1, o:76, a:1, s:1, b:0),
% 46.93/47.34 nand [58, 2] (w:1, o:75, a:1, s:1, b:0),
% 46.93/47.34 secret [59, 1] (w:1, o:40, a:1, s:1, b:0),
% 46.93/47.34 high [60, 1] (w:1, o:41, a:1, s:1, b:0),
% 46.93/47.34 var [61, 1] (w:1, o:42, a:1, s:1, b:0),
% 46.93/47.34 low [63, 1] (w:1, o:43, a:1, s:1, b:0),
% 46.93/47.34 tT [64, 0] (w:1, o:28, a:1, s:1, b:0),
% 46.93/47.34 fF [65, 0] (w:1, o:29, a:1, s:1, b:0),
% 46.93/47.34 notb [66, 1] (w:1, o:44, a:1, s:1, b:0),
% 46.93/47.34 l [67, 0] (w:1, o:30, a:1, s:1, b:0),
% 46.93/47.34 zero [68, 0] (w:1, o:31, a:1, s:1, b:0),
% 46.93/47.34 impl [69, 2] (w:1, o:77, a:1, s:1, b:0),
% 46.93/47.34 h [70, 0] (w:1, o:32, a:1, s:1, b:0),
% 46.93/47.34 nil [71, 0] (w:1, o:33, a:1, s:1, b:0),
% 46.93/47.34 elem [72, 2] (w:1, o:78, a:1, s:1, b:0),
% 46.93/47.34 eq2 [74, 2] (w:1, o:79, a:1, s:1, b:0),
% 46.93/47.34 andb [75, 2] (w:1, o:80, a:1, s:1, b:0),
% 46.93/47.34 eval [76, 2] (w:1, o:81, a:1, s:1, b:0),
% 46.93/47.34 skip [77, 0] (w:1, o:5, a:1, s:1, b:0),
% 46.93/47.34 assign [78, 2] (w:1, o:82, a:1, s:1, b:0),
% 46.93/47.34 seq [80, 2] (w:1, o:83, a:1, s:1, b:0),
% 46.93/47.34 ifThenElse [81, 3] (w:1, o:89, a:1, s:1, b:0),
% 46.93/47.34 typeCorrect [82, 1] (w:1, o:46, a:1, s:1, b:0),
% 46.93/47.34 prop [85, 2] (w:1, o:84, a:1, s:1, b:0),
% 46.93/47.34 eq5 [86, 2] (w:1, o:86, a:1, s:1, b:0),
% 46.93/47.34 eq3 [87, 2] (w:1, o:87, a:1, s:1, b:0),
% 46.93/47.34 eq [88, 2] (w:1, o:88, a:1, s:1, b:0),
% 46.93/47.34 suc [89, 1] (w:1, o:45, a:1, s:1, b:0),
% 46.93/47.34 eq4 [90, 2] (w:1, o:85, a:1, s:1, b:0).
% 46.93/47.34
% 46.93/47.34
% 46.93/47.34 Starting Search:
% 46.93/47.34
% 46.93/47.34 Resimplifying inuse:
% 46.93/47.34 Done
% 46.93/47.34
% 46.93/47.34 Failed to find proof!
% 172.93/173.37 maxweight = 15
% 172.93/173.37 maxnrclauses = 10000000
% 172.93/173.37 Generated: 21803
% 172.93/173.37 Kept: 575
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 The strategy used was not complete!
% 172.93/173.37
% 172.93/173.37 Increased maxweight to 16
% 172.93/173.37
% 172.93/173.37 Starting Search:
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Failed to find proof!
% 172.93/173.37 maxweight = 16
% 172.93/173.37 maxnrclauses = 10000000
% 172.93/173.37 Generated: 26872
% 172.93/173.37 Kept: 661
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 The strategy used was not complete!
% 172.93/173.37
% 172.93/173.37 Increased maxweight to 17
% 172.93/173.37
% 172.93/173.37 Starting Search:
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Failed to find proof!
% 172.93/173.37 maxweight = 17
% 172.93/173.37 maxnrclauses = 10000000
% 172.93/173.37 Generated: 39727
% 172.93/173.37 Kept: 872
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 The strategy used was not complete!
% 172.93/173.37
% 172.93/173.37 Increased maxweight to 18
% 172.93/173.37
% 172.93/173.37 Starting Search:
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Failed to find proof!
% 172.93/173.37 maxweight = 18
% 172.93/173.37 maxnrclauses = 10000000
% 172.93/173.37 Generated: 83885
% 172.93/173.37 Kept: 1348
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 The strategy used was not complete!
% 172.93/173.37
% 172.93/173.37 Increased maxweight to 19
% 172.93/173.37
% 172.93/173.37 Starting Search:
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Failed to find proof!
% 172.93/173.37 maxweight = 19
% 172.93/173.37 maxnrclauses = 10000000
% 172.93/173.37 Generated: 159797
% 172.93/173.37 Kept: 1893
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 The strategy used was not complete!
% 172.93/173.37
% 172.93/173.37 Increased maxweight to 20
% 172.93/173.37
% 172.93/173.37 Starting Search:
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 61060
% 172.93/173.37 Kept: 2000
% 172.93/173.37 Inuse: 989
% 172.93/173.37 Deleted: 130
% 172.93/173.37 Deletedinuse: 2
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Failed to find proof!
% 172.93/173.37 maxweight = 20
% 172.93/173.37 maxnrclauses = 10000000
% 172.93/173.37 Generated: 348054
% 172.93/173.37 Kept: 3216
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 The strategy used was not complete!
% 172.93/173.37
% 172.93/173.37 Increased maxweight to 21
% 172.93/173.37
% 172.93/173.37 Starting Search:
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 40073
% 172.93/173.37 Kept: 2004
% 172.93/173.37 Inuse: 769
% 172.93/173.37 Deleted: 85
% 172.93/173.37 Deletedinuse: 1
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 210966
% 172.93/173.37 Kept: 4004
% 172.93/173.37 Inuse: 2009
% 172.93/173.37 Deleted: 355
% 172.93/173.37 Deletedinuse: 4
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 443235
% 172.93/173.37 Kept: 6004
% 172.93/173.37 Inuse: 3535
% 172.93/173.37 Deleted: 710
% 172.93/173.37 Deletedinuse: 7
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Failed to find proof!
% 172.93/173.37 maxweight = 21
% 172.93/173.37 maxnrclauses = 10000000
% 172.93/173.37 Generated: 962302
% 172.93/173.37 Kept: 7381
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 The strategy used was not complete!
% 172.93/173.37
% 172.93/173.37 Increased maxweight to 22
% 172.93/173.37
% 172.93/173.37 Starting Search:
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 32260
% 172.93/173.37 Kept: 2021
% 172.93/173.37 Inuse: 677
% 172.93/173.37 Deleted: 70
% 172.93/173.37 Deletedinuse: 1
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 157552
% 172.93/173.37 Kept: 4022
% 172.93/173.37 Inuse: 1668
% 172.93/173.37 Deleted: 274
% 172.93/173.37 Deletedinuse: 3
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 252784
% 172.93/173.37 Kept: 6027
% 172.93/173.37 Inuse: 2350
% 172.93/173.37 Deleted: 410
% 172.93/173.37 Deletedinuse: 15
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 302866
% 172.93/173.37 Kept: 8034
% 172.93/173.37 Inuse: 2852
% 172.93/173.37 Deleted: 460
% 172.93/173.37 Deletedinuse: 15
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 431073
% 172.93/173.37 Kept: 10037
% 172.93/173.37 Inuse: 3759
% 172.93/173.37 Deleted: 676
% 172.93/173.37 Deletedinuse: 15
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 641739
% 172.93/173.37 Kept: 12046
% 172.93/173.37 Inuse: 4696
% 172.93/173.37 Deleted: 879
% 172.93/173.37 Deletedinuse: 15
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 1131526
% 172.93/173.37 Kept: 14046
% 172.93/173.37 Inuse: 6227
% 172.93/173.37 Deleted: 1147
% 172.93/173.37 Deletedinuse: 15
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 1711415
% 172.93/173.37 Kept: 16047
% 172.93/173.37 Inuse: 7629
% 172.93/173.37 Deleted: 1571
% 172.93/173.37 Deletedinuse: 15
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Failed to find proof!
% 172.93/173.37 maxweight = 22
% 172.93/173.37 maxnrclauses = 10000000
% 172.93/173.37 Generated: 3925258
% 172.93/173.37 Kept: 17366
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 The strategy used was not complete!
% 172.93/173.37
% 172.93/173.37 Increased maxweight to 23
% 172.93/173.37
% 172.93/173.37 Starting Search:
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 29849
% 172.93/173.37 Kept: 2088
% 172.93/173.37 Inuse: 657
% 172.93/173.37 Deleted: 70
% 172.93/173.37 Deletedinuse: 1
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37 Resimplifying inuse:
% 172.93/173.37 Done
% 172.93/173.37
% 172.93/173.37
% 172.93/173.37 Intermediate Status:
% 172.93/173.37 Generated: 84930
% 172.93/173.37 Kept: 4224
% 172.93/173.37 Inuse: 1266
% 172.93/173.37 Deleted: 179
% 172.93/173.37 Deletedinuse: 3
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 216446
% 209.33/209.70 Kept: 6224
% 209.33/209.70 Inuse: 2038
% 209.33/209.70 Deleted: 342
% 209.33/209.70 Deletedinuse: 12
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 266593
% 209.33/209.70 Kept: 8229
% 209.33/209.70 Inuse: 2421
% 209.33/209.70 Deleted: 481
% 209.33/209.70 Deletedinuse: 13
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 338881
% 209.33/209.70 Kept: 10235
% 209.33/209.70 Inuse: 2964
% 209.33/209.70 Deleted: 582
% 209.33/209.70 Deletedinuse: 13
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 418532
% 209.33/209.70 Kept: 12235
% 209.33/209.70 Inuse: 3405
% 209.33/209.70 Deleted: 708
% 209.33/209.70 Deletedinuse: 13
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 454905
% 209.33/209.70 Kept: 14239
% 209.33/209.70 Inuse: 3698
% 209.33/209.70 Deleted: 750
% 209.33/209.70 Deletedinuse: 13
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 580103
% 209.33/209.70 Kept: 16239
% 209.33/209.70 Inuse: 4394
% 209.33/209.70 Deleted: 827
% 209.33/209.70 Deletedinuse: 13
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 737516
% 209.33/209.70 Kept: 18242
% 209.33/209.70 Inuse: 5353
% 209.33/209.70 Deleted: 1061
% 209.33/209.70 Deletedinuse: 13
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying clauses:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 836630
% 209.33/209.70 Kept: 20243
% 209.33/209.70 Inuse: 5665
% 209.33/209.70 Deleted: 5701
% 209.33/209.70 Deletedinuse: 272
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 1038999
% 209.33/209.70 Kept: 22245
% 209.33/209.70 Inuse: 6192
% 209.33/209.70 Deleted: 5801
% 209.33/209.70 Deletedinuse: 273
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 1334779
% 209.33/209.70 Kept: 24245
% 209.33/209.70 Inuse: 7115
% 209.33/209.70 Deleted: 5825
% 209.33/209.70 Deletedinuse: 273
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 1672077
% 209.33/209.70 Kept: 26246
% 209.33/209.70 Inuse: 7903
% 209.33/209.70 Deleted: 6021
% 209.33/209.70 Deletedinuse: 273
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 2048741
% 209.33/209.70 Kept: 28249
% 209.33/209.70 Inuse: 8917
% 209.33/209.70 Deleted: 6132
% 209.33/209.70 Deletedinuse: 273
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 2599224
% 209.33/209.70 Kept: 30250
% 209.33/209.70 Inuse: 9670
% 209.33/209.70 Deleted: 6135
% 209.33/209.70 Deletedinuse: 273
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 2777937
% 209.33/209.70 Kept: 32254
% 209.33/209.70 Inuse: 10347
% 209.33/209.70 Deleted: 6260
% 209.33/209.70 Deletedinuse: 275
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 4162505
% 209.33/209.70 Kept: 34254
% 209.33/209.70 Inuse: 13901
% 209.33/209.70 Deleted: 6791
% 209.33/209.70 Deletedinuse: 325
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 6120167
% 209.33/209.70 Kept: 36258
% 209.33/209.70 Inuse: 18280
% 209.33/209.70 Deleted: 7786
% 209.33/209.70 Deletedinuse: 361
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Failed to find proof!
% 209.33/209.70 maxweight = 23
% 209.33/209.70 maxnrclauses = 10000000
% 209.33/209.70 Generated: 10823522
% 209.33/209.70 Kept: 37508
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 The strategy used was not complete!
% 209.33/209.70
% 209.33/209.70 Increased maxweight to 24
% 209.33/209.70
% 209.33/209.70 Starting Search:
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 18820
% 209.33/209.70 Kept: 2001
% 209.33/209.70 Inuse: 582
% 209.33/209.70 Deleted: 61
% 209.33/209.70 Deletedinuse: 1
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 66979
% 209.33/209.70 Kept: 4006
% 209.33/209.70 Inuse: 1126
% 209.33/209.70 Deleted: 151
% 209.33/209.70 Deletedinuse: 3
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 149537
% 209.33/209.70 Kept: 6008
% 209.33/209.70 Inuse: 1697
% 209.33/209.70 Deleted: 296
% 209.33/209.70 Deletedinuse: 5
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 239573
% 209.33/209.70 Kept: 8018
% 209.33/209.70 Inuse: 2216
% 209.33/209.70 Deleted: 373
% 209.33/209.70 Deletedinuse: 11
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 308165
% 209.33/209.70 Kept: 10164
% 209.33/209.70 Inuse: 2613
% 209.33/209.70 Deleted: 436
% 209.33/209.70 Deletedinuse: 14
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70
% 209.33/209.70 Intermediate Status:
% 209.33/209.70 Generated: 359554
% 209.33/209.70 Kept: 12168
% 209.33/209.70 Inuse: 2985
% 209.33/209.70 Deleted: 508
% 209.33/209.70 Deletedinuse: 16
% 209.33/209.70
% 209.33/209.70 Resimplifying inuse:
% 209.33/209.70 Done
% 209.33/209.70
% 209.33/209.70 ResimTerminated
% 299.49/300.03 Bliksem ended
%------------------------------------------------------------------------------