%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX222+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n031.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:50 PM UTC 2026
% Result : Theorem 0.75s 1.66s
% Output : Refutation 0.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX222+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.18/0.34 % Computer : n031.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % DateTime : Tue May 5 12:35:08 EDT 2026
% 0.18/0.34 % CPUTime :
% 0.75/1.66 *** allocated 10000 integers for termspace/termends
% 0.75/1.66 *** allocated 10000 integers for clauses
% 0.75/1.66 *** allocated 10000 integers for justifications
% 0.75/1.66 Bliksem 1.12
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 Automatic Strategy Selection
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 Clauses:
% 0.75/1.66
% 0.75/1.66 { head( cons( X, Y ) ) = X }.
% 0.75/1.66 { tail( cons( X, Y ) ) = Y }.
% 0.75/1.66 { ! nil = cons( X, Y ) }.
% 0.75/1.66 { proj1Arr( arr( X, Y ) ) = X }.
% 0.75/1.66 { proj2Arr( arr( X, Y ) ) = Y }.
% 0.75/1.66 { ! arr( X, Y ) = a }.
% 0.75/1.66 { ! arr( X, Y ) = b }.
% 0.75/1.66 { ! arr( X, Y ) = c }.
% 0.75/1.66 { ! a = b }.
% 0.75/1.66 { ! a = c }.
% 0.75/1.66 { ! b = c }.
% 0.75/1.66 { proj1Suc( suc( X ) ) = X }.
% 0.75/1.66 { ! zero = suc( X ) }.
% 0.75/1.66 { proj1Just( just( X ) ) = X }.
% 0.75/1.66 { ! nothing = just( X ) }.
% 0.75/1.66 { proj1App( app( X, Y, Z ) ) = X }.
% 0.75/1.66 { proj2App( app( X, Y, Z ) ) = Y }.
% 0.75/1.66 { proj3App( app( X, Y, Z ) ) = Z }.
% 0.75/1.66 { proj1Lam( lam( X ) ) = X }.
% 0.75/1.66 { proj1Var( var( X ) ) = X }.
% 0.75/1.66 { ! app( X, Y, Z ) = lam( T ) }.
% 0.75/1.66 { ! app( X, Y, Z ) = var( T ) }.
% 0.75/1.66 { ! lam( X ) = var( Y ) }.
% 0.75/1.66 { X = lam( proj1Lam( X ) ), ! nf( app( X, Y, Z ) ), nf( X ) }.
% 0.75/1.66 { X = lam( proj1Lam( X ) ), ! nf( app( X, Y, Z ) ), nf( Y ) }.
% 0.75/1.66 { X = lam( proj1Lam( X ) ), ! nf( X ), ! nf( Y ), nf( app( X, Y, Z ) ) }.
% 0.75/1.66 { ! nf( app( lam( Z ), X, Y ) ) }.
% 0.75/1.66 { ! nf( lam( X ) ), nf( X ) }.
% 0.75/1.66 { ! nf( X ), nf( lam( X ) ) }.
% 0.75/1.66 { nf( var( X ) ) }.
% 0.75/1.66 { index( nil, X ) = nothing }.
% 0.75/1.66 { index( cons( X, Y ), zero ) = just( X ) }.
% 0.75/1.66 { index( cons( X, Y ), suc( Z ) ) = index( Y, Z ) }.
% 0.75/1.66 { ! tc( X, app( Z, T, U ), Y ), tc( X, Z, arr( U, Y ) ) }.
% 0.75/1.66 { ! tc( X, app( Z, T, U ), Y ), tc( X, T, U ) }.
% 0.75/1.66 { ! tc( X, Z, arr( U, Y ) ), ! tc( X, T, U ), tc( X, app( Z, T, U ), Y ) }
% 0.75/1.66 .
% 0.75/1.66 { X = arr( proj1Arr( X ), proj2Arr( X ) ), ! tc( Y, lam( Z ), X ) }.
% 0.75/1.66 { ! tc( X, lam( Y ), arr( Z, T ) ), tc( cons( Z, X ), Y, T ) }.
% 0.75/1.66 { ! tc( cons( Z, X ), Y, T ), tc( X, lam( Y ), arr( Z, T ) ) }.
% 0.75/1.66 { ! index( X, Y ) = nothing, ! tc( X, var( Y ), Z ) }.
% 0.75/1.66 { ! index( X, Y ) = just( Z ), ! tc( X, var( Y ), T ), Z = T }.
% 0.75/1.66 { ! index( X, Y ) = just( Z ), ! Z = T, tc( X, var( Y ), T ) }.
% 0.75/1.66 { ! nf( X ), ! tc( nil, X, arr( a, arr( b, b ) ) ) }.
% 0.75/1.66
% 0.75/1.66 percentage equality = 0.538462, percentage horn = 0.930233
% 0.75/1.66 This is a problem with some equality
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 Options Used:
% 0.75/1.66
% 0.75/1.66 useres = 1
% 0.75/1.66 useparamod = 1
% 0.75/1.66 useeqrefl = 1
% 0.75/1.66 useeqfact = 1
% 0.75/1.66 usefactor = 1
% 0.75/1.66 usesimpsplitting = 0
% 0.75/1.66 usesimpdemod = 5
% 0.75/1.66 usesimpres = 3
% 0.75/1.66
% 0.75/1.66 resimpinuse = 1000
% 0.75/1.66 resimpclauses = 20000
% 0.75/1.66 substype = eqrewr
% 0.75/1.66 backwardsubs = 1
% 0.75/1.66 selectoldest = 5
% 0.75/1.66
% 0.75/1.66 litorderings [0] = split
% 0.75/1.66 litorderings [1] = extend the termordering, first sorting on arguments
% 0.75/1.66
% 0.75/1.66 termordering = kbo
% 0.75/1.66
% 0.75/1.66 litapriori = 0
% 0.75/1.66 termapriori = 1
% 0.75/1.66 litaposteriori = 0
% 0.75/1.66 termaposteriori = 0
% 0.75/1.66 demodaposteriori = 0
% 0.75/1.66 ordereqreflfact = 0
% 0.75/1.66
% 0.75/1.66 litselect = negord
% 0.75/1.66
% 0.75/1.66 maxweight = 15
% 0.75/1.66 maxdepth = 30000
% 0.75/1.66 maxlength = 115
% 0.75/1.66 maxnrvars = 195
% 0.75/1.66 excuselevel = 1
% 0.75/1.66 increasemaxweight = 1
% 0.75/1.66
% 0.75/1.66 maxselected = 10000000
% 0.75/1.66 maxnrclauses = 10000000
% 0.75/1.66
% 0.75/1.66 showgenerated = 0
% 0.75/1.66 showkept = 0
% 0.75/1.66 showselected = 0
% 0.75/1.66 showdeleted = 0
% 0.75/1.66 showresimp = 1
% 0.75/1.66 showstatus = 2000
% 0.75/1.66
% 0.75/1.66 prologoutput = 0
% 0.75/1.66 nrgoals = 5000000
% 0.75/1.66 totalproof = 1
% 0.75/1.66
% 0.75/1.66 Symbols occurring in the translation:
% 0.75/1.66
% 0.75/1.66 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.75/1.66 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 0.75/1.66 ! [4, 1] (w:0, o:26, a:1, s:1, b:0),
% 0.75/1.66 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.75/1.66 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.75/1.66 cons [37, 2] (w:1, o:71, a:1, s:1, b:0),
% 0.75/1.66 head [38, 1] (w:1, o:31, a:1, s:1, b:0),
% 0.75/1.66 tail [39, 1] (w:1, o:33, a:1, s:1, b:0),
% 0.75/1.66 nil [40, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.75/1.66 arr [41, 2] (w:1, o:72, a:1, s:1, b:0),
% 0.75/1.66 proj1Arr [42, 1] (w:1, o:34, a:1, s:1, b:0),
% 0.75/1.66 proj2Arr [43, 1] (w:1, o:40, a:1, s:1, b:0),
% 0.75/1.66 a [44, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.75/1.66 b [45, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.75/1.66 c [46, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.75/1.66 suc [47, 1] (w:1, o:32, a:1, s:1, b:0),
% 0.75/1.66 proj1Suc [48, 1] (w:1, o:35, a:1, s:1, b:0),
% 0.75/1.66 zero [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.75/1.66 just [50, 1] (w:1, o:41, a:1, s:1, b:0),
% 0.75/1.66 proj1Just [51, 1] (w:1, o:36, a:1, s:1, b:0),
% 0.75/1.66 nothing [52, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.75/1.66 app [54, 3] (w:1, o:74, a:1, s:1, b:0),
% 0.75/1.66 proj1App [55, 1] (w:1, o:37, a:1, s:1, b:0),
% 0.75/1.66 proj2App [56, 1] (w:1, o:42, a:1, s:1, b:0),
% 0.75/1.66 proj3App [57, 1] (w:1, o:43, a:1, s:1, b:0),
% 0.75/1.66 lam [58, 1] (w:1, o:44, a:1, s:1, b:0),
% 0.75/1.66 proj1Lam [59, 1] (w:1, o:38, a:1, s:1, b:0),
% 0.75/1.66 var [60, 1] (w:1, o:45, a:1, s:1, b:0),
% 0.75/1.66 proj1Var [61, 1] (w:1, o:39, a:1, s:1, b:0),
% 0.75/1.66 nf [65, 1] (w:1, o:46, a:1, s:1, b:0),
% 0.75/1.66 index [67, 2] (w:1, o:73, a:1, s:1, b:0),
% 0.75/1.66 tc [72, 3] (w:1, o:75, a:1, s:1, b:0).
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 Starting Search:
% 0.75/1.66
% 0.75/1.66 *** allocated 15000 integers for clauses
% 0.75/1.66 *** allocated 22500 integers for clauses
% 0.75/1.66 *** allocated 33750 integers for clauses
% 0.75/1.66 *** allocated 15000 integers for termspace/termends
% 0.75/1.66 *** allocated 50625 integers for clauses
% 0.75/1.66 *** allocated 22500 integers for termspace/termends
% 0.75/1.66 *** allocated 75937 integers for clauses
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66 *** allocated 33750 integers for termspace/termends
% 0.75/1.66 *** allocated 113905 integers for clauses
% 0.75/1.66
% 0.75/1.66 Intermediate Status:
% 0.75/1.66 Generated: 6318
% 0.75/1.66 Kept: 2005
% 0.75/1.66 Inuse: 163
% 0.75/1.66 Deleted: 13
% 0.75/1.66 Deletedinuse: 3
% 0.75/1.66
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66 *** allocated 50625 integers for termspace/termends
% 0.75/1.66 *** allocated 170857 integers for clauses
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66 *** allocated 75937 integers for termspace/termends
% 0.75/1.66 *** allocated 256285 integers for clauses
% 0.75/1.66
% 0.75/1.66 Intermediate Status:
% 0.75/1.66 Generated: 20704
% 0.75/1.66 Kept: 4303
% 0.75/1.66 Inuse: 291
% 0.75/1.66 Deleted: 32
% 0.75/1.66 Deletedinuse: 3
% 0.75/1.66
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66 *** allocated 113905 integers for termspace/termends
% 0.75/1.66 *** allocated 384427 integers for clauses
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 Intermediate Status:
% 0.75/1.66 Generated: 34371
% 0.75/1.66 Kept: 6303
% 0.75/1.66 Inuse: 370
% 0.75/1.66 Deleted: 39
% 0.75/1.66 Deletedinuse: 3
% 0.75/1.66
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66 *** allocated 170857 integers for termspace/termends
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66 *** allocated 576640 integers for clauses
% 0.75/1.66
% 0.75/1.66 Intermediate Status:
% 0.75/1.66 Generated: 58957
% 0.75/1.66 Kept: 8307
% 0.75/1.66 Inuse: 489
% 0.75/1.66 Deleted: 39
% 0.75/1.66 Deletedinuse: 3
% 0.75/1.66
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66 Resimplifying inuse:
% 0.75/1.66 Done
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 Bliksems!, er is een bewijs:
% 0.75/1.66 % SZS status Theorem
% 0.75/1.66 % SZS output start Refutation
% 0.75/1.66
% 0.75/1.66 (28) {G0,W5,D3,L2,V1,M2} I { ! nf( X ), nf( lam( X ) ) }.
% 0.75/1.66 (29) {G0,W3,D3,L1,V1,M1} I { nf( var( X ) ) }.
% 0.75/1.66 (31) {G0,W8,D4,L1,V2,M1} I { index( cons( X, Y ), zero ) ==> just( X ) }.
% 0.75/1.66 (38) {G0,W13,D3,L2,V4,M2} I { ! tc( cons( Z, X ), Y, T ), tc( X, lam( Y ),
% 0.75/1.66 arr( Z, T ) ) }.
% 0.75/1.66 (41) {G0,W14,D3,L3,V4,M3} I { ! index( X, Y ) = just( Z ), ! Z = T, tc( X,
% 0.75/1.66 var( Y ), T ) }.
% 0.75/1.66 (42) {G0,W10,D4,L2,V1,M2} I { ! nf( X ), ! tc( nil, X, arr( a, arr( b, b )
% 0.75/1.66 ) ) }.
% 0.75/1.66 (47) {G1,W4,D4,L1,V1,M1} R(28,29) { nf( lam( var( X ) ) ) }.
% 0.75/1.66 (48) {G2,W5,D5,L1,V1,M1} R(47,28) { nf( lam( lam( var( X ) ) ) ) }.
% 0.75/1.66 (631) {G1,W15,D3,L3,V4,M3} P(31,41) { ! just( X ) = just( Z ), ! Z = T, tc
% 0.75/1.66 ( cons( X, Y ), var( zero ), T ) }.
% 0.75/1.66 (634) {G2,W12,D3,L2,V3,M2} Q(631) { ! just( X ) = just( Y ), tc( cons( X, Z
% 0.75/1.66 ), var( zero ), Y ) }.
% 0.75/1.66 (635) {G3,W7,D3,L1,V2,M1} Q(634) { tc( cons( X, Y ), var( zero ), X ) }.
% 0.75/1.66 (641) {G4,W8,D4,L1,V2,M1} R(635,38) { tc( X, lam( var( zero ) ), arr( Y, Y
% 0.75/1.66 ) ) }.
% 0.75/1.66 (859) {G1,W11,D3,L2,V1,M2} R(42,38) { ! nf( lam( X ) ), ! tc( cons( a, nil
% 0.75/1.66 ), X, arr( b, b ) ) }.
% 0.75/1.66 (9873) {G5,W0,D0,L0,V0,M0} R(859,641);r(48) { }.
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 % SZS output end Refutation
% 0.75/1.66 found a proof!
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 Unprocessed initial clauses:
% 0.75/1.66
% 0.75/1.66 (9875) {G0,W6,D4,L1,V2,M1} { head( cons( X, Y ) ) = X }.
% 0.75/1.66 (9876) {G0,W6,D4,L1,V2,M1} { tail( cons( X, Y ) ) = Y }.
% 0.75/1.66 (9877) {G0,W5,D3,L1,V2,M1} { ! nil = cons( X, Y ) }.
% 0.75/1.66 (9878) {G0,W6,D4,L1,V2,M1} { proj1Arr( arr( X, Y ) ) = X }.
% 0.75/1.66 (9879) {G0,W6,D4,L1,V2,M1} { proj2Arr( arr( X, Y ) ) = Y }.
% 0.75/1.66 (9880) {G0,W5,D3,L1,V2,M1} { ! arr( X, Y ) = a }.
% 0.75/1.66 (9881) {G0,W5,D3,L1,V2,M1} { ! arr( X, Y ) = b }.
% 0.75/1.66 (9882) {G0,W5,D3,L1,V2,M1} { ! arr( X, Y ) = c }.
% 0.75/1.66 (9883) {G0,W3,D2,L1,V0,M1} { ! a = b }.
% 0.75/1.66 (9884) {G0,W3,D2,L1,V0,M1} { ! a = c }.
% 0.75/1.66 (9885) {G0,W3,D2,L1,V0,M1} { ! b = c }.
% 0.75/1.66 (9886) {G0,W5,D4,L1,V1,M1} { proj1Suc( suc( X ) ) = X }.
% 0.75/1.66 (9887) {G0,W4,D3,L1,V1,M1} { ! zero = suc( X ) }.
% 0.75/1.66 (9888) {G0,W5,D4,L1,V1,M1} { proj1Just( just( X ) ) = X }.
% 0.75/1.66 (9889) {G0,W4,D3,L1,V1,M1} { ! nothing = just( X ) }.
% 0.75/1.66 (9890) {G0,W7,D4,L1,V3,M1} { proj1App( app( X, Y, Z ) ) = X }.
% 0.75/1.66 (9891) {G0,W7,D4,L1,V3,M1} { proj2App( app( X, Y, Z ) ) = Y }.
% 0.75/1.66 (9892) {G0,W7,D4,L1,V3,M1} { proj3App( app( X, Y, Z ) ) = Z }.
% 0.75/1.66 (9893) {G0,W5,D4,L1,V1,M1} { proj1Lam( lam( X ) ) = X }.
% 0.75/1.66 (9894) {G0,W5,D4,L1,V1,M1} { proj1Var( var( X ) ) = X }.
% 0.75/1.66 (9895) {G0,W7,D3,L1,V4,M1} { ! app( X, Y, Z ) = lam( T ) }.
% 0.75/1.66 (9896) {G0,W7,D3,L1,V4,M1} { ! app( X, Y, Z ) = var( T ) }.
% 0.75/1.66 (9897) {G0,W5,D3,L1,V2,M1} { ! lam( X ) = var( Y ) }.
% 0.75/1.66 (9898) {G0,W12,D4,L3,V3,M3} { X = lam( proj1Lam( X ) ), ! nf( app( X, Y, Z
% 0.75/1.66 ) ), nf( X ) }.
% 0.75/1.66 (9899) {G0,W12,D4,L3,V3,M3} { X = lam( proj1Lam( X ) ), ! nf( app( X, Y, Z
% 0.75/1.66 ) ), nf( Y ) }.
% 0.75/1.66 (9900) {G0,W14,D4,L4,V3,M4} { X = lam( proj1Lam( X ) ), ! nf( X ), ! nf( Y
% 0.75/1.66 ), nf( app( X, Y, Z ) ) }.
% 0.75/1.66 (9901) {G0,W6,D4,L1,V3,M1} { ! nf( app( lam( Z ), X, Y ) ) }.
% 0.75/1.66 (9902) {G0,W5,D3,L2,V1,M2} { ! nf( lam( X ) ), nf( X ) }.
% 0.75/1.66 (9903) {G0,W5,D3,L2,V1,M2} { ! nf( X ), nf( lam( X ) ) }.
% 0.75/1.66 (9904) {G0,W3,D3,L1,V1,M1} { nf( var( X ) ) }.
% 0.75/1.66 (9905) {G0,W5,D3,L1,V1,M1} { index( nil, X ) = nothing }.
% 0.75/1.66 (9906) {G0,W8,D4,L1,V2,M1} { index( cons( X, Y ), zero ) = just( X ) }.
% 0.75/1.66 (9907) {G0,W10,D4,L1,V3,M1} { index( cons( X, Y ), suc( Z ) ) = index( Y,
% 0.75/1.66 Z ) }.
% 0.75/1.66 (9908) {G0,W13,D3,L2,V5,M2} { ! tc( X, app( Z, T, U ), Y ), tc( X, Z, arr
% 0.75/1.66 ( U, Y ) ) }.
% 0.75/1.66 (9909) {G0,W11,D3,L2,V5,M2} { ! tc( X, app( Z, T, U ), Y ), tc( X, T, U )
% 0.75/1.66 }.
% 0.75/1.66 (9910) {G0,W17,D3,L3,V5,M3} { ! tc( X, Z, arr( U, Y ) ), ! tc( X, T, U ),
% 0.75/1.66 tc( X, app( Z, T, U ), Y ) }.
% 0.75/1.66 (9911) {G0,W12,D4,L2,V3,M2} { X = arr( proj1Arr( X ), proj2Arr( X ) ), !
% 0.75/1.66 tc( Y, lam( Z ), X ) }.
% 0.75/1.66 (9912) {G0,W13,D3,L2,V4,M2} { ! tc( X, lam( Y ), arr( Z, T ) ), tc( cons(
% 0.75/1.66 Z, X ), Y, T ) }.
% 0.75/1.66 (9913) {G0,W13,D3,L2,V4,M2} { ! tc( cons( Z, X ), Y, T ), tc( X, lam( Y )
% 0.75/1.66 , arr( Z, T ) ) }.
% 0.75/1.66 (9914) {G0,W10,D3,L2,V3,M2} { ! index( X, Y ) = nothing, ! tc( X, var( Y )
% 0.75/1.66 , Z ) }.
% 0.75/1.66 (9915) {G0,W14,D3,L3,V4,M3} { ! index( X, Y ) = just( Z ), ! tc( X, var( Y
% 0.75/1.66 ), T ), Z = T }.
% 0.75/1.66 (9916) {G0,W14,D3,L3,V4,M3} { ! index( X, Y ) = just( Z ), ! Z = T, tc( X
% 0.75/1.66 , var( Y ), T ) }.
% 0.75/1.66 (9917) {G0,W10,D4,L2,V1,M2} { ! nf( X ), ! tc( nil, X, arr( a, arr( b, b )
% 0.75/1.66 ) ) }.
% 0.75/1.66
% 0.75/1.66
% 0.75/1.66 Total Proof:
% 0.75/1.66
% 0.75/1.66 subsumption: (28) {G0,W5,D3,L2,V1,M2} I { ! nf( X ), nf( lam( X ) ) }.
% 0.75/1.66 parent0: (9903) {G0,W5,D3,L2,V1,M2} { ! nf( X ), nf( lam( X ) ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 1 ==> 1
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (29) {G0,W3,D3,L1,V1,M1} I { nf( var( X ) ) }.
% 0.75/1.66 parent0: (9904) {G0,W3,D3,L1,V1,M1} { nf( var( X ) ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (31) {G0,W8,D4,L1,V2,M1} I { index( cons( X, Y ), zero ) ==>
% 0.75/1.66 just( X ) }.
% 0.75/1.66 parent0: (9906) {G0,W8,D4,L1,V2,M1} { index( cons( X, Y ), zero ) = just(
% 0.75/1.66 X ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := Y
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (38) {G0,W13,D3,L2,V4,M2} I { ! tc( cons( Z, X ), Y, T ), tc(
% 0.75/1.66 X, lam( Y ), arr( Z, T ) ) }.
% 0.75/1.66 parent0: (9913) {G0,W13,D3,L2,V4,M2} { ! tc( cons( Z, X ), Y, T ), tc( X,
% 0.75/1.66 lam( Y ), arr( Z, T ) ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := Y
% 0.75/1.66 Z := Z
% 0.75/1.66 T := T
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 1 ==> 1
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (41) {G0,W14,D3,L3,V4,M3} I { ! index( X, Y ) = just( Z ), ! Z
% 0.75/1.66 = T, tc( X, var( Y ), T ) }.
% 0.75/1.66 parent0: (9916) {G0,W14,D3,L3,V4,M3} { ! index( X, Y ) = just( Z ), ! Z =
% 0.75/1.66 T, tc( X, var( Y ), T ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := Y
% 0.75/1.66 Z := Z
% 0.75/1.66 T := T
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 1 ==> 1
% 0.75/1.66 2 ==> 2
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (42) {G0,W10,D4,L2,V1,M2} I { ! nf( X ), ! tc( nil, X, arr( a
% 0.75/1.66 , arr( b, b ) ) ) }.
% 0.75/1.66 parent0: (9917) {G0,W10,D4,L2,V1,M2} { ! nf( X ), ! tc( nil, X, arr( a,
% 0.75/1.66 arr( b, b ) ) ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 1 ==> 1
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 resolution: (10118) {G1,W4,D4,L1,V1,M1} { nf( lam( var( X ) ) ) }.
% 0.75/1.66 parent0[0]: (28) {G0,W5,D3,L2,V1,M2} I { ! nf( X ), nf( lam( X ) ) }.
% 0.75/1.66 parent1[0]: (29) {G0,W3,D3,L1,V1,M1} I { nf( var( X ) ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := var( X )
% 0.75/1.66 end
% 0.75/1.66 substitution1:
% 0.75/1.66 X := X
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (47) {G1,W4,D4,L1,V1,M1} R(28,29) { nf( lam( var( X ) ) ) }.
% 0.75/1.66 parent0: (10118) {G1,W4,D4,L1,V1,M1} { nf( lam( var( X ) ) ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 resolution: (10119) {G1,W5,D5,L1,V1,M1} { nf( lam( lam( var( X ) ) ) ) }.
% 0.75/1.66 parent0[0]: (28) {G0,W5,D3,L2,V1,M2} I { ! nf( X ), nf( lam( X ) ) }.
% 0.75/1.66 parent1[0]: (47) {G1,W4,D4,L1,V1,M1} R(28,29) { nf( lam( var( X ) ) ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := lam( var( X ) )
% 0.75/1.66 end
% 0.75/1.66 substitution1:
% 0.75/1.66 X := X
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (48) {G2,W5,D5,L1,V1,M1} R(47,28) { nf( lam( lam( var( X ) ) )
% 0.75/1.66 ) }.
% 0.75/1.66 parent0: (10119) {G1,W5,D5,L1,V1,M1} { nf( lam( lam( var( X ) ) ) ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 eqswap: (10121) {G0,W14,D3,L3,V4,M3} { ! just( Z ) = index( X, Y ), ! Z =
% 0.75/1.66 T, tc( X, var( Y ), T ) }.
% 0.75/1.66 parent0[0]: (41) {G0,W14,D3,L3,V4,M3} I { ! index( X, Y ) = just( Z ), ! Z
% 0.75/1.66 = T, tc( X, var( Y ), T ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := Y
% 0.75/1.66 Z := Z
% 0.75/1.66 T := T
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 paramod: (10124) {G1,W15,D3,L3,V4,M3} { ! just( X ) = just( Y ), ! X = T,
% 0.75/1.66 tc( cons( Y, Z ), var( zero ), T ) }.
% 0.75/1.66 parent0[0]: (31) {G0,W8,D4,L1,V2,M1} I { index( cons( X, Y ), zero ) ==>
% 0.75/1.66 just( X ) }.
% 0.75/1.66 parent1[0; 4]: (10121) {G0,W14,D3,L3,V4,M3} { ! just( Z ) = index( X, Y )
% 0.75/1.66 , ! Z = T, tc( X, var( Y ), T ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := Y
% 0.75/1.66 Y := Z
% 0.75/1.66 end
% 0.75/1.66 substitution1:
% 0.75/1.66 X := cons( Y, Z )
% 0.75/1.66 Y := zero
% 0.75/1.66 Z := X
% 0.75/1.66 T := T
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 eqswap: (10125) {G1,W15,D3,L3,V4,M3} { ! just( Y ) = just( X ), ! X = Z,
% 0.75/1.66 tc( cons( Y, T ), var( zero ), Z ) }.
% 0.75/1.66 parent0[0]: (10124) {G1,W15,D3,L3,V4,M3} { ! just( X ) = just( Y ), ! X =
% 0.75/1.66 T, tc( cons( Y, Z ), var( zero ), T ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := Y
% 0.75/1.66 Z := T
% 0.75/1.66 T := Z
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (631) {G1,W15,D3,L3,V4,M3} P(31,41) { ! just( X ) = just( Z )
% 0.75/1.66 , ! Z = T, tc( cons( X, Y ), var( zero ), T ) }.
% 0.75/1.66 parent0: (10125) {G1,W15,D3,L3,V4,M3} { ! just( Y ) = just( X ), ! X = Z,
% 0.75/1.66 tc( cons( Y, T ), var( zero ), Z ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := Z
% 0.75/1.66 Y := X
% 0.75/1.66 Z := T
% 0.75/1.66 T := Y
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 1 ==> 1
% 0.75/1.66 2 ==> 2
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 eqswap: (10130) {G1,W15,D3,L3,V4,M3} { ! just( Y ) = just( X ), ! Y = Z,
% 0.75/1.66 tc( cons( X, T ), var( zero ), Z ) }.
% 0.75/1.66 parent0[0]: (631) {G1,W15,D3,L3,V4,M3} P(31,41) { ! just( X ) = just( Z ),
% 0.75/1.66 ! Z = T, tc( cons( X, Y ), var( zero ), T ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := T
% 0.75/1.66 Z := Y
% 0.75/1.66 T := Z
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 eqrefl: (10134) {G0,W12,D3,L2,V3,M2} { ! just( X ) = just( Y ), tc( cons(
% 0.75/1.66 Y, Z ), var( zero ), X ) }.
% 0.75/1.66 parent0[1]: (10130) {G1,W15,D3,L3,V4,M3} { ! just( Y ) = just( X ), ! Y =
% 0.75/1.66 Z, tc( cons( X, T ), var( zero ), Z ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := Y
% 0.75/1.66 Y := X
% 0.75/1.66 Z := X
% 0.75/1.66 T := Z
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 eqswap: (10135) {G0,W12,D3,L2,V3,M2} { ! just( Y ) = just( X ), tc( cons(
% 0.75/1.66 Y, Z ), var( zero ), X ) }.
% 0.75/1.66 parent0[0]: (10134) {G0,W12,D3,L2,V3,M2} { ! just( X ) = just( Y ), tc(
% 0.75/1.66 cons( Y, Z ), var( zero ), X ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := Y
% 0.75/1.66 Z := Z
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (634) {G2,W12,D3,L2,V3,M2} Q(631) { ! just( X ) = just( Y ),
% 0.75/1.66 tc( cons( X, Z ), var( zero ), Y ) }.
% 0.75/1.66 parent0: (10135) {G0,W12,D3,L2,V3,M2} { ! just( Y ) = just( X ), tc( cons
% 0.75/1.66 ( Y, Z ), var( zero ), X ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := Y
% 0.75/1.66 Y := X
% 0.75/1.66 Z := Z
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 1 ==> 1
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 eqswap: (10137) {G2,W12,D3,L2,V3,M2} { ! just( Y ) = just( X ), tc( cons(
% 0.75/1.66 X, Z ), var( zero ), Y ) }.
% 0.75/1.66 parent0[0]: (634) {G2,W12,D3,L2,V3,M2} Q(631) { ! just( X ) = just( Y ), tc
% 0.75/1.66 ( cons( X, Z ), var( zero ), Y ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := Y
% 0.75/1.66 Z := Z
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 eqrefl: (10138) {G0,W7,D3,L1,V2,M1} { tc( cons( X, Y ), var( zero ), X )
% 0.75/1.66 }.
% 0.75/1.66 parent0[0]: (10137) {G2,W12,D3,L2,V3,M2} { ! just( Y ) = just( X ), tc(
% 0.75/1.66 cons( X, Z ), var( zero ), Y ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := X
% 0.75/1.66 Z := Y
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 subsumption: (635) {G3,W7,D3,L1,V2,M1} Q(634) { tc( cons( X, Y ), var( zero
% 0.75/1.66 ), X ) }.
% 0.75/1.66 parent0: (10138) {G0,W7,D3,L1,V2,M1} { tc( cons( X, Y ), var( zero ), X )
% 0.75/1.66 }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := X
% 0.75/1.66 Y := Y
% 0.75/1.66 end
% 0.75/1.66 permutation0:
% 0.75/1.66 0 ==> 0
% 0.75/1.66 end
% 0.75/1.66
% 0.75/1.66 resolution: (10139) {G1,W8,D4,L1,V2,M1} { tc( Y, lam( var( zero ) ), arr(
% 0.75/1.66 X, X ) ) }.
% 0.75/1.66 parent0[0]: (38) {G0,W13,D3,L2,V4,M2} I { ! tc( cons( Z, X ), Y, T ), tc( X
% 0.75/1.66 , lam( Y ), arr( Z, T ) ) }.
% 0.75/1.66 parent1[0]: (635) {G3,W7,D3,L1,V2,M1} Q(634) { tc( cons( X, Y ), var( zero
% 0.75/1.66 ), X ) }.
% 0.75/1.66 substitution0:
% 0.75/1.66 X := Y
% 0.75/1.66 Y := var( zero )
% 0.75/1.67 Z := X
% 0.75/1.67 T := X
% 0.75/1.67 end
% 0.75/1.67 substitution1:
% 0.75/1.67 X := X
% 0.75/1.67 Y := Y
% 0.75/1.67 end
% 0.75/1.67
% 0.75/1.67 subsumption: (641) {G4,W8,D4,L1,V2,M1} R(635,38) { tc( X, lam( var( zero )
% 0.75/1.67 ), arr( Y, Y ) ) }.
% 0.75/1.67 parent0: (10139) {G1,W8,D4,L1,V2,M1} { tc( Y, lam( var( zero ) ), arr( X,
% 0.75/1.67 X ) ) }.
% 0.75/1.67 substitution0:
% 0.75/1.67 X := Y
% 0.75/1.67 Y := X
% 0.75/1.67 end
% 0.75/1.67 permutation0:
% 0.75/1.67 0 ==> 0
% 0.75/1.67 end
% 0.75/1.67
% 0.75/1.67 resolution: (10140) {G1,W11,D3,L2,V1,M2} { ! nf( lam( X ) ), ! tc( cons( a
% 0.75/1.67 , nil ), X, arr( b, b ) ) }.
% 0.75/1.67 parent0[1]: (42) {G0,W10,D4,L2,V1,M2} I { ! nf( X ), ! tc( nil, X, arr( a,
% 0.75/1.67 arr( b, b ) ) ) }.
% 0.75/1.67 parent1[1]: (38) {G0,W13,D3,L2,V4,M2} I { ! tc( cons( Z, X ), Y, T ), tc( X
% 0.75/1.67 , lam( Y ), arr( Z, T ) ) }.
% 0.75/1.67 substitution0:
% 0.75/1.67 X := lam( X )
% 0.75/1.67 end
% 0.75/1.67 substitution1:
% 0.75/1.67 X := nil
% 0.75/1.67 Y := X
% 0.75/1.67 Z := a
% 0.75/1.67 T := arr( b, b )
% 0.75/1.67 end
% 0.75/1.67
% 0.75/1.67 subsumption: (859) {G1,W11,D3,L2,V1,M2} R(42,38) { ! nf( lam( X ) ), ! tc(
% 0.75/1.67 cons( a, nil ), X, arr( b, b ) ) }.
% 0.75/1.67 parent0: (10140) {G1,W11,D3,L2,V1,M2} { ! nf( lam( X ) ), ! tc( cons( a,
% 0.75/1.67 nil ), X, arr( b, b ) ) }.
% 0.75/1.67 substitution0:
% 0.75/1.67 X := X
% 0.75/1.67 end
% 0.75/1.67 permutation0:
% 0.75/1.67 0 ==> 0
% 0.75/1.67 1 ==> 1
% 0.75/1.67 end
% 0.75/1.67
% 0.75/1.67 resolution: (10141) {G2,W5,D5,L1,V0,M1} { ! nf( lam( lam( var( zero ) ) )
% 0.75/1.67 ) }.
% 0.75/1.67 parent0[1]: (859) {G1,W11,D3,L2,V1,M2} R(42,38) { ! nf( lam( X ) ), ! tc(
% 0.75/1.67 cons( a, nil ), X, arr( b, b ) ) }.
% 0.75/1.67 parent1[0]: (641) {G4,W8,D4,L1,V2,M1} R(635,38) { tc( X, lam( var( zero ) )
% 0.75/1.67 , arr( Y, Y ) ) }.
% 0.75/1.67 substitution0:
% 0.75/1.67 X := lam( var( zero ) )
% 0.75/1.67 end
% 0.75/1.67 substitution1:
% 0.75/1.67 X := cons( a, nil )
% 0.75/1.67 Y := b
% 0.75/1.67 end
% 0.75/1.67
% 0.75/1.67 resolution: (10142) {G3,W0,D0,L0,V0,M0} { }.
% 0.75/1.67 parent0[0]: (10141) {G2,W5,D5,L1,V0,M1} { ! nf( lam( lam( var( zero ) ) )
% 0.75/1.67 ) }.
% 0.75/1.67 parent1[0]: (48) {G2,W5,D5,L1,V1,M1} R(47,28) { nf( lam( lam( var( X ) ) )
% 0.75/1.67 ) }.
% 0.75/1.67 substitution0:
% 0.75/1.67 end
% 0.75/1.67 substitution1:
% 0.75/1.67 X := zero
% 0.75/1.67 end
% 0.75/1.67
% 0.75/1.67 subsumption: (9873) {G5,W0,D0,L0,V0,M0} R(859,641);r(48) { }.
% 0.75/1.67 parent0: (10142) {G3,W0,D0,L0,V0,M0} { }.
% 0.75/1.67 substitution0:
% 0.75/1.67 end
% 0.75/1.67 permutation0:
% 0.75/1.67 end
% 0.75/1.67
% 0.75/1.67 Proof check complete!
% 0.75/1.67
% 0.75/1.67 Memory use:
% 0.75/1.67
% 0.75/1.67 space for terms: 154472
% 0.75/1.67 space for clauses: 477989
% 0.75/1.67
% 0.75/1.67
% 0.75/1.67 clauses generated: 88955
% 0.75/1.67 clauses kept: 9874
% 0.75/1.67 clauses selected: 670
% 0.75/1.67 clauses deleted: 47
% 0.75/1.67 clauses inuse deleted: 5
% 0.75/1.67
% 0.75/1.67 subsentry: 94484
% 0.75/1.67 literals s-matched: 61183
% 0.75/1.67 literals matched: 60610
% 0.75/1.67 full subsumption: 7915
% 0.75/1.67
% 0.75/1.67 checksum: -468958738
% 0.75/1.67
% 0.75/1.67
% 0.75/1.67 Bliksem ended
%------------------------------------------------------------------------------