%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX231-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n010.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:52 PM UTC 2026
% Result : Timeout 299.65s 300.03s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX231-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.16/0.33 % Computer : n010.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % DateTime : Tue May 5 13:01:21 EDT 2026
% 0.16/0.33 % CPUTime :
% 2.51/3.02 *** allocated 10000 integers for termspace/termends
% 2.51/3.02 *** allocated 10000 integers for clauses
% 2.51/3.02 *** allocated 10000 integers for justifications
% 2.51/3.02 Bliksem 1.12
% 2.51/3.02
% 2.51/3.02
% 2.51/3.02 Automatic Strategy Selection
% 2.51/3.02
% 2.51/3.02 Clauses:
% 2.51/3.02 [
% 2.51/3.02 [ =( aux( X, Y, btrue ), nil3 ) ],
% 2.51/3.02 [ =( aux( X, Y, bfalse ), cons3( X, enumFromToNat( suc( X ), Y ) ) ) ]
% 2.51/3.02 ,
% 2.51/3.02 [ =( aux2( X, Y, Z, T, nothing ), cons4( bfalse, colouring( X, Y ) ) ) ]
% 2.51/3.02 ,
% 2.51/3.02 [ =( aux2( X, Y, Z, T, just( U ) ), cons4( notb( eq( T, U ) ), colouring(
% 2.51/3.02 X, Y ) ) ) ],
% 2.51/3.02 [ =( aux3( X, Y, Z, T, nothing ), cons4( bfalse, colouring( X, Y ) ) ) ]
% 2.51/3.02 ,
% 2.51/3.02 [ =( aux3( X, Y, Z, T, just( U ) ), aux2( X, Y, T, U, index( X, T ) ) )
% 2.51/3.02 ],
% 2.51/3.02 [ =( ten, suc( suc( suc( suc( suc( suc( suc( suc( suc( suc( zero ) ) ) )
% 2.51/3.02 ) ) ) ) ) ) ) ],
% 2.51/3.02 [ =( predNat( zero ), zero ) ],
% 2.51/3.02 [ =( predNat( suc( X ) ), X ) ],
% 2.51/3.02 [ =( petersen2( nil3 ), nil ) ],
% 2.51/3.02 [ =( petersen2( cons3( X, Y ) ), cons( pair2( X, suc( X ) ), petersen2(
% 2.51/3.02 Y ) ) ) ],
% 2.51/3.02 [ =( one, suc( zero ) ) ],
% 2.51/3.02 [ =( two, suc( one ) ) ],
% 2.51/3.02 [ =( three, suc( two ) ) ],
% 2.51/3.02 [ =( notb( btrue ), bfalse ) ],
% 2.51/3.02 [ =( notb( bfalse ), btrue ) ],
% 2.51/3.02 [ =( lt( zero, zero ), bfalse ) ],
% 2.51/3.02 [ =( lt( zero, suc( X ) ), btrue ) ],
% 2.51/3.02 [ =( lt( suc( X ), zero ), bfalse ) ],
% 2.51/3.02 [ =( lt( suc( X ), suc( Y ) ), lt( X, Y ) ) ],
% 2.51/3.02 [ =( 'prop_p31'( nil3 ), nil4 ) ],
% 2.51/3.02 [ =( 'prop_p31'( cons3( X, Y ) ), cons4( lt( X, three ), 'prop_p31'( Y )
% 2.51/3.02 ) ) ],
% 2.51/3.02 [ =( index( nil3, X ), nothing ) ],
% 2.51/3.02 [ =( index( cons3( X, Y ), zero ), just( X ) ) ],
% 2.51/3.02 [ =( index( cons3( X, Y ), suc( Z ) ), index( Y, Z ) ) ],
% 2.51/3.02 [ =( four, suc( three ) ) ],
% 2.51/3.02 [ =( five, suc( four ) ) ],
% 2.51/3.02 [ =( seven, suc( suc( five ) ) ) ],
% 2.51/3.02 [ =( nine, suc( suc( seven ) ) ) ],
% 2.51/3.02 [ =( enumFromToNat( X, Y ), aux( X, Y, lt( Y, X ) ) ) ],
% 2.51/3.02 [ =( eleven, suc( suc( nine ) ) ) ],
% 2.51/3.02 [ =( colouring( X, nil ), nil4 ) ],
% 2.51/3.02 [ =( colouring( X, cons( pair2( Y, Z ), T ) ), aux3( X, T, Y, Z, index(
% 2.51/3.02 X, Y ) ) ) ],
% 2.51/3.02 [ =( append( nil, X ), X ) ],
% 2.51/3.02 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 2.51/3.02 [ =( concat( nil2 ), nil ) ],
% 2.51/3.02 [ =( concat( cons2( X, Y ) ), append( X, concat( Y ) ) ) ],
% 2.51/3.02 [ =( andb( btrue, X ), X ) ],
% 2.51/3.02 [ =( andb( bfalse, X ), bfalse ) ],
% 2.51/3.02 [ =( and2( nil4 ), btrue ) ],
% 2.51/3.02 [ =( and2( cons4( X, Y ) ), andb( X, and2( Y ) ) ) ],
% 2.51/3.02 [ =( colouring2( X, Y ), and2( colouring( Y, X ) ) ) ],
% 2.51/3.02 [ =( add( zero, X ), X ) ],
% 2.51/3.02 [ =( add( suc( X ), Y ), suc( add( X, Y ) ) ) ],
% 2.51/3.02 [ =( petersen( X, nil ), nil2 ) ],
% 2.51/3.02 [ =( petersen( X, cons( pair2( Y, Z ), T ) ), cons2( cons( pair2( Y, Z )
% 2.51/3.02 , cons( pair2( add( suc( X ), Y ), add( suc( X ), Z ) ), nil ) ),
% 2.51/3.02 petersen( X, T ) ) ) ],
% 2.51/3.02 [ =( petersen3( X, nil3 ), nil ) ],
% 2.51/3.02 [ =( petersen3( X, cons3( Y, Z ) ), cons( pair2( Y, add( suc( X ), Y ) )
% 2.51/3.02 , petersen3( X, Z ) ) ) ],
% 2.51/3.02 [ =( petersen4( zero ), nil ) ],
% 2.51/3.02 [ =( petersen4( suc( X ) ), append( concat( petersen( X, cons( pair2( X
% 2.51/3.02 , zero ), petersen2( enumFromToNat( zero, X ) ) ) ) ), petersen3( X,
% 2.51/3.02 enumFromToNat( zero, suc( X ) ) ) ) ) ],
% 2.51/3.02 [ =( twentyOne, add( ten, eleven ) ) ],
% 2.51/3.02 [ =( thirtyOne, add( twentyOne, ten ) ) ],
% 2.51/3.02 [ =( 'prop_p312'( X ), notb( andb( colouring2( petersen4( thirtyOne ), X
% 2.51/3.02 ), and2( 'prop_p31'( X ) ) ) ) ) ],
% 2.51/3.02 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 2.51/3.02 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 2.51/3.02 [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ],
% 2.51/3.02 [ =( eq( zero, suc( X ) ), bfalse ) ],
% 2.51/3.02 [ =( eq( suc( X ), zero ), bfalse ) ],
% 2.51/3.02 [ =( eq( X, X ), btrue ) ],
% 2.51/3.02 [ =( eq2( X, X ), btrue ) ],
% 2.51/3.02 [ ~( =( eq2( 'prop_p312'( X ), bfalse ), btrue ) ) ]
% 2.51/3.02 ] .
% 2.51/3.02
% 2.51/3.02
% 2.51/3.02 percentage equality = 1.000000, percentage horn = 1.000000
% 2.51/3.02 This is a pure equality problem
% 2.51/3.02
% 2.51/3.02
% 2.51/3.02
% 2.51/3.02 Options Used:
% 2.51/3.02
% 2.51/3.02 useres = 1
% 2.51/3.02 useparamod = 1
% 2.51/3.02 useeqrefl = 1
% 2.51/3.02 useeqfact = 1
% 2.51/3.02 usefactor = 1
% 2.51/3.02 usesimpsplitting = 0
% 2.51/3.02 usesimpdemod = 5
% 2.51/3.02 usesimpres = 3
% 2.51/3.02
% 2.51/3.02 resimpinuse = 1000
% 2.51/3.02 resimpclauses = 20000
% 2.51/3.02 substype = eqrewr
% 2.51/3.02 backwardsubs = 1
% 2.51/3.02 selectoldest = 5
% 2.51/3.02
% 2.51/3.02 litorderings [0] = split
% 2.51/3.02 litorderings [1] = extend the termordering, first sorting on arguments
% 2.51/3.02
% 2.51/3.02 termordering = kbo
% 2.51/3.02
% 2.51/3.02 litapriori = 0
% 46.20/46.66 termapriori = 1
% 46.20/46.66 litaposteriori = 0
% 46.20/46.66 termaposteriori = 0
% 46.20/46.66 demodaposteriori = 0
% 46.20/46.66 ordereqreflfact = 0
% 46.20/46.66
% 46.20/46.66 litselect = negord
% 46.20/46.66
% 46.20/46.66 maxweight = 15
% 46.20/46.66 maxdepth = 30000
% 46.20/46.66 maxlength = 115
% 46.20/46.66 maxnrvars = 195
% 46.20/46.66 excuselevel = 1
% 46.20/46.66 increasemaxweight = 1
% 46.20/46.66
% 46.20/46.66 maxselected = 10000000
% 46.20/46.66 maxnrclauses = 10000000
% 46.20/46.66
% 46.20/46.66 showgenerated = 0
% 46.20/46.66 showkept = 0
% 46.20/46.66 showselected = 0
% 46.20/46.66 showdeleted = 0
% 46.20/46.66 showresimp = 1
% 46.20/46.66 showstatus = 2000
% 46.20/46.66
% 46.20/46.66 prologoutput = 1
% 46.20/46.66 nrgoals = 5000000
% 46.20/46.66 totalproof = 1
% 46.20/46.66
% 46.20/46.66 Symbols occurring in the translation:
% 46.20/46.66
% 46.20/46.66 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 46.20/46.66 . [1, 2] (w:1, o:56, a:1, s:1, b:0),
% 46.20/46.66 ! [4, 1] (w:0, o:41, a:1, s:1, b:0),
% 46.20/46.66 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 46.20/46.66 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 46.20/46.66 btrue [41, 0] (w:1, o:18, a:1, s:1, b:0),
% 46.20/46.66 aux [42, 3] (w:1, o:98, a:1, s:1, b:0),
% 46.20/46.66 nil3 [43, 0] (w:1, o:19, a:1, s:1, b:0),
% 46.20/46.66 bfalse [44, 0] (w:1, o:20, a:1, s:1, b:0),
% 46.20/46.66 suc [45, 1] (w:1, o:46, a:1, s:1, b:0),
% 46.20/46.66 enumFromToNat [46, 2] (w:1, o:81, a:1, s:1, b:0),
% 46.20/46.66 cons3 [47, 2] (w:1, o:83, a:1, s:1, b:0),
% 46.20/46.66 nothing [52, 0] (w:1, o:27, a:1, s:1, b:0),
% 46.20/46.66 aux2 [53, 5] (w:1, o:99, a:1, s:1, b:0),
% 46.20/46.66 colouring [54, 2] (w:1, o:84, a:1, s:1, b:0),
% 46.20/46.66 cons4 [55, 2] (w:1, o:85, a:1, s:1, b:0),
% 46.20/46.66 just [57, 1] (w:1, o:47, a:1, s:1, b:0),
% 46.20/46.66 eq [58, 2] (w:1, o:86, a:1, s:1, b:0),
% 46.20/46.66 notb [59, 1] (w:1, o:48, a:1, s:1, b:0),
% 46.20/46.66 aux3 [61, 5] (w:1, o:100, a:1, s:1, b:0),
% 46.20/46.66 index [62, 2] (w:1, o:87, a:1, s:1, b:0),
% 46.20/46.66 ten [63, 0] (w:1, o:29, a:1, s:1, b:0),
% 46.20/46.66 zero [64, 0] (w:1, o:30, a:1, s:1, b:0),
% 46.20/46.66 predNat [65, 1] (w:1, o:49, a:1, s:1, b:0),
% 46.20/46.66 petersen2 [66, 1] (w:1, o:50, a:1, s:1, b:0),
% 46.20/46.66 nil [67, 0] (w:1, o:31, a:1, s:1, b:0),
% 46.20/46.66 pair2 [68, 2] (w:1, o:88, a:1, s:1, b:0),
% 46.20/46.66 cons [69, 2] (w:1, o:89, a:1, s:1, b:0),
% 46.20/46.66 one [70, 0] (w:1, o:11, a:1, s:1, b:0),
% 46.20/46.66 two [71, 0] (w:1, o:32, a:1, s:1, b:0),
% 46.20/46.66 three [72, 0] (w:1, o:33, a:1, s:1, b:0),
% 46.20/46.66 lt [73, 2] (w:1, o:90, a:1, s:1, b:0),
% 46.20/46.66 'prop_p31' [76, 1] (w:1, o:51, a:1, s:1, b:0),
% 46.20/46.66 nil4 [77, 0] (w:1, o:8, a:1, s:1, b:0),
% 46.20/46.66 four [79, 0] (w:1, o:36, a:1, s:1, b:0),
% 46.20/46.66 five [80, 0] (w:1, o:37, a:1, s:1, b:0),
% 46.20/46.66 seven [81, 0] (w:1, o:5, a:1, s:1, b:0),
% 46.20/46.66 nine [82, 0] (w:1, o:9, a:1, s:1, b:0),
% 46.20/46.66 eleven [83, 0] (w:1, o:35, a:1, s:1, b:0),
% 46.20/46.66 append [84, 2] (w:1, o:91, a:1, s:1, b:0),
% 46.20/46.66 nil2 [86, 0] (w:1, o:10, a:1, s:1, b:0),
% 46.20/46.66 concat [87, 1] (w:1, o:52, a:1, s:1, b:0),
% 46.20/46.66 cons2 [88, 2] (w:1, o:82, a:1, s:1, b:0),
% 46.20/46.66 andb [90, 2] (w:1, o:92, a:1, s:1, b:0),
% 46.20/46.66 and2 [91, 1] (w:1, o:53, a:1, s:1, b:0),
% 46.20/46.66 colouring2 [92, 2] (w:1, o:93, a:1, s:1, b:0),
% 46.20/46.66 add [93, 2] (w:1, o:94, a:1, s:1, b:0),
% 46.20/46.66 petersen [94, 2] (w:1, o:95, a:1, s:1, b:0),
% 46.20/46.66 petersen3 [95, 2] (w:1, o:96, a:1, s:1, b:0),
% 46.20/46.66 petersen4 [96, 1] (w:1, o:54, a:1, s:1, b:0),
% 46.20/46.66 twentyOne [97, 0] (w:1, o:39, a:1, s:1, b:0),
% 46.20/46.66 thirtyOne [98, 0] (w:1, o:40, a:1, s:1, b:0),
% 46.20/46.66 'prop_p312' [99, 1] (w:1, o:55, a:1, s:1, b:0),
% 46.20/46.66 eq2 [100, 2] (w:1, o:97, a:1, s:1, b:0).
% 46.20/46.66
% 46.20/46.66
% 46.20/46.66 Starting Search:
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66
% 46.20/46.66 Intermediate Status:
% 46.20/46.66 Generated: 7577
% 46.20/46.66 Kept: 2007
% 46.20/46.66 Inuse: 999
% 46.20/46.66 Deleted: 85
% 46.20/46.66 Deletedinuse: 27
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66
% 46.20/46.66 Intermediate Status:
% 46.20/46.66 Generated: 20420
% 46.20/46.66 Kept: 4060
% 46.20/46.66 Inuse: 1975
% 46.20/46.66 Deleted: 259
% 46.20/46.66 Deletedinuse: 86
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66
% 46.20/46.66 Intermediate Status:
% 46.20/46.66 Generated: 32170
% 46.20/46.66 Kept: 6062
% 46.20/46.66 Inuse: 2858
% 46.20/46.66 Deleted: 439
% 46.20/46.66 Deletedinuse: 140
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66
% 46.20/46.66 Intermediate Status:
% 46.20/46.66 Generated: 48069
% 46.20/46.66 Kept: 8097
% 46.20/46.66 Inuse: 3937
% 46.20/46.66 Deleted: 895
% 46.20/46.66 Deletedinuse: 442
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 Done
% 46.20/46.66
% 46.20/46.66
% 46.20/46.66 Intermediate Status:
% 46.20/46.66 Generated: 59321
% 46.20/46.66 Kept: 10097
% 46.20/46.66 Inuse: 4608
% 46.20/46.66 Deleted: 1153
% 46.20/46.66 Deletedinuse: 648
% 46.20/46.66
% 46.20/46.66 Resimplifying inuse:
% 46.20/46.66 DonTerminated
% 299.65/300.03 Bliksem ended
%------------------------------------------------------------------------------