%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX212-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n024.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:49 PM UTC 2026
% Result : Timeout 299.61s 300.01s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : SWX212-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.06 % Command : bliksem %s
% 0.07/0.24 % Computer : n024.cluster.edu
% 0.07/0.24 % Model : x86_64 x86_64
% 0.07/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.24 % Memory : 8042.1875MB
% 0.07/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.24 % CPULimit : 300
% 0.07/0.24 % DateTime : Tue May 5 06:56:41 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.80/1.29 *** allocated 10000 integers for termspace/termends
% 0.80/1.29 *** allocated 10000 integers for clauses
% 0.80/1.29 *** allocated 10000 integers for justifications
% 0.80/1.29 Bliksem 1.12
% 0.80/1.29
% 0.80/1.29
% 0.80/1.29 Automatic Strategy Selection
% 0.80/1.29
% 0.80/1.29 Clauses:
% 0.80/1.29 [
% 0.80/1.29 [ =( aux( X, Y, btrue ), eps ) ],
% 0.80/1.29 [ =( aux( X, Y, bfalse ), nil2 ) ],
% 0.80/1.29 [ =( aux2( X, Y, Z, btrue ), x( y( step( Y, X ), Z ), step( Z, X ) ) ) ]
% 0.80/1.29 ,
% 0.80/1.29 [ =( aux2( X, Y, Z, bfalse ), x( y( step( Y, X ), Z ), nil2 ) ) ],
% 0.80/1.29 [ =( z( nil2, X ), nil2 ) ],
% 0.80/1.29 [ =( z( eps, X ), X ) ],
% 0.80/1.29 [ =( z( atom( X ), nil2 ), nil2 ) ],
% 0.80/1.29 [ =( z( atom( X ), eps ), atom( X ) ) ],
% 0.80/1.29 [ =( z( atom( X ), atom( Y ) ), y( atom( X ), atom( Y ) ) ) ],
% 0.80/1.29 [ =( z( atom( X ), x( Y, Z ) ), y( atom( X ), x( Y, Z ) ) ) ],
% 0.80/1.29 [ =( z( atom( X ), y( Y, Z ) ), y( atom( X ), y( Y, Z ) ) ) ],
% 0.80/1.29 [ =( z( atom( X ), star( Y ) ), y( atom( X ), star( Y ) ) ) ],
% 0.80/1.29 [ =( z( x( X, Y ), nil2 ), nil2 ) ],
% 0.80/1.29 [ =( z( x( X, Y ), eps ), x( X, Y ) ) ],
% 0.80/1.29 [ =( z( x( X, Y ), atom( Z ) ), y( x( X, Y ), atom( Z ) ) ) ],
% 0.80/1.29 [ =( z( x( X, Y ), x( Z, T ) ), y( x( X, Y ), x( Z, T ) ) ) ],
% 0.80/1.29 [ =( z( x( X, Y ), y( Z, T ) ), y( x( X, Y ), y( Z, T ) ) ) ],
% 0.80/1.29 [ =( z( x( X, Y ), star( Z ) ), y( x( X, Y ), star( Z ) ) ) ],
% 0.80/1.29 [ =( z( y( X, Y ), nil2 ), nil2 ) ],
% 0.80/1.29 [ =( z( y( X, Y ), eps ), y( X, Y ) ) ],
% 0.80/1.29 [ =( z( y( X, Y ), atom( Z ) ), y( y( X, Y ), atom( Z ) ) ) ],
% 0.80/1.29 [ =( z( y( X, Y ), x( Z, T ) ), y( y( X, Y ), x( Z, T ) ) ) ],
% 0.80/1.29 [ =( z( y( X, Y ), y( Z, T ) ), y( y( X, Y ), y( Z, T ) ) ) ],
% 0.80/1.29 [ =( z( y( X, Y ), star( Z ) ), y( y( X, Y ), star( Z ) ) ) ],
% 0.80/1.29 [ =( z( star( X ), nil2 ), nil2 ) ],
% 0.80/1.29 [ =( z( star( X ), eps ), star( X ) ) ],
% 0.80/1.29 [ =( z( star( X ), atom( Y ) ), y( star( X ), atom( Y ) ) ) ],
% 0.80/1.29 [ =( z( star( X ), x( Y, Z ) ), y( star( X ), x( Y, Z ) ) ) ],
% 0.80/1.29 [ =( z( star( X ), y( Y, Z ) ), y( star( X ), y( Y, Z ) ) ) ],
% 0.80/1.29 [ =( z( star( X ), star( Y ) ), y( star( X ), star( Y ) ) ) ],
% 0.80/1.29 [ =( x2( nil2, X ), X ) ],
% 0.80/1.29 [ =( x2( eps, nil2 ), eps ) ],
% 0.80/1.29 [ =( x2( eps, eps ), x( eps, eps ) ) ],
% 0.80/1.29 [ =( x2( eps, atom( X ) ), x( eps, atom( X ) ) ) ],
% 0.80/1.29 [ =( x2( eps, x( X, Y ) ), x( eps, x( X, Y ) ) ) ],
% 0.80/1.29 [ =( x2( eps, y( X, Y ) ), x( eps, y( X, Y ) ) ) ],
% 0.80/1.29 [ =( x2( eps, star( X ) ), x( eps, star( X ) ) ) ],
% 0.80/1.29 [ =( x2( atom( X ), nil2 ), atom( X ) ) ],
% 0.80/1.29 [ =( x2( atom( X ), eps ), x( atom( X ), eps ) ) ],
% 0.80/1.29 [ =( x2( atom( X ), atom( Y ) ), x( atom( X ), atom( Y ) ) ) ],
% 0.80/1.29 [ =( x2( atom( X ), x( Y, Z ) ), x( atom( X ), x( Y, Z ) ) ) ],
% 0.80/1.29 [ =( x2( atom( X ), y( Y, Z ) ), x( atom( X ), y( Y, Z ) ) ) ],
% 0.80/1.29 [ =( x2( atom( X ), star( Y ) ), x( atom( X ), star( Y ) ) ) ],
% 0.80/1.29 [ =( x2( x( X, Y ), nil2 ), x( X, Y ) ) ],
% 0.80/1.29 [ =( x2( x( X, Y ), eps ), x( x( X, Y ), eps ) ) ],
% 0.80/1.29 [ =( x2( x( X, Y ), atom( Z ) ), x( x( X, Y ), atom( Z ) ) ) ],
% 0.80/1.29 [ =( x2( x( X, Y ), x( Z, T ) ), x( x( X, Y ), x( Z, T ) ) ) ],
% 0.80/1.29 [ =( x2( x( X, Y ), y( Z, T ) ), x( x( X, Y ), y( Z, T ) ) ) ],
% 0.80/1.29 [ =( x2( x( X, Y ), star( Z ) ), x( x( X, Y ), star( Z ) ) ) ],
% 0.80/1.29 [ =( x2( y( X, Y ), nil2 ), y( X, Y ) ) ],
% 0.80/1.29 [ =( x2( y( X, Y ), eps ), x( y( X, Y ), eps ) ) ],
% 0.80/1.29 [ =( x2( y( X, Y ), atom( Z ) ), x( y( X, Y ), atom( Z ) ) ) ],
% 0.80/1.29 [ =( x2( y( X, Y ), x( Z, T ) ), x( y( X, Y ), x( Z, T ) ) ) ],
% 0.80/1.29 [ =( x2( y( X, Y ), y( Z, T ) ), x( y( X, Y ), y( Z, T ) ) ) ],
% 0.80/1.29 [ =( x2( y( X, Y ), star( Z ) ), x( y( X, Y ), star( Z ) ) ) ],
% 0.80/1.29 [ =( x2( star( X ), nil2 ), star( X ) ) ],
% 0.80/1.29 [ =( x2( star( X ), eps ), x( star( X ), eps ) ) ],
% 0.80/1.29 [ =( x2( star( X ), atom( Y ) ), x( star( X ), atom( Y ) ) ) ],
% 0.80/1.29 [ =( x2( star( X ), x( Y, Z ) ), x( star( X ), x( Y, Z ) ) ) ],
% 0.80/1.29 [ =( x2( star( X ), y( Y, Z ) ), x( star( X ), y( Y, Z ) ) ) ],
% 0.80/1.29 [ =( x2( star( X ), star( Y ) ), x( star( X ), star( Y ) ) ) ],
% 0.80/1.29 [ =( orb( btrue, X ), btrue ) ],
% 0.80/1.29 [ =( orb( bfalse, X ), X ) ],
% 0.80/1.29 [ =( andb( btrue, X ), X ) ],
% 0.80/1.29 [ =( andb( bfalse, X ), bfalse ) ],
% 0.80/1.29 [ =( eps2( eps ), btrue ) ],
% 0.80/1.29 [ =( eps2( x( X, Y ) ), orb( eps2( X ), eps2( Y ) ) ) ],
% 0.80/1.29 [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) ) ],
% 0.80/1.29 [ =( eps2( star( X ) ), btrue ) ],
% 0.80/1.29 [ =( eps2( nil2 ), bfalse ) ],
% 0.80/1.29 [ =( eps2( atom( X ) ), bfalse ) ],
% 0.80/1.29 [ =( step( atom( X ), Y ), aux( Y, X, eq( X, Y ) ) ) ],
% 176.49/176.90 [ =( step( x( X, Y ), Z ), x( step( X, Z ), step( Y, Z ) ) ) ],
% 176.49/176.90 [ =( step( y( X, Y ), Z ), aux2( Z, X, Y, eps2( X ) ) ) ],
% 176.49/176.90 [ =( step( star( X ), Y ), y( step( X, Y ), star( X ) ) ) ],
% 176.49/176.90 [ =( step( nil2, X ), nil2 ) ],
% 176.49/176.90 [ =( step( eps, X ), nil2 ) ],
% 176.49/176.90 [ =( rec( X, nil ), eps2( X ) ) ],
% 176.49/176.90 [ =( rec( X, cons( Y, Z ) ), rec( step( X, Y ), Z ) ) ],
% 176.49/176.90 [ =( 'prop_koen'( X, Y, Z ), eq2( rec( y( X, Y ), Z ), rec( y( Y, X ), Z
% 176.49/176.90 ) ) ) ],
% 176.49/176.90 [ =( eq( a, b ), bfalse ) ],
% 176.49/176.90 [ =( eq( a, c ), bfalse ) ],
% 176.49/176.90 [ =( eq( b, a ), bfalse ) ],
% 176.49/176.90 [ =( eq( b, c ), bfalse ) ],
% 176.49/176.90 [ =( eq( c, a ), bfalse ) ],
% 176.49/176.90 [ =( eq( c, b ), bfalse ) ],
% 176.49/176.90 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 176.49/176.90 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 176.49/176.90 [ =( eq( X, X ), btrue ) ],
% 176.49/176.90 [ =( eq2( X, X ), btrue ) ],
% 176.49/176.90 [ ~( =( eq2( 'prop_koen'( X, Y, Z ), bfalse ), btrue ) ) ]
% 176.49/176.90 ] .
% 176.49/176.90
% 176.49/176.90
% 176.49/176.90 percentage equality = 1.000000, percentage horn = 1.000000
% 176.49/176.90 This is a pure equality problem
% 176.49/176.90
% 176.49/176.90
% 176.49/176.90
% 176.49/176.90 Options Used:
% 176.49/176.90
% 176.49/176.90 useres = 1
% 176.49/176.90 useparamod = 1
% 176.49/176.90 useeqrefl = 1
% 176.49/176.90 useeqfact = 1
% 176.49/176.90 usefactor = 1
% 176.49/176.90 usesimpsplitting = 0
% 176.49/176.90 usesimpdemod = 5
% 176.49/176.90 usesimpres = 3
% 176.49/176.90
% 176.49/176.90 resimpinuse = 1000
% 176.49/176.90 resimpclauses = 20000
% 176.49/176.90 substype = eqrewr
% 176.49/176.90 backwardsubs = 1
% 176.49/176.90 selectoldest = 5
% 176.49/176.90
% 176.49/176.90 litorderings [0] = split
% 176.49/176.90 litorderings [1] = extend the termordering, first sorting on arguments
% 176.49/176.90
% 176.49/176.90 termordering = kbo
% 176.49/176.90
% 176.49/176.90 litapriori = 0
% 176.49/176.90 termapriori = 1
% 176.49/176.90 litaposteriori = 0
% 176.49/176.90 termaposteriori = 0
% 176.49/176.90 demodaposteriori = 0
% 176.49/176.90 ordereqreflfact = 0
% 176.49/176.90
% 176.49/176.90 litselect = negord
% 176.49/176.90
% 176.49/176.90 maxweight = 15
% 176.49/176.90 maxdepth = 30000
% 176.49/176.90 maxlength = 115
% 176.49/176.90 maxnrvars = 195
% 176.49/176.90 excuselevel = 1
% 176.49/176.90 increasemaxweight = 1
% 176.49/176.90
% 176.49/176.90 maxselected = 10000000
% 176.49/176.90 maxnrclauses = 10000000
% 176.49/176.90
% 176.49/176.90 showgenerated = 0
% 176.49/176.90 showkept = 0
% 176.49/176.90 showselected = 0
% 176.49/176.90 showdeleted = 0
% 176.49/176.90 showresimp = 1
% 176.49/176.90 showstatus = 2000
% 176.49/176.90
% 176.49/176.90 prologoutput = 1
% 176.49/176.90 nrgoals = 5000000
% 176.49/176.90 totalproof = 1
% 176.49/176.90
% 176.49/176.90 Symbols occurring in the translation:
% 176.49/176.90
% 176.49/176.90 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 176.49/176.90 . [1, 2] (w:1, o:38, a:1, s:1, b:0),
% 176.49/176.90 ! [4, 1] (w:0, o:30, a:1, s:1, b:0),
% 176.49/176.90 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 176.49/176.90 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 176.49/176.90 btrue [41, 0] (w:1, o:17, a:1, s:1, b:0),
% 176.49/176.90 aux [42, 3] (w:1, o:74, a:1, s:1, b:0),
% 176.49/176.90 eps [43, 0] (w:1, o:18, a:1, s:1, b:0),
% 176.49/176.90 bfalse [44, 0] (w:1, o:19, a:1, s:1, b:0),
% 176.49/176.90 nil2 [45, 0] (w:1, o:20, a:1, s:1, b:0),
% 176.49/176.90 aux2 [48, 4] (w:1, o:76, a:1, s:1, b:0),
% 176.49/176.90 step [49, 2] (w:1, o:64, a:1, s:1, b:0),
% 176.49/176.90 y [50, 2] (w:1, o:67, a:1, s:1, b:0),
% 176.49/176.90 x [51, 2] (w:1, o:65, a:1, s:1, b:0),
% 176.49/176.90 z [52, 2] (w:1, o:68, a:1, s:1, b:0),
% 176.49/176.90 atom [54, 1] (w:1, o:35, a:1, s:1, b:0),
% 176.49/176.90 star [57, 1] (w:1, o:36, a:1, s:1, b:0),
% 176.49/176.90 x2 [59, 2] (w:1, o:66, a:1, s:1, b:0),
% 176.49/176.90 orb [61, 2] (w:1, o:69, a:1, s:1, b:0),
% 176.49/176.90 andb [62, 2] (w:1, o:70, a:1, s:1, b:0),
% 176.49/176.90 eps2 [63, 1] (w:1, o:37, a:1, s:1, b:0),
% 176.49/176.90 eq [65, 2] (w:1, o:71, a:1, s:1, b:0),
% 176.49/176.90 nil [67, 0] (w:1, o:26, a:1, s:1, b:0),
% 176.49/176.90 rec [68, 2] (w:1, o:63, a:1, s:1, b:0),
% 176.49/176.90 cons [71, 2] (w:1, o:72, a:1, s:1, b:0),
% 176.49/176.90 'prop_koen' [72, 3] (w:1, o:75, a:1, s:1, b:0),
% 176.49/176.90 eq2 [73, 2] (w:1, o:73, a:1, s:1, b:0),
% 176.49/176.90 a [74, 0] (w:1, o:16, a:1, s:1, b:0),
% 176.49/176.90 b [75, 0] (w:1, o:28, a:1, s:1, b:0),
% 176.49/176.90 c [76, 0] (w:1, o:29, a:1, s:1, b:0).
% 176.49/176.90
% 176.49/176.90
% 176.49/176.90 Starting Search:
% 176.49/176.90
% 176.49/176.90 Resimplifying inuse:
% 176.49/176.90 Done
% 176.49/176.90
% 176.49/176.90
% 176.49/176.90 Intermediate Status:
% 176.49/176.90 Generated: 6441
% 176.49/176.90 Kept: 2000
% 176.49/176.90 Inuse: 395
% 176.49/176.90 Deleted: 133
% 176.49/176.90 Deletedinuse: 23
% 176.49/176.90
% 176.49/176.90 Resimplifying inuse:
% 176.49/176.90 Done
% 176.49/176.90
% 176.49/176.90 Resimplifying inuse:
% 176.49/176.90 Done
% 176.49/176.90
% 176.49/176.90
% 176.49/176.90 Intermediate Status:
% 176.49/176.90 Generated: 22963
% 176.49/176.90 Kept: 4005
% 176.49/176.90 Inuse: 846
% 176.49/176.90 Deleted: 461
% 176.49/176.90 Deletedinuse: 45
% 176.49/176.90
% 176.49/176.90 Resimplifying inuse:
% 176.49/176.90 Done
% 176.49/176.90
% 176.49/176.90 Resimplifying inuse:
% 176.49/176.90 Done
% 176.49/176.90
% 176.49/176.90
% 176.49/176.90 Intermediate Status:
% 176.49/176.90 Generated: 35307
% 176.49/176.90 Kept: 6006
% 176.49/176.90 Inuse: 1171
% 176.49/176.90 Deleted: 540
% 176.49/176.90 Deletedinuse: 59
% 176.49/176.90
% 176.49/176.90 Resimplifying inuse:
% 176.49/176.90 Done
% 176.49/176.90
% 176.49/176.90 Resimplifying inuse:
% 176.49/176.90 Done
% 176.49/176.90
% 176.49/176.90
% 176.49/176.90 Intermediate Status:
% 176.49/176.90 Generated: 55191
% 176.49/176.90 Kept: 8317
% 176.49/176.90 Inuse: 1525
% 176.49/176.90 Deleted: 626
% 176.49/176.90 Deletedinuse: 83
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 86281
% 258.50/259.00 Kept: 10320
% 258.50/259.00 Inuse: 2208
% 258.50/259.00 Deleted: 783
% 258.50/259.00 Deletedinuse: 136
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 147241
% 258.50/259.00 Kept: 12325
% 258.50/259.00 Inuse: 2935
% 258.50/259.00 Deleted: 1170
% 258.50/259.00 Deletedinuse: 261
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 191134
% 258.50/259.00 Kept: 14334
% 258.50/259.00 Inuse: 3495
% 258.50/259.00 Deleted: 1453
% 258.50/259.00 Deletedinuse: 408
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 226322
% 258.50/259.00 Kept: 16336
% 258.50/259.00 Inuse: 4080
% 258.50/259.00 Deleted: 1640
% 258.50/259.00 Deletedinuse: 461
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 255000
% 258.50/259.00 Kept: 18343
% 258.50/259.00 Inuse: 4533
% 258.50/259.00 Deleted: 1775
% 258.50/259.00 Deletedinuse: 490
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying clauses:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 295483
% 258.50/259.00 Kept: 20347
% 258.50/259.00 Inuse: 5045
% 258.50/259.00 Deleted: 6473
% 258.50/259.00 Deletedinuse: 490
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 397792
% 258.50/259.00 Kept: 22351
% 258.50/259.00 Inuse: 6347
% 258.50/259.00 Deleted: 6778
% 258.50/259.00 Deletedinuse: 777
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 556564
% 258.50/259.00 Kept: 24352
% 258.50/259.00 Inuse: 8000
% 258.50/259.00 Deleted: 6891
% 258.50/259.00 Deletedinuse: 861
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 782781
% 258.50/259.00 Kept: 26352
% 258.50/259.00 Inuse: 10093
% 258.50/259.00 Deleted: 7057
% 258.50/259.00 Deletedinuse: 987
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 934520
% 258.50/259.00 Kept: 28352
% 258.50/259.00 Inuse: 12060
% 258.50/259.00 Deleted: 7250
% 258.50/259.00 Deletedinuse: 1097
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 1091222
% 258.50/259.00 Kept: 30400
% 258.50/259.00 Inuse: 14350
% 258.50/259.00 Deleted: 7425
% 258.50/259.00 Deletedinuse: 1145
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 1311110
% 258.50/259.00 Kept: 32401
% 258.50/259.00 Inuse: 17934
% 258.50/259.00 Deleted: 7650
% 258.50/259.00 Deletedinuse: 1161
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 1545819
% 258.50/259.00 Kept: 34401
% 258.50/259.00 Inuse: 21912
% 258.50/259.00 Deleted: 7852
% 258.50/259.00 Deletedinuse: 1206
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 1758077
% 258.50/259.00 Kept: 36401
% 258.50/259.00 Inuse: 25499
% 258.50/259.00 Deleted: 8010
% 258.50/259.00 Deletedinuse: 1208
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 1957987
% 258.50/259.00 Kept: 38401
% 258.50/259.00 Inuse: 29127
% 258.50/259.00 Deleted: 8114
% 258.50/259.00 Deletedinuse: 1216
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Failed to find proof!
% 258.50/259.00 maxweight = 15
% 258.50/259.00 maxnrclauses = 10000000
% 258.50/259.00 Generated: 2013062
% 258.50/259.00 Kept: 38729
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 The strategy used was not complete!
% 258.50/259.00
% 258.50/259.00 Increased maxweight to 16
% 258.50/259.00
% 258.50/259.00 Starting Search:
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 5795
% 258.50/259.00 Kept: 2006
% 258.50/259.00 Inuse: 370
% 258.50/259.00 Deleted: 117
% 258.50/259.00 Deletedinuse: 23
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 17772
% 258.50/259.00 Kept: 4007
% 258.50/259.00 Inuse: 713
% 258.50/259.00 Deleted: 367
% 258.50/259.00 Deletedinuse: 27
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 29505
% 258.50/259.00 Kept: 6009
% 258.50/259.00 Inuse: 1044
% 258.50/259.00 Deleted: 508
% 258.50/259.00 Deletedinuse: 49
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 50316
% 258.50/259.00 Kept: 8010
% 258.50/259.00 Inuse: 1421
% 258.50/259.00 Deleted: 599
% 258.50/259.00 Deletedinuse: 78
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 61426
% 258.50/259.00 Kept: 10010
% 258.50/259.00 Inuse: 1619
% 258.50/259.00 Deleted: 682
% 258.50/259.00 Deletedinuse: 116
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 112138
% 258.50/259.00 Kept: 12015
% 258.50/259.00 Inuse: 2495
% 258.50/259.00 Deleted: 1208
% 258.50/259.00 Deletedinuse: 316
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 258.50/259.00
% 258.50/259.00 Intermediate Status:
% 258.50/259.00 Generated: 160778
% 258.50/259.00 Kept: 14027
% 258.50/259.00 Inuse: 2871
% 258.50/259.00 Deleted: 1613
% 258.50/259.00 Deletedinuse: 536
% 258.50/259.00
% 258.50/259.00 Resimplifying inuse:
% 258.50/259.00 Done
% 258.50/259.00
% 299.61/300.01 Terminated
% 299.61/300.01 Bliksem ended
%------------------------------------------------------------------------------