%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX230-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n009.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:51 PM UTC 2026
% Result : Timeout 299.66s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX230-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.15/0.34 % Computer : n009.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % DateTime : Tue May 5 12:59:10 EDT 2026
% 0.15/0.34 % CPUTime :
% 2.03/2.47 *** allocated 10000 integers for termspace/termends
% 2.03/2.47 *** allocated 10000 integers for clauses
% 2.03/2.47 *** allocated 10000 integers for justifications
% 2.03/2.47 Bliksem 1.12
% 2.03/2.47
% 2.03/2.47
% 2.03/2.47 Automatic Strategy Selection
% 2.03/2.47
% 2.03/2.47 Clauses:
% 2.03/2.47 [
% 2.03/2.47 [ =( aux( X, Y, btrue ), nil2 ) ],
% 2.03/2.47 [ =( aux( X, Y, bfalse ), cons2( X, enumFromToNat( suc( X ), Y ) ) ) ]
% 2.03/2.47 ,
% 2.03/2.47 [ =( aux2( X, Y, Z, T, nothing ), cons3( bfalse, colouring( X, Y ) ) ) ]
% 2.03/2.47 ,
% 2.03/2.47 [ =( aux2( X, Y, Z, T, just( U ) ), cons3( notb( eq( T, U ) ), colouring(
% 2.03/2.47 X, Y ) ) ) ],
% 2.03/2.47 [ =( aux3( X, Y, Z, T, nothing ), cons3( bfalse, colouring( X, Y ) ) ) ]
% 2.03/2.47 ,
% 2.03/2.47 [ =( aux3( X, Y, Z, T, just( U ) ), aux2( X, Y, T, U, index( X, T ) ) )
% 2.03/2.47 ],
% 2.03/2.47 [ =( predNat( zero ), zero ) ],
% 2.03/2.47 [ =( predNat( suc( X ) ), X ) ],
% 2.03/2.47 [ =( one, suc( zero ) ) ],
% 2.03/2.47 [ =( two, suc( one ) ) ],
% 2.03/2.47 [ =( three, suc( two ) ) ],
% 2.03/2.47 [ =( notb( btrue ), bfalse ) ],
% 2.03/2.47 [ =( notb( bfalse ), btrue ) ],
% 2.03/2.47 [ =( lt( zero, zero ), bfalse ) ],
% 2.03/2.47 [ =( lt( zero, suc( X ) ), btrue ) ],
% 2.03/2.47 [ =( lt( suc( X ), zero ), bfalse ) ],
% 2.03/2.47 [ =( lt( suc( X ), suc( Y ) ), lt( X, Y ) ) ],
% 2.03/2.47 [ =( 'prop_d5'( nil2 ), nil3 ) ],
% 2.03/2.47 [ =( 'prop_d5'( cons2( X, Y ) ), cons3( lt( X, three ), 'prop_d5'( Y ) )
% 2.03/2.47 ) ],
% 2.03/2.47 [ =( index( nil2, X ), nothing ) ],
% 2.03/2.47 [ =( index( cons2( X, Y ), zero ), just( X ) ) ],
% 2.03/2.47 [ =( index( cons2( X, Y ), suc( Z ) ), index( Y, Z ) ) ],
% 2.03/2.47 [ =( four, suc( three ) ) ],
% 2.03/2.47 [ =( five, suc( four ) ) ],
% 2.03/2.47 [ =( enumFromToNat( X, Y ), aux( X, Y, lt( Y, X ) ) ) ],
% 2.03/2.47 [ =( dodeca( nil2 ), nil ) ],
% 2.03/2.47 [ =( dodeca( cons2( X, Y ) ), cons( pair2( X, suc( X ) ), dodeca( Y ) )
% 2.03/2.47 ) ],
% 2.03/2.47 [ =( colouring( X, nil ), nil3 ) ],
% 2.03/2.47 [ =( colouring( X, cons( pair2( Y, Z ), T ) ), aux3( X, T, Y, Z, index(
% 2.03/2.47 X, Y ) ) ) ],
% 2.03/2.47 [ =( append( nil, X ), X ) ],
% 2.03/2.47 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 2.03/2.47 [ =( andb( btrue, X ), X ) ],
% 2.03/2.47 [ =( andb( bfalse, X ), bfalse ) ],
% 2.03/2.47 [ =( and2( nil3 ), btrue ) ],
% 2.03/2.47 [ =( and2( cons3( X, Y ) ), andb( X, and2( Y ) ) ) ],
% 2.03/2.47 [ =( colouring2( X, Y ), and2( colouring( Y, X ) ) ) ],
% 2.03/2.47 [ =( add( zero, X ), X ) ],
% 2.03/2.47 [ =( add( suc( X ), Y ), suc( add( X, Y ) ) ) ],
% 2.03/2.47 [ =( dodeca2( X, nil2 ), nil ) ],
% 2.03/2.47 [ =( dodeca2( X, cons2( Y, Z ) ), cons( pair2( Y, add( suc( X ), Y ) ),
% 2.03/2.47 dodeca2( X, Z ) ) ) ],
% 2.03/2.47 [ =( dodeca3( X, nil2 ), nil ) ],
% 2.03/2.47 [ =( dodeca3( X, cons2( Y, Z ) ), cons( pair2( add( suc( X ), Y ), add(
% 2.03/2.47 add( suc( X ), suc( X ) ), Y ) ), dodeca3( X, Z ) ) ) ],
% 2.03/2.47 [ =( dodeca4( X, nil2 ), nil ) ],
% 2.03/2.47 [ =( dodeca4( X, cons2( Y, Z ) ), cons( pair2( add( suc( X ), suc( Y ) )
% 2.03/2.47 , add( add( suc( X ), suc( X ) ), Y ) ), dodeca4( X, Z ) ) ) ],
% 2.03/2.47 [ =( dodeca5( X, nil2 ), nil ) ],
% 2.03/2.47 [ =( dodeca5( X, cons2( Y, Z ) ), cons( pair2( add( add( suc( X ), suc(
% 2.03/2.47 X ) ), Y ), add( add( add( suc( X ), suc( X ) ), suc( X ) ), Y ) ),
% 2.03/2.47 dodeca5( X, Z ) ) ) ],
% 2.03/2.47 [ =( dodeca6( X, nil2 ), nil ) ],
% 2.03/2.47 [ =( dodeca6( X, cons2( Y, Z ) ), cons( pair2( add( add( add( suc( X ),
% 2.03/2.47 suc( X ) ), suc( X ) ), Y ), add( add( add( suc( X ), suc( X ) ), suc( X
% 2.03/2.47 ) ), suc( Y ) ) ), dodeca6( X, Z ) ) ) ],
% 2.03/2.47 [ =( dodeca7( zero ), nil ) ],
% 2.03/2.47 [ =( dodeca7( suc( X ) ), append( cons( pair2( X, zero ), dodeca(
% 2.03/2.47 enumFromToNat( zero, X ) ) ), append( dodeca2( X, enumFromToNat( zero,
% 2.03/2.47 suc( X ) ) ), append( dodeca3( X, enumFromToNat( zero, suc( X ) ) ),
% 2.03/2.47 append( cons( pair2( suc( X ), add( add( suc( X ), suc( X ) ), X ) ),
% 2.03/2.47 dodeca4( X, enumFromToNat( zero, X ) ) ), append( dodeca5( X,
% 2.03/2.47 enumFromToNat( zero, suc( X ) ) ), cons( pair2( add( add( add( suc( X ),
% 2.03/2.47 suc( X ) ), suc( X ) ), X ), add( add( add( suc( X ), suc( X ) ), suc( X
% 2.03/2.47 ) ), zero ) ), dodeca6( X, enumFromToNat( zero, X ) ) ) ) ) ) ) ) ) ]
% 2.03/2.47 ,
% 2.03/2.47 [ =( 'prop_d52'( X ), notb( andb( colouring2( dodeca7( five ), X ), and2(
% 2.03/2.47 'prop_d5'( X ) ) ) ) ) ],
% 2.03/2.47 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 2.03/2.47 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 2.03/2.47 [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ],
% 2.03/2.47 [ =( eq( zero, suc( X ) ), bfalse ) ],
% 2.03/2.47 [ =( eq( suc( X ), zero ), bfalse ) ],
% 2.03/2.47 [ =( eq( X, X ), btrue ) ],
% 2.03/2.47 [ =( eq2( X, X ), btrue ) ],
% 2.03/2.47 [ ~( =( eq2( 'prop_d52'( X ), bfalse ), btrue ) ) ]
% 2.03/2.47 ] .
% 2.03/2.47
% 2.03/2.47
% 2.03/2.47 percentage equality = 1.000000, percentage horn = 1.000000
% 48.94/49.30 This is a pure equality problem
% 48.94/49.30
% 48.94/49.30
% 48.94/49.30
% 48.94/49.30 Options Used:
% 48.94/49.30
% 48.94/49.30 useres = 1
% 48.94/49.30 useparamod = 1
% 48.94/49.30 useeqrefl = 1
% 48.94/49.30 useeqfact = 1
% 48.94/49.30 usefactor = 1
% 48.94/49.30 usesimpsplitting = 0
% 48.94/49.30 usesimpdemod = 5
% 48.94/49.30 usesimpres = 3
% 48.94/49.30
% 48.94/49.30 resimpinuse = 1000
% 48.94/49.30 resimpclauses = 20000
% 48.94/49.30 substype = eqrewr
% 48.94/49.30 backwardsubs = 1
% 48.94/49.30 selectoldest = 5
% 48.94/49.30
% 48.94/49.30 litorderings [0] = split
% 48.94/49.30 litorderings [1] = extend the termordering, first sorting on arguments
% 48.94/49.30
% 48.94/49.30 termordering = kbo
% 48.94/49.30
% 48.94/49.30 litapriori = 0
% 48.94/49.30 termapriori = 1
% 48.94/49.30 litaposteriori = 0
% 48.94/49.30 termaposteriori = 0
% 48.94/49.30 demodaposteriori = 0
% 48.94/49.30 ordereqreflfact = 0
% 48.94/49.30
% 48.94/49.30 litselect = negord
% 48.94/49.30
% 48.94/49.30 maxweight = 15
% 48.94/49.30 maxdepth = 30000
% 48.94/49.30 maxlength = 115
% 48.94/49.30 maxnrvars = 195
% 48.94/49.30 excuselevel = 1
% 48.94/49.30 increasemaxweight = 1
% 48.94/49.30
% 48.94/49.30 maxselected = 10000000
% 48.94/49.30 maxnrclauses = 10000000
% 48.94/49.30
% 48.94/49.30 showgenerated = 0
% 48.94/49.30 showkept = 0
% 48.94/49.30 showselected = 0
% 48.94/49.30 showdeleted = 0
% 48.94/49.30 showresimp = 1
% 48.94/49.30 showstatus = 2000
% 48.94/49.30
% 48.94/49.30 prologoutput = 1
% 48.94/49.30 nrgoals = 5000000
% 48.94/49.30 totalproof = 1
% 48.94/49.30
% 48.94/49.30 Symbols occurring in the translation:
% 48.94/49.30
% 48.94/49.30 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 48.94/49.30 . [1, 2] (w:1, o:48, a:1, s:1, b:0),
% 48.94/49.30 ! [4, 1] (w:0, o:34, a:1, s:1, b:0),
% 48.94/49.30 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 48.94/49.30 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 48.94/49.30 btrue [41, 0] (w:1, o:16, a:1, s:1, b:0),
% 48.94/49.30 aux [42, 3] (w:1, o:92, a:1, s:1, b:0),
% 48.94/49.30 nil2 [43, 0] (w:1, o:17, a:1, s:1, b:0),
% 48.94/49.30 bfalse [44, 0] (w:1, o:18, a:1, s:1, b:0),
% 48.94/49.30 suc [45, 1] (w:1, o:39, a:1, s:1, b:0),
% 48.94/49.30 enumFromToNat [46, 2] (w:1, o:78, a:1, s:1, b:0),
% 48.94/49.30 cons2 [47, 2] (w:1, o:79, a:1, s:1, b:0),
% 48.94/49.30 nothing [52, 0] (w:1, o:25, a:1, s:1, b:0),
% 48.94/49.30 aux2 [53, 5] (w:1, o:93, a:1, s:1, b:0),
% 48.94/49.30 colouring [54, 2] (w:1, o:80, a:1, s:1, b:0),
% 48.94/49.30 cons3 [55, 2] (w:1, o:81, a:1, s:1, b:0),
% 48.94/49.30 just [57, 1] (w:1, o:40, a:1, s:1, b:0),
% 48.94/49.30 eq [58, 2] (w:1, o:82, a:1, s:1, b:0),
% 48.94/49.30 notb [59, 1] (w:1, o:41, a:1, s:1, b:0),
% 48.94/49.30 aux3 [61, 5] (w:1, o:94, a:1, s:1, b:0),
% 48.94/49.30 index [62, 2] (w:1, o:83, a:1, s:1, b:0),
% 48.94/49.30 zero [63, 0] (w:1, o:27, a:1, s:1, b:0),
% 48.94/49.30 predNat [64, 1] (w:1, o:42, a:1, s:1, b:0),
% 48.94/49.30 one [65, 0] (w:1, o:9, a:1, s:1, b:0),
% 48.94/49.30 two [66, 0] (w:1, o:28, a:1, s:1, b:0),
% 48.94/49.30 three [67, 0] (w:1, o:29, a:1, s:1, b:0),
% 48.94/49.30 lt [68, 2] (w:1, o:84, a:1, s:1, b:0),
% 48.94/49.30 'prop_d5' [71, 1] (w:1, o:43, a:1, s:1, b:0),
% 48.94/49.30 nil3 [72, 0] (w:1, o:7, a:1, s:1, b:0),
% 48.94/49.30 four [74, 0] (w:1, o:31, a:1, s:1, b:0),
% 48.94/49.30 five [75, 0] (w:1, o:32, a:1, s:1, b:0),
% 48.94/49.30 dodeca [76, 1] (w:1, o:44, a:1, s:1, b:0),
% 48.94/49.30 nil [77, 0] (w:1, o:8, a:1, s:1, b:0),
% 48.94/49.30 pair2 [78, 2] (w:1, o:85, a:1, s:1, b:0),
% 48.94/49.30 cons [79, 2] (w:1, o:86, a:1, s:1, b:0),
% 48.94/49.30 append [80, 2] (w:1, o:87, a:1, s:1, b:0),
% 48.94/49.30 andb [83, 2] (w:1, o:88, a:1, s:1, b:0),
% 48.94/49.30 and2 [84, 1] (w:1, o:45, a:1, s:1, b:0),
% 48.94/49.30 colouring2 [85, 2] (w:1, o:89, a:1, s:1, b:0),
% 48.94/49.30 add [86, 2] (w:1, o:90, a:1, s:1, b:0),
% 48.94/49.30 dodeca2 [87, 2] (w:1, o:73, a:1, s:1, b:0),
% 48.94/49.30 dodeca3 [88, 2] (w:1, o:74, a:1, s:1, b:0),
% 48.94/49.30 dodeca4 [89, 2] (w:1, o:75, a:1, s:1, b:0),
% 48.94/49.30 dodeca5 [90, 2] (w:1, o:76, a:1, s:1, b:0),
% 48.94/49.30 dodeca6 [91, 2] (w:1, o:77, a:1, s:1, b:0),
% 48.94/49.30 dodeca7 [92, 1] (w:1, o:46, a:1, s:1, b:0),
% 48.94/49.30 'prop_d52' [93, 1] (w:1, o:47, a:1, s:1, b:0),
% 48.94/49.30 eq2 [94, 2] (w:1, o:91, a:1, s:1, b:0).
% 48.94/49.30
% 48.94/49.30
% 48.94/49.30 Starting Search:
% 48.94/49.30
% 48.94/49.30 Resimplifying inuse:
% 48.94/49.30 Done
% 48.94/49.30
% 48.94/49.30
% 48.94/49.30 Intermediate Status:
% 48.94/49.30 Generated: 11943
% 48.94/49.30 Kept: 2000
% 48.94/49.30 Inuse: 1187
% 48.94/49.30 Deleted: 153
% 48.94/49.30 Deletedinuse: 7
% 48.94/49.30
% 48.94/49.30 Resimplifying inuse:
% 48.94/49.30 Done
% 48.94/49.30
% 48.94/49.30 Resimplifying inuse:
% 48.94/49.30 Done
% 48.94/49.30
% 48.94/49.30
% 48.94/49.30 Intermediate Status:
% 48.94/49.30 Generated: 41718
% 48.94/49.30 Kept: 4000
% 48.94/49.30 Inuse: 2906
% 48.94/49.30 Deleted: 522
% 48.94/49.30 Deletedinuse: 31
% 48.94/49.30
% 48.94/49.30 Resimplifying inuse:
% 48.94/49.30 Done
% 48.94/49.30
% 48.94/49.30 Resimplifying inuse:
% 48.94/49.30 Done
% 48.94/49.30
% 48.94/49.30 Failed to find proof!
% 48.94/49.30 maxweight = 15
% 48.94/49.30 maxnrclauses = 10000000
% 48.94/49.30 Generated: 52755
% 48.94/49.30 Kept: 4166
% 48.94/49.30
% 48.94/49.30
% 48.94/49.30 The strategy used was not complete!
% 48.94/49.30
% 48.94/49.30 Increased maxweight to 16
% 48.94/49.30
% 48.94/49.30 Starting Search:
% 48.94/49.30
% 48.94/49.30 Resimplifying inuse:
% 48.94/49.30 Done
% 48.94/49.30
% 48.94/49.30
% 48.94/49.30 Intermediate Status:
% 48.94/49.30 Generated: 10649
% 186.02/186.42 Kept: 2000
% 186.02/186.42 Inuse: 1108
% 186.02/186.42 Deleted: 147
% 186.02/186.42 Deletedinuse: 9
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 33456
% 186.02/186.42 Kept: 4002
% 186.02/186.42 Inuse: 2466
% 186.02/186.42 Deleted: 367
% 186.02/186.42 Deletedinuse: 40
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Failed to find proof!
% 186.02/186.42 maxweight = 16
% 186.02/186.42 maxnrclauses = 10000000
% 186.02/186.42 Generated: 72984
% 186.02/186.42 Kept: 5092
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 The strategy used was not complete!
% 186.02/186.42
% 186.02/186.42 Increased maxweight to 17
% 186.02/186.42
% 186.02/186.42 Starting Search:
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 9408
% 186.02/186.42 Kept: 2003
% 186.02/186.42 Inuse: 994
% 186.02/186.42 Deleted: 106
% 186.02/186.42 Deletedinuse: 9
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 22303
% 186.02/186.42 Kept: 4018
% 186.02/186.42 Inuse: 2111
% 186.02/186.42 Deleted: 209
% 186.02/186.42 Deletedinuse: 19
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 31863
% 186.02/186.42 Kept: 6021
% 186.02/186.42 Inuse: 2885
% 186.02/186.42 Deleted: 321
% 186.02/186.42 Deletedinuse: 57
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 41964
% 186.02/186.42 Kept: 8021
% 186.02/186.42 Inuse: 3644
% 186.02/186.42 Deleted: 356
% 186.02/186.42 Deletedinuse: 64
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 53716
% 186.02/186.42 Kept: 10024
% 186.02/186.42 Inuse: 4649
% 186.02/186.42 Deleted: 470
% 186.02/186.42 Deletedinuse: 66
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 64349
% 186.02/186.42 Kept: 12069
% 186.02/186.42 Inuse: 5791
% 186.02/186.42 Deleted: 533
% 186.02/186.42 Deletedinuse: 68
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 71783
% 186.02/186.42 Kept: 14070
% 186.02/186.42 Inuse: 6291
% 186.02/186.42 Deleted: 633
% 186.02/186.42 Deletedinuse: 96
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 78179
% 186.02/186.42 Kept: 16076
% 186.02/186.42 Inuse: 6693
% 186.02/186.42 Deleted: 673
% 186.02/186.42 Deletedinuse: 96
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 103933
% 186.02/186.42 Kept: 18076
% 186.02/186.42 Inuse: 8492
% 186.02/186.42 Deleted: 917
% 186.02/186.42 Deletedinuse: 97
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying clauses:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 130459
% 186.02/186.42 Kept: 20082
% 186.02/186.42 Inuse: 10263
% 186.02/186.42 Deleted: 7098
% 186.02/186.42 Deletedinuse: 1811
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 147100
% 186.02/186.42 Kept: 22093
% 186.02/186.42 Inuse: 11422
% 186.02/186.42 Deleted: 7681
% 186.02/186.42 Deletedinuse: 2380
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 153208
% 186.02/186.42 Kept: 24094
% 186.02/186.42 Inuse: 12030
% 186.02/186.42 Deleted: 7681
% 186.02/186.42 Deletedinuse: 2380
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 202351
% 186.02/186.42 Kept: 26094
% 186.02/186.42 Inuse: 14898
% 186.02/186.42 Deleted: 7783
% 186.02/186.42 Deletedinuse: 2384
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 238736
% 186.02/186.42 Kept: 28098
% 186.02/186.42 Inuse: 16682
% 186.02/186.42 Deleted: 7980
% 186.02/186.42 Deletedinuse: 2509
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Failed to find proof!
% 186.02/186.42 maxweight = 17
% 186.02/186.42 maxnrclauses = 10000000
% 186.02/186.42 Generated: 362238
% 186.02/186.42 Kept: 29333
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 The strategy used was not complete!
% 186.02/186.42
% 186.02/186.42 Increased maxweight to 18
% 186.02/186.42
% 186.02/186.42 Starting Search:
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 9169
% 186.02/186.42 Kept: 2004
% 186.02/186.42 Inuse: 944
% 186.02/186.42 Deleted: 107
% 186.02/186.42 Deletedinuse: 7
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 21720
% 186.02/186.42 Kept: 4006
% 186.02/186.42 Inuse: 1975
% 186.02/186.42 Deleted: 220
% 186.02/186.42 Deletedinuse: 14
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 30589
% 186.02/186.42 Kept: 6008
% 186.02/186.42 Inuse: 2681
% 186.02/186.42 Deleted: 367
% 186.02/186.42 Deletedinuse: 55
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 39291
% 186.02/186.42 Kept: 8008
% 186.02/186.42 Inuse: 3464
% 186.02/186.42 Deleted: 457
% 186.02/186.42 Deletedinuse: 63
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 49500
% 186.02/186.42 Kept: 10008
% 186.02/186.42 Inuse: 4111
% 186.02/186.42 Deleted: 664
% 186.02/186.42 Deletedinuse: 241
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42 Resimplifying inuse:
% 186.02/186.42 Done
% 186.02/186.42
% 186.02/186.42
% 186.02/186.42 Intermediate Status:
% 186.02/186.42 Generated: 56935
% 186.02/186.42 Kept: 12009
% 265.83/266.22 Inuse: 4493
% 265.83/266.22 Deleted: 893
% 265.83/266.22 Deletedinuse: 353
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 65330
% 265.83/266.22 Kept: 14029
% 265.83/266.22 Inuse: 5129
% 265.83/266.22 Deleted: 946
% 265.83/266.22 Deletedinuse: 353
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 75753
% 265.83/266.22 Kept: 16046
% 265.83/266.22 Inuse: 6266
% 265.83/266.22 Deleted: 1002
% 265.83/266.22 Deletedinuse: 357
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 81829
% 265.83/266.22 Kept: 18049
% 265.83/266.22 Inuse: 6821
% 265.83/266.22 Deleted: 1028
% 265.83/266.22 Deletedinuse: 359
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying clauses:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 89297
% 265.83/266.22 Kept: 20096
% 265.83/266.22 Inuse: 7199
% 265.83/266.22 Deleted: 2923
% 265.83/266.22 Deletedinuse: 363
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 97650
% 265.83/266.22 Kept: 22103
% 265.83/266.22 Inuse: 7702
% 265.83/266.22 Deleted: 2933
% 265.83/266.22 Deletedinuse: 365
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 135278
% 265.83/266.22 Kept: 24111
% 265.83/266.22 Inuse: 9555
% 265.83/266.22 Deleted: 2988
% 265.83/266.22 Deletedinuse: 371
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 155922
% 265.83/266.22 Kept: 26113
% 265.83/266.22 Inuse: 10696
% 265.83/266.22 Deleted: 3259
% 265.83/266.22 Deletedinuse: 608
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 184108
% 265.83/266.22 Kept: 28123
% 265.83/266.22 Inuse: 12655
% 265.83/266.22 Deleted: 3926
% 265.83/266.22 Deletedinuse: 1116
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 207287
% 265.83/266.22 Kept: 30126
% 265.83/266.22 Inuse: 14194
% 265.83/266.22 Deleted: 4120
% 265.83/266.22 Deletedinuse: 1176
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 236513
% 265.83/266.22 Kept: 32131
% 265.83/266.22 Inuse: 15849
% 265.83/266.22 Deleted: 4318
% 265.83/266.22 Deletedinuse: 1256
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 245756
% 265.83/266.22 Kept: 34134
% 265.83/266.22 Inuse: 16811
% 265.83/266.22 Deleted: 5947
% 265.83/266.22 Deletedinuse: 2698
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 251837
% 265.83/266.22 Kept: 36142
% 265.83/266.22 Inuse: 17217
% 265.83/266.22 Deleted: 6057
% 265.83/266.22 Deletedinuse: 2698
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 269645
% 265.83/266.22 Kept: 38142
% 265.83/266.22 Inuse: 18291
% 265.83/266.22 Deleted: 6443
% 265.83/266.22 Deletedinuse: 2698
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying clauses:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 294314
% 265.83/266.22 Kept: 40160
% 265.83/266.22 Inuse: 20117
% 265.83/266.22 Deleted: 11863
% 265.83/266.22 Deletedinuse: 2701
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 338120
% 265.83/266.22 Kept: 42164
% 265.83/266.22 Inuse: 21928
% 265.83/266.22 Deleted: 14371
% 265.83/266.22 Deletedinuse: 5118
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 353151
% 265.83/266.22 Kept: 44165
% 265.83/266.22 Inuse: 22598
% 265.83/266.22 Deleted: 14509
% 265.83/266.22 Deletedinuse: 5180
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 393559
% 265.83/266.22 Kept: 46231
% 265.83/266.22 Inuse: 25092
% 265.83/266.22 Deleted: 14530
% 265.83/266.22 Deletedinuse: 5187
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 429503
% 265.83/266.22 Kept: 48237
% 265.83/266.22 Inuse: 27255
% 265.83/266.22 Deleted: 15220
% 265.83/266.22 Deletedinuse: 5592
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 479431
% 265.83/266.22 Kept: 50237
% 265.83/266.22 Inuse: 29324
% 265.83/266.22 Deleted: 15767
% 265.83/266.22 Deletedinuse: 5877
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 521083
% 265.83/266.22 Kept: 52239
% 265.83/266.22 Inuse: 31199
% 265.83/266.22 Deleted: 15835
% 265.83/266.22 Deletedinuse: 5879
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 561220
% 265.83/266.22 Kept: 54239
% 265.83/266.22 Inuse: 32414
% 265.83/266.22 Deleted: 16383
% 265.83/266.22 Deletedinuse: 6344
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 698929
% 265.83/266.22 Kept: 56240
% 265.83/266.22 Inuse: 38077
% 265.83/266.22 Deleted: 17649
% 265.83/266.22 Deletedinuse: 6617
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22 Resimplifying inuse:
% 265.83/266.22 Done
% 265.83/266.22
% 265.83/266.22
% 265.83/266.22 Intermediate Status:
% 265.83/266.22 Generated: 731959
% 265.83/266.22 Kept: Terminated
% 299.66/300.03 Bliksem ended
%------------------------------------------------------------------------------