%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX242-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n023.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:53 PM UTC 2026
% Result : Timeout 291.44s 291.89s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX242-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.17/0.35 % Computer : n023.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % DateTime : Tue May 5 13:29:53 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.84/1.24 *** allocated 10000 integers for termspace/termends
% 0.84/1.24 *** allocated 10000 integers for clauses
% 0.84/1.24 *** allocated 10000 integers for justifications
% 0.84/1.24 Bliksem 1.12
% 0.84/1.24
% 0.84/1.24
% 0.84/1.24 Automatic Strategy Selection
% 0.84/1.24
% 0.84/1.24 Clauses:
% 0.84/1.24 [
% 0.84/1.24 [ =( aux( X, Y, Z, btrue ), Y ) ],
% 0.84/1.24 [ =( aux( X, Y, Z, bfalse ), var( Z ) ) ],
% 0.84/1.24 [ =( aux2( X, Y, Z, T, btrue ), Y ) ],
% 0.84/1.24 [ =( aux2( X, Y, Z, T, bfalse ), apply1( Z, T ) ) ],
% 0.84/1.24 [ =( aux3( X, Y, Z, T, U, W, V0, btrue ), unifyloop( X, append( T, Y ),
% 0.84/1.24 append( V0, U ) ) ) ],
% 0.84/1.24 [ =( aux3( X, Y, Z, T, U, W, V0, bfalse ), fail( X, cons( app( W, V0 ),
% 0.84/1.24 U ), app( Z, T ), Y ) ) ],
% 0.84/1.24 [ =( aux4( X, Y, Z, T, U, W, btrue ), nothing ) ],
% 0.84/1.24 [ =( aux4( X, Y, Z, T, U, W, bfalse ), unifybind( X, Y, app( U, W ), Z,
% 0.84/1.24 T ) ) ],
% 0.84/1.24 [ =( aux5( X, Y, Z, T, U, btrue ), unifyloop( X, Z, T ) ) ],
% 0.84/1.24 [ =( aux5( X, Y, Z, T, U, bfalse ), unifybind( X, Y, var( U ), Z, T ) )
% 0.84/1.24 ],
% 0.84/1.24 [ =( aux6( X, Y, nothing ), btrue ) ],
% 0.84/1.24 [ =( aux6( X, Y, just( Z ) ), eq3( subst( Z, X ), subst( Z, Y ) ) ) ]
% 0.84/1.24 ,
% 0.84/1.24 [ =( aux7( X, Y, Z, T, btrue ), Z ) ],
% 0.84/1.24 [ =( aux7( X, Y, Z, T, bfalse ), subst( lam( Y, Z ), apply1( X, T ) ) )
% 0.84/1.24 ],
% 0.84/1.24 [ =( fail( X, nil, Y, Z ), nothing ) ],
% 0.84/1.24 [ =( fail( X, cons( app( Y, Z ), T ), U, W ), nothing ) ],
% 0.84/1.24 [ =( fail( X, cons( var( Y ), Z ), T, U ), unifyvar( X, Y, T, U, Z ) ) ]
% 0.84/1.24 ,
% 0.84/1.24 [ =( sub( X, Y, Z ), lam2( X, Y, Z ) ) ],
% 0.84/1.24 [ =( subst( X, app( Y, Z ) ), app( Y, substList( X, Z ) ) ) ],
% 0.84/1.24 [ =( subst( X, var( Y ) ), apply1( X, Y ) ) ],
% 0.84/1.24 [ =( substList( X, nil ), nil ) ],
% 0.84/1.24 [ =( substList( X, cons( Y, Z ) ), cons( subst( X, Y ), substList( X, Z
% 0.84/1.24 ) ) ) ],
% 0.84/1.24 [ =( substSubst( X, Y, Z ), subst( X, apply1( Y, Z ) ) ) ],
% 0.84/1.24 [ =( singleton( X, Y, Z ), aux( X, Y, Z, eq2( X, Z ) ) ) ],
% 0.84/1.24 [ =( orb( btrue, X ), btrue ) ],
% 0.84/1.24 [ =( orb( bfalse, X ), X ) ],
% 0.84/1.24 [ =( unify( X, nil ), bfalse ) ],
% 0.84/1.24 [ =( unify( X, cons( Y, Z ) ), orb( unifyoccurs( X, Y ), unify( X, Z ) )
% 0.84/1.24 ) ],
% 0.84/1.24 [ =( unifyoccurs( X, app( Y, Z ) ), unify( X, Z ) ) ],
% 0.84/1.24 [ =( unifyoccurs( X, var( Y ) ), eq2( X, Y ) ) ],
% 0.84/1.24 [ =( extend( X, Y, Z, T ), aux2( X, Y, Z, T, eq2( X, T ) ) ) ],
% 0.84/1.24 [ =( unifyloop( X, nil, nil ), just( X ) ) ],
% 0.84/1.24 [ =( unifyloop( X, nil, cons( Y, Z ) ), nothing ) ],
% 0.84/1.24 [ =( unifyloop( X, cons( app( Y, Z ), T ), nil ), fail( X, nil, app( Y,
% 0.84/1.24 Z ), T ) ) ],
% 0.84/1.24 [ =( unifyloop( X, cons( app( Y, Z ), T ), cons( app( U, W ), V0 ) ),
% 0.84/1.24 aux3( X, T, Y, Z, V0, U, W, eq2( Y, U ) ) ) ],
% 0.84/1.24 [ =( unifyloop( X, cons( app( Y, Z ), T ), cons( var( U ), W ) ), fail(
% 0.84/1.24 X, cons( var( U ), W ), app( Y, Z ), T ) ) ],
% 0.84/1.24 [ =( unifyloop( X, cons( var( Y ), Z ), nil ), fail( X, nil, var( Y ), Z
% 0.84/1.24 ) ) ],
% 0.84/1.24 [ =( unifyloop( X, cons( var( Y ), Z ), cons( T, U ) ), unifyvar( X, Y,
% 0.84/1.24 T, Z, U ) ) ],
% 0.84/1.24 [ =( unifyvar( X, Y, app( Z, T ), U, W ), aux4( X, Y, U, W, Z, T,
% 0.84/1.24 unifyoccurs( Y, app( Z, T ) ) ) ) ],
% 0.84/1.24 [ =( unifyvar( X, Y, var( Z ), T, U ), aux5( X, Y, T, U, Z, eq2( Y, Z )
% 0.84/1.24 ) ) ],
% 0.84/1.24 [ =( unifybind( X, Y, Z, T, U ), unifyloop( sub( X, Y, Z ), substList(
% 0.84/1.24 sub( X, Y, Z ), T ), substList( sub( X, Y, Z ), U ) ) ) ],
% 0.84/1.24 [ =( unify2( X, Y ), unifyloop( lam3, cons( X, nil ), cons( Y, nil ) ) )
% 0.84/1.24 ],
% 0.84/1.24 [ =( unificationOK( X, Y ), aux6( X, Y, unify2( X, Y ) ) ) ],
% 0.84/1.24 [ =( 'prop_unify_makes_equal'( X, Y ), eq4( unificationOK( X, Y ), btrue
% 0.84/1.24 ) ) ],
% 0.84/1.24 [ =( isJust2( nothing ), bfalse ) ],
% 0.84/1.24 [ =( isJust2( just( X ) ), btrue ) ],
% 0.84/1.24 [ =( append( nil, X ), X ) ],
% 0.84/1.24 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 0.84/1.24 [ =( eq2( a, b ), bfalse ) ],
% 0.84/1.24 [ =( eq2( a, c ), bfalse ) ],
% 0.84/1.24 [ =( eq2( b, a ), bfalse ) ],
% 0.84/1.24 [ =( eq2( b, c ), bfalse ) ],
% 0.84/1.24 [ =( eq2( c, a ), bfalse ) ],
% 0.84/1.24 [ =( eq2( c, b ), bfalse ) ],
% 0.84/1.24 [ =( eq4( bfalse, btrue ), bfalse ) ],
% 0.84/1.24 [ =( eq4( btrue, bfalse ), bfalse ) ],
% 0.84/1.24 [ =( eq2( X, X ), btrue ) ],
% 0.84/1.24 [ =( eq3( X, X ), btrue ) ],
% 0.84/1.24 [ =( eq4( X, X ), btrue ) ],
% 0.84/1.24 [ =( eq( X, X ), btrue ) ],
% 0.84/1.24 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq( cons( X, Z ), cons( Y, T ) ),
% 0.84/1.24 bfalse ) ],
% 0.84/1.24 [ ~( =( eq3( X, Y ), btrue ) ), =( eq( cons( X, Z ), cons( Y, T ) ), eq(
% 0.84/1.24 Z, T ) ) ],
% 0.84/1.24 [ =( eq( nil, cons( X, Y ) ), bfalse ) ],
% 0.84/1.24 [ =( eq( cons( X, Y ), nil ), bfalse ) ],
% 24.55/24.93 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq3( app( X, Z ), app( Y, T ) ),
% 24.55/24.93 bfalse ) ],
% 24.55/24.93 [ ~( =( eq2( X, Y ), btrue ) ), =( eq3( app( X, Z ), app( Y, T ) ), eq(
% 24.55/24.93 Z, T ) ) ],
% 24.55/24.93 [ =( eq3( var( X ), var( Y ) ), eq2( X, Y ) ) ],
% 24.55/24.93 [ =( eq3( app( X, Y ), var( Z ) ), bfalse ) ],
% 24.55/24.93 [ =( eq3( var( X ), app( Y, Z ) ), bfalse ) ],
% 24.55/24.93 [ =( apply1( lam2( X, Y, Z ), T ), aux7( X, Y, Z, T, eq2( Y, T ) ) ) ]
% 24.55/24.93 ,
% 24.55/24.93 [ =( apply1( lam( X, Y ), Z ), singleton( X, Y, Z ) ) ],
% 24.55/24.93 [ =( apply1( lam3, X ), var( X ) ) ],
% 24.55/24.93 [ ~( =( eq4( 'prop_unify_makes_equal'( X, Y ), bfalse ), btrue ) ) ]
% 24.55/24.93 ] .
% 24.55/24.93
% 24.55/24.93
% 24.55/24.93 percentage equality = 1.000000, percentage horn = 1.000000
% 24.55/24.93 This is a pure equality problem
% 24.55/24.93
% 24.55/24.93
% 24.55/24.93
% 24.55/24.93 Options Used:
% 24.55/24.93
% 24.55/24.93 useres = 1
% 24.55/24.93 useparamod = 1
% 24.55/24.93 useeqrefl = 1
% 24.55/24.93 useeqfact = 1
% 24.55/24.93 usefactor = 1
% 24.55/24.93 usesimpsplitting = 0
% 24.55/24.93 usesimpdemod = 5
% 24.55/24.93 usesimpres = 3
% 24.55/24.93
% 24.55/24.93 resimpinuse = 1000
% 24.55/24.93 resimpclauses = 20000
% 24.55/24.93 substype = eqrewr
% 24.55/24.93 backwardsubs = 1
% 24.55/24.93 selectoldest = 5
% 24.55/24.93
% 24.55/24.93 litorderings [0] = split
% 24.55/24.93 litorderings [1] = extend the termordering, first sorting on arguments
% 24.55/24.93
% 24.55/24.93 termordering = kbo
% 24.55/24.93
% 24.55/24.93 litapriori = 0
% 24.55/24.93 termapriori = 1
% 24.55/24.93 litaposteriori = 0
% 24.55/24.93 termaposteriori = 0
% 24.55/24.93 demodaposteriori = 0
% 24.55/24.93 ordereqreflfact = 0
% 24.55/24.93
% 24.55/24.93 litselect = negord
% 24.55/24.93
% 24.55/24.93 maxweight = 15
% 24.55/24.93 maxdepth = 30000
% 24.55/24.93 maxlength = 115
% 24.55/24.93 maxnrvars = 195
% 24.55/24.93 excuselevel = 1
% 24.55/24.93 increasemaxweight = 1
% 24.55/24.93
% 24.55/24.93 maxselected = 10000000
% 24.55/24.93 maxnrclauses = 10000000
% 24.55/24.93
% 24.55/24.93 showgenerated = 0
% 24.55/24.93 showkept = 0
% 24.55/24.93 showselected = 0
% 24.55/24.93 showdeleted = 0
% 24.55/24.93 showresimp = 1
% 24.55/24.93 showstatus = 2000
% 24.55/24.93
% 24.55/24.93 prologoutput = 1
% 24.55/24.93 nrgoals = 5000000
% 24.55/24.93 totalproof = 1
% 24.55/24.93
% 24.55/24.93 Symbols occurring in the translation:
% 24.55/24.93
% 24.55/24.93 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 24.55/24.93 . [1, 2] (w:1, o:49, a:1, s:1, b:0),
% 24.55/24.93 ! [4, 1] (w:0, o:41, a:1, s:1, b:0),
% 24.55/24.93 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 24.55/24.93 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 24.55/24.93 btrue [42, 0] (w:1, o:25, a:1, s:1, b:0),
% 24.55/24.93 aux [43, 4] (w:1, o:97, a:1, s:1, b:0),
% 24.55/24.94 bfalse [44, 0] (w:1, o:26, a:1, s:1, b:0),
% 24.55/24.94 var [45, 1] (w:1, o:46, a:1, s:1, b:0),
% 24.55/24.94 aux2 [47, 5] (w:1, o:100, a:1, s:1, b:0),
% 24.55/24.94 apply1 [48, 2] (w:1, o:74, a:1, s:1, b:0),
% 24.55/24.94 aux3 [55, 8] (w:1, o:106, a:1, s:1, b:0),
% 24.55/24.94 append [56, 2] (w:1, o:75, a:1, s:1, b:0),
% 24.55/24.94 unifyloop [57, 3] (w:1, o:91, a:1, s:1, b:0),
% 24.55/24.94 app [58, 2] (w:1, o:76, a:1, s:1, b:0),
% 24.55/24.94 cons [59, 2] (w:1, o:77, a:1, s:1, b:0),
% 24.55/24.94 fail [60, 4] (w:1, o:99, a:1, s:1, b:0),
% 24.55/24.94 aux4 [64, 7] (w:1, o:105, a:1, s:1, b:0),
% 24.55/24.94 nothing [65, 0] (w:1, o:35, a:1, s:1, b:0),
% 24.55/24.94 unifybind [66, 5] (w:1, o:101, a:1, s:1, b:0),
% 24.55/24.94 aux5 [68, 6] (w:1, o:104, a:1, s:1, b:0),
% 24.55/24.94 aux6 [69, 3] (w:1, o:92, a:1, s:1, b:0),
% 24.55/24.94 just [71, 1] (w:1, o:48, a:1, s:1, b:0),
% 24.55/24.94 subst [72, 2] (w:1, o:78, a:1, s:1, b:0),
% 24.55/24.94 eq3 [73, 2] (w:1, o:80, a:1, s:1, b:0),
% 24.55/24.94 aux7 [74, 5] (w:1, o:102, a:1, s:1, b:0),
% 24.55/24.94 lam [75, 2] (w:1, o:81, a:1, s:1, b:0),
% 24.55/24.94 nil [76, 0] (w:1, o:36, a:1, s:1, b:0),
% 24.55/24.94 unifyvar [80, 5] (w:1, o:103, a:1, s:1, b:0),
% 24.55/24.94 sub [81, 3] (w:1, o:93, a:1, s:1, b:0),
% 24.55/24.94 lam2 [82, 3] (w:1, o:94, a:1, s:1, b:0),
% 24.55/24.94 substList [84, 2] (w:1, o:82, a:1, s:1, b:0),
% 24.55/24.94 substSubst [85, 3] (w:1, o:95, a:1, s:1, b:0),
% 24.55/24.94 singleton [86, 3] (w:1, o:96, a:1, s:1, b:0),
% 24.55/24.94 eq2 [87, 2] (w:1, o:79, a:1, s:1, b:0),
% 24.55/24.94 orb [89, 2] (w:1, o:83, a:1, s:1, b:0),
% 24.55/24.94 unify [90, 2] (w:1, o:84, a:1, s:1, b:0),
% 24.55/24.94 unifyoccurs [91, 2] (w:1, o:85, a:1, s:1, b:0),
% 24.55/24.94 extend [92, 4] (w:1, o:98, a:1, s:1, b:0),
% 24.55/24.94 unify2 [97, 2] (w:1, o:86, a:1, s:1, b:0),
% 24.55/24.94 lam3 [98, 0] (w:1, o:38, a:1, s:1, b:0),
% 24.55/24.94 unificationOK [99, 2] (w:1, o:87, a:1, s:1, b:0),
% 24.55/24.94 'prop_unify_makes_equal' [100, 2] (w:1, o:88, a:1, s:1, b:0),
% 24.55/24.94 eq4 [101, 2] (w:1, o:89, a:1, s:1, b:0),
% 24.55/24.94 isJust2 [102, 1] (w:1, o:47, a:1, s:1, b:0),
% 24.55/24.94 a [103, 0] (w:1, o:24, a:1, s:1, b:0),
% 24.55/24.94 b [104, 0] (w:1, o:39, a:1, s:1, b:0),
% 24.55/24.94 c [105, 0] (w:1, o:40, a:1, s:1, b:0),
% 89.55/89.92 eq [106, 2] (w:1, o:90, a:1, s:1, b:0).
% 89.55/89.92
% 89.55/89.92
% 89.55/89.92 Starting Search:
% 89.55/89.92
% 89.55/89.92 Resimplifying inuse:
% 89.55/89.92 Done
% 89.55/89.92
% 89.55/89.92 Failed to find proof!
% 89.55/89.92 maxweight = 15
% 89.55/89.92 maxnrclauses = 10000000
% 89.55/89.92 Generated: 6202
% 89.55/89.92 Kept: 517
% 89.55/89.92
% 89.55/89.92
% 89.55/89.92 The strategy used was not complete!
% 89.55/89.92
% 89.55/89.92 Increased maxweight to 16
% 89.55/89.92
% 89.55/89.92 Starting Search:
% 89.55/89.92
% 89.55/89.92 Resimplifying inuse:
% 89.55/89.92 Done
% 89.55/89.92
% 89.55/89.92 Failed to find proof!
% 89.55/89.92 maxweight = 16
% 89.55/89.92 maxnrclauses = 10000000
% 89.55/89.92 Generated: 7166
% 89.55/89.92 Kept: 610
% 89.55/89.92
% 89.55/89.92
% 89.55/89.92 The strategy used was not complete!
% 89.55/89.92
% 89.55/89.92 Increased maxweight to 17
% 89.55/89.92
% 89.55/89.92 Starting Search:
% 89.55/89.92
% 89.55/89.92 Resimplifying inuse:
% 89.55/89.92 Done
% 89.55/89.92
% 89.55/89.92 Failed to find proof!
% 89.55/89.92 maxweight = 17
% 89.55/89.92 maxnrclauses = 10000000
% 89.55/89.92 Generated: 13378
% 89.55/89.92 Kept: 995
% 89.55/89.92
% 89.55/89.92
% 89.55/89.92 The strategy used was not complete!
% 89.55/89.92
% 89.55/89.92 Increased maxweight to 18
% 89.55/89.92
% 89.55/89.92 Starting Search:
% 89.55/89.92
% 89.55/89.92 Resimplifying inuse:
% 89.55/89.92 Done
% 89.55/89.92
% 89.55/89.92 Resimplifying inuse:
% 89.55/89.92 Done
% 89.55/89.92
% 89.55/89.92 Failed to find proof!
% 89.55/89.92 maxweight = 18
% 89.55/89.92 maxnrclauses = 10000000
% 89.55/89.92 Generated: 23399
% 89.55/89.92 Kept: 1620
% 89.55/89.92
% 89.55/89.92
% 89.55/89.92 The strategy used was not complete!
% 89.55/89.92
% 89.55/89.92 Increased maxweight to 19
% 89.55/89.92
% 89.55/89.92 Starting Search:
% 89.55/89.92
% 89.55/89.92 Resimplifying inuse:
% 89.55/89.92 Done
% 89.55/89.92
% 89.55/89.92
% 89.55/89.92 Intermediate Status:
% 89.55/89.92 Generated: 16957
% 89.55/89.92 Kept: 2003
% 89.55/89.92 Inuse: 907
% 89.55/89.92 Deleted: 34
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Failed to find proof!
% 89.55/89.93 maxweight = 19
% 89.55/89.93 maxnrclauses = 10000000
% 89.55/89.93 Generated: 55978
% 89.55/89.93 Kept: 2741
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 The strategy used was not complete!
% 89.55/89.93
% 89.55/89.93 Increased maxweight to 20
% 89.55/89.93
% 89.55/89.93 Starting Search:
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 13250
% 89.55/89.93 Kept: 2016
% 89.55/89.93 Inuse: 740
% 89.55/89.93 Deleted: 16
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 86430
% 89.55/89.93 Kept: 4027
% 89.55/89.93 Inuse: 2779
% 89.55/89.93 Deleted: 255
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Failed to find proof!
% 89.55/89.93 maxweight = 20
% 89.55/89.93 maxnrclauses = 10000000
% 89.55/89.93 Generated: 122898
% 89.55/89.93 Kept: 4093
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 The strategy used was not complete!
% 89.55/89.93
% 89.55/89.93 Increased maxweight to 21
% 89.55/89.93
% 89.55/89.93 Starting Search:
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 13306
% 89.55/89.93 Kept: 2054
% 89.55/89.93 Inuse: 774
% 89.55/89.93 Deleted: 16
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 29761
% 89.55/89.93 Kept: 4055
% 89.55/89.93 Inuse: 1288
% 89.55/89.93 Deleted: 84
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 67468
% 89.55/89.93 Kept: 6055
% 89.55/89.93 Inuse: 2303
% 89.55/89.93 Deleted: 201
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Failed to find proof!
% 89.55/89.93 maxweight = 21
% 89.55/89.93 maxnrclauses = 10000000
% 89.55/89.93 Generated: 299739
% 89.55/89.93 Kept: 7408
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 The strategy used was not complete!
% 89.55/89.93
% 89.55/89.93 Increased maxweight to 22
% 89.55/89.93
% 89.55/89.93 Starting Search:
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 15176
% 89.55/89.93 Kept: 2269
% 89.55/89.93 Inuse: 829
% 89.55/89.93 Deleted: 16
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 26455
% 89.55/89.93 Kept: 4270
% 89.55/89.93 Inuse: 1125
% 89.55/89.93 Deleted: 46
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 41149
% 89.55/89.93 Kept: 6271
% 89.55/89.93 Inuse: 1556
% 89.55/89.93 Deleted: 102
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 86578
% 89.55/89.93 Kept: 8272
% 89.55/89.93 Inuse: 2582
% 89.55/89.93 Deleted: 273
% 89.55/89.93 Deletedinuse: 63
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 149182
% 89.55/89.93 Kept: 10273
% 89.55/89.93 Inuse: 3456
% 89.55/89.93 Deleted: 511
% 89.55/89.93 Deletedinuse: 63
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Failed to find proof!
% 89.55/89.93 maxweight = 22
% 89.55/89.93 maxnrclauses = 10000000
% 89.55/89.93 Generated: 746055
% 89.55/89.93 Kept: 11869
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 The strategy used was not complete!
% 89.55/89.93
% 89.55/89.93 Increased maxweight to 23
% 89.55/89.93
% 89.55/89.93 Starting Search:
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 11158
% 89.55/89.93 Kept: 2000
% 89.55/89.93 Inuse: 719
% 89.55/89.93 Deleted: 18
% 89.55/89.93 Deletedinuse: 9
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 24135
% 89.55/89.93 Kept: 4007
% 89.55/89.93 Inuse: 990
% 89.55/89.93 Deleted: 40
% 89.55/89.93 Deletedinuse: 11
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93 Resimplifying inuse:
% 89.55/89.93 Done
% 89.55/89.93
% 89.55/89.93
% 89.55/89.93 Intermediate Status:
% 89.55/89.93 Generated: 34683
% 89.55/89.93 Kept: 6018
% 89.55/89.93 Inuse: 1274
% 89.55/89.93 Deleted: 74
% 89.55/89.93 Deletedinuse: 11
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89
% 291.44/291.89 Intermediate Status:
% 291.44/291.89 Generated: 39840
% 291.44/291.89 Kept: 8031
% 291.44/291.89 Inuse: 1437
% 291.44/291.89 Deleted: 108
% 291.44/291.89 Deletedinuse: 11
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89
% 291.44/291.89 Intermediate Status:
% 291.44/291.89 Generated: 65619
% 291.44/291.89 Kept: 10038
% 291.44/291.89 Inuse: 1895
% 291.44/291.89 Deleted: 136
% 291.44/291.89 Deletedinuse: 11
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89
% 291.44/291.89 Intermediate Status:
% 291.44/291.89 Generated: 107119
% 291.44/291.89 Kept: 12040
% 291.44/291.89 Inuse: 2596
% 291.44/291.89 Deleted: 214
% 291.44/291.89 Deletedinuse: 41
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89
% 291.44/291.89 Intermediate Status:
% 291.44/291.89 Generated: 134674
% 291.44/291.89 Kept: 14042
% 291.44/291.89 Inuse: 3219
% 291.44/291.89 Deleted: 428
% 291.44/291.89 Deletedinuse: 41
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89
% 291.44/291.89 Intermediate Status:
% 291.44/291.89 Generated: 233783
% 291.44/291.89 Kept: 16043
% 291.44/291.89 Inuse: 4124
% 291.44/291.89 Deleted: 572
% 291.44/291.89 Deletedinuse: 43
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89 Resimplifying inuse:
% 291.44/291.89 Done
% 291.44/291.89
% 291.44/291.89
% 291.44/291.89 Intermediate Status:
% 291.44/291.89 Generated: 356409
% 291.44/291.89 Kept: 18044
% 291.44/291.89 Inuse: 5124
% 291.44/291.89 Deleted: 940
% 291.44/291.89 Deletedinuse: 46
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying clauses:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 500182
% 291.44/291.90 Kept: 20045
% 291.44/291.90 Inuse: 6505
% 291.44/291.90 Deleted: 6153
% 291.44/291.90 Deletedinuse: 53
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 1211620
% 291.44/291.90 Kept: 22045
% 291.44/291.90 Inuse: 10427
% 291.44/291.90 Deleted: 6189
% 291.44/291.90 Deletedinuse: 53
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Failed to find proof!
% 291.44/291.90 maxweight = 23
% 291.44/291.90 maxnrclauses = 10000000
% 291.44/291.90 Generated: 3033581
% 291.44/291.90 Kept: 22850
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 The strategy used was not complete!
% 291.44/291.90
% 291.44/291.90 Increased maxweight to 24
% 291.44/291.90
% 291.44/291.90 Starting Search:
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 10503
% 291.44/291.90 Kept: 2001
% 291.44/291.90 Inuse: 660
% 291.44/291.90 Deleted: 18
% 291.44/291.90 Deletedinuse: 9
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 22332
% 291.44/291.90 Kept: 4015
% 291.44/291.90 Inuse: 947
% 291.44/291.90 Deleted: 35
% 291.44/291.90 Deletedinuse: 11
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 34396
% 291.44/291.90 Kept: 6028
% 291.44/291.90 Inuse: 1267
% 291.44/291.90 Deleted: 66
% 291.44/291.90 Deletedinuse: 11
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 39288
% 291.44/291.90 Kept: 8029
% 291.44/291.90 Inuse: 1410
% 291.44/291.90 Deleted: 104
% 291.44/291.90 Deletedinuse: 11
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 55646
% 291.44/291.90 Kept: 10030
% 291.44/291.90 Inuse: 1764
% 291.44/291.90 Deleted: 121
% 291.44/291.90 Deletedinuse: 11
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 73509
% 291.44/291.90 Kept: 12041
% 291.44/291.90 Inuse: 1960
% 291.44/291.90 Deleted: 171
% 291.44/291.90 Deletedinuse: 11
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 98526
% 291.44/291.90 Kept: 14042
% 291.44/291.90 Inuse: 2294
% 291.44/291.90 Deleted: 210
% 291.44/291.90 Deletedinuse: 41
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 126461
% 291.44/291.90 Kept: 16051
% 291.44/291.90 Inuse: 2805
% 291.44/291.90 Deleted: 235
% 291.44/291.90 Deletedinuse: 41
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 147639
% 291.44/291.90 Kept: 18188
% 291.44/291.90 Inuse: 3103
% 291.44/291.90 Deleted: 383
% 291.44/291.90 Deletedinuse: 41
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying clauses:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 193801
% 291.44/291.90 Kept: 20189
% 291.44/291.90 Inuse: 3614
% 291.44/291.90 Deleted: 8527
% 291.44/291.90 Deletedinuse: 43
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 302307
% 291.44/291.90 Kept: 22190
% 291.44/291.90 Inuse: 4241
% 291.44/291.90 Deleted: 8527
% 291.44/291.90 Deletedinuse: 43
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 417600
% 291.44/291.90 Kept: 24192
% 291.44/291.90 Inuse: 5032
% 291.44/291.90 Deleted: 8540
% 291.44/291.90 Deletedinuse: 44
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 557338
% 291.44/291.90 Kept: 26192
% 291.44/291.90 Inuse: 5776
% 291.44/291.90 Deleted: 8564
% 291.44/291.90 Deletedinuse: 52
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90
% 291.44/291.90 Intermediate Status:
% 291.44/291.90 Generated: 777221
% 291.44/291.90 Kept: 28194
% 291.44/291.90 Inuse: 6991
% 291.44/291.90 Deleted: 8609
% 291.44/291.90 Deletedinuse: 59
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 Done
% 291.44/291.90
% 291.44/291.90 Resimplifying inuse:
% 291.44/291.90 DTerminated
% 299.66/300.03 Bliksem ended
%------------------------------------------------------------------------------