%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX234-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Tue May 5 06:56:52 PM UTC 2026
% Result : Timeout 299.52s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX234-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : bliksem %s
% 0.15/0.33 % Computer : n013.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % DateTime : Tue May 5 13:07:56 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.74/1.14 *** allocated 10000 integers for termspace/termends
% 0.74/1.14 *** allocated 10000 integers for clauses
% 0.74/1.14 *** allocated 10000 integers for justifications
% 0.74/1.14 Bliksem 1.12
% 0.74/1.14
% 0.74/1.14
% 0.74/1.14 Automatic Strategy Selection
% 0.74/1.14
% 0.74/1.14 Clauses:
% 0.74/1.14 [
% 0.74/1.14 [ =( aux( X, Y, btrue ), eps ) ],
% 0.74/1.14 [ =( aux( X, Y, bfalse ), nil4 ) ],
% 0.74/1.14 [ =( aux2( X, Y, Z, btrue ), x( y( step( Y, X ), Z ), step( Z, X ) ) ) ]
% 0.74/1.14 ,
% 0.74/1.14 [ =( aux2( X, Y, Z, bfalse ), x( y( step( Y, X ), Z ), nil4 ) ) ],
% 0.74/1.14 [ =( aux3( X, Y, Z, btrue ), rec( y( X, star( X ) ), cons2( Y, Z ) ) ) ]
% 0.74/1.14 ,
% 0.74/1.14 [ =( aux3( X, Y, Z, bfalse ), bfalse ) ],
% 0.74/1.14 [ =( z( nil4, X ), nil4 ) ],
% 0.74/1.14 [ =( z( eps, X ), X ) ],
% 0.74/1.14 [ =( z( atom( X ), nil4 ), nil4 ) ],
% 0.74/1.14 [ =( z( atom( X ), eps ), atom( X ) ) ],
% 0.74/1.14 [ =( z( atom( X ), atom( Y ) ), y( atom( X ), atom( Y ) ) ) ],
% 0.74/1.14 [ =( z( atom( X ), x( Y, Z ) ), y( atom( X ), x( Y, Z ) ) ) ],
% 0.74/1.14 [ =( z( atom( X ), y( Y, Z ) ), y( atom( X ), y( Y, Z ) ) ) ],
% 0.74/1.14 [ =( z( atom( X ), star( Y ) ), y( atom( X ), star( Y ) ) ) ],
% 0.74/1.14 [ =( z( x( X, Y ), nil4 ), nil4 ) ],
% 0.74/1.14 [ =( z( x( X, Y ), eps ), x( X, Y ) ) ],
% 0.74/1.14 [ =( z( x( X, Y ), atom( Z ) ), y( x( X, Y ), atom( Z ) ) ) ],
% 0.74/1.14 [ =( z( x( X, Y ), x( Z, T ) ), y( x( X, Y ), x( Z, T ) ) ) ],
% 0.74/1.14 [ =( z( x( X, Y ), y( Z, T ) ), y( x( X, Y ), y( Z, T ) ) ) ],
% 0.74/1.14 [ =( z( x( X, Y ), star( Z ) ), y( x( X, Y ), star( Z ) ) ) ],
% 0.74/1.14 [ =( z( y( X, Y ), nil4 ), nil4 ) ],
% 0.74/1.14 [ =( z( y( X, Y ), eps ), y( X, Y ) ) ],
% 0.74/1.14 [ =( z( y( X, Y ), atom( Z ) ), y( y( X, Y ), atom( Z ) ) ) ],
% 0.74/1.14 [ =( z( y( X, Y ), x( Z, T ) ), y( y( X, Y ), x( Z, T ) ) ) ],
% 0.74/1.14 [ =( z( y( X, Y ), y( Z, T ) ), y( y( X, Y ), y( Z, T ) ) ) ],
% 0.74/1.14 [ =( z( y( X, Y ), star( Z ) ), y( y( X, Y ), star( Z ) ) ) ],
% 0.74/1.14 [ =( z( star( X ), nil4 ), nil4 ) ],
% 0.74/1.14 [ =( z( star( X ), eps ), star( X ) ) ],
% 0.74/1.14 [ =( z( star( X ), atom( Y ) ), y( star( X ), atom( Y ) ) ) ],
% 0.74/1.14 [ =( z( star( X ), x( Y, Z ) ), y( star( X ), x( Y, Z ) ) ) ],
% 0.74/1.14 [ =( z( star( X ), y( Y, Z ) ), y( star( X ), y( Y, Z ) ) ) ],
% 0.74/1.14 [ =( z( star( X ), star( Y ) ), y( star( X ), star( Y ) ) ) ],
% 0.74/1.14 [ =( x2( nil4, X ), X ) ],
% 0.74/1.14 [ =( x2( eps, nil4 ), eps ) ],
% 0.74/1.14 [ =( x2( eps, eps ), x( eps, eps ) ) ],
% 0.74/1.14 [ =( x2( eps, atom( X ) ), x( eps, atom( X ) ) ) ],
% 0.74/1.14 [ =( x2( eps, x( X, Y ) ), x( eps, x( X, Y ) ) ) ],
% 0.74/1.14 [ =( x2( eps, y( X, Y ) ), x( eps, y( X, Y ) ) ) ],
% 0.74/1.14 [ =( x2( eps, star( X ) ), x( eps, star( X ) ) ) ],
% 0.74/1.14 [ =( x2( atom( X ), nil4 ), atom( X ) ) ],
% 0.74/1.14 [ =( x2( atom( X ), eps ), x( atom( X ), eps ) ) ],
% 0.74/1.14 [ =( x2( atom( X ), atom( Y ) ), x( atom( X ), atom( Y ) ) ) ],
% 0.74/1.14 [ =( x2( atom( X ), x( Y, Z ) ), x( atom( X ), x( Y, Z ) ) ) ],
% 0.74/1.14 [ =( x2( atom( X ), y( Y, Z ) ), x( atom( X ), y( Y, Z ) ) ) ],
% 0.74/1.14 [ =( x2( atom( X ), star( Y ) ), x( atom( X ), star( Y ) ) ) ],
% 0.74/1.14 [ =( x2( x( X, Y ), nil4 ), x( X, Y ) ) ],
% 0.74/1.14 [ =( x2( x( X, Y ), eps ), x( x( X, Y ), eps ) ) ],
% 0.74/1.14 [ =( x2( x( X, Y ), atom( Z ) ), x( x( X, Y ), atom( Z ) ) ) ],
% 0.74/1.14 [ =( x2( x( X, Y ), x( Z, T ) ), x( x( X, Y ), x( Z, T ) ) ) ],
% 0.74/1.14 [ =( x2( x( X, Y ), y( Z, T ) ), x( x( X, Y ), y( Z, T ) ) ) ],
% 0.74/1.14 [ =( x2( x( X, Y ), star( Z ) ), x( x( X, Y ), star( Z ) ) ) ],
% 0.74/1.14 [ =( x2( y( X, Y ), nil4 ), y( X, Y ) ) ],
% 0.74/1.14 [ =( x2( y( X, Y ), eps ), x( y( X, Y ), eps ) ) ],
% 0.74/1.14 [ =( x2( y( X, Y ), atom( Z ) ), x( y( X, Y ), atom( Z ) ) ) ],
% 0.74/1.14 [ =( x2( y( X, Y ), x( Z, T ) ), x( y( X, Y ), x( Z, T ) ) ) ],
% 0.74/1.14 [ =( x2( y( X, Y ), y( Z, T ) ), x( y( X, Y ), y( Z, T ) ) ) ],
% 0.74/1.14 [ =( x2( y( X, Y ), star( Z ) ), x( y( X, Y ), star( Z ) ) ) ],
% 0.74/1.14 [ =( x2( star( X ), nil4 ), star( X ) ) ],
% 0.74/1.14 [ =( x2( star( X ), eps ), x( star( X ), eps ) ) ],
% 0.74/1.14 [ =( x2( star( X ), atom( Y ) ), x( star( X ), atom( Y ) ) ) ],
% 0.74/1.14 [ =( x2( star( X ), x( Y, Z ) ), x( star( X ), x( Y, Z ) ) ) ],
% 0.74/1.14 [ =( x2( star( X ), y( Y, Z ) ), x( star( X ), y( Y, Z ) ) ) ],
% 0.74/1.14 [ =( x2( star( X ), star( Y ) ), x( star( X ), star( Y ) ) ) ],
% 0.74/1.14 [ =( splits( X, nil ), nil ) ],
% 0.74/1.14 [ =( splits( X, cons( pair2( Y, Z ), T ) ), cons( pair2( cons2( X, Y ),
% 0.74/1.14 Z ), splits( X, T ) ) ) ],
% 0.74/1.14 [ =( splits2( nil2 ), cons( pair2( nil2, nil2 ), nil ) ) ],
% 0.74/1.14 [ =( splits2( cons2( X, Y ) ), cons( pair2( nil2, cons2( X, Y ) ),
% 0.74/1.14 splits( X, splits2( Y ) ) ) ) ],
% 57.46/57.99 [ =( orb( btrue, X ), btrue ) ],
% 57.46/57.99 [ =( orb( bfalse, X ), X ) ],
% 57.46/57.99 [ =( or2( nil3 ), bfalse ) ],
% 57.46/57.99 [ =( or2( cons3( X, Y ) ), orb( X, or2( Y ) ) ) ],
% 57.46/57.99 [ =( notb( btrue ), bfalse ) ],
% 57.46/57.99 [ =( notb( bfalse ), btrue ) ],
% 57.46/57.99 [ =( andb( btrue, X ), X ) ],
% 57.46/57.99 [ =( andb( bfalse, X ), bfalse ) ],
% 57.46/57.99 [ =( eps2( eps ), btrue ) ],
% 57.46/57.99 [ =( eps2( x( X, Y ) ), orb( eps2( X ), eps2( Y ) ) ) ],
% 57.46/57.99 [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) ) ],
% 57.46/57.99 [ =( eps2( star( X ) ), btrue ) ],
% 57.46/57.99 [ =( eps2( nil4 ), bfalse ) ],
% 57.46/57.99 [ =( eps2( atom( X ) ), bfalse ) ],
% 57.46/57.99 [ =( step( atom( X ), Y ), aux( Y, X, eq( X, Y ) ) ) ],
% 57.46/57.99 [ =( step( x( X, Y ), Z ), x( step( X, Z ), step( Y, Z ) ) ) ],
% 57.46/57.99 [ =( step( y( X, Y ), Z ), aux2( Z, X, Y, eps2( X ) ) ) ],
% 57.46/57.99 [ =( step( star( X ), Y ), y( step( X, Y ), star( X ) ) ) ],
% 57.46/57.99 [ =( step( nil4, X ), nil4 ) ],
% 57.46/57.99 [ =( step( eps, X ), nil4 ) ],
% 57.46/57.99 [ =( rec( X, nil2 ), eps2( X ) ) ],
% 57.46/57.99 [ =( rec( X, cons2( Y, Z ) ), rec( step( X, Y ), Z ) ) ],
% 57.46/57.99 [ =( reck( X, Y, nil ), nil3 ) ],
% 57.46/57.99 [ =( reck( X, Y, cons( pair2( Z, T ), U ) ), cons3( andb( reck2( X, Z )
% 57.46/57.99 , rec( Y, T ) ), reck( X, Y, U ) ) ) ],
% 57.46/57.99 [ =( reck2( nil4, X ), bfalse ) ],
% 57.46/57.99 [ =( reck2( eps, nil2 ), btrue ) ],
% 57.46/57.99 [ =( reck2( eps, cons2( X, Y ) ), bfalse ) ],
% 57.46/57.99 [ =( reck2( atom( X ), nil2 ), bfalse ) ],
% 57.46/57.99 [ =( reck2( atom( X ), cons2( Y, nil2 ) ), eq( X, Y ) ) ],
% 57.46/57.99 [ =( reck2( atom( X ), cons2( Y, cons2( Z, T ) ) ), bfalse ) ],
% 57.46/57.99 [ =( reck2( x( X, Y ), Z ), orb( reck2( X, Z ), reck2( Y, Z ) ) ) ],
% 57.46/57.99 [ =( reck2( y( X, Y ), Z ), or2( reck( X, Y, splits2( Z ) ) ) ) ],
% 57.46/57.99 [ =( reck2( star( X ), nil2 ), btrue ) ],
% 57.46/57.99 [ =( reck2( star( X ), cons2( Y, Z ) ), aux3( X, Y, Z, notb( eps2( X ) )
% 57.46/57.99 ) ) ],
% 57.46/57.99 [ =( 'prop_kfind1'( X ), notb( reck2( X, cons2( a, cons2( b, cons2( b,
% 57.46/57.99 nil2 ) ) ) ) ) ) ],
% 57.46/57.99 [ =( eq( a, b ), bfalse ) ],
% 57.46/57.99 [ =( eq( a, c ), bfalse ) ],
% 57.46/57.99 [ =( eq( b, a ), bfalse ) ],
% 57.46/57.99 [ =( eq( b, c ), bfalse ) ],
% 57.46/57.99 [ =( eq( c, a ), bfalse ) ],
% 57.46/57.99 [ =( eq( c, b ), bfalse ) ],
% 57.46/57.99 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 57.46/57.99 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 57.46/57.99 [ =( eq( X, X ), btrue ) ],
% 57.46/57.99 [ =( eq2( X, X ), btrue ) ],
% 57.46/57.99 [ ~( =( eq2( 'prop_kfind1'( X ), bfalse ), btrue ) ) ]
% 57.46/57.99 ] .
% 57.46/57.99
% 57.46/57.99
% 57.46/57.99 percentage equality = 1.000000, percentage horn = 1.000000
% 57.46/57.99 This is a pure equality problem
% 57.46/57.99
% 57.46/57.99
% 57.46/57.99
% 57.46/57.99 Options Used:
% 57.46/57.99
% 57.46/57.99 useres = 1
% 57.46/57.99 useparamod = 1
% 57.46/57.99 useeqrefl = 1
% 57.46/57.99 useeqfact = 1
% 57.46/57.99 usefactor = 1
% 57.46/57.99 usesimpsplitting = 0
% 57.46/57.99 usesimpdemod = 5
% 57.46/57.99 usesimpres = 3
% 57.46/57.99
% 57.46/57.99 resimpinuse = 1000
% 57.46/57.99 resimpclauses = 20000
% 57.46/57.99 substype = eqrewr
% 57.46/57.99 backwardsubs = 1
% 57.46/57.99 selectoldest = 5
% 57.46/57.99
% 57.46/57.99 litorderings [0] = split
% 57.46/57.99 litorderings [1] = extend the termordering, first sorting on arguments
% 57.46/57.99
% 57.46/57.99 termordering = kbo
% 57.46/57.99
% 57.46/57.99 litapriori = 0
% 57.46/57.99 termapriori = 1
% 57.46/57.99 litaposteriori = 0
% 57.46/57.99 termaposteriori = 0
% 57.46/57.99 demodaposteriori = 0
% 57.46/57.99 ordereqreflfact = 0
% 57.46/57.99
% 57.46/57.99 litselect = negord
% 57.46/57.99
% 57.46/57.99 maxweight = 15
% 57.46/57.99 maxdepth = 30000
% 57.46/57.99 maxlength = 115
% 57.46/57.99 maxnrvars = 195
% 57.46/57.99 excuselevel = 1
% 57.46/57.99 increasemaxweight = 1
% 57.46/57.99
% 57.46/57.99 maxselected = 10000000
% 57.46/57.99 maxnrclauses = 10000000
% 57.46/57.99
% 57.46/57.99 showgenerated = 0
% 57.46/57.99 showkept = 0
% 57.46/57.99 showselected = 0
% 57.46/57.99 showdeleted = 0
% 57.46/57.99 showresimp = 1
% 57.46/57.99 showstatus = 2000
% 57.46/57.99
% 57.46/57.99 prologoutput = 1
% 57.46/57.99 nrgoals = 5000000
% 57.46/57.99 totalproof = 1
% 57.46/57.99
% 57.46/57.99 Symbols occurring in the translation:
% 57.46/57.99
% 57.46/57.99 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 57.46/57.99 . [1, 2] (w:1, o:52, a:1, s:1, b:0),
% 57.46/57.99 ! [4, 1] (w:0, o:40, a:1, s:1, b:0),
% 57.46/57.99 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 57.46/57.99 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 57.46/57.99 btrue [41, 0] (w:1, o:20, a:1, s:1, b:0),
% 57.46/57.99 aux [42, 3] (w:1, o:93, a:1, s:1, b:0),
% 57.46/57.99 eps [43, 0] (w:1, o:21, a:1, s:1, b:0),
% 57.46/57.99 bfalse [44, 0] (w:1, o:22, a:1, s:1, b:0),
% 57.46/57.99 nil4 [45, 0] (w:1, o:24, a:1, s:1, b:0),
% 57.46/57.99 aux2 [48, 4] (w:1, o:95, a:1, s:1, b:0),
% 57.46/57.99 step [49, 2] (w:1, o:79, a:1, s:1, b:0),
% 57.46/57.99 y [50, 2] (w:1, o:82, a:1, s:1, b:0),
% 57.46/57.99 x [51, 2] (w:1, o:80, a:1, s:1, b:0),
% 57.46/57.99 aux3 [55, 4] (w:1, o:96, a:1, s:1, b:0),
% 57.46/57.99 star [56, 1] (w:1, o:45, a:1, s:1, b:0),
% 108.62/109.16 cons2 [57, 2] (w:1, o:83, a:1, s:1, b:0),
% 108.62/109.16 rec [58, 2] (w:1, o:77, a:1, s:1, b:0),
% 108.62/109.16 z [59, 2] (w:1, o:84, a:1, s:1, b:0),
% 108.62/109.16 atom [61, 1] (w:1, o:46, a:1, s:1, b:0),
% 108.62/109.16 x2 [65, 2] (w:1, o:81, a:1, s:1, b:0),
% 108.62/109.16 nil [66, 0] (w:1, o:30, a:1, s:1, b:0),
% 108.62/109.16 splits [67, 2] (w:1, o:85, a:1, s:1, b:0),
% 108.62/109.16 pair2 [70, 2] (w:1, o:87, a:1, s:1, b:0),
% 108.62/109.16 cons [71, 2] (w:1, o:88, a:1, s:1, b:0),
% 108.62/109.16 nil2 [72, 0] (w:1, o:34, a:1, s:1, b:0),
% 108.62/109.16 splits2 [73, 1] (w:1, o:47, a:1, s:1, b:0),
% 108.62/109.16 orb [76, 2] (w:1, o:86, a:1, s:1, b:0),
% 108.62/109.16 nil3 [77, 0] (w:1, o:23, a:1, s:1, b:0),
% 108.62/109.16 or2 [78, 1] (w:1, o:49, a:1, s:1, b:0),
% 108.62/109.16 cons3 [79, 2] (w:1, o:89, a:1, s:1, b:0),
% 108.62/109.16 notb [80, 1] (w:1, o:48, a:1, s:1, b:0),
% 108.62/109.16 andb [81, 2] (w:1, o:90, a:1, s:1, b:0),
% 108.62/109.16 eps2 [82, 1] (w:1, o:50, a:1, s:1, b:0),
% 108.62/109.16 eq [84, 2] (w:1, o:91, a:1, s:1, b:0),
% 108.62/109.16 reck [86, 3] (w:1, o:94, a:1, s:1, b:0),
% 108.62/109.16 reck2 [88, 2] (w:1, o:78, a:1, s:1, b:0),
% 108.62/109.16 'prop_kfind1' [92, 1] (w:1, o:51, a:1, s:1, b:0),
% 108.62/109.16 a [93, 0] (w:1, o:19, a:1, s:1, b:0),
% 108.62/109.16 b [94, 0] (w:1, o:38, a:1, s:1, b:0),
% 108.62/109.16 c [95, 0] (w:1, o:39, a:1, s:1, b:0),
% 108.62/109.16 eq2 [96, 2] (w:1, o:92, a:1, s:1, b:0).
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Starting Search:
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 6427
% 108.62/109.16 Kept: 2003
% 108.62/109.16 Inuse: 431
% 108.62/109.16 Deleted: 118
% 108.62/109.16 Deletedinuse: 24
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 22528
% 108.62/109.16 Kept: 4003
% 108.62/109.16 Inuse: 883
% 108.62/109.16 Deleted: 412
% 108.62/109.16 Deletedinuse: 43
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 35110
% 108.62/109.16 Kept: 6003
% 108.62/109.16 Inuse: 1205
% 108.62/109.16 Deleted: 530
% 108.62/109.16 Deletedinuse: 53
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 62558
% 108.62/109.16 Kept: 8003
% 108.62/109.16 Inuse: 1713
% 108.62/109.16 Deleted: 653
% 108.62/109.16 Deletedinuse: 73
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 111170
% 108.62/109.16 Kept: 10004
% 108.62/109.16 Inuse: 2221
% 108.62/109.16 Deleted: 1060
% 108.62/109.16 Deletedinuse: 161
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 167974
% 108.62/109.16 Kept: 12004
% 108.62/109.16 Inuse: 2665
% 108.62/109.16 Deleted: 1223
% 108.62/109.16 Deletedinuse: 169
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 209575
% 108.62/109.16 Kept: 14006
% 108.62/109.16 Inuse: 3082
% 108.62/109.16 Deleted: 1339
% 108.62/109.16 Deletedinuse: 199
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 259536
% 108.62/109.16 Kept: 16007
% 108.62/109.16 Inuse: 3532
% 108.62/109.16 Deleted: 1592
% 108.62/109.16 Deletedinuse: 255
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 403115
% 108.62/109.16 Kept: 18007
% 108.62/109.16 Inuse: 4548
% 108.62/109.16 Deleted: 3026
% 108.62/109.16 Deletedinuse: 460
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying clauses:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 570795
% 108.62/109.16 Kept: 20008
% 108.62/109.16 Inuse: 5923
% 108.62/109.16 Deleted: 6885
% 108.62/109.16 Deletedinuse: 555
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 759402
% 108.62/109.16 Kept: 22009
% 108.62/109.16 Inuse: 7728
% 108.62/109.16 Deleted: 7002
% 108.62/109.16 Deletedinuse: 652
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 996204
% 108.62/109.16 Kept: 24009
% 108.62/109.16 Inuse: 9106
% 108.62/109.16 Deleted: 7333
% 108.62/109.16 Deletedinuse: 778
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 1620888
% 108.62/109.16 Kept: 26009
% 108.62/109.16 Inuse: 15065
% 108.62/109.16 Deleted: 7710
% 108.62/109.16 Deletedinuse: 852
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Failed to find proof!
% 108.62/109.16 maxweight = 15
% 108.62/109.16 maxnrclauses = 10000000
% 108.62/109.16 Generated: 1953468
% 108.62/109.16 Kept: 27338
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 The strategy used was not complete!
% 108.62/109.16
% 108.62/109.16 Increased maxweight to 16
% 108.62/109.16
% 108.62/109.16 Starting Search:
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 5879
% 108.62/109.16 Kept: 2005
% 108.62/109.16 Inuse: 408
% 108.62/109.16 Deleted: 112
% 108.62/109.16 Deletedinuse: 24
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16 Resimplifying inuse:
% 108.62/109.16 Done
% 108.62/109.16
% 108.62/109.16
% 108.62/109.16 Intermediate Status:
% 108.62/109.16 Generated: 17992
% 108.62/109.16 Kept: 4005
% 108.62/109.16 Inuse: 748
% 108.62/109.16 Deleted: 362
% 108.62/109.16 Deletedinuse: 25
% 108.62/109.16
% 108.62/109.16 ResimpTerminated
% 299.52/300.03 Bliksem ended
%------------------------------------------------------------------------------