%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX226-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n025.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.60s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX226-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : bliksem %s
% 0.15/0.34 % Computer : n025.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:49:28 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.81/1.74 *** allocated 10000 integers for termspace/termends
% 0.81/1.74 *** allocated 10000 integers for clauses
% 0.81/1.74 *** allocated 10000 integers for justifications
% 0.81/1.74 Bliksem 1.12
% 0.81/1.74
% 0.81/1.74
% 0.81/1.74 Automatic Strategy Selection
% 0.81/1.74
% 0.81/1.74 Clauses:
% 0.81/1.74 [
% 0.81/1.74 [ =( aux( X, Y, nothing ), nothing ) ],
% 0.81/1.74 [ =( aux( X, Y, just( Z ) ), astep( Y, Z ) ) ],
% 0.81/1.74 [ =( fail( X, Y ), par( X, Y, step( X ), step( Y ) ) ) ],
% 0.81/1.74 [ =( par( X, Y, nothing, nothing ), nothing ) ],
% 0.81/1.74 [ =( par( X, Y, nothing, just( Z ) ), just( x( X, Z ) ) ) ],
% 0.81/1.74 [ =( par( X, Y, just( Z ), nothing ), just( x( Z, Y ) ) ) ],
% 0.81/1.74 [ =( par( X, Y, just( Z ), just( T ) ), just( x( Z, T ) ) ) ],
% 0.81/1.74 [ =( step( x( x( x( s, X ), Y ), Z ) ), just( x( x( X, Z ), x( Y, Z ) )
% 0.81/1.74 ) ) ],
% 0.81/1.74 [ =( step( x( x( x( b, X ), Y ), Z ) ), just( x( X, x( Y, Z ) ) ) ) ]
% 0.81/1.74 ,
% 0.81/1.74 [ =( step( x( x( x( c, X ), Y ), Z ) ), just( x( x( X, Z ), Y ) ) ) ]
% 0.81/1.74 ,
% 0.81/1.74 [ =( step( x( x( x( x( X, Y ), Z ), T ), U ) ), fail( x( x( x( X, Y ), Z
% 0.81/1.74 ), T ), U ) ) ],
% 0.81/1.74 [ =( step( x( x( x( theVar, X ), Y ), Z ) ), fail( x( x( theVar, X ), Y
% 0.81/1.74 ), Z ) ) ],
% 0.81/1.74 [ =( step( x( x( x( k, X ), Y ), Z ) ), fail( x( x( k, X ), Y ), Z ) ) ]
% 0.81/1.74 ,
% 0.81/1.74 [ =( step( x( x( x( i, X ), Y ), Z ) ), fail( x( x( i, X ), Y ), Z ) ) ]
% 0.81/1.74 ,
% 0.81/1.74 [ =( step( x( x( k, X ), Y ) ), just( X ) ) ],
% 0.81/1.74 [ =( step( x( x( theVar, X ), Y ) ), fail( x( theVar, X ), Y ) ) ],
% 0.81/1.74 [ =( step( x( x( i, X ), Y ) ), fail( x( i, X ), Y ) ) ],
% 0.81/1.74 [ =( step( x( x( s, X ), Y ) ), fail( x( s, X ), Y ) ) ],
% 0.81/1.74 [ =( step( x( x( b, X ), Y ) ), fail( x( b, X ), Y ) ) ],
% 0.81/1.74 [ =( step( x( x( c, X ), Y ) ), fail( x( c, X ), Y ) ) ],
% 0.81/1.74 [ =( step( x( i, X ) ), just( X ) ) ],
% 0.81/1.74 [ =( step( x( theVar, X ) ), fail( theVar, X ) ) ],
% 0.81/1.74 [ =( step( x( k, X ) ), fail( k, X ) ) ],
% 0.81/1.74 [ =( step( x( s, X ) ), fail( s, X ) ) ],
% 0.81/1.74 [ =( step( x( b, X ) ), fail( b, X ) ) ],
% 0.81/1.74 [ =( step( x( c, X ) ), fail( c, X ) ) ],
% 0.81/1.74 [ =( step( theVar ), nothing ) ],
% 0.81/1.74 [ =( step( k ), nothing ) ],
% 0.81/1.74 [ =( step( i ), nothing ) ],
% 0.81/1.74 [ =( step( s ), nothing ) ],
% 0.81/1.74 [ =( step( b ), nothing ) ],
% 0.81/1.74 [ =( step( c ), nothing ) ],
% 0.81/1.74 [ =( orb( btrue, X ), btrue ) ],
% 0.81/1.74 [ =( orb( bfalse, X ), X ) ],
% 0.81/1.74 [ =( impl( btrue, X ), X ) ],
% 0.81/1.74 [ =( impl( bfalse, X ), btrue ) ],
% 0.81/1.74 [ =( cheating( x( X, Y ) ), orb( cheating( X ), cheating( Y ) ) ) ],
% 0.81/1.74 [ =( cheating( theVar ), btrue ) ],
% 0.81/1.74 [ =( cheating( k ), bfalse ) ],
% 0.81/1.74 [ =( cheating( i ), bfalse ) ],
% 0.81/1.74 [ =( cheating( s ), bfalse ) ],
% 0.81/1.74 [ =( cheating( b ), bfalse ) ],
% 0.81/1.74 [ =( cheating( c ), bfalse ) ],
% 0.81/1.74 [ =( astep( suc( X ), Y ), aux( Y, X, step( Y ) ) ) ],
% 0.81/1.74 [ =( astep( z, X ), just( X ) ) ],
% 0.81/1.74 [ =( 'thm_why'( X, Y ), impl( eq3( astep( X, x( Y, theVar ) ), just( x(
% 0.81/1.74 theVar, x( Y, theVar ) ) ) ), eq4( cheating( Y ), btrue ) ) ) ],
% 0.81/1.74 [ =( eq( theVar, k ), bfalse ) ],
% 0.81/1.74 [ =( eq( theVar, i ), bfalse ) ],
% 0.81/1.74 [ =( eq( theVar, s ), bfalse ) ],
% 0.81/1.74 [ =( eq( theVar, b ), bfalse ) ],
% 0.81/1.74 [ =( eq( theVar, c ), bfalse ) ],
% 0.81/1.74 [ =( eq( k, theVar ), bfalse ) ],
% 0.81/1.74 [ =( eq( k, i ), bfalse ) ],
% 0.81/1.74 [ =( eq( k, s ), bfalse ) ],
% 0.81/1.74 [ =( eq( k, b ), bfalse ) ],
% 0.81/1.74 [ =( eq( k, c ), bfalse ) ],
% 0.81/1.74 [ =( eq( i, theVar ), bfalse ) ],
% 0.81/1.74 [ =( eq( i, k ), bfalse ) ],
% 0.81/1.74 [ =( eq( i, s ), bfalse ) ],
% 0.81/1.74 [ =( eq( i, b ), bfalse ) ],
% 0.81/1.74 [ =( eq( i, c ), bfalse ) ],
% 0.81/1.74 [ =( eq( s, theVar ), bfalse ) ],
% 0.81/1.74 [ =( eq( s, k ), bfalse ) ],
% 0.81/1.74 [ =( eq( s, i ), bfalse ) ],
% 0.81/1.74 [ =( eq( s, b ), bfalse ) ],
% 0.81/1.74 [ =( eq( s, c ), bfalse ) ],
% 0.81/1.74 [ =( eq( b, theVar ), bfalse ) ],
% 0.81/1.74 [ =( eq( b, k ), bfalse ) ],
% 0.81/1.74 [ =( eq( b, i ), bfalse ) ],
% 0.81/1.74 [ =( eq( b, s ), bfalse ) ],
% 0.81/1.74 [ =( eq( b, c ), bfalse ) ],
% 0.81/1.74 [ =( eq( c, theVar ), bfalse ) ],
% 0.81/1.74 [ =( eq( c, k ), bfalse ) ],
% 0.81/1.74 [ =( eq( c, i ), bfalse ) ],
% 0.81/1.74 [ =( eq( c, s ), bfalse ) ],
% 0.81/1.74 [ =( eq( c, b ), bfalse ) ],
% 0.81/1.74 [ =( eq4( bfalse, btrue ), bfalse ) ],
% 0.81/1.74 [ =( eq4( btrue, bfalse ), bfalse ) ],
% 0.81/1.74 [ ~( =( eq( X, Y ), bfalse ) ), =( eq( x( X, Z ), x( Y, T ) ), bfalse )
% 0.81/1.74 ],
% 0.81/1.74 [ ~( =( eq( X, Y ), btrue ) ), =( eq( x( X, Z ), x( Y, T ) ), eq( Z, T )
% 0.81/1.74 ) ],
% 0.81/1.74 [ =( eq( x( X, Y ), theVar ), bfalse ) ],
% 0.81/1.74 [ =( eq( x( X, Y ), k ), bfalse ) ],
% 0.81/1.74 [ =( eq( x( X, Y ), i ), bfalse ) ],
% 0.81/1.74 [ =( eq( x( X, Y ), s ), bfalse ) ],
% 12.54/12.93 [ =( eq( x( X, Y ), b ), bfalse ) ],
% 12.54/12.93 [ =( eq( x( X, Y ), c ), bfalse ) ],
% 12.54/12.93 [ =( eq( theVar, x( X, Y ) ), bfalse ) ],
% 12.54/12.93 [ =( eq( k, x( X, Y ) ), bfalse ) ],
% 12.54/12.93 [ =( eq( i, x( X, Y ) ), bfalse ) ],
% 12.54/12.93 [ =( eq( s, x( X, Y ) ), bfalse ) ],
% 12.54/12.93 [ =( eq( b, x( X, Y ) ), bfalse ) ],
% 12.54/12.93 [ =( eq( c, x( X, Y ) ), bfalse ) ],
% 12.54/12.93 [ =( eq2( suc( X ), suc( Y ) ), eq2( X, Y ) ) ],
% 12.54/12.93 [ =( eq2( suc( X ), z ), bfalse ) ],
% 12.54/12.93 [ =( eq2( z, suc( X ) ), bfalse ) ],
% 12.54/12.93 [ =( eq( X, X ), btrue ) ],
% 12.54/12.93 [ =( eq2( X, X ), btrue ) ],
% 12.54/12.93 [ =( eq3( X, X ), btrue ) ],
% 12.54/12.93 [ =( eq4( X, X ), btrue ) ],
% 12.54/12.93 [ =( eq3( just( X ), just( Y ) ), eq( X, Y ) ) ],
% 12.54/12.93 [ =( eq3( nothing, just( X ) ), bfalse ) ],
% 12.54/12.93 [ =( eq3( just( X ), nothing ), bfalse ) ],
% 12.54/12.93 [ ~( =( eq4( 'thm_why'( X, Y ), bfalse ), btrue ) ) ]
% 12.54/12.93 ] .
% 12.54/12.93
% 12.54/12.93
% 12.54/12.93 percentage equality = 1.000000, percentage horn = 1.000000
% 12.54/12.93 This is a pure equality problem
% 12.54/12.93
% 12.54/12.93
% 12.54/12.93
% 12.54/12.93 Options Used:
% 12.54/12.93
% 12.54/12.93 useres = 1
% 12.54/12.93 useparamod = 1
% 12.54/12.93 useeqrefl = 1
% 12.54/12.93 useeqfact = 1
% 12.54/12.93 usefactor = 1
% 12.54/12.93 usesimpsplitting = 0
% 12.54/12.93 usesimpdemod = 5
% 12.54/12.93 usesimpres = 3
% 12.54/12.93
% 12.54/12.93 resimpinuse = 1000
% 12.54/12.93 resimpclauses = 20000
% 12.54/12.93 substype = eqrewr
% 12.54/12.93 backwardsubs = 1
% 12.54/12.93 selectoldest = 5
% 12.54/12.93
% 12.54/12.93 litorderings [0] = split
% 12.54/12.93 litorderings [1] = extend the termordering, first sorting on arguments
% 12.54/12.93
% 12.54/12.93 termordering = kbo
% 12.54/12.93
% 12.54/12.93 litapriori = 0
% 12.54/12.93 termapriori = 1
% 12.54/12.93 litaposteriori = 0
% 12.54/12.93 termaposteriori = 0
% 12.54/12.93 demodaposteriori = 0
% 12.54/12.93 ordereqreflfact = 0
% 12.54/12.93
% 12.54/12.93 litselect = negord
% 12.54/12.93
% 12.54/12.93 maxweight = 15
% 12.54/12.93 maxdepth = 30000
% 12.54/12.93 maxlength = 115
% 12.54/12.93 maxnrvars = 195
% 12.54/12.93 excuselevel = 1
% 12.54/12.93 increasemaxweight = 1
% 12.54/12.93
% 12.54/12.93 maxselected = 10000000
% 12.54/12.93 maxnrclauses = 10000000
% 12.54/12.93
% 12.54/12.93 showgenerated = 0
% 12.54/12.93 showkept = 0
% 12.54/12.93 showselected = 0
% 12.54/12.93 showdeleted = 0
% 12.54/12.93 showresimp = 1
% 12.54/12.93 showstatus = 2000
% 12.54/12.93
% 12.54/12.93 prologoutput = 1
% 12.54/12.93 nrgoals = 5000000
% 12.54/12.93 totalproof = 1
% 12.54/12.93
% 12.54/12.93 Symbols occurring in the translation:
% 12.54/12.93
% 12.54/12.93 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 12.54/12.93 . [1, 2] (w:1, o:42, a:1, s:1, b:0),
% 12.54/12.93 ! [4, 1] (w:0, o:33, a:1, s:1, b:0),
% 12.54/12.93 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 12.54/12.93 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 12.54/12.93 nothing [41, 0] (w:1, o:14, a:1, s:1, b:0),
% 12.54/12.93 aux [42, 3] (w:1, o:77, a:1, s:1, b:0),
% 12.54/12.93 just [44, 1] (w:1, o:38, a:1, s:1, b:0),
% 12.54/12.93 astep [45, 2] (w:1, o:67, a:1, s:1, b:0),
% 12.54/12.93 fail [47, 2] (w:1, o:72, a:1, s:1, b:0),
% 12.54/12.93 step [48, 1] (w:1, o:39, a:1, s:1, b:0),
% 12.54/12.93 par [49, 4] (w:1, o:78, a:1, s:1, b:0),
% 12.54/12.93 x [52, 2] (w:1, o:73, a:1, s:1, b:0),
% 12.54/12.93 s [55, 0] (w:1, o:5, a:1, s:1, b:0),
% 12.54/12.93 b [58, 0] (w:1, o:22, a:1, s:1, b:0),
% 12.54/12.93 c [59, 0] (w:1, o:25, a:1, s:1, b:0),
% 12.54/12.93 theVar [61, 0] (w:1, o:26, a:1, s:1, b:0),
% 12.54/12.93 k [62, 0] (w:1, o:27, a:1, s:1, b:0),
% 12.54/12.93 i [63, 0] (w:1, o:28, a:1, s:1, b:0),
% 12.54/12.93 btrue [64, 0] (w:1, o:23, a:1, s:1, b:0),
% 12.54/12.93 orb [66, 2] (w:1, o:74, a:1, s:1, b:0),
% 12.54/12.93 bfalse [67, 0] (w:1, o:24, a:1, s:1, b:0),
% 12.54/12.93 impl [68, 2] (w:1, o:75, a:1, s:1, b:0),
% 12.54/12.93 cheating [71, 1] (w:1, o:40, a:1, s:1, b:0),
% 12.54/12.93 suc [72, 1] (w:1, o:41, a:1, s:1, b:0),
% 12.54/12.93 z [73, 0] (w:1, o:32, a:1, s:1, b:0),
% 12.54/12.93 'thm_why' [74, 2] (w:1, o:76, a:1, s:1, b:0),
% 12.54/12.93 eq3 [75, 2] (w:1, o:69, a:1, s:1, b:0),
% 12.54/12.93 eq4 [76, 2] (w:1, o:70, a:1, s:1, b:0),
% 12.54/12.93 eq [77, 2] (w:1, o:71, a:1, s:1, b:0),
% 12.54/12.93 eq2 [78, 2] (w:1, o:68, a:1, s:1, b:0).
% 12.54/12.93
% 12.54/12.93
% 12.54/12.93 Starting Search:
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 12.54/12.93 Done
% 12.54/12.93
% 12.54/12.93
% 12.54/12.93 Intermediate Status:
% 12.54/12.93 Generated: 11870
% 12.54/12.93 Kept: 2002
% 12.54/12.93 Inuse: 714
% 12.54/12.93 Deleted: 72
% 12.54/12.93 Deletedinuse: 3
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 12.54/12.93 Done
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 12.54/12.93 Done
% 12.54/12.93
% 12.54/12.93
% 12.54/12.93 Intermediate Status:
% 12.54/12.93 Generated: 16746
% 12.54/12.93 Kept: 4013
% 12.54/12.93 Inuse: 1048
% 12.54/12.93 Deleted: 92
% 12.54/12.93 Deletedinuse: 3
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 12.54/12.93 Done
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 12.54/12.93 Done
% 12.54/12.93
% 12.54/12.93
% 12.54/12.93 Intermediate Status:
% 12.54/12.93 Generated: 21871
% 12.54/12.93 Kept: 6024
% 12.54/12.93 Inuse: 1464
% 12.54/12.93 Deleted: 96
% 12.54/12.93 Deletedinuse: 3
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 12.54/12.93 Done
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 12.54/12.93 Done
% 12.54/12.93
% 12.54/12.93
% 12.54/12.93 Intermediate Status:
% 12.54/12.93 Generated: 25287
% 12.54/12.93 Kept: 8025
% 12.54/12.93 Inuse: 1829
% 12.54/12.93 Deleted: 97
% 12.54/12.93 Deletedinuse: 3
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 12.54/12.93 Done
% 12.54/12.93
% 12.54/12.93 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 28713
% 63.22/63.69 Kept: 10029
% 63.22/63.69 Inuse: 2218
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 31863
% 63.22/63.69 Kept: 12031
% 63.22/63.69 Inuse: 2521
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 35797
% 63.22/63.69 Kept: 14033
% 63.22/63.69 Inuse: 3173
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 39345
% 63.22/63.69 Kept: 16038
% 63.22/63.69 Inuse: 3552
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 42643
% 63.22/63.69 Kept: 18045
% 63.22/63.69 Inuse: 3907
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying clauses:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 45907
% 63.22/63.69 Kept: 20048
% 63.22/63.69 Inuse: 4263
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 49151
% 63.22/63.69 Kept: 22049
% 63.22/63.69 Inuse: 4624
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 52421
% 63.22/63.69 Kept: 24060
% 63.22/63.69 Inuse: 4983
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 55677
% 63.22/63.69 Kept: 26065
% 63.22/63.69 Inuse: 5344
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 58942
% 63.22/63.69 Kept: 28073
% 63.22/63.69 Inuse: 5705
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 62218
% 63.22/63.69 Kept: 30078
% 63.22/63.69 Inuse: 6064
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 65499
% 63.22/63.69 Kept: 32082
% 63.22/63.69 Inuse: 6415
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 68740
% 63.22/63.69 Kept: 34087
% 63.22/63.69 Inuse: 6768
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 71977
% 63.22/63.69 Kept: 36090
% 63.22/63.69 Inuse: 7122
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 75221
% 63.22/63.69 Kept: 38102
% 63.22/63.69 Inuse: 7478
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying clauses:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 78478
% 63.22/63.69 Kept: 40105
% 63.22/63.69 Inuse: 7830
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 81755
% 63.22/63.69 Kept: 42106
% 63.22/63.69 Inuse: 8180
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 85061
% 63.22/63.69 Kept: 44109
% 63.22/63.69 Inuse: 8528
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 88384
% 63.22/63.69 Kept: 46114
% 63.22/63.69 Inuse: 8880
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 91686
% 63.22/63.69 Kept: 48121
% 63.22/63.69 Inuse: 9234
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 95005
% 63.22/63.69 Kept: 50122
% 63.22/63.69 Inuse: 9592
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 98317
% 63.22/63.69 Kept: 52122
% 63.22/63.69 Inuse: 9948
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 101631
% 63.22/63.69 Kept: 54124
% 63.22/63.69 Inuse: 10302
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 63.22/63.69 Done
% 63.22/63.69
% 63.22/63.69
% 63.22/63.69 Intermediate Status:
% 63.22/63.69 Generated: 104955
% 63.22/63.69 Kept: 56134
% 63.22/63.69 Inuse: 10661
% 63.22/63.69 Deleted: 97
% 63.22/63.69 Deletedinuse: 3
% 63.22/63.69
% 63.22/63.69 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 108278
% 170.98/171.46 Kept: 58146
% 170.98/171.46 Inuse: 11016
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying clauses:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 111593
% 170.98/171.46 Kept: 60147
% 170.98/171.46 Inuse: 11372
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 114893
% 170.98/171.46 Kept: 62157
% 170.98/171.46 Inuse: 11731
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 118200
% 170.98/171.46 Kept: 64168
% 170.98/171.46 Inuse: 12092
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 122637
% 170.98/171.46 Kept: 66168
% 170.98/171.46 Inuse: 12999
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 128032
% 170.98/171.46 Kept: 68176
% 170.98/171.46 Inuse: 14204
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 131865
% 170.98/171.46 Kept: 70181
% 170.98/171.46 Inuse: 14618
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 135658
% 170.98/171.46 Kept: 72185
% 170.98/171.46 Inuse: 15025
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 139478
% 170.98/171.46 Kept: 74190
% 170.98/171.46 Inuse: 15437
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 143291
% 170.98/171.46 Kept: 76194
% 170.98/171.46 Inuse: 15851
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 147108
% 170.98/171.46 Kept: 78199
% 170.98/171.46 Inuse: 16260
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying clauses:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 150932
% 170.98/171.46 Kept: 80203
% 170.98/171.46 Inuse: 16672
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 154746
% 170.98/171.46 Kept: 82208
% 170.98/171.46 Inuse: 17081
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 158530
% 170.98/171.46 Kept: 84212
% 170.98/171.46 Inuse: 17491
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 162357
% 170.98/171.46 Kept: 86217
% 170.98/171.46 Inuse: 17905
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 166166
% 170.98/171.46 Kept: 88222
% 170.98/171.46 Inuse: 18319
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 169978
% 170.98/171.46 Kept: 90227
% 170.98/171.46 Inuse: 18733
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 173803
% 170.98/171.46 Kept: 92232
% 170.98/171.46 Inuse: 19146
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 177598
% 170.98/171.46 Kept: 94236
% 170.98/171.46 Inuse: 19554
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 181426
% 170.98/171.46 Kept: 96241
% 170.98/171.46 Inuse: 19970
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 185245
% 170.98/171.46 Kept: 98246
% 170.98/171.46 Inuse: 20386
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying clauses:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 189066
% 170.98/171.46 Kept: 100251
% 170.98/171.46 Inuse: 20800
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 Generated: 192902
% 170.98/171.46 Kept: 102256
% 170.98/171.46 Inuse: 21214
% 170.98/171.46 Deleted: 97
% 170.98/171.46 Deletedinuse: 3
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46 Resimplifying inuse:
% 170.98/171.46 Done
% 170.98/171.46
% 170.98/171.46
% 170.98/171.46 Intermediate Status:
% 170.98/171.46 GeneratedTerminated
% 299.60/300.03 Bliksem ended
% 299.60/300.03 Terminated
%------------------------------------------------------------------------------