%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX232-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n028.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:52 PM UTC 2026
% Result : Timeout 299.26s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX232-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.15/0.33 % Computer : n028.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:04:15 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.71/1.11 *** allocated 10000 integers for termspace/termends
% 0.71/1.11 *** allocated 10000 integers for clauses
% 0.71/1.11 *** allocated 10000 integers for justifications
% 0.71/1.11 Bliksem 1.12
% 0.71/1.11
% 0.71/1.11
% 0.71/1.11 Automatic Strategy Selection
% 0.71/1.11
% 0.71/1.11 Clauses:
% 0.71/1.11 [
% 0.71/1.11 [ =( aux( X, Y, btrue ), Y ) ],
% 0.71/1.11 [ =( aux( X, Y, bfalse ), X ) ],
% 0.71/1.11 [ =( aux2( X, Y, btrue ), nil2 ) ],
% 0.71/1.11 [ =( aux2( X, Y, bfalse ), cons2( X, enumFromToNat( suc( X ), Y ) ) ) ]
% 0.71/1.11 ,
% 0.71/1.11 [ =( aux3( X, Y, btrue ), bfalse ) ],
% 0.71/1.11 [ =( aux3( X, Y, bfalse ), unique( Y ) ) ],
% 0.71/1.11 [ =( predNat( zero ), zero ) ],
% 0.71/1.11 [ =( predNat( suc( X ) ), X ) ],
% 0.71/1.11 [ =( orb( btrue, X ), btrue ) ],
% 0.71/1.11 [ =( orb( bfalse, X ), X ) ],
% 0.71/1.11 [ =( or2( nil3 ), bfalse ) ],
% 0.71/1.11 [ =( or2( cons3( X, Y ) ), orb( X, or2( Y ) ) ) ],
% 0.71/1.11 [ =( one, suc( zero ) ) ],
% 0.71/1.11 [ =( two, suc( one ) ) ],
% 0.71/1.11 [ =( three, suc( two ) ) ],
% 0.71/1.11 [ =( notb( btrue ), bfalse ) ],
% 0.71/1.11 [ =( notb( bfalse ), btrue ) ],
% 0.71/1.11 [ =( lt( zero, zero ), bfalse ) ],
% 0.71/1.11 [ =( lt( zero, suc( X ) ), btrue ) ],
% 0.71/1.11 [ =( lt( suc( X ), zero ), bfalse ) ],
% 0.71/1.11 [ =( lt( suc( X ), suc( Y ) ), lt( X, Y ) ) ],
% 0.71/1.11 [ =( maxNat( X, Y ), aux( X, Y, lt( X, Y ) ) ) ],
% 0.71/1.11 [ =( maximum( X, nil ), X ) ],
% 0.71/1.11 [ =( maximum( X, cons( pair2( Y, Z ), T ) ), maximum( maxNat( X, maxNat(
% 0.71/1.11 Y, Z ) ), T ) ) ],
% 0.71/1.11 [ =( len( nil2 ), zero ) ],
% 0.71/1.11 [ =( len( cons2( X, Y ) ), suc( len( Y ) ) ) ],
% 0.71/1.11 [ =( last( X, nil2 ), X ) ],
% 0.71/1.11 [ =( last( X, cons2( Y, Z ) ), last( Y, Z ) ) ],
% 0.71/1.11 [ =( enumFromToNat( X, Y ), aux2( X, Y, lt( Y, X ) ) ) ],
% 0.71/1.11 [ =( elem( X, nil2 ), bfalse ) ],
% 0.71/1.11 [ =( elem( X, cons2( Y, Z ) ), orb( eq( Y, X ), elem( X, Z ) ) ) ],
% 0.71/1.11 [ =( unique( nil2 ), btrue ) ],
% 0.71/1.11 [ =( unique( cons2( X, Y ) ), aux3( X, Y, elem( X, Y ) ) ) ],
% 0.71/1.11 [ =( dodeca( nil2 ), nil ) ],
% 0.71/1.11 [ =( dodeca( cons2( X, Y ) ), cons( pair2( X, suc( X ) ), dodeca( Y ) )
% 0.71/1.11 ) ],
% 0.71/1.11 [ =( append( nil, X ), X ) ],
% 0.71/1.11 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 0.71/1.11 [ =( andb( btrue, X ), X ) ],
% 0.71/1.11 [ =( andb( bfalse, X ), bfalse ) ],
% 0.71/1.11 [ =( path( X, Y, nil ), nil3 ) ],
% 0.71/1.11 [ =( path( X, Y, cons( pair2( Z, T ), U ) ), cons3( orb( andb( eq( Z, X
% 0.71/1.11 ), eq( T, Y ) ), andb( eq( Z, Y ), eq( T, X ) ) ), path( X, Y, U ) ) ) ]
% 0.71/1.11 ,
% 0.71/1.11 [ =( path2( nil2, X ), btrue ) ],
% 0.71/1.11 [ =( path2( cons2( X, nil2 ), Y ), btrue ) ],
% 0.71/1.11 [ =( path2( cons2( X, cons2( Y, Z ) ), T ), andb( or2( path( X, Y, T ) )
% 0.71/1.11 , path2( cons2( Y, Z ), T ) ) ) ],
% 0.71/1.11 [ =( add( zero, X ), X ) ],
% 0.71/1.11 [ =( add( suc( X ), Y ), suc( add( X, Y ) ) ) ],
% 0.71/1.11 [ =( dodeca2( X, nil2 ), nil ) ],
% 0.71/1.11 [ =( dodeca2( X, cons2( Y, Z ) ), cons( pair2( Y, add( suc( X ), Y ) ),
% 0.71/1.11 dodeca2( X, Z ) ) ) ],
% 0.71/1.11 [ =( dodeca3( X, nil2 ), nil ) ],
% 0.71/1.11 [ =( dodeca3( X, cons2( Y, Z ) ), cons( pair2( add( suc( X ), Y ), add(
% 0.71/1.11 add( suc( X ), suc( X ) ), Y ) ), dodeca3( X, Z ) ) ) ],
% 0.71/1.11 [ =( dodeca4( X, nil2 ), nil ) ],
% 0.71/1.11 [ =( dodeca4( X, cons2( Y, Z ) ), cons( pair2( add( suc( X ), suc( Y ) )
% 0.71/1.11 , add( add( suc( X ), suc( X ) ), Y ) ), dodeca4( X, Z ) ) ) ],
% 0.71/1.11 [ =( dodeca5( X, nil2 ), nil ) ],
% 0.71/1.11 [ =( dodeca5( X, cons2( Y, Z ) ), cons( pair2( add( add( suc( X ), suc(
% 0.71/1.11 X ) ), Y ), add( add( add( suc( X ), suc( X ) ), suc( X ) ), Y ) ),
% 0.71/1.11 dodeca5( X, Z ) ) ) ],
% 0.71/1.11 [ =( dodeca6( X, nil2 ), nil ) ],
% 0.71/1.11 [ =( dodeca6( X, cons2( Y, Z ) ), cons( pair2( add( add( add( suc( X ),
% 0.71/1.11 suc( X ) ), suc( X ) ), Y ), add( add( add( suc( X ), suc( X ) ), suc( X
% 0.71/1.11 ) ), suc( Y ) ) ), dodeca6( X, Z ) ) ) ],
% 0.71/1.11 [ =( dodeca7( zero ), nil ) ],
% 0.71/1.11 [ =( dodeca7( suc( X ) ), append( cons( pair2( X, zero ), dodeca(
% 0.71/1.11 enumFromToNat( zero, X ) ) ), append( dodeca2( X, enumFromToNat( zero,
% 0.71/1.11 suc( X ) ) ), append( dodeca3( X, enumFromToNat( zero, suc( X ) ) ),
% 0.71/1.11 append( cons( pair2( suc( X ), add( add( suc( X ), suc( X ) ), X ) ),
% 0.71/1.11 dodeca4( X, enumFromToNat( zero, X ) ) ), append( dodeca5( X,
% 0.71/1.11 enumFromToNat( zero, suc( X ) ) ), cons( pair2( add( add( add( suc( X ),
% 0.71/1.11 suc( X ) ), suc( X ) ), X ), add( add( add( suc( X ), suc( X ) ), suc( X
% 0.71/1.11 ) ), zero ) ), dodeca6( X, enumFromToNat( zero, X ) ) ) ) ) ) ) ) ) ]
% 0.71/1.11 ,
% 0.71/1.11 [ =( tour( nil2, nil ), btrue ) ],
% 0.71/1.11 [ =( tour( nil2, cons( X, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( tour( cons2( X, Y ), nil ), bfalse ) ],
% 0.71/1.11 [ =( tour( cons2( X, Y ), cons( pair2( Z, T ), U ) ), andb( eq( X, last(
% 41.22/41.63 X, Y ) ), andb( path2( cons2( X, Y ), cons( pair2( Z, T ), U ) ), andb(
% 41.22/41.63 unique( Y ), eq( len( cons2( X, Y ) ), add( two, maximum( maxNat( Z, T )
% 41.22/41.63 , U ) ) ) ) ) ) ) ],
% 41.22/41.63 [ =( 'prop_t3'( X ), notb( tour( X, dodeca7( three ) ) ) ) ],
% 41.22/41.63 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 41.22/41.63 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 41.22/41.63 [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ],
% 41.22/41.63 [ =( eq( zero, suc( X ) ), bfalse ) ],
% 41.22/41.63 [ =( eq( suc( X ), zero ), bfalse ) ],
% 41.22/41.63 [ =( eq( X, X ), btrue ) ],
% 41.22/41.63 [ =( eq2( X, X ), btrue ) ],
% 41.22/41.63 [ ~( =( eq2( 'prop_t3'( X ), bfalse ), btrue ) ) ]
% 41.22/41.63 ] .
% 41.22/41.63
% 41.22/41.63
% 41.22/41.63 percentage equality = 1.000000, percentage horn = 1.000000
% 41.22/41.63 This is a pure equality problem
% 41.22/41.63
% 41.22/41.63
% 41.22/41.63
% 41.22/41.63 Options Used:
% 41.22/41.63
% 41.22/41.63 useres = 1
% 41.22/41.63 useparamod = 1
% 41.22/41.63 useeqrefl = 1
% 41.22/41.63 useeqfact = 1
% 41.22/41.63 usefactor = 1
% 41.22/41.63 usesimpsplitting = 0
% 41.22/41.63 usesimpdemod = 5
% 41.22/41.63 usesimpres = 3
% 41.22/41.63
% 41.22/41.63 resimpinuse = 1000
% 41.22/41.63 resimpclauses = 20000
% 41.22/41.63 substype = eqrewr
% 41.22/41.63 backwardsubs = 1
% 41.22/41.63 selectoldest = 5
% 41.22/41.63
% 41.22/41.63 litorderings [0] = split
% 41.22/41.63 litorderings [1] = extend the termordering, first sorting on arguments
% 41.22/41.63
% 41.22/41.63 termordering = kbo
% 41.22/41.63
% 41.22/41.63 litapriori = 0
% 41.22/41.63 termapriori = 1
% 41.22/41.63 litaposteriori = 0
% 41.22/41.63 termaposteriori = 0
% 41.22/41.63 demodaposteriori = 0
% 41.22/41.63 ordereqreflfact = 0
% 41.22/41.63
% 41.22/41.63 litselect = negord
% 41.22/41.63
% 41.22/41.63 maxweight = 15
% 41.22/41.63 maxdepth = 30000
% 41.22/41.63 maxlength = 115
% 41.22/41.63 maxnrvars = 195
% 41.22/41.63 excuselevel = 1
% 41.22/41.63 increasemaxweight = 1
% 41.22/41.63
% 41.22/41.63 maxselected = 10000000
% 41.22/41.63 maxnrclauses = 10000000
% 41.22/41.63
% 41.22/41.63 showgenerated = 0
% 41.22/41.63 showkept = 0
% 41.22/41.63 showselected = 0
% 41.22/41.63 showdeleted = 0
% 41.22/41.63 showresimp = 1
% 41.22/41.63 showstatus = 2000
% 41.22/41.63
% 41.22/41.63 prologoutput = 1
% 41.22/41.63 nrgoals = 5000000
% 41.22/41.63 totalproof = 1
% 41.22/41.63
% 41.22/41.63 Symbols occurring in the translation:
% 41.22/41.63
% 41.22/41.63 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 41.22/41.63 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 41.22/41.63 ! [4, 1] (w:0, o:33, a:1, s:1, b:0),
% 41.22/41.63 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 41.22/41.63 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 41.22/41.63 btrue [41, 0] (w:1, o:17, a:1, s:1, b:0),
% 41.22/41.63 aux [42, 3] (w:1, o:95, a:1, s:1, b:0),
% 41.22/41.63 bfalse [43, 0] (w:1, o:18, a:1, s:1, b:0),
% 41.22/41.63 aux2 [44, 3] (w:1, o:96, a:1, s:1, b:0),
% 41.22/41.63 nil2 [45, 0] (w:1, o:19, a:1, s:1, b:0),
% 41.22/41.63 suc [46, 1] (w:1, o:38, a:1, s:1, b:0),
% 41.22/41.63 enumFromToNat [47, 2] (w:1, o:77, a:1, s:1, b:0),
% 41.22/41.63 cons2 [48, 2] (w:1, o:78, a:1, s:1, b:0),
% 41.22/41.63 aux3 [50, 3] (w:1, o:97, a:1, s:1, b:0),
% 41.22/41.63 unique [51, 1] (w:1, o:39, a:1, s:1, b:0),
% 41.22/41.63 zero [52, 0] (w:1, o:20, a:1, s:1, b:0),
% 41.22/41.63 predNat [53, 1] (w:1, o:42, a:1, s:1, b:0),
% 41.22/41.63 orb [55, 2] (w:1, o:79, a:1, s:1, b:0),
% 41.22/41.63 nil3 [56, 0] (w:1, o:22, a:1, s:1, b:0),
% 41.22/41.63 or2 [57, 1] (w:1, o:41, a:1, s:1, b:0),
% 41.22/41.63 cons3 [58, 2] (w:1, o:80, a:1, s:1, b:0),
% 41.22/41.63 one [59, 0] (w:1, o:8, a:1, s:1, b:0),
% 41.22/41.63 two [60, 0] (w:1, o:23, a:1, s:1, b:0),
% 41.22/41.63 three [61, 0] (w:1, o:24, a:1, s:1, b:0),
% 41.22/41.63 notb [62, 1] (w:1, o:40, a:1, s:1, b:0),
% 41.22/41.63 lt [63, 2] (w:1, o:81, a:1, s:1, b:0),
% 41.22/41.63 maxNat [67, 2] (w:1, o:83, a:1, s:1, b:0),
% 41.22/41.63 nil [68, 0] (w:1, o:7, a:1, s:1, b:0),
% 41.22/41.63 maximum [69, 2] (w:1, o:84, a:1, s:1, b:0),
% 41.22/41.63 pair2 [71, 2] (w:1, o:85, a:1, s:1, b:0),
% 41.22/41.63 cons [73, 2] (w:1, o:86, a:1, s:1, b:0),
% 41.22/41.63 len [74, 1] (w:1, o:43, a:1, s:1, b:0),
% 41.22/41.63 last [75, 2] (w:1, o:82, a:1, s:1, b:0),
% 41.22/41.63 elem [77, 2] (w:1, o:87, a:1, s:1, b:0),
% 41.22/41.63 eq [78, 2] (w:1, o:88, a:1, s:1, b:0),
% 41.22/41.63 dodeca [79, 1] (w:1, o:44, a:1, s:1, b:0),
% 41.22/41.63 append [80, 2] (w:1, o:89, a:1, s:1, b:0),
% 41.22/41.63 andb [81, 2] (w:1, o:90, a:1, s:1, b:0),
% 41.22/41.63 path [82, 3] (w:1, o:98, a:1, s:1, b:0),
% 41.22/41.63 path2 [86, 2] (w:1, o:91, a:1, s:1, b:0),
% 41.22/41.63 add [87, 2] (w:1, o:92, a:1, s:1, b:0),
% 41.22/41.63 dodeca2 [88, 2] (w:1, o:72, a:1, s:1, b:0),
% 41.22/41.63 dodeca3 [89, 2] (w:1, o:73, a:1, s:1, b:0),
% 41.22/41.63 dodeca4 [90, 2] (w:1, o:74, a:1, s:1, b:0),
% 41.22/41.63 dodeca5 [91, 2] (w:1, o:75, a:1, s:1, b:0),
% 41.22/41.63 dodeca6 [92, 2] (w:1, o:76, a:1, s:1, b:0),
% 41.22/41.63 dodeca7 [93, 1] (w:1, o:45, a:1, s:1, b:0),
% 41.22/41.63 tour [94, 2] (w:1, o:93, a:1, s:1, b:0),
% 186.22/186.81 'prop_t3' [97, 1] (w:1, o:46, a:1, s:1, b:0),
% 186.22/186.81 eq2 [98, 2] (w:1, o:94, a:1, s:1, b:0).
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Starting Search:
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 13134
% 186.22/186.81 Kept: 2006
% 186.22/186.81 Inuse: 1074
% 186.22/186.81 Deleted: 127
% 186.22/186.81 Deletedinuse: 50
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 31540
% 186.22/186.81 Kept: 4009
% 186.22/186.81 Inuse: 2115
% 186.22/186.81 Deleted: 242
% 186.22/186.81 Deletedinuse: 73
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 59741
% 186.22/186.81 Kept: 6229
% 186.22/186.81 Inuse: 3217
% 186.22/186.81 Deleted: 371
% 186.22/186.81 Deletedinuse: 84
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Failed to find proof!
% 186.22/186.81 maxweight = 15
% 186.22/186.81 maxnrclauses = 10000000
% 186.22/186.81 Generated: 179863
% 186.22/186.81 Kept: 7857
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 The strategy used was not complete!
% 186.22/186.81
% 186.22/186.81 Increased maxweight to 16
% 186.22/186.81
% 186.22/186.81 Starting Search:
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 12096
% 186.22/186.81 Kept: 2001
% 186.22/186.81 Inuse: 977
% 186.22/186.81 Deleted: 108
% 186.22/186.81 Deletedinuse: 35
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 26826
% 186.22/186.81 Kept: 4004
% 186.22/186.81 Inuse: 1988
% 186.22/186.81 Deleted: 356
% 186.22/186.81 Deletedinuse: 117
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 46046
% 186.22/186.81 Kept: 6025
% 186.22/186.81 Inuse: 2741
% 186.22/186.81 Deleted: 463
% 186.22/186.81 Deletedinuse: 120
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 69044
% 186.22/186.81 Kept: 8025
% 186.22/186.81 Inuse: 3686
% 186.22/186.81 Deleted: 559
% 186.22/186.81 Deletedinuse: 132
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 116151
% 186.22/186.81 Kept: 10030
% 186.22/186.81 Inuse: 5237
% 186.22/186.81 Deleted: 690
% 186.22/186.81 Deletedinuse: 146
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 257520
% 186.22/186.81 Kept: 12067
% 186.22/186.81 Inuse: 8407
% 186.22/186.81 Deleted: 900
% 186.22/186.81 Deletedinuse: 157
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Failed to find proof!
% 186.22/186.81 maxweight = 16
% 186.22/186.81 maxnrclauses = 10000000
% 186.22/186.81 Generated: 429019
% 186.22/186.81 Kept: 13021
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 The strategy used was not complete!
% 186.22/186.81
% 186.22/186.81 Increased maxweight to 17
% 186.22/186.81
% 186.22/186.81 Starting Search:
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 11171
% 186.22/186.81 Kept: 2003
% 186.22/186.81 Inuse: 874
% 186.22/186.81 Deleted: 91
% 186.22/186.81 Deletedinuse: 16
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 21945
% 186.22/186.81 Kept: 4005
% 186.22/186.81 Inuse: 1661
% 186.22/186.81 Deleted: 273
% 186.22/186.81 Deletedinuse: 104
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 37294
% 186.22/186.81 Kept: 6017
% 186.22/186.81 Inuse: 2666
% 186.22/186.81 Deleted: 440
% 186.22/186.81 Deletedinuse: 127
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 53161
% 186.22/186.81 Kept: 8018
% 186.22/186.81 Inuse: 3340
% 186.22/186.81 Deleted: 521
% 186.22/186.81 Deletedinuse: 137
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 63944
% 186.22/186.81 Kept: 10018
% 186.22/186.81 Inuse: 3890
% 186.22/186.81 Deleted: 549
% 186.22/186.81 Deletedinuse: 147
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 80042
% 186.22/186.81 Kept: 12020
% 186.22/186.81 Inuse: 4589
% 186.22/186.81 Deleted: 647
% 186.22/186.81 Deletedinuse: 165
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 104842
% 186.22/186.81 Kept: 14020
% 186.22/186.81 Inuse: 5414
% 186.22/186.81 Deleted: 761
% 186.22/186.81 Deletedinuse: 180
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 128906
% 186.22/186.81 Kept: 16253
% 186.22/186.81 Inuse: 6496
% 186.22/186.81 Deleted: 865
% 186.22/186.81 Deletedinuse: 225
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 156057
% 186.22/186.81 Kept: 18810
% 186.22/186.81 Inuse: 7467
% 186.22/186.81 Deleted: 972
% 186.22/186.81 Deletedinuse: 241
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying clauses:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 174660
% 186.22/186.81 Kept: 20811
% 186.22/186.81 Inuse: 7986
% 186.22/186.81 Deleted: 2934
% 186.22/186.81 Deletedinuse: 751
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 241810
% 186.22/186.81 Kept: 22811
% 186.22/186.81 Inuse: 9448
% 186.22/186.81 Deleted: 2940
% 186.22/186.81 Deletedinuse: 755
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81 Resimplifying inuse:
% 186.22/186.81 Done
% 186.22/186.81
% 186.22/186.81
% 186.22/186.81 Intermediate Status:
% 186.22/186.81 Generated: 353339
% 186.22/186.81 KeTerminated
% 299.26/300.03 Bliksem ended
%------------------------------------------------------------------------------