%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX202-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n027.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:47 PM UTC 2026
% Result : Timeout 299.46s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX202-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.12 % Command : bliksem %s
% 0.15/0.33 % Computer : n027.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % DateTime : Tue May 5 11:22:49 EDT 2026
% 0.15/0.34 % CPUTime :
% 8.43/8.85 *** allocated 10000 integers for termspace/termends
% 8.43/8.85 *** allocated 10000 integers for clauses
% 8.43/8.85 *** allocated 10000 integers for justifications
% 8.43/8.85 Bliksem 1.12
% 8.43/8.85
% 8.43/8.85
% 8.43/8.85 Automatic Strategy Selection
% 8.43/8.85
% 8.43/8.85 Clauses:
% 8.43/8.85 [
% 8.43/8.85 [ =( aux( X, Y, Z, pair2( T, U ) ), pair2( cons( Y, T ), U ) ) ],
% 8.43/8.85 [ =( aux2( X, Y, Z, T, btrue ), cons( X, merge( Y, cons( Z, T ) ) ) ) ]
% 8.43/8.85 ,
% 8.43/8.85 [ =( aux2( X, Y, Z, T, bfalse ), cons( Z, merge( cons( X, Y ), T ) ) ) ]
% 8.43/8.85 ,
% 8.43/8.85 [ =( aux3( X, Y, Z, pair2( T, U ) ), merge( msort( T ), msort( U ) ) ) ]
% 8.43/8.85 ,
% 8.43/8.85 [ =( aux4( X, Y, Z, btrue ), s( count( X, Z ) ) ) ],
% 8.43/8.85 [ =( aux4( X, Y, Z, bfalse ), count( X, Z ) ) ],
% 8.43/8.85 [ =( splitAtNat( z, X ), pair2( nil, X ) ) ],
% 8.43/8.85 [ =( splitAtNat( s( X ), nil ), pair2( nil, nil ) ) ],
% 8.43/8.85 [ =( splitAtNat( s( X ), cons( Y, Z ) ), aux( X, Y, Z, splitAtNat( X, Z
% 8.43/8.85 ) ) ) ],
% 8.43/8.85 [ =( leqNat( z, X ), btrue ) ],
% 8.43/8.85 [ =( leqNat( s( X ), z ), bfalse ) ],
% 8.43/8.85 [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ],
% 8.43/8.85 [ =( merge( nil, X ), X ) ],
% 8.43/8.85 [ =( merge( cons( X, Y ), nil ), cons( X, Y ) ) ],
% 8.43/8.85 [ =( merge( cons( X, Y ), cons( Z, T ) ), aux2( X, Y, Z, T, leqNat( X, Z
% 8.43/8.85 ) ) ) ],
% 8.43/8.85 [ =( lengthNat( nil ), z ) ],
% 8.43/8.85 [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ],
% 8.43/8.85 [ =( impl( btrue, X ), X ) ],
% 8.43/8.85 [ =( impl( bfalse, X ), btrue ) ],
% 8.43/8.85 [ =( div2( z ), z ) ],
% 8.43/8.85 [ =( div2( s( z ) ), z ) ],
% 8.43/8.85 [ =( div2( s( s( X ) ) ), s( div2( X ) ) ) ],
% 8.43/8.85 [ =( msort( nil ), nil ) ],
% 8.43/8.85 [ =( msort( cons( X, nil ) ), cons( X, nil ) ) ],
% 8.43/8.85 [ =( msort( cons( X, cons( Y, Z ) ) ), aux3( X, Y, Z, splitAtNat( div2(
% 8.43/8.85 lengthNat( cons( X, cons( Y, Z ) ) ) ), cons( X, cons( Y, Z ) ) ) ) ) ]
% 8.43/8.85 ,
% 8.43/8.85 [ =( count( X, nil ), z ) ],
% 8.43/8.85 [ =( count( X, cons( Y, Z ) ), aux4( X, Y, Z, eq( Y, X ) ) ) ],
% 8.43/8.85 [ =( 'prop_msort_permutation_wrong2'( X, Y ), impl( eq2( leqNat( count(
% 8.43/8.85 Y, X ), s( s( s( s( s( z ) ) ) ) ) ), bfalse ), eq( count( s( Y ), X ),
% 8.43/8.85 count( Y, msort( X ) ) ) ) ) ],
% 8.43/8.85 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 8.43/8.85 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 8.43/8.85 [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ],
% 8.43/8.85 [ =( eq( z, s( X ) ), bfalse ) ],
% 8.43/8.85 [ =( eq( s( X ), z ), bfalse ) ],
% 8.43/8.85 [ =( eq( X, X ), btrue ) ],
% 8.43/8.85 [ =( eq2( X, X ), btrue ) ],
% 8.43/8.85 [ ~( =( eq2( 'prop_msort_permutation_wrong2'( X, Y ), bfalse ), btrue )
% 8.43/8.85 ) ]
% 8.43/8.85 ] .
% 8.43/8.85
% 8.43/8.85
% 8.43/8.85 percentage equality = 1.000000, percentage horn = 1.000000
% 8.43/8.85 This is a pure equality problem
% 8.43/8.85
% 8.43/8.85
% 8.43/8.85
% 8.43/8.85 Options Used:
% 8.43/8.85
% 8.43/8.85 useres = 1
% 8.43/8.85 useparamod = 1
% 8.43/8.85 useeqrefl = 1
% 8.43/8.85 useeqfact = 1
% 8.43/8.85 usefactor = 1
% 8.43/8.85 usesimpsplitting = 0
% 8.43/8.85 usesimpdemod = 5
% 8.43/8.85 usesimpres = 3
% 8.43/8.85
% 8.43/8.85 resimpinuse = 1000
% 8.43/8.85 resimpclauses = 20000
% 8.43/8.85 substype = eqrewr
% 8.43/8.85 backwardsubs = 1
% 8.43/8.85 selectoldest = 5
% 8.43/8.85
% 8.43/8.85 litorderings [0] = split
% 8.43/8.85 litorderings [1] = extend the termordering, first sorting on arguments
% 8.43/8.85
% 8.43/8.85 termordering = kbo
% 8.43/8.85
% 8.43/8.85 litapriori = 0
% 8.43/8.85 termapriori = 1
% 8.43/8.85 litaposteriori = 0
% 8.43/8.85 termaposteriori = 0
% 8.43/8.85 demodaposteriori = 0
% 8.43/8.85 ordereqreflfact = 0
% 8.43/8.85
% 8.43/8.85 litselect = negord
% 8.43/8.85
% 8.43/8.85 maxweight = 15
% 8.43/8.85 maxdepth = 30000
% 8.43/8.85 maxlength = 115
% 8.43/8.85 maxnrvars = 195
% 8.43/8.85 excuselevel = 1
% 8.43/8.85 increasemaxweight = 1
% 8.43/8.85
% 8.43/8.85 maxselected = 10000000
% 8.43/8.85 maxnrclauses = 10000000
% 8.43/8.85
% 8.43/8.85 showgenerated = 0
% 8.43/8.85 showkept = 0
% 8.43/8.85 showselected = 0
% 8.43/8.85 showdeleted = 0
% 8.43/8.85 showresimp = 1
% 8.43/8.85 showstatus = 2000
% 8.43/8.85
% 8.43/8.85 prologoutput = 1
% 8.43/8.85 nrgoals = 5000000
% 8.43/8.85 totalproof = 1
% 8.43/8.85
% 8.43/8.85 Symbols occurring in the translation:
% 8.43/8.85
% 8.43/8.85 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 8.43/8.85 . [1, 2] (w:1, o:35, a:1, s:1, b:0),
% 8.43/8.85 ! [4, 1] (w:0, o:26, a:1, s:1, b:0),
% 8.43/8.85 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 8.43/8.85 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 8.43/8.85 pair2 [44, 2] (w:1, o:60, a:1, s:1, b:0),
% 8.43/8.85 aux [45, 4] (w:1, o:70, a:1, s:1, b:0),
% 8.43/8.85 cons [46, 2] (w:1, o:61, a:1, s:1, b:0),
% 8.43/8.85 btrue [50, 0] (w:1, o:19, a:1, s:1, b:0),
% 8.43/8.85 aux2 [51, 5] (w:1, o:73, a:1, s:1, b:0),
% 8.43/8.85 merge [52, 2] (w:1, o:63, a:1, s:1, b:0),
% 8.43/8.85 bfalse [53, 0] (w:1, o:20, a:1, s:1, b:0),
% 8.43/8.85 aux3 [55, 4] (w:1, o:71, a:1, s:1, b:0),
% 8.43/8.85 msort [56, 1] (w:1, o:32, a:1, s:1, b:0),
% 8.43/8.85 aux4 [58, 4] (w:1, o:72, a:1, s:1, b:0),
% 98.35/98.79 count [59, 2] (w:1, o:64, a:1, s:1, b:0),
% 98.35/98.79 s [60, 1] (w:1, o:33, a:1, s:1, b:0),
% 98.35/98.79 z [61, 0] (w:1, o:21, a:1, s:1, b:0),
% 98.35/98.79 splitAtNat [62, 2] (w:1, o:65, a:1, s:1, b:0),
% 98.35/98.79 nil [63, 0] (w:1, o:22, a:1, s:1, b:0),
% 98.35/98.79 leqNat [64, 2] (w:1, o:62, a:1, s:1, b:0),
% 98.35/98.79 lengthNat [66, 1] (w:1, o:31, a:1, s:1, b:0),
% 98.35/98.79 impl [68, 2] (w:1, o:66, a:1, s:1, b:0),
% 98.35/98.79 div2 [69, 1] (w:1, o:34, a:1, s:1, b:0),
% 98.35/98.79 eq [71, 2] (w:1, o:67, a:1, s:1, b:0),
% 98.35/98.79 'prop_msort_permutation_wrong2' [72, 2] (w:1, o:68, a:1, s:1, b:0),
% 98.35/98.79 eq2 [73, 2] (w:1, o:69, a:1, s:1, b:0).
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 15
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 628
% 98.35/98.79 Kept: 90
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 16
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 16
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 628
% 98.35/98.79 Kept: 90
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 17
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 17
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 961
% 98.35/98.79 Kept: 121
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 18
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 18
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 1095
% 98.35/98.79 Kept: 133
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 19
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 19
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 1427
% 98.35/98.79 Kept: 156
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 20
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 20
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 1499
% 98.35/98.79 Kept: 163
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 21
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 21
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 3843
% 98.35/98.79 Kept: 326
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 22
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 22
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 5274
% 98.35/98.79 Kept: 410
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 23
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 23
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 17169
% 98.35/98.79 Kept: 914
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 24
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 24
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 36833
% 98.35/98.79 Kept: 1369
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 25
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 Intermediate Status:
% 98.35/98.79 Generated: 22834
% 98.35/98.79 Kept: 2001
% 98.35/98.79 Inuse: 810
% 98.35/98.79 Deleted: 85
% 98.35/98.79 Deletedinuse: 11
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 25
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 103375
% 98.35/98.79 Kept: 2327
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 26
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 Intermediate Status:
% 98.35/98.79 Generated: 14470
% 98.35/98.79 Kept: 2001
% 98.35/98.79 Inuse: 583
% 98.35/98.79 Deleted: 72
% 98.35/98.79 Deletedinuse: 10
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 26
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 153921
% 98.35/98.79 Kept: 2837
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 27
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 Intermediate Status:
% 98.35/98.79 Generated: 11920
% 98.35/98.79 Kept: 2004
% 98.35/98.79 Inuse: 510
% 98.35/98.79 Deleted: 88
% 98.35/98.79 Deletedinuse: 10
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 Intermediate Status:
% 98.35/98.79 Generated: 80357
% 98.35/98.79 Kept: 4005
% 98.35/98.79 Inuse: 1478
% 98.35/98.79 Deleted: 169
% 98.35/98.79 Deletedinuse: 15
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79 Failed to find proof!
% 98.35/98.79 maxweight = 27
% 98.35/98.79 maxnrclauses = 10000000
% 98.35/98.79 Generated: 490425
% 98.35/98.79 Kept: 4558
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 The strategy used was not complete!
% 98.35/98.79
% 98.35/98.79 Increased maxweight to 28
% 98.35/98.79
% 98.35/98.79 Starting Search:
% 98.35/98.79
% 98.35/98.79 Resimplifying inuse:
% 98.35/98.79 Done
% 98.35/98.79
% 98.35/98.79
% 98.35/98.79 Intermediate Status:
% 98.35/98.79 Generated: 8906
% 98.35/98.79 Kept: 2003
% 98.35/98.79 Inuse: 459
% 98.35/98.79 Deleted: 96
% 98.35/98.79 Deletedinuse: 11
% 98.35/98.79
% 98.35/98.79 Resimplifying inuseTerminated
% 299.46/300.03 Bliksem ended
%------------------------------------------------------------------------------