%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX229-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:51 PM UTC 2026
% Result : Timeout 299.44s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX229-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.15/0.34 % Computer : n029.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:57:44 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 ), nil4 ) ],
% 0.71/1.11 [ =( aux2( X, Y, bfalse ), cons4( X, enumFromToNat( suc( X ), Y ) ) ) ]
% 0.71/1.11 ,
% 0.71/1.11 [ =( aux3( X, btrue ), cons6( o, bin( halfNat( suc( X ) ) ) ) ) ],
% 0.71/1.11 [ =( aux3( X, bfalse ), cons6( i, bin( halfNat( suc( X ) ) ) ) ) ],
% 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( nil5 ), bfalse ) ],
% 0.71/1.11 [ =( or2( cons5( 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, nil2 ), X ) ],
% 0.71/1.11 [ =( maximum( X, cons2( pair22( Y, Z ), T ) ), maximum( maxNat( X,
% 0.71/1.11 maxNat( Y, Z ) ), T ) ) ],
% 0.71/1.11 [ =( len( nil3 ), zero ) ],
% 0.71/1.11 [ =( len( cons3( X, Y ) ), suc( len( Y ) ) ) ],
% 0.71/1.11 [ =( last( X, nil3 ), X ) ],
% 0.71/1.11 [ =( last( X, cons3( Y, Z ) ), last( Y, Z ) ) ],
% 0.71/1.11 [ =( halfNat( zero ), zero ) ],
% 0.71/1.11 [ =( halfNat( suc( zero ) ), zero ) ],
% 0.71/1.11 [ =( halfNat( suc( suc( X ) ) ), suc( halfNat( X ) ) ) ],
% 0.71/1.11 [ =( evenNat( zero ), btrue ) ],
% 0.71/1.11 [ =( evenNat( suc( zero ) ), bfalse ) ],
% 0.71/1.11 [ =( evenNat( suc( suc( X ) ) ), evenNat( X ) ) ],
% 0.71/1.11 [ =( enumFromToNat( X, Y ), aux2( X, Y, lt( Y, X ) ) ) ],
% 0.71/1.11 [ =( dodeca( nil4 ), nil2 ) ],
% 0.71/1.11 [ =( dodeca( cons4( X, Y ) ), cons2( pair22( X, suc( X ) ), dodeca( Y )
% 0.71/1.11 ) ) ],
% 0.71/1.11 [ =( bin( zero ), nil6 ) ],
% 0.71/1.11 [ =( bin( suc( X ) ), aux3( X, evenNat( suc( X ) ) ) ) ],
% 0.71/1.11 [ =( bgraph( nil2 ), nil ) ],
% 0.71/1.11 [ =( bgraph( cons2( pair22( X, Y ), Z ) ), cons( pair2( bin( X ), bin( Y
% 0.71/1.11 ) ), bgraph( Z ) ) ) ],
% 0.71/1.11 [ =( beq( nil6, nil6 ), btrue ) ],
% 0.71/1.11 [ =( beq( nil6, cons6( X, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( beq( cons6( i, X ), nil6 ), bfalse ) ],
% 0.71/1.11 [ =( beq( cons6( i, X ), cons6( i, Y ) ), beq( X, Y ) ) ],
% 0.71/1.11 [ =( beq( cons6( i, X ), cons6( o, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( beq( cons6( o, X ), nil6 ), bfalse ) ],
% 0.71/1.11 [ =( beq( cons6( o, X ), cons6( i, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( beq( cons6( o, X ), cons6( o, Y ) ), beq( X, Y ) ) ],
% 0.71/1.11 [ =( belem( X, nil3 ), nil5 ) ],
% 0.71/1.11 [ =( belem( X, cons3( Y, Z ) ), cons5( beq( X, Y ), belem( X, Z ) ) ) ]
% 0.71/1.11 ,
% 0.71/1.11 [ =( belem2( X, Y ), or2( belem( X, Y ) ) ) ],
% 0.71/1.11 [ =( append( nil2, X ), X ) ],
% 0.71/1.11 [ =( append( cons2( X, Y ), Z ), cons2( X, append( Y, Z ) ) ) ],
% 0.71/1.11 [ =( andb( btrue, X ), X ) ],
% 0.71/1.11 [ =( andb( bfalse, X ), bfalse ) ],
% 0.71/1.11 [ =( bpath( X, Y, nil ), nil5 ) ],
% 0.71/1.11 [ =( bpath( X, Y, cons( pair2( Z, T ), U ) ), cons5( orb( andb( beq( Z,
% 0.71/1.11 X ), beq( T, Y ) ), andb( beq( Z, Y ), beq( T, X ) ) ), bpath( X, Y, U )
% 0.71/1.11 ) ) ],
% 0.71/1.11 [ =( bpath2( nil3, X ), btrue ) ],
% 0.71/1.11 [ =( bpath2( cons3( X, nil3 ), Y ), btrue ) ],
% 0.71/1.11 [ =( bpath2( cons3( X, cons3( Y, Z ) ), T ), andb( or2( bpath( X, Y, T )
% 0.71/1.11 ), bpath2( cons3( Y, Z ), T ) ) ) ],
% 0.71/1.11 [ =( bunique( nil3 ), btrue ) ],
% 0.71/1.11 [ =( bunique( cons3( X, Y ) ), andb( notb( belem2( X, Y ) ), bunique( Y
% 0.71/1.11 ) ) ) ],
% 0.71/1.11 [ =( add( zero, X ), X ) ],
% 0.71/1.11 [ =( add( suc( X ), Y ), suc( add( X, Y ) ) ) ],
% 0.71/1.11 [ =( btour( nil3, nil2 ), btrue ) ],
% 0.71/1.11 [ =( btour( nil3, cons2( X, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( btour( cons3( X, Y ), nil2 ), bfalse ) ],
% 0.71/1.11 [ =( btour( cons3( X, Y ), cons2( pair22( Z, T ), U ) ), andb( beq( X,
% 0.71/1.11 last( X, Y ) ), andb( bpath2( cons3( X, Y ), bgraph( cons2( pair22( Z, T
% 0.71/1.11 ), U ) ) ), andb( bunique( Y ), eq( len( cons3( X, Y ) ), add( two,
% 0.71/1.11 maximum( maxNat( Z, T ), U ) ) ) ) ) ) ) ],
% 0.71/1.11 [ =( dodeca2( X, nil4 ), nil2 ) ],
% 0.71/1.11 [ =( dodeca2( X, cons4( Y, Z ) ), cons2( pair22( Y, add( suc( X ), Y ) )
% 0.71/1.11 , dodeca2( X, Z ) ) ) ],
% 0.71/1.11 [ =( dodeca3( X, nil4 ), nil2 ) ],
% 0.71/1.11 [ =( dodeca3( X, cons4( Y, Z ) ), cons2( pair22( add( suc( X ), Y ), add(
% 5.65/6.06 add( suc( X ), suc( X ) ), Y ) ), dodeca3( X, Z ) ) ) ],
% 5.65/6.06 [ =( dodeca4( X, nil4 ), nil2 ) ],
% 5.65/6.06 [ =( dodeca4( X, cons4( Y, Z ) ), cons2( pair22( add( suc( X ), suc( Y )
% 5.65/6.06 ), add( add( suc( X ), suc( X ) ), Y ) ), dodeca4( X, Z ) ) ) ],
% 5.65/6.06 [ =( dodeca5( X, nil4 ), nil2 ) ],
% 5.65/6.06 [ =( dodeca5( X, cons4( Y, Z ) ), cons2( pair22( add( add( suc( X ), suc(
% 5.65/6.06 X ) ), Y ), add( add( add( suc( X ), suc( X ) ), suc( X ) ), Y ) ),
% 5.65/6.06 dodeca5( X, Z ) ) ) ],
% 5.65/6.06 [ =( dodeca6( X, nil4 ), nil2 ) ],
% 5.65/6.06 [ =( dodeca6( X, cons4( Y, Z ) ), cons2( pair22( add( add( add( suc( X )
% 5.65/6.06 , suc( X ) ), suc( X ) ), Y ), add( add( add( suc( X ), suc( X ) ), suc(
% 5.65/6.06 X ) ), suc( Y ) ) ), dodeca6( X, Z ) ) ) ],
% 5.65/6.06 [ =( dodeca7( zero ), nil2 ) ],
% 5.65/6.06 [ =( dodeca7( suc( X ) ), append( cons2( pair22( X, zero ), dodeca(
% 5.65/6.06 enumFromToNat( zero, X ) ) ), append( dodeca2( X, enumFromToNat( zero,
% 5.65/6.06 suc( X ) ) ), append( dodeca3( X, enumFromToNat( zero, suc( X ) ) ),
% 5.65/6.06 append( cons2( pair22( suc( X ), add( add( suc( X ), suc( X ) ), X ) ),
% 5.65/6.06 dodeca4( X, enumFromToNat( zero, X ) ) ), append( dodeca5( X,
% 5.65/6.06 enumFromToNat( zero, suc( X ) ) ), cons2( pair22( add( add( add( suc( X )
% 5.65/6.06 , suc( X ) ), suc( X ) ), X ), add( add( add( suc( X ), suc( X ) ), suc(
% 5.65/6.06 X ) ), zero ) ), dodeca6( X, enumFromToNat( zero, X ) ) ) ) ) ) ) ) ) ]
% 5.65/6.06 ,
% 5.65/6.06 [ =( 'prop_bt3'( X ), notb( btour( X, dodeca7( three ) ) ) ) ],
% 5.65/6.06 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 5.65/6.06 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 5.65/6.06 [ =( eq3( i, o ), bfalse ) ],
% 5.65/6.06 [ =( eq3( o, i ), bfalse ) ],
% 5.65/6.06 [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ],
% 5.65/6.06 [ =( eq( zero, suc( X ) ), bfalse ) ],
% 5.65/6.06 [ =( eq( suc( X ), zero ), bfalse ) ],
% 5.65/6.06 [ =( eq( X, X ), btrue ) ],
% 5.65/6.06 [ =( eq2( X, X ), btrue ) ],
% 5.65/6.06 [ =( eq3( X, X ), btrue ) ],
% 5.65/6.06 [ ~( =( eq2( 'prop_bt3'( X ), bfalse ), btrue ) ) ]
% 5.65/6.06 ] .
% 5.65/6.06
% 5.65/6.06
% 5.65/6.06 percentage equality = 1.000000, percentage horn = 1.000000
% 5.65/6.06 This is a pure equality problem
% 5.65/6.06
% 5.65/6.06
% 5.65/6.06
% 5.65/6.06 Options Used:
% 5.65/6.06
% 5.65/6.06 useres = 1
% 5.65/6.06 useparamod = 1
% 5.65/6.06 useeqrefl = 1
% 5.65/6.06 useeqfact = 1
% 5.65/6.06 usefactor = 1
% 5.65/6.06 usesimpsplitting = 0
% 5.65/6.06 usesimpdemod = 5
% 5.65/6.06 usesimpres = 3
% 5.65/6.06
% 5.65/6.06 resimpinuse = 1000
% 5.65/6.06 resimpclauses = 20000
% 5.65/6.06 substype = eqrewr
% 5.65/6.06 backwardsubs = 1
% 5.65/6.06 selectoldest = 5
% 5.65/6.06
% 5.65/6.06 litorderings [0] = split
% 5.65/6.06 litorderings [1] = extend the termordering, first sorting on arguments
% 5.65/6.06
% 5.65/6.06 termordering = kbo
% 5.65/6.06
% 5.65/6.06 litapriori = 0
% 5.65/6.06 termapriori = 1
% 5.65/6.06 litaposteriori = 0
% 5.65/6.06 termaposteriori = 0
% 5.65/6.06 demodaposteriori = 0
% 5.65/6.06 ordereqreflfact = 0
% 5.65/6.06
% 5.65/6.06 litselect = negord
% 5.65/6.06
% 5.65/6.06 maxweight = 15
% 5.65/6.06 maxdepth = 30000
% 5.65/6.06 maxlength = 115
% 5.65/6.06 maxnrvars = 195
% 5.65/6.06 excuselevel = 1
% 5.65/6.06 increasemaxweight = 1
% 5.65/6.06
% 5.65/6.06 maxselected = 10000000
% 5.65/6.06 maxnrclauses = 10000000
% 5.65/6.06
% 5.65/6.06 showgenerated = 0
% 5.65/6.06 showkept = 0
% 5.65/6.06 showselected = 0
% 5.65/6.06 showdeleted = 0
% 5.65/6.06 showresimp = 1
% 5.65/6.06 showstatus = 2000
% 5.65/6.06
% 5.65/6.06 prologoutput = 1
% 5.65/6.06 nrgoals = 5000000
% 5.65/6.06 totalproof = 1
% 5.65/6.06
% 5.65/6.06 Symbols occurring in the translation:
% 5.65/6.06
% 5.65/6.06 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 5.65/6.06 . [1, 2] (w:1, o:58, a:1, s:1, b:0),
% 5.65/6.06 ! [4, 1] (w:0, o:40, a:1, s:1, b:0),
% 5.65/6.06 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.65/6.06 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.65/6.06 btrue [41, 0] (w:1, o:22, a:1, s:1, b:0),
% 5.65/6.06 aux [42, 3] (w:1, o:114, a:1, s:1, b:0),
% 5.65/6.06 bfalse [43, 0] (w:1, o:23, a:1, s:1, b:0),
% 5.65/6.06 aux2 [44, 3] (w:1, o:115, a:1, s:1, b:0),
% 5.65/6.06 nil4 [45, 0] (w:1, o:24, a:1, s:1, b:0),
% 5.65/6.06 suc [46, 1] (w:1, o:45, a:1, s:1, b:0),
% 5.65/6.06 enumFromToNat [47, 2] (w:1, o:88, a:1, s:1, b:0),
% 5.65/6.06 cons4 [48, 2] (w:1, o:98, a:1, s:1, b:0),
% 5.65/6.06 aux3 [49, 2] (w:1, o:99, a:1, s:1, b:0),
% 5.65/6.06 o [50, 0] (w:1, o:12, a:1, s:1, b:0),
% 5.65/6.06 halfNat [51, 1] (w:1, o:46, a:1, s:1, b:0),
% 5.65/6.06 bin [52, 1] (w:1, o:47, a:1, s:1, b:0),
% 5.65/6.06 cons6 [53, 2] (w:1, o:101, a:1, s:1, b:0),
% 5.65/6.06 i [54, 0] (w:1, o:25, a:1, s:1, b:0),
% 5.65/6.06 zero [55, 0] (w:1, o:26, a:1, s:1, b:0),
% 5.65/6.06 predNat [56, 1] (w:1, o:50, a:1, s:1, b:0),
% 5.65/6.06 orb [58, 2] (w:1, o:102, a:1, s:1, b:0),
% 5.65/6.06 nil5 [59, 0] (w:1, o:7, a:1, s:1, b:0),
% 49.65/50.07 or2 [60, 1] (w:1, o:49, a:1, s:1, b:0),
% 49.65/50.07 cons5 [62, 2] (w:1, o:100, a:1, s:1, b:0),
% 49.65/50.07 one [63, 0] (w:1, o:13, a:1, s:1, b:0),
% 49.65/50.07 two [64, 0] (w:1, o:28, a:1, s:1, b:0),
% 49.65/50.07 three [65, 0] (w:1, o:29, a:1, s:1, b:0),
% 49.65/50.07 notb [66, 1] (w:1, o:48, a:1, s:1, b:0),
% 49.65/50.07 lt [67, 2] (w:1, o:103, a:1, s:1, b:0),
% 49.65/50.07 maxNat [71, 2] (w:1, o:105, a:1, s:1, b:0),
% 49.65/50.07 nil2 [72, 0] (w:1, o:8, a:1, s:1, b:0),
% 49.65/50.07 maximum [73, 2] (w:1, o:106, a:1, s:1, b:0),
% 49.65/50.07 pair22 [75, 2] (w:1, o:107, a:1, s:1, b:0),
% 49.65/50.07 cons2 [77, 2] (w:1, o:108, a:1, s:1, b:0),
% 49.65/50.07 nil3 [78, 0] (w:1, o:9, a:1, s:1, b:0),
% 49.65/50.07 len [79, 1] (w:1, o:51, a:1, s:1, b:0),
% 49.65/50.07 cons3 [80, 2] (w:1, o:97, a:1, s:1, b:0),
% 49.65/50.07 last [81, 2] (w:1, o:104, a:1, s:1, b:0),
% 49.65/50.07 evenNat [84, 1] (w:1, o:54, a:1, s:1, b:0),
% 49.65/50.07 dodeca [85, 1] (w:1, o:52, a:1, s:1, b:0),
% 49.65/50.07 nil6 [86, 0] (w:1, o:10, a:1, s:1, b:0),
% 49.65/50.07 bgraph [87, 1] (w:1, o:55, a:1, s:1, b:0),
% 49.65/50.07 nil [88, 0] (w:1, o:11, a:1, s:1, b:0),
% 49.65/50.07 pair2 [91, 2] (w:1, o:109, a:1, s:1, b:0),
% 49.65/50.07 cons [92, 2] (w:1, o:110, a:1, s:1, b:0),
% 49.65/50.07 beq [93, 2] (w:1, o:92, a:1, s:1, b:0),
% 49.65/50.07 belem [95, 2] (w:1, o:93, a:1, s:1, b:0),
% 49.65/50.07 belem2 [96, 2] (w:1, o:94, a:1, s:1, b:0),
% 49.65/50.07 append [97, 2] (w:1, o:89, a:1, s:1, b:0),
% 49.65/50.07 andb [98, 2] (w:1, o:90, a:1, s:1, b:0),
% 49.65/50.07 bpath [99, 3] (w:1, o:116, a:1, s:1, b:0),
% 49.65/50.07 bpath2 [101, 2] (w:1, o:95, a:1, s:1, b:0),
% 49.65/50.07 bunique [102, 1] (w:1, o:56, a:1, s:1, b:0),
% 49.65/50.07 add [103, 2] (w:1, o:91, a:1, s:1, b:0),
% 49.65/50.07 btour [104, 2] (w:1, o:96, a:1, s:1, b:0),
% 49.65/50.07 eq [107, 2] (w:1, o:111, a:1, s:1, b:0),
% 49.65/50.07 dodeca2 [108, 2] (w:1, o:83, a:1, s:1, b:0),
% 49.65/50.07 dodeca3 [109, 2] (w:1, o:84, a:1, s:1, b:0),
% 49.65/50.07 dodeca4 [110, 2] (w:1, o:85, a:1, s:1, b:0),
% 49.65/50.07 dodeca5 [111, 2] (w:1, o:86, a:1, s:1, b:0),
% 49.65/50.07 dodeca6 [112, 2] (w:1, o:87, a:1, s:1, b:0),
% 49.65/50.07 dodeca7 [113, 1] (w:1, o:53, a:1, s:1, b:0),
% 49.65/50.07 'prop_bt3' [114, 1] (w:1, o:57, a:1, s:1, b:0),
% 49.65/50.07 eq2 [115, 2] (w:1, o:112, a:1, s:1, b:0),
% 49.65/50.07 eq3 [116, 2] (w:1, o:113, a:1, s:1, b:0).
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 Starting Search:
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 Intermediate Status:
% 49.65/50.07 Generated: 18885
% 49.65/50.07 Kept: 2000
% 49.65/50.07 Inuse: 1624
% 49.65/50.07 Deleted: 164
% 49.65/50.07 Deletedinuse: 5
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Failed to find proof!
% 49.65/50.07 maxweight = 15
% 49.65/50.07 maxnrclauses = 10000000
% 49.65/50.07 Generated: 21612
% 49.65/50.07 Kept: 2113
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 The strategy used was not complete!
% 49.65/50.07
% 49.65/50.07 Increased maxweight to 16
% 49.65/50.07
% 49.65/50.07 Starting Search:
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 Intermediate Status:
% 49.65/50.07 Generated: 17080
% 49.65/50.07 Kept: 2001
% 49.65/50.07 Inuse: 1452
% 49.65/50.07 Deleted: 126
% 49.65/50.07 Deletedinuse: 5
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Failed to find proof!
% 49.65/50.07 maxweight = 16
% 49.65/50.07 maxnrclauses = 10000000
% 49.65/50.07 Generated: 26845
% 49.65/50.07 Kept: 2604
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 The strategy used was not complete!
% 49.65/50.07
% 49.65/50.07 Increased maxweight to 17
% 49.65/50.07
% 49.65/50.07 Starting Search:
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 Intermediate Status:
% 49.65/50.07 Generated: 14909
% 49.65/50.07 Kept: 2008
% 49.65/50.07 Inuse: 1245
% 49.65/50.07 Deleted: 116
% 49.65/50.07 Deletedinuse: 4
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Failed to find proof!
% 49.65/50.07 maxweight = 17
% 49.65/50.07 maxnrclauses = 10000000
% 49.65/50.07 Generated: 43231
% 49.65/50.07 Kept: 3822
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 The strategy used was not complete!
% 49.65/50.07
% 49.65/50.07 Increased maxweight to 18
% 49.65/50.07
% 49.65/50.07 Starting Search:
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 Intermediate Status:
% 49.65/50.07 Generated: 13299
% 49.65/50.07 Kept: 2000
% 49.65/50.07 Inuse: 1135
% 49.65/50.07 Deleted: 105
% 49.65/50.07 Deletedinuse: 4
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 Intermediate Status:
% 49.65/50.07 Generated: 32160
% 49.65/50.07 Kept: 4001
% 49.65/50.07 Inuse: 2575
% 49.65/50.07 Deleted: 454
% 49.65/50.07 Deletedinuse: 134
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07 Failed to find proof!
% 49.65/50.07 maxweight = 18
% 49.65/50.07 maxnrclauses = 10000000
% 49.65/50.07 Generated: 71599
% 49.65/50.07 Kept: 5901
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 The strategy used was not complete!
% 49.65/50.07
% 49.65/50.07 Increased maxweight to 19
% 49.65/50.07
% 49.65/50.07 Starting Search:
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 49.65/50.07 Done
% 49.65/50.07
% 49.65/50.07
% 49.65/50.07 Intermediate Status:
% 49.65/50.07 Generated: 12693
% 49.65/50.07 Kept: 2001
% 49.65/50.07 Inuse: 1076
% 49.65/50.07 Deleted: 94
% 49.65/50.07 Deletedinuse: 4
% 49.65/50.07
% 49.65/50.07 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 29193
% 182.14/182.77 Kept: 4004
% 182.14/182.77 Inuse: 2322
% 182.14/182.77 Deleted: 416
% 182.14/182.77 Deletedinuse: 98
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 47222
% 182.14/182.77 Kept: 6009
% 182.14/182.77 Inuse: 3491
% 182.14/182.77 Deleted: 705
% 182.14/182.77 Deletedinuse: 184
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 81462
% 182.14/182.77 Kept: 8009
% 182.14/182.77 Inuse: 5154
% 182.14/182.77 Deleted: 1266
% 182.14/182.77 Deletedinuse: 327
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Failed to find proof!
% 182.14/182.77 maxweight = 19
% 182.14/182.77 maxnrclauses = 10000000
% 182.14/182.77 Generated: 185665
% 182.14/182.77 Kept: 9686
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 The strategy used was not complete!
% 182.14/182.77
% 182.14/182.77 Increased maxweight to 20
% 182.14/182.77
% 182.14/182.77 Starting Search:
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 11593
% 182.14/182.77 Kept: 2007
% 182.14/182.77 Inuse: 953
% 182.14/182.77 Deleted: 73
% 182.14/182.77 Deletedinuse: 4
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 25998
% 182.14/182.77 Kept: 4009
% 182.14/182.77 Inuse: 2021
% 182.14/182.77 Deleted: 355
% 182.14/182.77 Deletedinuse: 99
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 41695
% 182.14/182.77 Kept: 6010
% 182.14/182.77 Inuse: 3160
% 182.14/182.77 Deleted: 578
% 182.14/182.77 Deletedinuse: 143
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 56022
% 182.14/182.77 Kept: 8019
% 182.14/182.77 Inuse: 4028
% 182.14/182.77 Deleted: 863
% 182.14/182.77 Deletedinuse: 220
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 87443
% 182.14/182.77 Kept: 10024
% 182.14/182.77 Inuse: 5537
% 182.14/182.77 Deleted: 1361
% 182.14/182.77 Deletedinuse: 280
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 128441
% 182.14/182.77 Kept: 12025
% 182.14/182.77 Inuse: 7295
% 182.14/182.77 Deleted: 1954
% 182.14/182.77 Deletedinuse: 393
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 232249
% 182.14/182.77 Kept: 14025
% 182.14/182.77 Inuse: 9427
% 182.14/182.77 Deleted: 2706
% 182.14/182.77 Deletedinuse: 579
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Failed to find proof!
% 182.14/182.77 maxweight = 20
% 182.14/182.77 maxnrclauses = 10000000
% 182.14/182.77 Generated: 328958
% 182.14/182.77 Kept: 15417
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 The strategy used was not complete!
% 182.14/182.77
% 182.14/182.77 Increased maxweight to 21
% 182.14/182.77
% 182.14/182.77 Starting Search:
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 10688
% 182.14/182.77 Kept: 2000
% 182.14/182.77 Inuse: 876
% 182.14/182.77 Deleted: 74
% 182.14/182.77 Deletedinuse: 4
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 23332
% 182.14/182.77 Kept: 4000
% 182.14/182.77 Inuse: 1874
% 182.14/182.77 Deleted: 315
% 182.14/182.77 Deletedinuse: 100
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 34501
% 182.14/182.77 Kept: 6004
% 182.14/182.77 Inuse: 2651
% 182.14/182.77 Deleted: 494
% 182.14/182.77 Deletedinuse: 145
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 49174
% 182.14/182.77 Kept: 8004
% 182.14/182.77 Inuse: 3685
% 182.14/182.77 Deleted: 822
% 182.14/182.77 Deletedinuse: 194
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 64473
% 182.14/182.77 Kept: 10005
% 182.14/182.77 Inuse: 4464
% 182.14/182.77 Deleted: 1051
% 182.14/182.77 Deletedinuse: 280
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 87658
% 182.14/182.77 Kept: 12027
% 182.14/182.77 Inuse: 5519
% 182.14/182.77 Deleted: 1405
% 182.14/182.77 Deletedinuse: 316
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 124043
% 182.14/182.77 Kept: 14027
% 182.14/182.77 Inuse: 6926
% 182.14/182.77 Deleted: 1912
% 182.14/182.77 Deletedinuse: 418
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 151853
% 182.14/182.77 Kept: 16027
% 182.14/182.77 Inuse: 8121
% 182.14/182.77 Deleted: 2314
% 182.14/182.77 Deletedinuse: 495
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 236371
% 182.14/182.77 Kept: 18027
% 182.14/182.77 Inuse: 9490
% 182.14/182.77 Deleted: 2925
% 182.14/182.77 Deletedinuse: 629
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying clauses:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 300700
% 182.14/182.77 Kept: 20144
% 182.14/182.77 Inuse: 11515
% 182.14/182.77 Deleted: 5657
% 182.14/182.77 Deletedinuse: 844
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77 Resimplifying inuse:
% 182.14/182.77 Done
% 182.14/182.77
% 182.14/182.77
% 182.14/182.77 Intermediate Status:
% 182.14/182.77 Generated: 359863
% 182.14/182.77 Kept: 22150
% 182.14/182.77 Inuse: 13019
% 182.14/182.77 Deleted: Terminated
% 299.44/300.03 Bliksem ended
%------------------------------------------------------------------------------