%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX207+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:48 PM UTC 2026
% Result : Theorem 0.70s 1.14s
% Output : Refutation 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX207+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 11:34:36 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.70/1.13 *** allocated 10000 integers for termspace/termends
% 0.70/1.13 *** allocated 10000 integers for clauses
% 0.70/1.13 *** allocated 10000 integers for justifications
% 0.70/1.13 Bliksem 1.12
% 0.70/1.13
% 0.70/1.13
% 0.70/1.13 Automatic Strategy Selection
% 0.70/1.13
% 0.70/1.13
% 0.70/1.13 Clauses:
% 0.70/1.13
% 0.70/1.13 { head( cons( X, Y ) ) = X }.
% 0.70/1.13 { tail( cons( X, Y ) ) = Y }.
% 0.70/1.13 { ! nil = cons( X, Y ) }.
% 0.70/1.13 { ! a = b }.
% 0.70/1.13 { proj1AP( aP( X ) ) = X }.
% 0.70/1.13 { proj1BP( bP( X ) ) = X }.
% 0.70/1.13 { ! aP( X ) = bP( Y ) }.
% 0.70/1.13 { ! aP( X ) = pA }.
% 0.70/1.13 { ! aP( X ) = pB }.
% 0.70/1.13 { ! aP( X ) = pE }.
% 0.70/1.13 { ! bP( X ) = pA }.
% 0.70/1.13 { ! bP( X ) = pB }.
% 0.70/1.13 { ! bP( X ) = pE }.
% 0.70/1.13 { ! pA = pB }.
% 0.70/1.13 { ! pA = pE }.
% 0.70/1.13 { ! pB = pE }.
% 0.70/1.13 { proj1C( c2( X, Y ) ) = X }.
% 0.70/1.13 { proj2C( c2( X, Y ) ) = Y }.
% 0.70/1.13 { append( nil, X ) = X }.
% 0.70/1.13 { append( cons( Y, Z ), X ) = cons( Y, append( Z, X ) ) }.
% 0.70/1.13 { linP( aP( X ) ) = append( cons( a, nil ), append( linP( X ), cons( a, nil
% 0.70/1.13 ) ) ) }.
% 0.70/1.13 { linP( bP( X ) ) = append( cons( b, nil ), append( linP( X ), cons( b, nil
% 0.70/1.13 ) ) ) }.
% 0.70/1.13 { linP( pA ) = cons( a, nil ) }.
% 0.70/1.13 { linP( pB ) = cons( b, nil ) }.
% 0.70/1.13 { linP( pE ) = nil }.
% 0.70/1.13 { linC( c2( X, Y ) ) = append( linP( X ), linP( Y ) ) }.
% 0.70/1.13 { ! linC( X ) = linC( Y ), X = Y }.
% 0.70/1.13
% 0.70/1.13 percentage equality = 1.000000, percentage horn = 1.000000
% 0.70/1.13 This is a pure equality problem
% 0.70/1.13
% 0.70/1.13
% 0.70/1.13
% 0.70/1.13 Options Used:
% 0.70/1.13
% 0.70/1.13 useres = 1
% 0.70/1.13 useparamod = 1
% 0.70/1.13 useeqrefl = 1
% 0.70/1.13 useeqfact = 1
% 0.70/1.13 usefactor = 1
% 0.70/1.13 usesimpsplitting = 0
% 0.70/1.13 usesimpdemod = 5
% 0.70/1.13 usesimpres = 3
% 0.70/1.13
% 0.70/1.13 resimpinuse = 1000
% 0.70/1.13 resimpclauses = 20000
% 0.70/1.13 substype = eqrewr
% 0.70/1.13 backwardsubs = 1
% 0.70/1.13 selectoldest = 5
% 0.70/1.13
% 0.70/1.13 litorderings [0] = split
% 0.70/1.13 litorderings [1] = extend the termordering, first sorting on arguments
% 0.70/1.13
% 0.70/1.13 termordering = kbo
% 0.70/1.13
% 0.70/1.13 litapriori = 0
% 0.70/1.13 termapriori = 1
% 0.70/1.13 litaposteriori = 0
% 0.70/1.13 termaposteriori = 0
% 0.70/1.13 demodaposteriori = 0
% 0.70/1.13 ordereqreflfact = 0
% 0.70/1.13
% 0.70/1.13 litselect = negord
% 0.70/1.13
% 0.70/1.13 maxweight = 15
% 0.70/1.13 maxdepth = 30000
% 0.70/1.13 maxlength = 115
% 0.70/1.13 maxnrvars = 195
% 0.70/1.13 excuselevel = 1
% 0.70/1.13 increasemaxweight = 1
% 0.70/1.13
% 0.70/1.13 maxselected = 10000000
% 0.70/1.13 maxnrclauses = 10000000
% 0.70/1.13
% 0.70/1.13 showgenerated = 0
% 0.70/1.13 showkept = 0
% 0.70/1.13 showselected = 0
% 0.70/1.13 showdeleted = 0
% 0.70/1.13 showresimp = 1
% 0.70/1.13 showstatus = 2000
% 0.70/1.13
% 0.70/1.13 prologoutput = 0
% 0.70/1.13 nrgoals = 5000000
% 0.70/1.13 totalproof = 1
% 0.70/1.13
% 0.70/1.13 Symbols occurring in the translation:
% 0.70/1.13
% 0.70/1.13 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.70/1.13 . [1, 2] (w:1, o:36, a:1, s:1, b:0),
% 0.70/1.13 ! [4, 1] (w:0, o:21, a:1, s:1, b:0),
% 0.70/1.13 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.13 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.13 cons [37, 2] (w:1, o:60, a:1, s:1, b:0),
% 0.70/1.13 head [38, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.70/1.13 tail [39, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.70/1.13 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.70/1.13 a [41, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.70/1.13 b [42, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.70/1.13 aP [43, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.70/1.13 proj1AP [44, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.70/1.13 bP [45, 1] (w:1, o:30, a:1, s:1, b:0),
% 0.70/1.13 proj1BP [46, 1] (w:1, o:31, a:1, s:1, b:0),
% 0.70/1.13 pA [47, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.70/1.13 pB [48, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.70/1.13 pE [49, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.70/1.13 c2 [50, 2] (w:1, o:61, a:1, s:1, b:0),
% 0.70/1.13 proj1C [51, 1] (w:1, o:32, a:1, s:1, b:0),
% 0.70/1.14 proj2C [52, 1] (w:1, o:33, a:1, s:1, b:0),
% 0.70/1.14 append [54, 2] (w:1, o:62, a:1, s:1, b:0),
% 0.70/1.14 linP [58, 1] (w:1, o:34, a:1, s:1, b:0),
% 0.70/1.14 linC [60, 1] (w:1, o:35, a:1, s:1, b:0).
% 0.70/1.14
% 0.70/1.14
% 0.70/1.14 Starting Search:
% 0.70/1.14
% 0.70/1.14 *** allocated 15000 integers for clauses
% 0.70/1.14 *** allocated 22500 integers for clauses
% 0.70/1.14 *** allocated 33750 integers for clauses
% 0.70/1.14 *** allocated 50625 integers for clauses
% 0.70/1.14 *** allocated 15000 integers for termspace/termends
% 0.70/1.14
% 0.70/1.14 Bliksems!, er is een bewijs:
% 0.70/1.14 % SZS status Theorem
% 0.70/1.14 % SZS output start Refutation
% 0.70/1.14
% 0.70/1.14 (15) {G0,W3,D2,L1,V0,M1} I { ! pE ==> pB }.
% 0.70/1.14 (17) {G0,W6,D4,L1,V2,M1} I { proj2C( c2( X, Y ) ) ==> Y }.
% 0.70/1.14 (18) {G0,W5,D3,L1,V1,M1} I { append( nil, X ) ==> X }.
% 0.70/1.14 (19) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==> cons( Y, append
% 0.70/1.14 ( Z, X ) ) }.
% 0.70/1.14 (23) {G0,W6,D3,L1,V0,M1} I { cons( b, nil ) ==> linP( pB ) }.
% 0.70/1.14 (24) {G0,W4,D3,L1,V0,M1} I { linP( pE ) ==> nil }.
% 0.70/1.14 (25) {G0,W10,D4,L1,V2,M1} I { append( linP( X ), linP( Y ) ) ==> linC( c2(
% 0.70/1.14 X, Y ) ) }.
% 0.70/1.14 (26) {G0,W8,D3,L2,V2,M2} I { ! linC( X ) = linC( Y ), X = Y }.
% 0.70/1.14 (40) {G1,W11,D4,L2,V3,M2} P(26,17) { proj2C( Z ) = Y, ! linC( c2( X, Y ) )
% 0.70/1.14 = linC( Z ) }.
% 0.70/1.14 (92) {G1,W8,D4,L1,V1,M1} P(23,19);d(18) { append( linP( pB ), X ) ==> cons
% 0.70/1.14 ( b, X ) }.
% 0.70/1.14 (136) {G1,W7,D4,L1,V1,M1} P(24,25);d(18) { linC( c2( pE, X ) ) ==> linP( X
% 0.70/1.14 ) }.
% 0.70/1.14 (470) {G2,W9,D4,L1,V1,M1} P(92,25) { cons( b, linP( X ) ) ==> linC( c2( pB
% 0.70/1.14 , X ) ) }.
% 0.70/1.14 (554) {G3,W7,D4,L1,V0,M1} P(24,470);d(23) { linC( c2( pB, pE ) ) ==> linP(
% 0.70/1.14 pB ) }.
% 0.70/1.14 (576) {G2,W9,D3,L2,V2,M2} P(136,40) { proj2C( Y ) = X, ! linP( X ) = linC(
% 0.70/1.14 Y ) }.
% 0.70/1.14 (743) {G4,W8,D3,L2,V1,M2} P(554,576);d(17) { ! linP( X ) = linP( pB ), pE =
% 0.70/1.14 X }.
% 0.70/1.14 (904) {G5,W3,D2,L1,V0,M1} Q(743) { pE ==> pB }.
% 0.70/1.14 (907) {G6,W0,D0,L0,V0,M0} S(904);r(15) { }.
% 0.70/1.14
% 0.70/1.14
% 0.70/1.14 % SZS output end Refutation
% 0.70/1.14 found a proof!
% 0.70/1.14
% 0.70/1.14
% 0.70/1.14 Unprocessed initial clauses:
% 0.70/1.14
% 0.70/1.14 (909) {G0,W6,D4,L1,V2,M1} { head( cons( X, Y ) ) = X }.
% 0.70/1.14 (910) {G0,W6,D4,L1,V2,M1} { tail( cons( X, Y ) ) = Y }.
% 0.70/1.14 (911) {G0,W5,D3,L1,V2,M1} { ! nil = cons( X, Y ) }.
% 0.70/1.14 (912) {G0,W3,D2,L1,V0,M1} { ! a = b }.
% 0.70/1.14 (913) {G0,W5,D4,L1,V1,M1} { proj1AP( aP( X ) ) = X }.
% 0.70/1.14 (914) {G0,W5,D4,L1,V1,M1} { proj1BP( bP( X ) ) = X }.
% 0.70/1.14 (915) {G0,W5,D3,L1,V2,M1} { ! aP( X ) = bP( Y ) }.
% 0.70/1.14 (916) {G0,W4,D3,L1,V1,M1} { ! aP( X ) = pA }.
% 0.70/1.14 (917) {G0,W4,D3,L1,V1,M1} { ! aP( X ) = pB }.
% 0.70/1.14 (918) {G0,W4,D3,L1,V1,M1} { ! aP( X ) = pE }.
% 0.70/1.14 (919) {G0,W4,D3,L1,V1,M1} { ! bP( X ) = pA }.
% 0.70/1.14 (920) {G0,W4,D3,L1,V1,M1} { ! bP( X ) = pB }.
% 0.70/1.14 (921) {G0,W4,D3,L1,V1,M1} { ! bP( X ) = pE }.
% 0.70/1.14 (922) {G0,W3,D2,L1,V0,M1} { ! pA = pB }.
% 0.70/1.14 (923) {G0,W3,D2,L1,V0,M1} { ! pA = pE }.
% 0.70/1.14 (924) {G0,W3,D2,L1,V0,M1} { ! pB = pE }.
% 0.70/1.14 (925) {G0,W6,D4,L1,V2,M1} { proj1C( c2( X, Y ) ) = X }.
% 0.70/1.14 (926) {G0,W6,D4,L1,V2,M1} { proj2C( c2( X, Y ) ) = Y }.
% 0.70/1.14 (927) {G0,W5,D3,L1,V1,M1} { append( nil, X ) = X }.
% 0.70/1.14 (928) {G0,W11,D4,L1,V3,M1} { append( cons( Y, Z ), X ) = cons( Y, append(
% 0.70/1.14 Z, X ) ) }.
% 0.70/1.14 (929) {G0,W14,D5,L1,V1,M1} { linP( aP( X ) ) = append( cons( a, nil ),
% 0.70/1.14 append( linP( X ), cons( a, nil ) ) ) }.
% 0.70/1.14 (930) {G0,W14,D5,L1,V1,M1} { linP( bP( X ) ) = append( cons( b, nil ),
% 0.70/1.14 append( linP( X ), cons( b, nil ) ) ) }.
% 0.70/1.14 (931) {G0,W6,D3,L1,V0,M1} { linP( pA ) = cons( a, nil ) }.
% 0.70/1.14 (932) {G0,W6,D3,L1,V0,M1} { linP( pB ) = cons( b, nil ) }.
% 0.70/1.14 (933) {G0,W4,D3,L1,V0,M1} { linP( pE ) = nil }.
% 0.70/1.14 (934) {G0,W10,D4,L1,V2,M1} { linC( c2( X, Y ) ) = append( linP( X ), linP
% 0.70/1.14 ( Y ) ) }.
% 0.70/1.14 (935) {G0,W8,D3,L2,V2,M2} { ! linC( X ) = linC( Y ), X = Y }.
% 0.70/1.14
% 0.70/1.14
% 0.70/1.14 Total Proof:
% 0.70/1.14
% 0.70/1.14 eqswap: (951) {G0,W3,D2,L1,V0,M1} { ! pE = pB }.
% 0.70/1.14 parent0[0]: (924) {G0,W3,D2,L1,V0,M1} { ! pB = pE }.
% 0.70/1.14 substitution0:
% 0.70/1.14 end
% 0.70/1.14
% 0.70/1.14 subsumption: (15) {G0,W3,D2,L1,V0,M1} I { ! pE ==> pB }.
% 0.70/1.14 parent0: (951) {G0,W3,D2,L1,V0,M1} { ! pE = pB }.
% 0.70/1.14 substitution0:
% 0.70/1.14 end
% 0.70/1.14 permutation0:
% 0.70/1.14 0 ==> 0
% 0.70/1.14 end
% 0.70/1.14
% 0.70/1.14 subsumption: (17) {G0,W6,D4,L1,V2,M1} I { proj2C( c2( X, Y ) ) ==> Y }.
% 0.70/1.14 parent0: (926) {G0,W6,D4,L1,V2,M1} { proj2C( c2( X, Y ) ) = Y }.
% 0.70/1.14 substitution0:
% 0.70/1.14 X := X
% 0.70/1.14 Y := Y
% 0.70/1.14 end
% 0.70/1.14 permutation0:
% 0.70/1.14 0 ==> 0
% 0.70/1.14 end
% 0.70/1.14
% 0.70/1.14 subsumption: (18) {G0,W5,D3,L1,V1,M1} I { append( nil, X ) ==> X }.
% 0.70/1.14 parent0: (927) {G0,W5,D3,L1,V1,M1} { append( nil, X ) = X }.
% 0.70/1.14 substitution0:
% 0.70/1.14 X := X
% 0.70/1.14 end
% 0.70/1.14 permutation0:
% 0.70/1.14 0 ==> 0
% 0.70/1.14 end
% 0.70/1.14
% 0.70/1.14 subsumption: (19) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==>
% 0.70/1.14 cons( Y, append( Z, X ) ) }.
% 0.70/1.14 parent0: (928) {G0,W11,D4,L1,V3,M1} { append( cons( Y, Z ), X ) = cons( Y
% 0.70/1.14 , append( Z, X ) ) }.
% 0.70/1.14 substitution0:
% 0.70/1.14 X := X
% 0.70/1.14 Y := Y
% 0.70/1.14 Z := Z
% 0.70/1.14 end
% 0.70/1.14 permutation0:
% 0.70/1.14 0 ==> 0
% 0.70/1.14 end
% 0.70/1.14
% 0.70/1.14 eqswap: (1032) {G0,W6,D3,L1,V0,M1} { cons( b, nil ) = linP( pB ) }.
% 0.70/1.14 parent0[0]: (932) {G0,W6,D3,L1,V0,M1} { linP( pB ) = cons( b, nil ) }.
% 0.70/1.14 substitution0:
% 0.70/1.14 end
% 0.70/1.14
% 0.70/1.14 subsumption: (23) {G0,W6,D3,L1,V0,M1} I { cons( b, nil ) ==> linP( pB ) }.
% 0.70/1.14 parent0: (1032) {G0,W6,D3,L1,V0,M1} { cons( b, nil ) = linP( pB ) }.
% 0.70/1.14 substitution0:
% 0.70/1.14 end
% 0.70/1.14 permutation0:
% 0.70/1.14 0 ==> 0
% 0.70/1.14 end
% 0.70/1.14
% 0.70/1.14 subsumption: (24) {G0,W4,D3,L1,V0,M1} I { linP( pE ) ==> nil }.
% 0.70/1.14 parent0: (933) {G0,W4,D3,L1,V0,M1} { linP( pE ) = nil }.
% 0.70/1.14 substitution0:
% 0.70/1.14 end
% 0.70/1.14 permutation0:
% 0.70/1.14 0 ==> 0
% 0.70/1.14 end
% 0.70/1.14
% 0.70/1.14 eqswap: (1083) {G0,W10,D4,L1,V2,M1} { append( linP( X ), linP( Y ) ) =
% 0.70/1.14 linC( c2( X, Y ) ) }.
% 0.70/1.14 parent0[0]: (934) {G0,W10,D4,L1,V2,M1} { linC( c2( X, Y ) ) = append( linP
% 0.70/1.14 ( X ), linP( YTerminated
% 299.55/300.02 Bliksem ended
%------------------------------------------------------------------------------