%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX227+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n008.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 298.89s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX227+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.17/0.34 % Computer : n008.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % DateTime : Tue May 5 12:51:13 EDT 2026
% 0.17/0.34 % CPUTime :
% 31.24/31.82 *** allocated 10000 integers for termspace/termends
% 31.24/31.82 *** allocated 10000 integers for clauses
% 31.24/31.82 *** allocated 10000 integers for justifications
% 31.24/31.82 Bliksem 1.12
% 31.24/31.82
% 31.24/31.82
% 31.24/31.82 Automatic Strategy Selection
% 31.24/31.82
% 31.24/31.82
% 31.24/31.82 Clauses:
% 31.24/31.82
% 31.24/31.82 { proj1( x( X, Y ) ) = X }.
% 31.24/31.82 { proj2( x( X, Y ) ) = Y }.
% 31.24/31.82 { ! x( X, Y ) = theVar }.
% 31.24/31.82 { ! x( X, Y ) = k }.
% 31.24/31.82 { ! x( X, Y ) = i }.
% 31.24/31.82 { ! x( X, Y ) = s }.
% 31.24/31.82 { ! x( X, Y ) = b }.
% 31.24/31.82 { ! x( X, Y ) = c }.
% 31.24/31.82 { ! theVar = k }.
% 31.24/31.82 { ! theVar = i }.
% 31.24/31.82 { ! theVar = s }.
% 31.24/31.82 { ! theVar = b }.
% 31.24/31.82 { ! theVar = c }.
% 31.24/31.82 { ! k = i }.
% 31.24/31.82 { ! k = s }.
% 31.24/31.82 { ! k = b }.
% 31.24/31.82 { ! k = c }.
% 31.24/31.82 { ! i = s }.
% 31.24/31.82 { ! i = b }.
% 31.24/31.82 { ! i = c }.
% 31.24/31.82 { ! s = b }.
% 31.24/31.82 { ! s = c }.
% 31.24/31.82 { ! b = c }.
% 31.24/31.82 { proj1Suc( suc( X ) ) = X }.
% 31.24/31.82 { ! suc( X ) = z }.
% 31.24/31.82 { proj1Just( just( X ) ) = X }.
% 31.24/31.82 { ! nothing = just( X ) }.
% 31.24/31.82 { fail( X, Y ) = par( X, Y, step( X ), step( Y ) ) }.
% 31.24/31.82 { par( X, Y, nothing, nothing ) = nothing }.
% 31.24/31.82 { par( X, Y, nothing, just( Z ) ) = just( x( X, Z ) ) }.
% 31.24/31.82 { par( X, Y, just( Z ), nothing ) = just( x( Z, Y ) ) }.
% 31.24/31.82 { par( X, Y, just( Z ), just( T ) ) = just( x( Z, T ) ) }.
% 31.24/31.82 { X = x( proj1( X ), proj2( X ) ), step( X ) = nothing }.
% 31.24/31.82 { X = x( proj1( X ), proj2( X ) ), X = i, step( x( X, Y ) ) = fail( X, Y )
% 31.24/31.82 }.
% 31.24/31.82 { X = x( proj1( X ), proj2( X ) ), X = k, step( x( x( X, Z ), Y ) ) = fail
% 31.24/31.82 ( x( X, Z ), Y ) }.
% 31.24/31.82 { X = s, X = b, X = c, step( x( x( x( X, T ), Z ), Y ) ) = fail( x( x( X, T
% 31.24/31.82 ), Z ), Y ) }.
% 31.24/31.82 { step( x( x( x( s, Z ), Y ), X ) ) = just( x( x( Z, X ), x( Y, X ) ) ) }.
% 31.24/31.82 { step( x( x( x( b, Z ), Y ), X ) ) = just( x( Z, x( Y, X ) ) ) }.
% 31.24/31.82 { step( x( x( x( c, Z ), Y ), X ) ) = just( x( x( Z, X ), Y ) ) }.
% 31.24/31.82 { step( x( x( k, Y ), X ) ) = just( Y ) }.
% 31.24/31.82 { step( x( i, X ) ) = just( X ) }.
% 31.24/31.82 { X = x( proj1( X ), proj2( X ) ), X = theVar, ! cheating( X ) }.
% 31.24/31.82 { ! cheating( x( X, Y ) ), cheating( X ), cheating( Y ) }.
% 31.24/31.82 { ! cheating( X ), cheating( x( X, Y ) ) }.
% 31.24/31.82 { ! cheating( Y ), cheating( x( X, Y ) ) }.
% 31.24/31.82 { cheating( theVar ) }.
% 31.24/31.82 { ! step( X ) = nothing, astep( suc( Y ), X ) = nothing }.
% 31.24/31.82 { ! step( X ) = just( Y ), astep( suc( Z ), X ) = astep( Z, Y ) }.
% 31.24/31.82 { astep( z, X ) = just( X ) }.
% 31.24/31.82 { ! astep( suc( suc( suc( suc( z ) ) ) ), x( X, theVar ) ) = just( x(
% 31.24/31.82 theVar, x( X, theVar ) ) ), cheating( X ) }.
% 31.24/31.82
% 31.24/31.82 percentage equality = 0.850746, percentage horn = 0.880000
% 31.24/31.82 This is a pure equality problem
% 31.24/31.82
% 31.24/31.82
% 31.24/31.82
% 31.24/31.82 Options Used:
% 31.24/31.82
% 31.24/31.82 useres = 1
% 31.24/31.82 useparamod = 1
% 31.24/31.82 useeqrefl = 1
% 31.24/31.82 useeqfact = 1
% 31.24/31.82 usefactor = 1
% 31.24/31.82 usesimpsplitting = 0
% 31.24/31.82 usesimpdemod = 5
% 31.24/31.82 usesimpres = 3
% 31.24/31.82
% 31.24/31.82 resimpinuse = 1000
% 31.24/31.82 resimpclauses = 20000
% 31.24/31.82 substype = eqrewr
% 31.24/31.82 backwardsubs = 1
% 31.24/31.82 selectoldest = 5
% 31.24/31.82
% 31.24/31.82 litorderings [0] = split
% 31.24/31.82 litorderings [1] = extend the termordering, first sorting on arguments
% 31.24/31.82
% 31.24/31.82 termordering = kbo
% 31.24/31.82
% 31.24/31.82 litapriori = 0
% 31.24/31.82 termapriori = 1
% 31.24/31.82 litaposteriori = 0
% 31.24/31.82 termaposteriori = 0
% 31.24/31.82 demodaposteriori = 0
% 31.24/31.82 ordereqreflfact = 0
% 31.24/31.82
% 31.24/31.82 litselect = negord
% 31.24/31.82
% 31.24/31.82 maxweight = 15
% 31.24/31.82 maxdepth = 30000
% 31.24/31.82 maxlength = 115
% 31.24/31.82 maxnrvars = 195
% 31.24/31.82 excuselevel = 1
% 31.24/31.82 increasemaxweight = 1
% 31.24/31.82
% 31.24/31.82 maxselected = 10000000
% 31.24/31.82 maxnrclauses = 10000000
% 31.24/31.82
% 31.24/31.82 showgenerated = 0
% 31.24/31.82 showkept = 0
% 31.24/31.82 showselected = 0
% 31.24/31.82 showdeleted = 0
% 31.24/31.82 showresimp = 1
% 31.24/31.82 showstatus = 2000
% 31.24/31.82
% 31.24/31.82 prologoutput = 0
% 31.24/31.82 nrgoals = 5000000
% 31.24/31.82 totalproof = 1
% 31.24/31.82
% 31.24/31.82 Symbols occurring in the translation:
% 31.24/31.82
% 31.24/31.82 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 31.24/31.82 . [1, 2] (w:1, o:41, a:1, s:1, b:0),
% 31.24/31.82 ! [4, 1] (w:0, o:28, a:1, s:1, b:0),
% 31.24/31.82 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 31.24/31.82 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 31.24/31.82 x [37, 2] (w:1, o:65, a:1, s:1, b:0),
% 31.24/31.82 proj1 [38, 1] (w:1, o:33, a:1, s:1, b:0),
% 31.24/31.82 proj2 [39, 1] (w:1, o:36, a:1, s:1, b:0),
% 31.24/31.82 theVar [40, 0] (w:1, o:9, a:1, s:1, b:0),
% 31.24/31.82 k [41, 0] (w:1, o:10, a:1, s:1, b:0),
% 31.24/31.82 i [42, 0] (w:1, o:11, a:1, s:1, b:0),
% 31.24/31.82 s [43, 0] (w:1, o:8, a:1, s:1, b:0),
% 31.24/31.82 b [44, 0] (w:1, o:12, a:1, s:1, b:0),
% 31.24/31.82 c [45, 0] (w:1, o:13, a:1, s:1, b:0),
% 31.24/31.82 suc [46, 1] (w:1, o:38, a:1, s:1, b:0),
% 31.24/31.82 proj1Suc [47, 1] (w:1, o:34, a:1, s:1, b:0),
% 31.24/31.82 z [48, 0] (w:1, o:14, a:1, s:1, b:0),
% 31.24/31.82 just [49, 1] (w:1, o:39, a:1, s:1, b:0),
% 31.24/31.82 proj1Just [50, 1] (w:1, o:35, a:1, s:1, b:0),
% 228.47/229.62 nothing [51, 0] (w:1, o:15, a:1, s:1, b:0),
% 228.47/229.62 fail [54, 2] (w:1, o:66, a:1, s:1, b:0),
% 228.47/229.62 step [55, 1] (w:1, o:37, a:1, s:1, b:0),
% 228.47/229.62 par [56, 4] (w:1, o:68, a:1, s:1, b:0),
% 228.47/229.62 cheating [63, 1] (w:1, o:40, a:1, s:1, b:0),
% 228.47/229.62 astep [67, 2] (w:1, o:67, a:1, s:1, b:0).
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Starting Search:
% 228.47/229.62
% 228.47/229.62 *** allocated 15000 integers for clauses
% 228.47/229.62 *** allocated 22500 integers for clauses
% 228.47/229.62 *** allocated 33750 integers for clauses
% 228.47/229.62 *** allocated 15000 integers for termspace/termends
% 228.47/229.62 *** allocated 50625 integers for clauses
% 228.47/229.62 *** allocated 22500 integers for termspace/termends
% 228.47/229.62 *** allocated 75937 integers for clauses
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 33750 integers for termspace/termends
% 228.47/229.62 *** allocated 113905 integers for clauses
% 228.47/229.62 *** allocated 170857 integers for clauses
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 7803
% 228.47/229.62 Kept: 2208
% 228.47/229.62 Inuse: 151
% 228.47/229.62 Deleted: 5
% 228.47/229.62 Deletedinuse: 0
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 50625 integers for termspace/termends
% 228.47/229.62 *** allocated 256285 integers for clauses
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 75937 integers for termspace/termends
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 13767
% 228.47/229.62 Kept: 4266
% 228.47/229.62 Inuse: 196
% 228.47/229.62 Deleted: 5
% 228.47/229.62 Deletedinuse: 0
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 384427 integers for clauses
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 113905 integers for termspace/termends
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 19855
% 228.47/229.62 Kept: 6286
% 228.47/229.62 Inuse: 243
% 228.47/229.62 Deleted: 5
% 228.47/229.62 Deletedinuse: 0
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 576640 integers for clauses
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 27037
% 228.47/229.62 Kept: 8291
% 228.47/229.62 Inuse: 287
% 228.47/229.62 Deleted: 5
% 228.47/229.62 Deletedinuse: 0
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 170857 integers for termspace/termends
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 34217
% 228.47/229.62 Kept: 10308
% 228.47/229.62 Inuse: 344
% 228.47/229.62 Deleted: 5
% 228.47/229.62 Deletedinuse: 0
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 864960 integers for clauses
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 40647
% 228.47/229.62 Kept: 12311
% 228.47/229.62 Inuse: 389
% 228.47/229.62 Deleted: 5
% 228.47/229.62 Deletedinuse: 0
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 256285 integers for termspace/termends
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 48743
% 228.47/229.62 Kept: 14466
% 228.47/229.62 Inuse: 441
% 228.47/229.62 Deleted: 5
% 228.47/229.62 Deletedinuse: 0
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 69225
% 228.47/229.62 Kept: 16496
% 228.47/229.62 Inuse: 487
% 228.47/229.62 Deleted: 6
% 228.47/229.62 Deletedinuse: 0
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 89605
% 228.47/229.62 Kept: 18499
% 228.47/229.62 Inuse: 539
% 228.47/229.62 Deleted: 9
% 228.47/229.62 Deletedinuse: 2
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 1297440 integers for clauses
% 228.47/229.62 *** allocated 384427 integers for termspace/termends
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 Resimplifying clauses:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 108194
% 228.47/229.62 Kept: 20711
% 228.47/229.62 Inuse: 609
% 228.47/229.62 Deleted: 145
% 228.47/229.62 Deletedinuse: 2
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 121646
% 228.47/229.62 Kept: 22801
% 228.47/229.62 Inuse: 647
% 228.47/229.62 Deleted: 145
% 228.47/229.62 Deletedinuse: 2
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 126139
% 228.47/229.62 Kept: 25265
% 228.47/229.62 Inuse: 653
% 228.47/229.62 Deleted: 145
% 228.47/229.62 Deletedinuse: 2
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 129912
% 228.47/229.62 Kept: 27265
% 228.47/229.62 Inuse: 658
% 228.47/229.62 Deleted: 145
% 228.47/229.62 Deletedinuse: 2
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 1946160 integers for clauses
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 133733
% 228.47/229.62 Kept: 29289
% 228.47/229.62 Inuse: 663
% 228.47/229.62 Deleted: 145
% 228.47/229.62 Deletedinuse: 2
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 *** allocated 576640 integers for termspace/termends
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 138394
% 228.47/229.62 Kept: 31497
% 228.47/229.62 Inuse: 668
% 228.47/229.62 Deleted: 145
% 228.47/229.62 Deletedinuse: 2
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62 Resimplifying inuse:
% 228.47/229.62 Done
% 228.47/229.62
% 228.47/229.62
% 228.47/229.62 Intermediate Status:
% 228.47/229.62 Generated: 143107
% 228.47/229.62 Kept: 33565
% 228.47/229.62 Inuse: 673
% 228.47/229.62 Deleted: 145
% 228.47/229.62 Deletedinuse: 2
% 228.47/229.62
% 228.47/229.62 Resimplifying iTerminated
% 298.89/300.03 Bliksem ended
%------------------------------------------------------------------------------