%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX218-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n021.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:50 PM UTC 2026
% Result : Timeout 299.33s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX218-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.12 % Command : bliksem %s
% 0.16/0.33 % Computer : n021.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % DateTime : Tue May 5 12:19:55 EDT 2026
% 0.16/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, Z, T, btrue ), T ) ],
% 0.71/1.11 [ =( aux( X, Y, Z, T, bfalse ), apply( Y, X ) ) ],
% 0.71/1.11 [ =( aux2( X, Y, Z, T, pair23( U, W ) ), right( tuple2( T, W, cons2( U,
% 0.71/1.11 cons2( Y, Z ) ) ) ) ) ],
% 0.71/1.11 [ =( aux3( X, Y, Z, T, U, pair24( W, V0 ) ), act( V0, Z, W, U ) ) ],
% 0.71/1.11 [ =( aux4( X, Y, Z, T, pair23( U, W ) ), aux3( X, Y, Z, U, W, apply( X,
% 0.71/1.11 pair22( Y, U ) ) ) ) ],
% 0.71/1.11 [ =( aux5( X, Y, left( Z ) ), Z ) ],
% 0.71/1.11 [ =( aux5( X, Y, right( Z ) ), steps( X, Z ) ) ],
% 0.71/1.11 [ =( aux6( X, nil2 ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, nil2 ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, nil2 ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, nil2 ) ) ) ), bfalse ) ]
% 0.71/1.11 ,
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( a2, nil2 ) ) ) ) )
% 0.71/1.11 , bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2
% 0.71/1.11 ) ) ) ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b,
% 0.71/1.11 cons2( b, nil2 ) ) ) ) ) ) ), btrue ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b,
% 0.71/1.11 cons2( b, cons2( Y, Z ) ) ) ) ) ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b,
% 0.71/1.11 cons2( o, Y ) ) ) ) ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( b,
% 0.71/1.11 cons2( a2, Y ) ) ) ) ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( o, Y )
% 0.71/1.11 ) ) ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( a2, cons2( a2, Y )
% 0.71/1.11 ) ) ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( o, Y ) ) ) ) ),
% 0.71/1.11 bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( a2, cons2( b, Y ) ) ) ) ),
% 0.71/1.11 bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( o, Y ) ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( a2, cons2( b, Y ) ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( o, Y ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( a2, cons2( b, Y ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( o, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( aux6( X, cons2( b, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( aux7( X, nil2 ), bfalse ) ],
% 0.71/1.11 [ =( aux7( X, cons2( a2, nil2 ) ), aux6( X, runt( X, cons2( b, cons2( a2
% 0.71/1.11 , cons2( a2, cons2( a2, cons2( a2, cons2( b, nil2 ) ) ) ) ) ) ) ) ) ]
% 0.71/1.11 ,
% 0.71/1.11 [ =( aux7( X, cons2( a2, cons2( Y, Z ) ) ), bfalse ) ],
% 0.71/1.11 [ =( aux7( X, cons2( o, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( aux7( X, cons2( b, Y ) ), bfalse ) ],
% 0.71/1.11 [ =( split( nil2 ), pair23( o, nil2 ) ) ],
% 0.71/1.11 [ =( split( cons2( X, Y ) ), pair23( X, Y ) ) ],
% 0.71/1.11 [ =( rev( nil2, X ), X ) ],
% 0.71/1.11 [ =( rev( cons2( o, X ), Y ), Y ) ],
% 0.71/1.11 [ =( rev( cons2( a2, X ), Y ), rev( X, cons2( a2, Y ) ) ) ],
% 0.71/1.11 [ =( rev( cons2( b, X ), Y ), rev( X, cons2( b, Y ) ) ) ],
% 0.71/1.11 [ =( one, succ( zero ) ) ],
% 0.71/1.11 [ =( two, succ( one ) ) ],
% 0.71/1.11 [ =( apply( nil, X ), pair24( o, stp ) ) ],
% 0.71/1.11 [ =( apply( cons( pair2( X, Y ), Z ), T ), aux( T, Z, X, Y, eq( X, T ) )
% 0.71/1.11 ) ],
% 0.71/1.11 [ =( act( lft( X ), Y, Z, T ), aux2( Y, Z, T, X, split( Y ) ) ) ],
% 0.71/1.11 [ =( act( rgt( X ), Y, Z, T ), right( tuple2( X, cons2( Z, Y ), T ) ) )
% 0.71/1.11 ],
% 0.71/1.11 [ =( act( stp, X, Y, Z ), left( rev( X, cons2( Y, Z ) ) ) ) ],
% 0.71/1.11 [ =( step( X, tuple2( Y, Z, T ) ), aux4( X, Y, Z, T, split( T ) ) ) ]
% 0.71/1.11 ,
% 0.71/1.11 [ =( steps( X, Y ), aux5( X, Y, step( X, Y ) ) ) ],
% 0.71/1.11 [ =( runt( X, Y ), steps( X, tuple2( zero, nil2, Y ) ) ) ],
% 0.71/1.11 [ =( prog0( X ), aux7( X, runt( X, cons2( a2, nil2 ) ) ) ) ],
% 0.71/1.11 [ =( 'prop_help'( X, Y, Z, T, U ), eq3( prog0( cons( pair2( pair22( zero
% 0.71/1.11 , a2 ), X ), cons( pair2( pair22( zero, b ), Y ), cons( pair2( pair22(
% 0.71/1.11 one, a2 ), Z ), cons( pair2( pair22( one, b ), T ), cons( pair2( pair22(
% 0.71/1.11 two, a2 ), U ), nil ) ) ) ) ) ), bfalse ) ) ],
% 0.71/1.11 [ =( eq3( bfalse, btrue ), bfalse ) ],
% 0.71/1.11 [ =( eq3( btrue, bfalse ), bfalse ) ],
% 0.71/1.11 [ =( eq5( o, a2 ), bfalse ) ],
% 0.71/1.11 [ =( eq5( o, b ), bfalse ) ],
% 0.71/1.11 [ =( eq5( a2, o ), bfalse ) ],
% 0.71/1.11 [ =( eq5( a2, b ), bfalse ) ],
% 0.71/1.11 [ =( eq5( b, o ), bfalse ) ],
% 2.51/2.95 [ =( eq5( b, a2 ), bfalse ) ],
% 2.51/2.95 [ =( eq2( succ( X ), succ( Y ) ), eq2( X, Y ) ) ],
% 2.51/2.95 [ =( eq2( zero, succ( X ) ), bfalse ) ],
% 2.51/2.95 [ =( eq2( succ( X ), zero ), bfalse ) ],
% 2.51/2.95 [ =( eq4( lft( X ), lft( Y ) ), eq2( X, Y ) ) ],
% 2.51/2.95 [ =( eq4( rgt( X ), rgt( Y ) ), eq2( X, Y ) ) ],
% 2.51/2.95 [ =( eq4( lft( X ), rgt( Y ) ), bfalse ) ],
% 2.51/2.95 [ =( eq4( lft( X ), stp ), bfalse ) ],
% 2.51/2.95 [ =( eq4( rgt( X ), lft( Y ) ), bfalse ) ],
% 2.51/2.95 [ =( eq4( rgt( X ), stp ), bfalse ) ],
% 2.51/2.95 [ =( eq4( stp, lft( X ) ), bfalse ) ],
% 2.51/2.95 [ =( eq4( stp, rgt( X ) ), bfalse ) ],
% 2.51/2.95 [ =( eq( X, X ), btrue ) ],
% 2.51/2.95 [ =( eq2( X, X ), btrue ) ],
% 2.51/2.95 [ =( eq3( X, X ), btrue ) ],
% 2.51/2.95 [ =( eq4( X, X ), btrue ) ],
% 2.51/2.95 [ =( eq5( X, X ), btrue ) ],
% 2.51/2.95 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq( pair22( X, Z ), pair22( Y, T ) )
% 2.51/2.95 , bfalse ) ],
% 2.51/2.95 [ ~( =( eq2( X, Y ), btrue ) ), =( eq( pair22( X, Z ), pair22( Y, T ) )
% 2.51/2.95 , eq5( Z, T ) ) ],
% 2.51/2.95 [ ~( =( eq3( 'prop_help'( X, Y, Z, T, U ), bfalse ), btrue ) ) ]
% 2.51/2.95 ] .
% 2.51/2.95
% 2.51/2.95
% 2.51/2.95 percentage equality = 1.000000, percentage horn = 1.000000
% 2.51/2.95 This is a pure equality problem
% 2.51/2.95
% 2.51/2.95
% 2.51/2.95
% 2.51/2.95 Options Used:
% 2.51/2.95
% 2.51/2.95 useres = 1
% 2.51/2.95 useparamod = 1
% 2.51/2.95 useeqrefl = 1
% 2.51/2.95 useeqfact = 1
% 2.51/2.95 usefactor = 1
% 2.51/2.95 usesimpsplitting = 0
% 2.51/2.95 usesimpdemod = 5
% 2.51/2.95 usesimpres = 3
% 2.51/2.95
% 2.51/2.95 resimpinuse = 1000
% 2.51/2.95 resimpclauses = 20000
% 2.51/2.95 substype = eqrewr
% 2.51/2.95 backwardsubs = 1
% 2.51/2.95 selectoldest = 5
% 2.51/2.95
% 2.51/2.95 litorderings [0] = split
% 2.51/2.95 litorderings [1] = extend the termordering, first sorting on arguments
% 2.51/2.95
% 2.51/2.95 termordering = kbo
% 2.51/2.95
% 2.51/2.95 litapriori = 0
% 2.51/2.95 termapriori = 1
% 2.51/2.95 litaposteriori = 0
% 2.51/2.95 termaposteriori = 0
% 2.51/2.95 demodaposteriori = 0
% 2.51/2.95 ordereqreflfact = 0
% 2.51/2.95
% 2.51/2.95 litselect = negord
% 2.51/2.95
% 2.51/2.95 maxweight = 15
% 2.51/2.95 maxdepth = 30000
% 2.51/2.95 maxlength = 115
% 2.51/2.95 maxnrvars = 195
% 2.51/2.95 excuselevel = 1
% 2.51/2.95 increasemaxweight = 1
% 2.51/2.95
% 2.51/2.95 maxselected = 10000000
% 2.51/2.95 maxnrclauses = 10000000
% 2.51/2.95
% 2.51/2.95 showgenerated = 0
% 2.51/2.95 showkept = 0
% 2.51/2.95 showselected = 0
% 2.51/2.95 showdeleted = 0
% 2.51/2.95 showresimp = 1
% 2.51/2.95 showstatus = 2000
% 2.51/2.95
% 2.51/2.95 prologoutput = 1
% 2.51/2.95 nrgoals = 5000000
% 2.51/2.95 totalproof = 1
% 2.51/2.95
% 2.51/2.95 Symbols occurring in the translation:
% 2.51/2.95
% 2.51/2.95 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.51/2.95 . [1, 2] (w:1, o:62, a:1, s:1, b:0),
% 2.51/2.95 ! [4, 1] (w:0, o:50, a:1, s:1, b:0),
% 2.51/2.95 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.51/2.95 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.51/2.95 btrue [43, 0] (w:1, o:36, a:1, s:1, b:0),
% 2.51/2.95 aux [44, 5] (w:1, o:108, a:1, s:1, b:0),
% 2.51/2.95 bfalse [45, 0] (w:1, o:37, a:1, s:1, b:0),
% 2.51/2.95 apply [46, 2] (w:1, o:87, a:1, s:1, b:0),
% 2.51/2.95 pair23 [52, 2] (w:1, o:89, a:1, s:1, b:0),
% 2.51/2.95 aux2 [53, 5] (w:1, o:109, a:1, s:1, b:0),
% 2.51/2.95 cons2 [54, 2] (w:1, o:90, a:1, s:1, b:0),
% 2.51/2.95 tuple2 [55, 3] (w:1, o:105, a:1, s:1, b:0),
% 2.51/2.95 right [56, 1] (w:1, o:55, a:1, s:1, b:0),
% 2.51/2.95 pair24 [63, 2] (w:1, o:91, a:1, s:1, b:0),
% 2.51/2.95 aux3 [64, 6] (w:1, o:112, a:1, s:1, b:0),
% 2.51/2.95 act [65, 4] (w:1, o:107, a:1, s:1, b:0),
% 2.51/2.95 aux4 [67, 5] (w:1, o:110, a:1, s:1, b:0),
% 2.51/2.95 pair22 [68, 2] (w:1, o:88, a:1, s:1, b:0),
% 2.51/2.95 left [70, 1] (w:1, o:56, a:1, s:1, b:0),
% 2.51/2.95 aux5 [71, 3] (w:1, o:106, a:1, s:1, b:0),
% 2.51/2.95 steps [73, 2] (w:1, o:94, a:1, s:1, b:0),
% 2.51/2.95 nil2 [74, 0] (w:1, o:45, a:1, s:1, b:0),
% 2.51/2.95 aux6 [75, 2] (w:1, o:95, a:1, s:1, b:0),
% 2.51/2.95 a2 [76, 0] (w:1, o:35, a:1, s:1, b:0),
% 2.51/2.95 b [77, 0] (w:1, o:46, a:1, s:1, b:0),
% 2.51/2.95 o [80, 0] (w:1, o:9, a:1, s:1, b:0),
% 2.51/2.95 aux7 [87, 2] (w:1, o:96, a:1, s:1, b:0),
% 2.51/2.95 runt [88, 2] (w:1, o:92, a:1, s:1, b:0),
% 2.51/2.95 split [91, 1] (w:1, o:58, a:1, s:1, b:0),
% 2.51/2.95 rev [93, 2] (w:1, o:93, a:1, s:1, b:0),
% 2.51/2.95 one [94, 0] (w:1, o:10, a:1, s:1, b:0),
% 2.51/2.95 zero [95, 0] (w:1, o:47, a:1, s:1, b:0),
% 2.51/2.95 succ [96, 1] (w:1, o:59, a:1, s:1, b:0),
% 2.51/2.95 two [97, 0] (w:1, o:48, a:1, s:1, b:0),
% 2.51/2.95 nil [98, 0] (w:1, o:8, a:1, s:1, b:0),
% 2.51/2.95 stp [99, 0] (w:1, o:5, a:1, s:1, b:0),
% 2.51/2.95 pair2 [100, 2] (w:1, o:97, a:1, s:1, b:0),
% 2.51/2.95 cons [101, 2] (w:1, o:98, a:1, s:1, b:0),
% 2.51/2.95 eq [102, 2] (w:1, o:99, a:1, s:1, b:0),
% 2.51/2.95 lft [103, 1] (w:1, o:60, a:1, s:1, b:0),
% 2.51/2.95 rgt [105, 1] (w:1, o:57, a:1, s:1, b:0),
% 152.55/153.16 step [106, 2] (w:1, o:100, a:1, s:1, b:0),
% 152.55/153.16 prog0 [107, 1] (w:1, o:61, a:1, s:1, b:0),
% 152.55/153.16 'prop_help' [108, 5] (w:1, o:111, a:1, s:1, b:0),
% 152.55/153.16 eq3 [109, 2] (w:1, o:102, a:1, s:1, b:0),
% 152.55/153.16 eq5 [110, 2] (w:1, o:104, a:1, s:1, b:0),
% 152.55/153.16 eq2 [111, 2] (w:1, o:101, a:1, s:1, b:0),
% 152.55/153.16 eq4 [112, 2] (w:1, o:103, a:1, s:1, b:0).
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 15
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 1878
% 152.55/153.16 Kept: 170
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 16
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 16
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 2045
% 152.55/153.16 Kept: 179
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 17
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 17
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 2519
% 152.55/153.16 Kept: 203
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 18
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 18
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 2991
% 152.55/153.16 Kept: 222
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 19
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 19
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 3525
% 152.55/153.16 Kept: 245
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 20
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 20
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 4200
% 152.55/153.16 Kept: 268
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 21
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 21
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 4832
% 152.55/153.16 Kept: 297
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 22
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 22
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 6108
% 152.55/153.16 Kept: 333
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 23
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 23
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 7354
% 152.55/153.16 Kept: 374
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 24
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 24
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 9035
% 152.55/153.16 Kept: 419
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 25
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 25
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 10617
% 152.55/153.16 Kept: 469
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 26
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 26
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 12519
% 152.55/153.16 Kept: 525
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 27
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 27
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 14406
% 152.55/153.16 Kept: 581
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 28
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 28
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 16403
% 152.55/153.16 Kept: 633
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 29
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 29
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 19163
% 152.55/153.16 Kept: 721
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 30
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 30
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 22471
% 152.55/153.16 Kept: 822
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 31
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 31
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 27132
% 152.55/153.16 Kept: 1010
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 32
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 Failed to find proof!
% 152.55/153.16 maxweight = 32
% 152.55/153.16 maxnrclauses = 10000000
% 152.55/153.16 Generated: 27142
% 152.55/153.16 Kept: 1173
% 152.55/153.16
% 152.55/153.16
% 152.55/153.16 The strategy used was not complete!
% 152.55/153.16
% 152.55/153.16 Increased maxweight to 33
% 152.55/153.16
% 152.55/153.16 Starting Search:
% 152.55/153.16
% 152.55/153.16 Resimplifying inuse:
% 152.55/153.16 Done
% 152.55/153.16
% 152.55/153.16 ResimTerminated
% 299.33/300.03 Bliksem ended
%------------------------------------------------------------------------------