%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX225-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n005.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.56s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX225-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : bliksem %s
% 0.15/0.34 % Computer : n005.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:45:15 EDT 2026
% 0.15/0.34 % CPUTime :
% 2.94/3.33 *** allocated 10000 integers for termspace/termends
% 2.94/3.33 *** allocated 10000 integers for clauses
% 2.94/3.33 *** allocated 10000 integers for justifications
% 2.94/3.33 Bliksem 1.12
% 2.94/3.33
% 2.94/3.33
% 2.94/3.33 Automatic Strategy Selection
% 2.94/3.33
% 2.94/3.33 Clauses:
% 2.94/3.33 [
% 2.94/3.33 [ =( fail( X, Y ), par( X, Y, step( X ), step( Y ) ) ) ],
% 2.94/3.33 [ =( par( X, Y, nothing, nothing ), nothing ) ],
% 2.94/3.33 [ =( par( X, Y, nothing, just( Z ) ), just( x( X, Z ) ) ) ],
% 2.94/3.33 [ =( par( X, Y, just( Z ), nothing ), just( x( Z, Y ) ) ) ],
% 2.94/3.33 [ =( par( X, Y, just( Z ), just( T ) ), just( x( Z, T ) ) ) ],
% 2.94/3.33 [ =( step( x( x( x( s, X ), Y ), Z ) ), just( x( x( X, Z ), x( Y, Z ) )
% 2.94/3.33 ) ) ],
% 2.94/3.33 [ =( step( x( x( x( b, X ), Y ), Z ) ), just( x( X, x( Y, Z ) ) ) ) ]
% 2.94/3.33 ,
% 2.94/3.33 [ =( step( x( x( x( c, X ), Y ), Z ) ), just( x( x( X, Z ), Y ) ) ) ]
% 2.94/3.33 ,
% 2.94/3.33 [ =( step( x( x( x( x( X, Y ), Z ), T ), U ) ), fail( x( x( x( X, Y ), Z
% 2.94/3.33 ), T ), U ) ) ],
% 2.94/3.33 [ =( step( x( x( x( theVar, X ), Y ), Z ) ), fail( x( x( theVar, X ), Y
% 2.94/3.33 ), Z ) ) ],
% 2.94/3.33 [ =( step( x( x( x( k, X ), Y ), Z ) ), fail( x( x( k, X ), Y ), Z ) ) ]
% 2.94/3.33 ,
% 2.94/3.33 [ =( step( x( x( x( i, X ), Y ), Z ) ), fail( x( x( i, X ), Y ), Z ) ) ]
% 2.94/3.33 ,
% 2.94/3.33 [ =( step( x( x( k, X ), Y ) ), just( X ) ) ],
% 2.94/3.33 [ =( step( x( x( theVar, X ), Y ) ), fail( x( theVar, X ), Y ) ) ],
% 2.94/3.33 [ =( step( x( x( i, X ), Y ) ), fail( x( i, X ), Y ) ) ],
% 2.94/3.33 [ =( step( x( x( s, X ), Y ) ), fail( x( s, X ), Y ) ) ],
% 2.94/3.33 [ =( step( x( x( b, X ), Y ) ), fail( x( b, X ), Y ) ) ],
% 2.94/3.33 [ =( step( x( x( c, X ), Y ) ), fail( x( c, X ), Y ) ) ],
% 2.94/3.33 [ =( step( x( i, X ) ), just( X ) ) ],
% 2.94/3.33 [ =( step( x( theVar, X ) ), fail( theVar, X ) ) ],
% 2.94/3.33 [ =( step( x( k, X ) ), fail( k, X ) ) ],
% 2.94/3.33 [ =( step( x( s, X ) ), fail( s, X ) ) ],
% 2.94/3.33 [ =( step( x( b, X ) ), fail( b, X ) ) ],
% 2.94/3.33 [ =( step( x( c, X ) ), fail( c, X ) ) ],
% 2.94/3.33 [ =( step( theVar ), nothing ) ],
% 2.94/3.33 [ =( step( k ), nothing ) ],
% 2.94/3.33 [ =( step( i ), nothing ) ],
% 2.94/3.33 [ =( step( s ), nothing ) ],
% 2.94/3.33 [ =( step( b ), nothing ) ],
% 2.94/3.33 [ =( step( c ), nothing ) ],
% 2.94/3.33 [ =( impl( btrue, X ), X ) ],
% 2.94/3.33 [ =( impl( bfalse, X ), btrue ) ],
% 2.94/3.33 [ =( thm1( X ), impl( eq3( step( X ), just( X ) ), eq4( btrue, bfalse )
% 2.94/3.33 ) ) ],
% 2.94/3.33 [ =( eq( theVar, k ), bfalse ) ],
% 2.94/3.33 [ =( eq( theVar, i ), bfalse ) ],
% 2.94/3.33 [ =( eq( theVar, s ), bfalse ) ],
% 2.94/3.33 [ =( eq( theVar, b ), bfalse ) ],
% 2.94/3.33 [ =( eq( theVar, c ), bfalse ) ],
% 2.94/3.33 [ =( eq( k, theVar ), bfalse ) ],
% 2.94/3.33 [ =( eq( k, i ), bfalse ) ],
% 2.94/3.33 [ =( eq( k, s ), bfalse ) ],
% 2.94/3.33 [ =( eq( k, b ), bfalse ) ],
% 2.94/3.33 [ =( eq( k, c ), bfalse ) ],
% 2.94/3.33 [ =( eq( i, theVar ), bfalse ) ],
% 2.94/3.33 [ =( eq( i, k ), bfalse ) ],
% 2.94/3.33 [ =( eq( i, s ), bfalse ) ],
% 2.94/3.33 [ =( eq( i, b ), bfalse ) ],
% 2.94/3.33 [ =( eq( i, c ), bfalse ) ],
% 2.94/3.33 [ =( eq( s, theVar ), bfalse ) ],
% 2.94/3.33 [ =( eq( s, k ), bfalse ) ],
% 2.94/3.33 [ =( eq( s, i ), bfalse ) ],
% 2.94/3.33 [ =( eq( s, b ), bfalse ) ],
% 2.94/3.33 [ =( eq( s, c ), bfalse ) ],
% 2.94/3.33 [ =( eq( b, theVar ), bfalse ) ],
% 2.94/3.33 [ =( eq( b, k ), bfalse ) ],
% 2.94/3.33 [ =( eq( b, i ), bfalse ) ],
% 2.94/3.33 [ =( eq( b, s ), bfalse ) ],
% 2.94/3.33 [ =( eq( b, c ), bfalse ) ],
% 2.94/3.33 [ =( eq( c, theVar ), bfalse ) ],
% 2.94/3.33 [ =( eq( c, k ), bfalse ) ],
% 2.94/3.33 [ =( eq( c, i ), bfalse ) ],
% 2.94/3.33 [ =( eq( c, s ), bfalse ) ],
% 2.94/3.33 [ =( eq( c, b ), bfalse ) ],
% 2.94/3.33 [ =( eq4( bfalse, btrue ), bfalse ) ],
% 2.94/3.33 [ =( eq4( btrue, bfalse ), bfalse ) ],
% 2.94/3.33 [ ~( =( eq( X, Y ), bfalse ) ), =( eq( x( X, Z ), x( Y, T ) ), bfalse )
% 2.94/3.33 ],
% 2.94/3.33 [ ~( =( eq( X, Y ), btrue ) ), =( eq( x( X, Z ), x( Y, T ) ), eq( Z, T )
% 2.94/3.33 ) ],
% 2.94/3.33 [ =( eq( x( X, Y ), theVar ), bfalse ) ],
% 2.94/3.33 [ =( eq( x( X, Y ), k ), bfalse ) ],
% 2.94/3.33 [ =( eq( x( X, Y ), i ), bfalse ) ],
% 2.94/3.33 [ =( eq( x( X, Y ), s ), bfalse ) ],
% 2.94/3.33 [ =( eq( x( X, Y ), b ), bfalse ) ],
% 2.94/3.33 [ =( eq( x( X, Y ), c ), bfalse ) ],
% 2.94/3.33 [ =( eq( theVar, x( X, Y ) ), bfalse ) ],
% 2.94/3.33 [ =( eq( k, x( X, Y ) ), bfalse ) ],
% 2.94/3.33 [ =( eq( i, x( X, Y ) ), bfalse ) ],
% 2.94/3.33 [ =( eq( s, x( X, Y ) ), bfalse ) ],
% 2.94/3.33 [ =( eq( b, x( X, Y ) ), bfalse ) ],
% 2.94/3.33 [ =( eq( c, x( X, Y ) ), bfalse ) ],
% 2.94/3.33 [ =( eq2( suc( X ), suc( Y ) ), eq2( X, Y ) ) ],
% 2.94/3.33 [ =( eq2( suc( X ), z ), bfalse ) ],
% 2.94/3.33 [ =( eq2( z, suc( X ) ), bfalse ) ],
% 2.94/3.33 [ =( eq( X, X ), btrue ) ],
% 2.94/3.33 [ =( eq2( X, X ), btrue ) ],
% 2.94/3.33 [ =( eq3( X, X ), btrue ) ],
% 2.94/3.33 [ =( eq4( X, X ), btrue ) ],
% 2.94/3.33 [ =( eq3( just( X ), just( Y ) ), eq( X, Y ) ) ],
% 32.44/32.84 [ =( eq3( nothing, just( X ) ), bfalse ) ],
% 32.44/32.84 [ =( eq3( just( X ), nothing ), bfalse ) ],
% 32.44/32.84 [ ~( =( eq4( thm1( X ), bfalse ), btrue ) ) ]
% 32.44/32.84 ] .
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 percentage equality = 1.000000, percentage horn = 1.000000
% 32.44/32.84 This is a pure equality problem
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Options Used:
% 32.44/32.84
% 32.44/32.84 useres = 1
% 32.44/32.84 useparamod = 1
% 32.44/32.84 useeqrefl = 1
% 32.44/32.84 useeqfact = 1
% 32.44/32.84 usefactor = 1
% 32.44/32.84 usesimpsplitting = 0
% 32.44/32.84 usesimpdemod = 5
% 32.44/32.84 usesimpres = 3
% 32.44/32.84
% 32.44/32.84 resimpinuse = 1000
% 32.44/32.84 resimpclauses = 20000
% 32.44/32.84 substype = eqrewr
% 32.44/32.84 backwardsubs = 1
% 32.44/32.84 selectoldest = 5
% 32.44/32.84
% 32.44/32.84 litorderings [0] = split
% 32.44/32.84 litorderings [1] = extend the termordering, first sorting on arguments
% 32.44/32.84
% 32.44/32.84 termordering = kbo
% 32.44/32.84
% 32.44/32.84 litapriori = 0
% 32.44/32.84 termapriori = 1
% 32.44/32.84 litaposteriori = 0
% 32.44/32.84 termaposteriori = 0
% 32.44/32.84 demodaposteriori = 0
% 32.44/32.84 ordereqreflfact = 0
% 32.44/32.84
% 32.44/32.84 litselect = negord
% 32.44/32.84
% 32.44/32.84 maxweight = 15
% 32.44/32.84 maxdepth = 30000
% 32.44/32.84 maxlength = 115
% 32.44/32.84 maxnrvars = 195
% 32.44/32.84 excuselevel = 1
% 32.44/32.84 increasemaxweight = 1
% 32.44/32.84
% 32.44/32.84 maxselected = 10000000
% 32.44/32.84 maxnrclauses = 10000000
% 32.44/32.84
% 32.44/32.84 showgenerated = 0
% 32.44/32.84 showkept = 0
% 32.44/32.84 showselected = 0
% 32.44/32.84 showdeleted = 0
% 32.44/32.84 showresimp = 1
% 32.44/32.84 showstatus = 2000
% 32.44/32.84
% 32.44/32.84 prologoutput = 1
% 32.44/32.84 nrgoals = 5000000
% 32.44/32.84 totalproof = 1
% 32.44/32.84
% 32.44/32.84 Symbols occurring in the translation:
% 32.44/32.84
% 32.44/32.84 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 32.44/32.84 . [1, 2] (w:1, o:38, a:1, s:1, b:0),
% 32.44/32.84 ! [4, 1] (w:0, o:29, a:1, s:1, b:0),
% 32.44/32.84 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 32.44/32.84 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 32.44/32.84 fail [41, 2] (w:1, o:67, a:1, s:1, b:0),
% 32.44/32.84 step [42, 1] (w:1, o:34, a:1, s:1, b:0),
% 32.44/32.84 par [43, 4] (w:1, o:70, a:1, s:1, b:0),
% 32.44/32.84 nothing [45, 0] (w:1, o:14, a:1, s:1, b:0),
% 32.44/32.84 just [47, 1] (w:1, o:35, a:1, s:1, b:0),
% 32.44/32.84 x [48, 2] (w:1, o:68, a:1, s:1, b:0),
% 32.44/32.84 s [51, 0] (w:1, o:5, a:1, s:1, b:0),
% 32.44/32.84 b [54, 0] (w:1, o:20, a:1, s:1, b:0),
% 32.44/32.84 c [55, 0] (w:1, o:23, a:1, s:1, b:0),
% 32.44/32.84 theVar [57, 0] (w:1, o:24, a:1, s:1, b:0),
% 32.44/32.84 k [58, 0] (w:1, o:25, a:1, s:1, b:0),
% 32.44/32.84 i [59, 0] (w:1, o:26, a:1, s:1, b:0),
% 32.44/32.84 btrue [60, 0] (w:1, o:21, a:1, s:1, b:0),
% 32.44/32.84 impl [62, 2] (w:1, o:69, a:1, s:1, b:0),
% 32.44/32.84 bfalse [63, 0] (w:1, o:22, a:1, s:1, b:0),
% 32.44/32.84 thm1 [64, 1] (w:1, o:37, a:1, s:1, b:0),
% 32.44/32.84 eq3 [65, 2] (w:1, o:64, a:1, s:1, b:0),
% 32.44/32.84 eq4 [66, 2] (w:1, o:65, a:1, s:1, b:0),
% 32.44/32.84 eq [67, 2] (w:1, o:66, a:1, s:1, b:0),
% 32.44/32.84 suc [68, 1] (w:1, o:36, a:1, s:1, b:0),
% 32.44/32.84 eq2 [69, 2] (w:1, o:63, a:1, s:1, b:0),
% 32.44/32.84 z [70, 0] (w:1, o:28, a:1, s:1, b:0).
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Starting Search:
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 10186
% 32.44/32.84 Kept: 2023
% 32.44/32.84 Inuse: 628
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 15809
% 32.44/32.84 Kept: 4030
% 32.44/32.84 Inuse: 1194
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 19779
% 32.44/32.84 Kept: 6034
% 32.44/32.84 Inuse: 1593
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 22997
% 32.44/32.84 Kept: 8040
% 32.44/32.84 Inuse: 1907
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 26550
% 32.44/32.84 Kept: 10043
% 32.44/32.84 Inuse: 2326
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 30020
% 32.44/32.84 Kept: 12045
% 32.44/32.84 Inuse: 2747
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 36035
% 32.44/32.84 Kept: 14049
% 32.44/32.84 Inuse: 3922
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 39421
% 32.44/32.84 Kept: 16051
% 32.44/32.84 Inuse: 4295
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84 Resimplifying inuse:
% 32.44/32.84 Done
% 32.44/32.84
% 32.44/32.84
% 32.44/32.84 Intermediate Status:
% 32.44/32.84 Generated: 42805
% 32.44/32.84 Kept: 18053
% 32.44/32.84 Inuse: 4665
% 32.44/32.84 Deleted: 51
% 32.44/32.84 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying clauses:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 46139
% 104.92/105.44 Kept: 20055
% 104.92/105.44 Inuse: 5035
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 49453
% 104.92/105.44 Kept: 22057
% 104.92/105.44 Inuse: 5405
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 52827
% 104.92/105.44 Kept: 24059
% 104.92/105.44 Inuse: 5773
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 56192
% 104.92/105.44 Kept: 26061
% 104.92/105.44 Inuse: 6145
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 59584
% 104.92/105.44 Kept: 28063
% 104.92/105.44 Inuse: 6515
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 62966
% 104.92/105.44 Kept: 30065
% 104.92/105.44 Inuse: 6885
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 66325
% 104.92/105.44 Kept: 32067
% 104.92/105.44 Inuse: 7255
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 69673
% 104.92/105.44 Kept: 34069
% 104.92/105.44 Inuse: 7625
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 73046
% 104.92/105.44 Kept: 36071
% 104.92/105.44 Inuse: 7995
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 76442
% 104.92/105.44 Kept: 38073
% 104.92/105.44 Inuse: 8365
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying clauses:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 79789
% 104.92/105.44 Kept: 40075
% 104.92/105.44 Inuse: 8735
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 83131
% 104.92/105.44 Kept: 42077
% 104.92/105.44 Inuse: 9103
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 86498
% 104.92/105.44 Kept: 44079
% 104.92/105.44 Inuse: 9475
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 89828
% 104.92/105.44 Kept: 46081
% 104.92/105.44 Inuse: 9847
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 93206
% 104.92/105.44 Kept: 48083
% 104.92/105.44 Inuse: 10215
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 96542
% 104.92/105.44 Kept: 50085
% 104.92/105.44 Inuse: 10585
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 99892
% 104.92/105.44 Kept: 52087
% 104.92/105.44 Inuse: 10955
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 103204
% 104.92/105.44 Kept: 54089
% 104.92/105.44 Inuse: 11322
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 106360
% 104.92/105.44 Kept: 56091
% 104.92/105.44 Inuse: 11692
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 109634
% 104.92/105.44 Kept: 58093
% 104.92/105.44 Inuse: 12065
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying clauses:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 112962
% 104.92/105.44 Kept: 60095
% 104.92/105.44 Inuse: 12432
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 117799
% 104.92/105.44 Kept: 62097
% 104.92/105.44 Inuse: 13303
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 126289
% 104.92/105.44 Kept: 64099
% 104.92/105.44 Inuse: 15383
% 104.92/105.44 Deleted: 51
% 104.92/105.44 Deletedinuse: 3
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44 Resimplifying inuse:
% 104.92/105.44 Done
% 104.92/105.44
% 104.92/105.44
% 104.92/105.44 Intermediate Status:
% 104.92/105.44 Generated: 134322
% 104.92/105.44 Kept: 66101
% 208.03/208.50 Inuse: 17311
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 137650
% 208.03/208.50 Kept: 68103
% 208.03/208.50 Inuse: 17681
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 141002
% 208.03/208.50 Kept: 70105
% 208.03/208.50 Inuse: 18051
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 144354
% 208.03/208.50 Kept: 72107
% 208.03/208.50 Inuse: 18421
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 147704
% 208.03/208.50 Kept: 74109
% 208.03/208.50 Inuse: 18791
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 151034
% 208.03/208.50 Kept: 76111
% 208.03/208.50 Inuse: 19159
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 154382
% 208.03/208.50 Kept: 78113
% 208.03/208.50 Inuse: 19529
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying clauses:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 157720
% 208.03/208.50 Kept: 80115
% 208.03/208.50 Inuse: 19896
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 161078
% 208.03/208.50 Kept: 82117
% 208.03/208.50 Inuse: 20269
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 164414
% 208.03/208.50 Kept: 84119
% 208.03/208.50 Inuse: 20639
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 167752
% 208.03/208.50 Kept: 86121
% 208.03/208.50 Inuse: 21006
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 171100
% 208.03/208.50 Kept: 88123
% 208.03/208.50 Inuse: 21376
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 174448
% 208.03/208.50 Kept: 90125
% 208.03/208.50 Inuse: 21746
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 177778
% 208.03/208.50 Kept: 92127
% 208.03/208.50 Inuse: 22114
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 181132
% 208.03/208.50 Kept: 94129
% 208.03/208.50 Inuse: 22486
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 184480
% 208.03/208.50 Kept: 96131
% 208.03/208.50 Inuse: 22856
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 187822
% 208.03/208.50 Kept: 98133
% 208.03/208.50 Inuse: 23224
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying clauses:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 191158
% 208.03/208.50 Kept: 100135
% 208.03/208.50 Inuse: 23594
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 194504
% 208.03/208.50 Kept: 102137
% 208.03/208.50 Inuse: 23963
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 197852
% 208.03/208.50 Kept: 104139
% 208.03/208.50 Inuse: 24333
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 201202
% 208.03/208.50 Kept: 106141
% 208.03/208.50 Inuse: 24704
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 204542
% 208.03/208.50 Kept: 108143
% 208.03/208.50 Inuse: 25073
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 207892
% 208.03/208.50 Kept: 110145
% 208.03/208.50 Inuse: 25443
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50
% 208.03/208.50 Intermediate Status:
% 208.03/208.50 Generated: 211244
% 208.03/208.50 Kept: 112147
% 208.03/208.50 Inuse: 25813
% 208.03/208.50 Deleted: 51
% 208.03/208.50 Deletedinuse: 3
% 208.03/208.50
% 208.03/208.50 Resimplifying inuse:
% 208.03/208.50 Done
% 208.03/208.50
% 208.03/208.50 ResimpTerminated
% 299.56/300.03 Bliksem ended
%------------------------------------------------------------------------------