%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX185-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n001.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:45 PM UTC 2026
% Result : Timeout 293.79s 294.29s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX185-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.16/0.35 % Computer : n001.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % DateTime : Tue May 5 09:34:18 EDT 2026
% 0.16/0.35 % CPUTime :
% 5.42/5.87 *** allocated 10000 integers for termspace/termends
% 5.42/5.87 *** allocated 10000 integers for clauses
% 5.42/5.87 *** allocated 10000 integers for justifications
% 5.42/5.87 Bliksem 1.12
% 5.42/5.87
% 5.42/5.87
% 5.42/5.87 Automatic Strategy Selection
% 5.42/5.87
% 5.42/5.87 Clauses:
% 5.42/5.87 [
% 5.42/5.87 [ =( impl( btrue, X ), X ) ],
% 5.42/5.87 [ =( impl( bfalse, X ), btrue ) ],
% 5.42/5.87 [ =( assoc( z( z( X, Y ), Z ) ), assoc( z( X, z( Y, Z ) ) ) ) ],
% 5.42/5.87 [ =( assoc( z( x2( X, Y ), Z ) ), z( assoc( x2( X, Y ) ), assoc( Z ) ) )
% 5.42/5.87 ],
% 5.42/5.87 [ =( assoc( z( eX, X ) ), z( assoc( eX ), assoc( X ) ) ) ],
% 5.42/5.87 [ =( assoc( z( eY, X ) ), z( assoc( eY ), assoc( X ) ) ) ],
% 5.42/5.87 [ =( assoc( x2( X, Y ) ), x2( assoc( X ), assoc( Y ) ) ) ],
% 5.42/5.87 [ =( assoc( eX ), eX ) ],
% 5.42/5.87 [ =( assoc( eY ), eY ) ],
% 5.42/5.87 [ =( append( nil, X ), X ) ],
% 5.42/5.87 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 5.42/5.87 [ =( linTerm( x2( X, Y ) ), append( cons( c, nil ), append( lin( z( X, Y
% 5.42/5.87 ) ), cons( d, nil ) ) ) ) ],
% 5.42/5.87 [ =( linTerm( z( X, Y ) ), lin( z( X, Y ) ) ) ],
% 5.42/5.87 [ =( linTerm( eX ), lin( eX ) ) ],
% 5.42/5.87 [ =( linTerm( eY ), lin( eY ) ) ],
% 5.42/5.87 [ =( lin( z( X, Y ) ), append( linTerm( X ), append( cons( plus, nil ),
% 5.42/5.87 linTerm( Y ) ) ) ) ],
% 5.42/5.87 [ =( lin( x2( X, Y ) ), append( lin( X ), append( cons( mul, nil ), lin(
% 5.42/5.87 Y ) ) ) ) ],
% 5.42/5.87 [ =( lin( eX ), cons( x, nil ) ) ],
% 5.42/5.87 [ =( lin( eY ), cons( y, nil ) ) ],
% 5.42/5.87 [ =( 'prop_unambig'( X, Y ), impl( eq( lin( X ), lin( Y ) ), eq3( assoc(
% 5.42/5.87 X ), assoc( Y ) ) ) ) ],
% 5.42/5.87 [ =( eq2( c, d ), bfalse ) ],
% 5.42/5.87 [ =( eq2( c, x ), bfalse ) ],
% 5.42/5.87 [ =( eq2( c, y ), bfalse ) ],
% 5.42/5.87 [ =( eq2( c, plus ), bfalse ) ],
% 5.42/5.87 [ =( eq2( c, mul ), bfalse ) ],
% 5.42/5.87 [ =( eq2( d, c ), bfalse ) ],
% 5.42/5.87 [ =( eq2( d, x ), bfalse ) ],
% 5.42/5.87 [ =( eq2( d, y ), bfalse ) ],
% 5.42/5.87 [ =( eq2( d, plus ), bfalse ) ],
% 5.42/5.87 [ =( eq2( d, mul ), bfalse ) ],
% 5.42/5.87 [ =( eq2( x, c ), bfalse ) ],
% 5.42/5.87 [ =( eq2( x, d ), bfalse ) ],
% 5.42/5.87 [ =( eq2( x, y ), bfalse ) ],
% 5.42/5.87 [ =( eq2( x, plus ), bfalse ) ],
% 5.42/5.87 [ =( eq2( x, mul ), bfalse ) ],
% 5.42/5.87 [ =( eq2( y, c ), bfalse ) ],
% 5.42/5.87 [ =( eq2( y, d ), bfalse ) ],
% 5.42/5.87 [ =( eq2( y, x ), bfalse ) ],
% 5.42/5.87 [ =( eq2( y, plus ), bfalse ) ],
% 5.42/5.87 [ =( eq2( y, mul ), bfalse ) ],
% 5.42/5.87 [ =( eq2( plus, c ), bfalse ) ],
% 5.42/5.87 [ =( eq2( plus, d ), bfalse ) ],
% 5.42/5.87 [ =( eq2( plus, x ), bfalse ) ],
% 5.42/5.87 [ =( eq2( plus, y ), bfalse ) ],
% 5.42/5.87 [ =( eq2( plus, mul ), bfalse ) ],
% 5.42/5.87 [ =( eq2( mul, c ), bfalse ) ],
% 5.42/5.87 [ =( eq2( mul, d ), bfalse ) ],
% 5.42/5.87 [ =( eq2( mul, x ), bfalse ) ],
% 5.42/5.87 [ =( eq2( mul, y ), bfalse ) ],
% 5.42/5.87 [ =( eq2( mul, plus ), bfalse ) ],
% 5.42/5.87 [ =( eq3( eX, eY ), bfalse ) ],
% 5.42/5.87 [ =( eq3( eY, eX ), bfalse ) ],
% 5.42/5.87 [ =( eq4( bfalse, btrue ), bfalse ) ],
% 5.42/5.87 [ =( eq4( btrue, bfalse ), bfalse ) ],
% 5.42/5.87 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( z( X, Z ), z( Y, T ) ), bfalse
% 5.42/5.87 ) ],
% 5.42/5.87 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( z( X, Z ), z( Y, T ) ), eq3( Z,
% 5.42/5.87 T ) ) ],
% 5.42/5.87 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( x2( X, Z ), x2( Y, T ) ),
% 5.42/5.87 bfalse ) ],
% 5.42/5.87 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( x2( X, Z ), x2( Y, T ) ), eq3( Z
% 5.42/5.87 , T ) ) ],
% 5.42/5.87 [ =( eq3( z( X, Y ), x2( Z, T ) ), bfalse ) ],
% 5.42/5.87 [ =( eq3( z( X, Y ), eX ), bfalse ) ],
% 5.42/5.87 [ =( eq3( z( X, Y ), eY ), bfalse ) ],
% 5.42/5.87 [ =( eq3( x2( X, Y ), z( Z, T ) ), bfalse ) ],
% 5.42/5.87 [ =( eq3( x2( X, Y ), eX ), bfalse ) ],
% 5.42/5.87 [ =( eq3( x2( X, Y ), eY ), bfalse ) ],
% 5.42/5.87 [ =( eq3( eX, z( X, Y ) ), bfalse ) ],
% 5.42/5.87 [ =( eq3( eX, x2( X, Y ) ), bfalse ) ],
% 5.42/5.87 [ =( eq3( eY, z( X, Y ) ), bfalse ) ],
% 5.42/5.87 [ =( eq3( eY, x2( X, Y ) ), bfalse ) ],
% 5.42/5.87 [ =( eq( X, X ), btrue ) ],
% 5.42/5.87 [ =( eq2( X, X ), btrue ) ],
% 5.42/5.87 [ =( eq3( X, X ), btrue ) ],
% 5.42/5.87 [ =( eq4( X, X ), btrue ) ],
% 5.42/5.87 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq( cons( X, Z ), cons( Y, T ) ),
% 5.42/5.87 bfalse ) ],
% 5.42/5.87 [ ~( =( eq2( X, Y ), btrue ) ), =( eq( cons( X, Z ), cons( Y, T ) ), eq(
% 5.42/5.87 Z, T ) ) ],
% 5.42/5.87 [ =( eq( nil, cons( X, Y ) ), bfalse ) ],
% 5.42/5.87 [ =( eq( cons( X, Y ), nil ), bfalse ) ],
% 5.42/5.87 [ ~( =( eq4( 'prop_unambig'( X, Y ), bfalse ), btrue ) ) ]
% 5.42/5.87 ] .
% 5.42/5.87
% 5.42/5.87
% 5.42/5.87 percentage equality = 1.000000, percentage horn = 1.000000
% 5.42/5.87 This is a pure equality problem
% 5.42/5.87
% 5.42/5.87
% 5.42/5.87
% 5.42/5.87 Options Used:
% 5.42/5.87
% 5.42/5.87 useres = 1
% 5.42/5.87 useparamod = 1
% 5.42/5.87 useeqrefl = 1
% 5.42/5.87 useeqfact = 1
% 5.42/5.87 usefactor = 1
% 5.42/5.87 usesimpsplitting = 0
% 5.42/5.87 usesimpdemod = 5
% 5.42/5.87 usesimpres = 3
% 26.75/27.17
% 26.75/27.17 resimpinuse = 1000
% 26.75/27.17 resimpclauses = 20000
% 26.75/27.17 substype = eqrewr
% 26.75/27.17 backwardsubs = 1
% 26.75/27.17 selectoldest = 5
% 26.75/27.17
% 26.75/27.17 litorderings [0] = split
% 26.75/27.17 litorderings [1] = extend the termordering, first sorting on arguments
% 26.75/27.17
% 26.75/27.17 termordering = kbo
% 26.75/27.17
% 26.75/27.17 litapriori = 0
% 26.75/27.17 termapriori = 1
% 26.75/27.17 litaposteriori = 0
% 26.75/27.17 termaposteriori = 0
% 26.75/27.17 demodaposteriori = 0
% 26.75/27.17 ordereqreflfact = 0
% 26.75/27.17
% 26.75/27.17 litselect = negord
% 26.75/27.17
% 26.75/27.17 maxweight = 15
% 26.75/27.17 maxdepth = 30000
% 26.75/27.17 maxlength = 115
% 26.75/27.17 maxnrvars = 195
% 26.75/27.17 excuselevel = 1
% 26.75/27.17 increasemaxweight = 1
% 26.75/27.17
% 26.75/27.17 maxselected = 10000000
% 26.75/27.17 maxnrclauses = 10000000
% 26.75/27.17
% 26.75/27.17 showgenerated = 0
% 26.75/27.17 showkept = 0
% 26.75/27.17 showselected = 0
% 26.75/27.17 showdeleted = 0
% 26.75/27.17 showresimp = 1
% 26.75/27.17 showstatus = 2000
% 26.75/27.17
% 26.75/27.17 prologoutput = 1
% 26.75/27.17 nrgoals = 5000000
% 26.75/27.17 totalproof = 1
% 26.75/27.17
% 26.75/27.17 Symbols occurring in the translation:
% 26.75/27.17
% 26.75/27.17 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 26.75/27.17 . [1, 2] (w:1, o:40, a:1, s:1, b:0),
% 26.75/27.17 ! [4, 1] (w:0, o:32, a:1, s:1, b:0),
% 26.75/27.17 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 26.75/27.17 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 26.75/27.17 btrue [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 26.75/27.17 impl [41, 2] (w:1, o:65, a:1, s:1, b:0),
% 26.75/27.17 bfalse [42, 0] (w:1, o:11, a:1, s:1, b:0),
% 26.75/27.17 z [45, 2] (w:1, o:66, a:1, s:1, b:0),
% 26.75/27.17 assoc [47, 1] (w:1, o:37, a:1, s:1, b:0),
% 26.75/27.17 x2 [50, 2] (w:1, o:67, a:1, s:1, b:0),
% 26.75/27.17 eX [51, 0] (w:1, o:21, a:1, s:1, b:0),
% 26.75/27.17 eY [52, 0] (w:1, o:22, a:1, s:1, b:0),
% 26.75/27.17 nil [55, 0] (w:1, o:24, a:1, s:1, b:0),
% 26.75/27.17 append [57, 2] (w:1, o:68, a:1, s:1, b:0),
% 26.75/27.17 cons [60, 2] (w:1, o:69, a:1, s:1, b:0),
% 26.75/27.17 linTerm [61, 1] (w:1, o:38, a:1, s:1, b:0),
% 26.75/27.17 c [62, 0] (w:1, o:28, a:1, s:1, b:0),
% 26.75/27.17 lin [63, 1] (w:1, o:39, a:1, s:1, b:0),
% 26.75/27.17 d [64, 0] (w:1, o:20, a:1, s:1, b:0),
% 26.75/27.17 plus [65, 0] (w:1, o:29, a:1, s:1, b:0),
% 26.75/27.17 mul [67, 0] (w:1, o:23, a:1, s:1, b:0),
% 26.75/27.17 x [68, 0] (w:1, o:30, a:1, s:1, b:0),
% 26.75/27.17 y [69, 0] (w:1, o:31, a:1, s:1, b:0),
% 26.75/27.17 'prop_unambig' [70, 2] (w:1, o:70, a:1, s:1, b:0),
% 26.75/27.17 eq [71, 2] (w:1, o:71, a:1, s:1, b:0),
% 26.75/27.17 eq3 [72, 2] (w:1, o:73, a:1, s:1, b:0),
% 26.75/27.17 eq2 [73, 2] (w:1, o:72, a:1, s:1, b:0),
% 26.75/27.17 eq4 [74, 2] (w:1, o:74, a:1, s:1, b:0).
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Starting Search:
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 16528
% 26.75/27.17 Kept: 2002
% 26.75/27.17 Inuse: 688
% 26.75/27.17 Deleted: 57
% 26.75/27.17 Deletedinuse: 1
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 36346
% 26.75/27.17 Kept: 4003
% 26.75/27.17 Inuse: 1179
% 26.75/27.17 Deleted: 250
% 26.75/27.17 Deletedinuse: 2
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 51106
% 26.75/27.17 Kept: 6007
% 26.75/27.17 Inuse: 1606
% 26.75/27.17 Deleted: 438
% 26.75/27.17 Deletedinuse: 74
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 67263
% 26.75/27.17 Kept: 8009
% 26.75/27.17 Inuse: 2054
% 26.75/27.17 Deleted: 720
% 26.75/27.17 Deletedinuse: 102
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 74633
% 26.75/27.17 Kept: 10021
% 26.75/27.17 Inuse: 2444
% 26.75/27.17 Deleted: 806
% 26.75/27.17 Deletedinuse: 102
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 87720
% 26.75/27.17 Kept: 12021
% 26.75/27.17 Inuse: 2842
% 26.75/27.17 Deleted: 1109
% 26.75/27.17 Deletedinuse: 118
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 106771
% 26.75/27.17 Kept: 14022
% 26.75/27.17 Inuse: 3328
% 26.75/27.17 Deleted: 1482
% 26.75/27.17 Deletedinuse: 126
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 124972
% 26.75/27.17 Kept: 16030
% 26.75/27.17 Inuse: 3824
% 26.75/27.17 Deleted: 2433
% 26.75/27.17 Deletedinuse: 138
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 148151
% 26.75/27.17 Kept: 18037
% 26.75/27.17 Inuse: 4482
% 26.75/27.17 Deleted: 3286
% 26.75/27.17 Deletedinuse: 138
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying clauses:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 170908
% 26.75/27.17 Kept: 20037
% 26.75/27.17 Inuse: 4989
% 26.75/27.17 Deleted: 10760
% 26.75/27.17 Deletedinuse: 154
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17 Resimplifying inuse:
% 26.75/27.17 Done
% 26.75/27.17
% 26.75/27.17
% 26.75/27.17 Intermediate Status:
% 26.75/27.17 Generated: 201528
% 26.75/27.17 Kept: 22040
% 26.75/27.17 Inuse: 5786
% 26.75/27.17 Deleted: 10960
% 116.64/117.03 Deletedinuse: 226
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 231111
% 116.64/117.03 Kept: 24043
% 116.64/117.03 Inuse: 6907
% 116.64/117.03 Deleted: 11510
% 116.64/117.03 Deletedinuse: 248
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 268571
% 116.64/117.03 Kept: 26048
% 116.64/117.03 Inuse: 8042
% 116.64/117.03 Deleted: 12080
% 116.64/117.03 Deletedinuse: 282
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 402759
% 116.64/117.03 Kept: 28048
% 116.64/117.03 Inuse: 11570
% 116.64/117.03 Deleted: 15297
% 116.64/117.03 Deletedinuse: 294
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Failed to find proof!
% 116.64/117.03 maxweight = 15
% 116.64/117.03 maxnrclauses = 10000000
% 116.64/117.03 Generated: 423467
% 116.64/117.03 Kept: 28207
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 The strategy used was not complete!
% 116.64/117.03
% 116.64/117.03 Increased maxweight to 16
% 116.64/117.03
% 116.64/117.03 Starting Search:
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 15029
% 116.64/117.03 Kept: 2001
% 116.64/117.03 Inuse: 627
% 116.64/117.03 Deleted: 56
% 116.64/117.03 Deletedinuse: 1
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 30159
% 116.64/117.03 Kept: 4006
% 116.64/117.03 Inuse: 1006
% 116.64/117.03 Deleted: 144
% 116.64/117.03 Deletedinuse: 2
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 43996
% 116.64/117.03 Kept: 6009
% 116.64/117.03 Inuse: 1437
% 116.64/117.03 Deleted: 371
% 116.64/117.03 Deletedinuse: 70
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 57226
% 116.64/117.03 Kept: 8011
% 116.64/117.03 Inuse: 1795
% 116.64/117.03 Deleted: 530
% 116.64/117.03 Deletedinuse: 84
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 74366
% 116.64/117.03 Kept: 10014
% 116.64/117.03 Inuse: 2213
% 116.64/117.03 Deleted: 896
% 116.64/117.03 Deletedinuse: 98
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 81514
% 116.64/117.03 Kept: 12017
% 116.64/117.03 Inuse: 2596
% 116.64/117.03 Deleted: 940
% 116.64/117.03 Deletedinuse: 98
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 96616
% 116.64/117.03 Kept: 14019
% 116.64/117.03 Inuse: 3015
% 116.64/117.03 Deleted: 1263
% 116.64/117.03 Deletedinuse: 114
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 113998
% 116.64/117.03 Kept: 16019
% 116.64/117.03 Inuse: 3183
% 116.64/117.03 Deleted: 1373
% 116.64/117.03 Deletedinuse: 118
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 135399
% 116.64/117.03 Kept: 18027
% 116.64/117.03 Inuse: 3460
% 116.64/117.03 Deleted: 1473
% 116.64/117.03 Deletedinuse: 122
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying clauses:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 159061
% 116.64/117.03 Kept: 20034
% 116.64/117.03 Inuse: 3946
% 116.64/117.03 Deleted: 9895
% 116.64/117.03 Deletedinuse: 132
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 180992
% 116.64/117.03 Kept: 22043
% 116.64/117.03 Inuse: 4229
% 116.64/117.03 Deleted: 9931
% 116.64/117.03 Deletedinuse: 138
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 232710
% 116.64/117.03 Kept: 24050
% 116.64/117.03 Inuse: 4595
% 116.64/117.03 Deleted: 10148
% 116.64/117.03 Deletedinuse: 138
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 353515
% 116.64/117.03 Kept: 26072
% 116.64/117.03 Inuse: 6081
% 116.64/117.03 Deleted: 10239
% 116.64/117.03 Deletedinuse: 138
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 376292
% 116.64/117.03 Kept: 28076
% 116.64/117.03 Inuse: 6285
% 116.64/117.03 Deleted: 10263
% 116.64/117.03 Deletedinuse: 138
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 416741
% 116.64/117.03 Kept: 30094
% 116.64/117.03 Inuse: 6796
% 116.64/117.03 Deleted: 10301
% 116.64/117.03 Deletedinuse: 170
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 462628
% 116.64/117.03 Kept: 32096
% 116.64/117.03 Inuse: 7144
% 116.64/117.03 Deleted: 10613
% 116.64/117.03 Deletedinuse: 170
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 497803
% 116.64/117.03 Kept: 34096
% 116.64/117.03 Inuse: 7528
% 116.64/117.03 Deleted: 10772
% 116.64/117.03 Deletedinuse: 170
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 512316
% 116.64/117.03 Kept: 36144
% 116.64/117.03 Inuse: 7933
% 116.64/117.03 Deleted: 10915
% 116.64/117.03 Deletedinuse: 170
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 116.64/117.03 Done
% 116.64/117.03
% 116.64/117.03
% 116.64/117.03 Intermediate Status:
% 116.64/117.03 Generated: 538707
% 116.64/117.03 Kept: 38157
% 116.64/117.03 Inuse: 8211
% 116.64/117.03 Deleted: 11003
% 116.64/117.03 Deletedinuse: 170
% 116.64/117.03
% 116.64/117.03 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying clauses:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 569311
% 293.79/294.29 Kept: 40158
% 293.79/294.29 Inuse: 8410
% 293.79/294.29 Deleted: 19799
% 293.79/294.29 Deletedinuse: 178
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 604756
% 293.79/294.29 Kept: 42160
% 293.79/294.29 Inuse: 8693
% 293.79/294.29 Deleted: 19941
% 293.79/294.29 Deletedinuse: 186
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 658312
% 293.79/294.29 Kept: 44160
% 293.79/294.29 Inuse: 9320
% 293.79/294.29 Deleted: 20068
% 293.79/294.29 Deletedinuse: 215
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 725977
% 293.79/294.29 Kept: 46160
% 293.79/294.29 Inuse: 9986
% 293.79/294.29 Deleted: 20437
% 293.79/294.29 Deletedinuse: 236
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 794892
% 293.79/294.29 Kept: 48163
% 293.79/294.29 Inuse: 10688
% 293.79/294.29 Deleted: 20801
% 293.79/294.29 Deletedinuse: 292
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 818502
% 293.79/294.29 Kept: 50175
% 293.79/294.29 Inuse: 11002
% 293.79/294.29 Deleted: 20859
% 293.79/294.29 Deletedinuse: 334
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 847880
% 293.79/294.29 Kept: 52179
% 293.79/294.29 Inuse: 11464
% 293.79/294.29 Deleted: 21145
% 293.79/294.29 Deletedinuse: 370
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 868920
% 293.79/294.29 Kept: 54246
% 293.79/294.29 Inuse: 11774
% 293.79/294.29 Deleted: 21295
% 293.79/294.29 Deletedinuse: 382
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 930452
% 293.79/294.29 Kept: 56554
% 293.79/294.29 Inuse: 13211
% 293.79/294.29 Deleted: 21729
% 293.79/294.29 Deletedinuse: 394
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 981308
% 293.79/294.29 Kept: 58565
% 293.79/294.29 Inuse: 13778
% 293.79/294.29 Deleted: 22153
% 293.79/294.29 Deletedinuse: 578
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying clauses:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1045739
% 293.79/294.29 Kept: 60569
% 293.79/294.29 Inuse: 14452
% 293.79/294.29 Deleted: 29889
% 293.79/294.29 Deletedinuse: 578
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1078924
% 293.79/294.29 Kept: 62571
% 293.79/294.29 Inuse: 14975
% 293.79/294.29 Deleted: 30337
% 293.79/294.29 Deletedinuse: 882
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1133248
% 293.79/294.29 Kept: 64573
% 293.79/294.29 Inuse: 15374
% 293.79/294.29 Deleted: 30704
% 293.79/294.29 Deletedinuse: 906
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1231524
% 293.79/294.29 Kept: 66580
% 293.79/294.29 Inuse: 16233
% 293.79/294.29 Deleted: 31161
% 293.79/294.29 Deletedinuse: 950
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1272252
% 293.79/294.29 Kept: 68580
% 293.79/294.29 Inuse: 16830
% 293.79/294.29 Deleted: 31496
% 293.79/294.29 Deletedinuse: 950
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1445933
% 293.79/294.29 Kept: 70580
% 293.79/294.29 Inuse: 18607
% 293.79/294.29 Deleted: 31821
% 293.79/294.29 Deletedinuse: 950
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1507837
% 293.79/294.29 Kept: 72581
% 293.79/294.29 Inuse: 19251
% 293.79/294.29 Deleted: 32277
% 293.79/294.29 Deletedinuse: 970
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1560953
% 293.79/294.29 Kept: 74581
% 293.79/294.29 Inuse: 19935
% 293.79/294.29 Deleted: 32325
% 293.79/294.29 Deletedinuse: 974
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1649392
% 293.79/294.29 Kept: 76585
% 293.79/294.29 Inuse: 22510
% 293.79/294.29 Deleted: 33445
% 293.79/294.29 Deletedinuse: 974
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1740774
% 293.79/294.29 Kept: 78585
% 293.79/294.29 Inuse: 23368
% 293.79/294.29 Deleted: 33869
% 293.79/294.29 Deletedinuse: 974
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying clauses:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1856538
% 293.79/294.29 Kept: 80587
% 293.79/294.29 Inuse: 24197
% 293.79/294.29 Deleted: 42376
% 293.79/294.29 Deletedinuse: 1031
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 1942047
% 293.79/294.29 Kept: 82594
% 293.79/294.29 Inuse: 25375
% 293.79/294.29 Deleted: 43009
% 293.79/294.29 Deletedinuse: 1031
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29 Resimplifying inuse:
% 293.79/294.29 Done
% 293.79/294.29
% 293.79/294.29
% 293.79/294.29 Intermediate Status:
% 293.79/294.29 Generated: 2047715
% 293.79/294.29 Kept: 84596
% 293.79/294.29 Inuse: 26119
% 293.79/294.29 DelTerminated
% 299.61/300.03 Bliksem ended
%------------------------------------------------------------------------------