%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX185+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n011.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:45 PM UTC 2026
% Result : Theorem 36.77s 37.15s
% Output : Refutation 36.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX185+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.17/0.33 % Computer : n011.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % DateTime : Tue May 5 09:33:02 EDT 2026
% 0.17/0.33 % CPUTime :
% 36.77/37.15 *** allocated 10000 integers for termspace/termends
% 36.77/37.15 *** allocated 10000 integers for clauses
% 36.77/37.15 *** allocated 10000 integers for justifications
% 36.77/37.15 Bliksem 1.12
% 36.77/37.15
% 36.77/37.15
% 36.77/37.15 Automatic Strategy Selection
% 36.77/37.15
% 36.77/37.15
% 36.77/37.15 Clauses:
% 36.77/37.15
% 36.77/37.15 { head( cons( X, Y ) ) = X }.
% 36.77/37.15 { tail( cons( X, Y ) ) = Y }.
% 36.77/37.15 { ! nil = cons( X, Y ) }.
% 36.77/37.15 { ! c = d }.
% 36.77/37.15 { ! c = x }.
% 36.77/37.15 { ! c = y }.
% 36.77/37.15 { ! c = plus }.
% 36.77/37.15 { ! c = mul }.
% 36.77/37.15 { ! d = x }.
% 36.77/37.15 { ! d = y }.
% 36.77/37.15 { ! d = plus }.
% 36.77/37.15 { ! d = mul }.
% 36.77/37.15 { ! x = y }.
% 36.77/37.15 { ! x = plus }.
% 36.77/37.15 { ! x = mul }.
% 36.77/37.15 { ! y = plus }.
% 36.77/37.15 { ! y = mul }.
% 36.77/37.15 { ! plus = mul }.
% 36.77/37.15 { proj1( z( X, Y ) ) = X }.
% 36.77/37.15 { proj2( z( X, Y ) ) = Y }.
% 36.77/37.15 { proj12( x2( X, Y ) ) = X }.
% 36.77/37.15 { proj22( x2( X, Y ) ) = Y }.
% 36.77/37.15 { ! z( X, Y ) = x2( Z, T ) }.
% 36.77/37.15 { ! z( X, Y ) = eX }.
% 36.77/37.15 { ! z( X, Y ) = eY }.
% 36.77/37.15 { ! x2( X, Y ) = eX }.
% 36.77/37.15 { ! x2( X, Y ) = eY }.
% 36.77/37.15 { ! eX = eY }.
% 36.77/37.15 { X = z( proj1( X ), proj2( X ) ), X = x2( proj12( X ), proj22( X ) ),
% 36.77/37.15 assoc( X ) = X }.
% 36.77/37.15 { X = z( proj1( X ), proj2( X ) ), assoc( z( X, Y ) ) = z( assoc( X ),
% 36.77/37.15 assoc( Y ) ) }.
% 36.77/37.15 { assoc( z( z( Y, Z ), X ) ) = assoc( z( Y, z( Z, X ) ) ) }.
% 36.77/37.15 { assoc( x2( X, Y ) ) = x2( assoc( X ), assoc( Y ) ) }.
% 36.77/37.15 { append( nil, X ) = X }.
% 36.77/37.15 { append( cons( Y, Z ), X ) = cons( Y, append( Z, X ) ) }.
% 36.77/37.15 { X = x2( proj12( X ), proj22( X ) ), linTerm( X ) = lin( X ) }.
% 36.77/37.15 { linTerm( x2( X, Y ) ) = append( cons( c, nil ), append( lin( z( X, Y ) )
% 36.77/37.15 , cons( d, nil ) ) ) }.
% 36.77/37.15 { lin( z( X, Y ) ) = append( linTerm( X ), append( cons( plus, nil ),
% 36.77/37.15 linTerm( Y ) ) ) }.
% 36.77/37.15 { lin( x2( X, Y ) ) = append( lin( X ), append( cons( mul, nil ), lin( Y )
% 36.77/37.15 ) ) }.
% 36.77/37.15 { lin( eX ) = cons( x, nil ) }.
% 36.77/37.15 { lin( eY ) = cons( y, nil ) }.
% 36.77/37.15 { ! lin( X ) = lin( Y ), assoc( X ) = assoc( Y ) }.
% 36.77/37.15
% 36.77/37.15 percentage equality = 1.000000, percentage horn = 0.926829
% 36.77/37.15 This is a pure equality problem
% 36.77/37.15
% 36.77/37.15
% 36.77/37.15
% 36.77/37.15 Options Used:
% 36.77/37.15
% 36.77/37.15 useres = 1
% 36.77/37.15 useparamod = 1
% 36.77/37.15 useeqrefl = 1
% 36.77/37.15 useeqfact = 1
% 36.77/37.15 usefactor = 1
% 36.77/37.15 usesimpsplitting = 0
% 36.77/37.15 usesimpdemod = 5
% 36.77/37.15 usesimpres = 3
% 36.77/37.15
% 36.77/37.15 resimpinuse = 1000
% 36.77/37.15 resimpclauses = 20000
% 36.77/37.15 substype = eqrewr
% 36.77/37.15 backwardsubs = 1
% 36.77/37.15 selectoldest = 5
% 36.77/37.15
% 36.77/37.15 litorderings [0] = split
% 36.77/37.15 litorderings [1] = extend the termordering, first sorting on arguments
% 36.77/37.15
% 36.77/37.15 termordering = kbo
% 36.77/37.15
% 36.77/37.15 litapriori = 0
% 36.77/37.15 termapriori = 1
% 36.77/37.15 litaposteriori = 0
% 36.77/37.15 termaposteriori = 0
% 36.77/37.15 demodaposteriori = 0
% 36.77/37.15 ordereqreflfact = 0
% 36.77/37.15
% 36.77/37.15 litselect = negord
% 36.77/37.15
% 36.77/37.15 maxweight = 15
% 36.77/37.15 maxdepth = 30000
% 36.77/37.15 maxlength = 115
% 36.77/37.15 maxnrvars = 195
% 36.77/37.15 excuselevel = 1
% 36.77/37.15 increasemaxweight = 1
% 36.77/37.15
% 36.77/37.15 maxselected = 10000000
% 36.77/37.15 maxnrclauses = 10000000
% 36.77/37.15
% 36.77/37.15 showgenerated = 0
% 36.77/37.15 showkept = 0
% 36.77/37.15 showselected = 0
% 36.77/37.15 showdeleted = 0
% 36.77/37.15 showresimp = 1
% 36.77/37.15 showstatus = 2000
% 36.77/37.15
% 36.77/37.15 prologoutput = 0
% 36.77/37.15 nrgoals = 5000000
% 36.77/37.15 totalproof = 1
% 36.77/37.15
% 36.77/37.15 Symbols occurring in the translation:
% 36.77/37.15
% 36.77/37.15 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 36.77/37.15 . [1, 2] (w:1, o:44, a:1, s:1, b:0),
% 36.77/37.15 ! [4, 1] (w:0, o:30, a:1, s:1, b:0),
% 36.77/37.15 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 36.77/37.15 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 36.77/37.15 cons [37, 2] (w:1, o:68, a:1, s:1, b:0),
% 36.77/37.15 head [38, 1] (w:1, o:35, a:1, s:1, b:0),
% 36.77/37.15 tail [39, 1] (w:1, o:36, a:1, s:1, b:0),
% 36.77/37.15 nil [40, 0] (w:1, o:9, a:1, s:1, b:0),
% 36.77/37.15 c [41, 0] (w:1, o:10, a:1, s:1, b:0),
% 36.77/37.15 d [42, 0] (w:1, o:11, a:1, s:1, b:0),
% 36.77/37.15 x [43, 0] (w:1, o:12, a:1, s:1, b:0),
% 36.77/37.15 y [44, 0] (w:1, o:13, a:1, s:1, b:0),
% 36.77/37.15 plus [45, 0] (w:1, o:14, a:1, s:1, b:0),
% 36.77/37.15 mul [46, 0] (w:1, o:8, a:1, s:1, b:0),
% 36.77/37.15 z [47, 2] (w:1, o:69, a:1, s:1, b:0),
% 36.77/37.15 proj1 [48, 1] (w:1, o:37, a:1, s:1, b:0),
% 36.77/37.15 proj2 [49, 1] (w:1, o:39, a:1, s:1, b:0),
% 36.77/37.15 x2 [50, 2] (w:1, o:70, a:1, s:1, b:0),
% 36.77/37.15 proj12 [51, 1] (w:1, o:38, a:1, s:1, b:0),
% 36.77/37.15 proj22 [52, 1] (w:1, o:40, a:1, s:1, b:0),
% 36.77/37.15 eX [55, 0] (w:1, o:17, a:1, s:1, b:0),
% 36.77/37.15 eY [56, 0] (w:1, o:18, a:1, s:1, b:0),
% 36.77/37.15 assoc [57, 1] (w:1, o:41, a:1, s:1, b:0),
% 36.77/37.15 append [64, 2] (w:1, o:71, a:1, s:1, b:0),
% 36.77/37.15 linTerm [67, 1] (w:1, o:42, a:1, s:1, b:0),
% 36.77/37.15 lin [68, 1] (w:1, o:43, a:1, s:1, b:0).
% 36.77/37.15
% 36.77/37.15
% 36.77/37.15 Starting Search:
% 36.77/37.15
% 36.77/37.15 *** allocated 15000 integers for clauses
% 36.77/37.15 *** allocated 22500 integers for clauses
% 36.77/37.15 *** allocated 33750 integers for clauses
% 36.77/37.15 *** allocated 50625 integers for clauses
% 36.77/37.15 *** allocated 15000 integers for termspace/termends
% 36.77/37.15 *** allocated 75937 integers for clauses
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 22500 integers for termspace/termends
% 36.77/37.15 *** allocated 113905 integers for clauses
% 36.77/37.15 *** allocated 33750 integers for termspace/termends
% 36.77/37.15 *** allocated 170857 integers for clauses
% 36.77/37.15
% 36.77/37.15 Intermediate Status:
% 36.77/37.15 Generated: 47169
% 36.77/37.15 Kept: 2007
% 36.77/37.15 Inuse: 442
% 36.77/37.15 Deleted: 167
% 36.77/37.15 Deletedinuse: 16
% 36.77/37.15
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 50625 integers for termspace/termends
% 36.77/37.15 *** allocated 256285 integers for clauses
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 75937 integers for termspace/termends
% 36.77/37.15
% 36.77/37.15 Intermediate Status:
% 36.77/37.15 Generated: 191979
% 36.77/37.15 Kept: 4022
% 36.77/37.15 Inuse: 928
% 36.77/37.15 Deleted: 313
% 36.77/37.15 Deletedinuse: 19
% 36.77/37.15
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 384427 integers for clauses
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 113905 integers for termspace/termends
% 36.77/37.15
% 36.77/37.15 Intermediate Status:
% 36.77/37.15 Generated: 376386
% 36.77/37.15 Kept: 6025
% 36.77/37.15 Inuse: 1413
% 36.77/37.15 Deleted: 418
% 36.77/37.15 Deletedinuse: 31
% 36.77/37.15
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 576640 integers for clauses
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 170857 integers for termspace/termends
% 36.77/37.15
% 36.77/37.15 Intermediate Status:
% 36.77/37.15 Generated: 519191
% 36.77/37.15 Kept: 8026
% 36.77/37.15 Inuse: 1709
% 36.77/37.15 Deleted: 559
% 36.77/37.15 Deletedinuse: 31
% 36.77/37.15
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 864960 integers for clauses
% 36.77/37.15
% 36.77/37.15 Intermediate Status:
% 36.77/37.15 Generated: 951973
% 36.77/37.15 Kept: 10027
% 36.77/37.15 Inuse: 2201
% 36.77/37.15 Deleted: 857
% 36.77/37.15 Deletedinuse: 165
% 36.77/37.15
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15 *** allocated 256285 integers for termspace/termends
% 36.77/37.15
% 36.77/37.15 Intermediate Status:
% 36.77/37.15 Generated: 1581924
% 36.77/37.15 Kept: 12035
% 36.77/37.15 Inuse: 2934
% 36.77/37.15 Deleted: 1462
% 36.77/37.15 Deletedinuse: 198
% 36.77/37.15
% 36.77/37.15 Resimplifying inuse:
% 36.77/37.15 Done
% 36.77/37.15
% 36.77/37.15
% 36.77/37.15 Bliksems!, er is een bewijs:
% 36.77/37.15 % SZS status Theorem
% 36.77/37.15 % SZS output start Refutation
% 36.77/37.15
% 36.77/37.15 (21) {G0,W6,D4,L1,V2,M1} I { proj22( x2( X, Y ) ) ==> Y }.
% 36.77/37.15 (22) {G0,W7,D3,L1,V4,M1} I { ! z( X, Y ) = x2( Z, T ) }.
% 36.77/37.15 (24) {G0,W5,D3,L1,V2,M1} I { ! z( X, Y ) ==> eY }.
% 36.77/37.15 (25) {G0,W5,D3,L1,V2,M1} I { ! x2( X, Y ) ==> eX }.
% 36.77/37.15 (26) {G0,W5,D3,L1,V2,M1} I { ! x2( X, Y ) ==> eY }.
% 36.77/37.15 (28) {G0,W18,D4,L3,V1,M3} I { z( proj1( X ), proj2( X ) ) ==> X, x2( proj12
% 36.77/37.15 ( X ), proj22( X ) ) ==> X, assoc( X ) ==> X }.
% 36.77/37.15 (29) {G0,W17,D4,L2,V2,M2} I { z( proj1( X ), proj2( X ) ) ==> X, z( assoc(
% 36.77/37.15 X ), assoc( Y ) ) ==> assoc( z( X, Y ) ) }.
% 36.77/37.15 (31) {G0,W10,D4,L1,V2,M1} I { x2( assoc( X ), assoc( Y ) ) ==> assoc( x2( X
% 36.77/37.15 , Y ) ) }.
% 36.77/37.15 (32) {G0,W5,D3,L1,V1,M1} I { append( nil, X ) ==> X }.
% 36.77/37.15 (33) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==> cons( Y, append
% 36.77/37.15 ( Z, X ) ) }.
% 36.77/37.15 (34) {G0,W12,D4,L2,V1,M2} I { x2( proj12( X ), proj22( X ) ) ==> X, lin( X
% 36.77/37.15 ) ==> linTerm( X ) }.
% 36.77/37.15 (37) {G1,W12,D5,L1,V2,M1} I;d(33);d(32) { append( lin( X ), cons( mul, lin
% 36.77/37.15 ( Y ) ) ) ==> lin( x2( X, Y ) ) }.
% 36.77/37.15 (38) {G0,W6,D3,L1,V0,M1} I { cons( x, nil ) ==> lin( eX ) }.
% 36.77/37.15 (40) {G0,W10,D3,L2,V2,M2} I { ! lin( X ) = lin( Y ), assoc( X ) = assoc( Y
% 36.77/37.15 ) }.
% 36.77/37.15 (50) {G1,W8,D4,L1,V4,M1} P(31,22) { ! z( Z, T ) = assoc( x2( X, Y ) ) }.
% 36.77/37.16 (51) {G1,W8,D5,L1,V2,M1} P(31,21) { proj22( assoc( x2( X, Y ) ) ) ==> assoc
% 36.77/37.16 ( Y ) }.
% 36.77/37.16 (58) {G1,W4,D3,L1,V0,M1} R(28,24);r(26) { assoc( eY ) ==> eY }.
% 36.77/37.16 (82) {G2,W9,D4,L1,V1,M1} R(29,24);d(58) { z( eY, assoc( X ) ) ==> assoc( z
% 36.77/37.16 ( eY, X ) ) }.
% 36.77/37.16 (102) {G2,W13,D4,L2,V3,M2} P(40,51) { proj22( assoc( Z ) ) = assoc( Y ), !
% 36.77/37.16 lin( x2( X, Y ) ) = lin( Z ) }.
% 36.77/37.16 (125) {G1,W8,D4,L1,V1,M1} P(38,33);d(32) { append( lin( eX ), X ) ==> cons
% 36.77/37.16 ( x, X ) }.
% 36.77/37.16 (129) {G1,W5,D3,L1,V0,M1} R(34,25) { lin( eX ) ==> linTerm( eX ) }.
% 36.77/37.16 (133) {G2,W8,D4,L1,V1,M1} P(34,125);r(25) { append( linTerm( eX ), X ) ==>
% 36.77/37.16 cons( x, X ) }.
% 36.77/37.16 (170) {G3,W11,D5,L1,V1,M1} P(129,37);d(133) { cons( x, cons( mul, lin( X )
% 36.77/37.16 ) ) ==> lin( x2( eX, X ) ) }.
% 36.77/37.16 (307) {G3,W9,D4,L1,V3,M1} P(82,50) { ! assoc( z( eY, X ) ) = assoc( x2( Y,
% 36.77/37.16 Z ) ) }.
% 36.77/37.16 (1026) {G3,W14,D4,L2,V4,M2} P(102,51) { assoc( Z ) = assoc( Y ), ! lin( x2
% 36.77/37.16 ( T, Z ) ) = lin( x2( X, Y ) ) }.
% 36.77/37.16 (1591) {G4,W15,D6,L1,V2,M1} P(170,33);d(33) { cons( x, cons( mul, append(
% 36.77/37.16 lin( X ), Y ) ) ) ==> append( lin( x2( eX, X ) ), Y ) }.
% 36.77/37.16 (9502) {G4,W13,D5,L1,V5,M1} R(1026,307) { ! lin( x2( X, z( eY, Y ) ) ) =
% 36.77/37.16 lin( x2( Z, x2( T, U ) ) ) }.
% 36.77/37.16 (11773) {G5,W13,D5,L1,V2,M1} P(37,1591);d(170);d(37) { lin( x2( eX, x2( X,
% 36.77/37.16 Y ) ) ) ==> lin( x2( x2( eX, X ), Y ) ) }.
% 36.77/37.16 (12117) {G6,W13,D5,L1,V4,M1} P(11773,9502) { ! lin( x2( Z, z( eY, T ) ) ) =
% 36.77/37.16 lin( x2( x2( eX, X ), Y ) ) }.
% 36.77/37.16 (12129) {G7,W0,D0,L0,V0,M0} Q(12117) { }.
% 36.77/37.16
% 36.77/37.16
% 36.77/37.16 % SZS output end Refutation
% 36.77/37.16 found a proof!
% 36.77/37.16
% 36.77/37.16
% 36.77/37.16 Unprocessed initial clauses:
% 36.77/37.16
% 36.77/37.16 (12131) {G0,W6,D4,L1,V2,M1} { head( cons( X, Y ) ) = X }.
% 36.77/37.16 (12132) {G0,W6,D4,L1,V2,M1} { tail( cons( X, Y ) ) = Y }.
% 36.77/37.16 (12133) {G0,W5,D3,L1,V2,M1} { ! nil = cons( X, Y ) }.
% 36.77/37.16 (12134) {G0,W3,D2,L1,V0,M1} { ! c = d }.
% 36.77/37.16 (12135) {G0,W3,D2,L1,V0,M1} { ! c = x }.
% 36.77/37.16 (12136) {G0,W3,D2,L1,V0,M1} { ! c = y }.
% 36.77/37.16 (12137) {G0,W3,D2,L1,V0,M1} { ! c = plus }.
% 36.77/37.16 (12138) {G0,W3,D2,L1,V0,M1} { ! c = mul }.
% 36.77/37.16 (12139) {G0,W3,D2,L1,V0,M1} { ! d = x }.
% 36.77/37.16 (12140) {G0,W3,D2,L1,V0,M1} { ! d = y }.
% 36.77/37.16 (12141) {G0,W3,D2,L1,V0,M1} { ! d = plus }.
% 36.77/37.16 (12142) {G0,W3,D2,L1,V0,M1} { ! d = mul }.
% 36.77/37.16 (12143) {G0,W3,D2,L1,V0,M1} { ! x = y }.
% 36.77/37.16 (12144) {G0,W3,D2,L1,V0,M1} { ! x = plus }.
% 36.77/37.16 (12145) {G0,W3,D2,L1,V0,M1} { ! x = mul }.
% 36.77/37.16 (12146) {G0,W3,D2,L1,V0,M1} { ! y = plus }.
% 36.77/37.16 (12147) {G0,W3,D2,L1,V0,M1} { ! y = mul }.
% 36.77/37.16 (12148) {G0,W3,D2,L1,V0,M1} { ! plus = mul }.
% 36.77/37.16 (12149) {G0,W6,D4,L1,V2,M1} { proj1( z( X, Y ) ) = X }.
% 36.77/37.16 (12150) {G0,W6,D4,L1,V2,M1} { proj2( z( X, Y ) ) = Y }.
% 36.77/37.16 (12151) {G0,W6,D4,L1,V2,M1} { proj12( x2( X, Y ) ) = X }.
% 36.77/37.16 (12152) {G0,W6,D4,L1,V2,M1} { proj22( x2( X, Y ) ) = Y }.
% 36.77/37.16 (12153) {G0,W7,D3,L1,V4,M1} { ! z( X, Y ) = x2( Z, T ) }.
% 36.77/37.16 (12154) {G0,W5,D3,L1,V2,M1} { ! z( X, Y ) = eX }.
% 36.77/37.16 (12155) {G0,W5,D3,L1,V2,M1} { ! z( X, Y ) = eY }.
% 36.77/37.16 (12156) {G0,W5,D3,L1,V2,M1} { ! x2( X, Y ) = eX }.
% 36.77/37.16 (12157) {G0,W5,D3,L1,V2,M1} { ! x2( X, Y ) = eY }.
% 36.77/37.16 (12158) {G0,W3,D2,L1,V0,M1} { ! eX = eY }.
% 36.77/37.16 (12159) {G0,W18,D4,L3,V1,M3} { X = z( proj1( X ), proj2( X ) ), X = x2(
% 36.77/37.16 proj12( X ), proj22( X ) ), assoc( X ) = X }.
% 36.77/37.16 (12160) {G0,W17,D4,L2,V2,M2} { X = z( proj1( X ), proj2( X ) ), assoc( z(
% 36.77/37.16 X, Y ) ) = z( assoc( X ), assoc( Y ) ) }.
% 36.77/37.16 (12161) {G0,W13,D5,L1,V3,M1} { assoc( z( z( Y, Z ), X ) ) = assoc( z( Y, z
% 36.77/37.16 ( Z, X ) ) ) }.
% 36.77/37.16 (12162) {G0,W10,D4,L1,V2,M1} { assoc( x2( X, Y ) ) = x2( assoc( X ), assoc
% 36.77/37.16 ( Y ) ) }.
% 36.77/37.16 (12163) {G0,W5,D3,L1,V1,M1} { append( nil, X ) = X }.
% 36.77/37.16 (12164) {G0,W11,D4,L1,V3,M1} { append( cons( Y, Z ), X ) = cons( Y, append
% 36.77/37.16 ( Z, X ) ) }.
% 36.77/37.16 (12165) {G0,W12,D4,L2,V1,M2} { X = x2( proj12( X ), proj22( X ) ), linTerm
% 36.77/37.16 ( X ) = lin( X ) }.
% 36.77/37.16 (12166) {G0,W17,D6,L1,V2,M1} { linTerm( x2( X, Y ) ) = append( cons( c,
% 36.77/37.16 nil ), append( lin( z( X, Y ) ), cons( d, nil ) ) ) }.
% 36.77/37.16 (12167) {G0,W14,D5,L1,V2,M1} { lin( z( X, Y ) ) = append( linTerm( X ),
% 36.77/37.16 append( cons( plus, nil ), linTerm( Y ) ) ) }.
% 36.77/37.16 (12168) {G0,W14,D5,L1,V2,M1} { lin( x2( X, Y ) ) = append( lin( X ),
% 36.77/37.16 append( cons( mul, nil ), lin( Y ) ) ) }.
% 36.77/37.16 (12169) {G0,W6,D3,L1,V0,M1} { lin( eX ) = cons( x, nil ) }.
% 36.77/37.16 (12170) {G0,W6,D3,L1,V0,M1} { lin( eY ) = cons( y, nil ) }.
% 36.77/37.16 (12171) {G0,W10,D3,L2,V2,M2} { ! lin( X ) = lin( Y ), assoc( X ) = assoc(
% 36.77/37.16 Y ) }.
% 36.77/37.16
% 36.77/37.16
% 36.77/37.16 Total Proof:
% 36.77/37.16
% 36.77/37.16 subsumption: (21) {G0,W6,D4,L1,V2,M1} I { proj22( x2( X, Y ) ) ==> Y }.
% 36.77/37.16 parent0: (12152) {G0,W6,D4,L1,V2,M1} { proj22( x2( X, Y ) ) = Y }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (22) {G0,W7,D3,L1,V4,M1} I { ! z( X, Y ) = x2( Z, T ) }.
% 36.77/37.16 parent0: (12153) {G0,W7,D3,L1,V4,M1} { ! z( X, Y ) = x2( Z, T ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 Z := Z
% 36.77/37.16 T := T
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (24) {G0,W5,D3,L1,V2,M1} I { ! z( X, Y ) ==> eY }.
% 36.77/37.16 parent0: (12155) {G0,W5,D3,L1,V2,M1} { ! z( X, Y ) = eY }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (25) {G0,W5,D3,L1,V2,M1} I { ! x2( X, Y ) ==> eX }.
% 36.77/37.16 parent0: (12156) {G0,W5,D3,L1,V2,M1} { ! x2( X, Y ) = eX }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (26) {G0,W5,D3,L1,V2,M1} I { ! x2( X, Y ) ==> eY }.
% 36.77/37.16 parent0: (12157) {G0,W5,D3,L1,V2,M1} { ! x2( X, Y ) = eY }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12325) {G0,W18,D4,L3,V1,M3} { X = assoc( X ), X = z( proj1( X ),
% 36.77/37.16 proj2( X ) ), X = x2( proj12( X ), proj22( X ) ) }.
% 36.77/37.16 parent0[2]: (12159) {G0,W18,D4,L3,V1,M3} { X = z( proj1( X ), proj2( X ) )
% 36.77/37.16 , X = x2( proj12( X ), proj22( X ) ), assoc( X ) = X }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12327) {G0,W18,D4,L3,V1,M3} { x2( proj12( X ), proj22( X ) ) = X
% 36.77/37.16 , X = assoc( X ), X = z( proj1( X ), proj2( X ) ) }.
% 36.77/37.16 parent0[2]: (12325) {G0,W18,D4,L3,V1,M3} { X = assoc( X ), X = z( proj1( X
% 36.77/37.16 ), proj2( X ) ), X = x2( proj12( X ), proj22( X ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12328) {G0,W18,D4,L3,V1,M3} { z( proj1( X ), proj2( X ) ) = X, x2
% 36.77/37.16 ( proj12( X ), proj22( X ) ) = X, X = assoc( X ) }.
% 36.77/37.16 parent0[2]: (12327) {G0,W18,D4,L3,V1,M3} { x2( proj12( X ), proj22( X ) )
% 36.77/37.16 = X, X = assoc( X ), X = z( proj1( X ), proj2( X ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12329) {G0,W18,D4,L3,V1,M3} { assoc( X ) = X, z( proj1( X ),
% 36.77/37.16 proj2( X ) ) = X, x2( proj12( X ), proj22( X ) ) = X }.
% 36.77/37.16 parent0[2]: (12328) {G0,W18,D4,L3,V1,M3} { z( proj1( X ), proj2( X ) ) = X
% 36.77/37.16 , x2( proj12( X ), proj22( X ) ) = X, X = assoc( X ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (28) {G0,W18,D4,L3,V1,M3} I { z( proj1( X ), proj2( X ) ) ==>
% 36.77/37.16 X, x2( proj12( X ), proj22( X ) ) ==> X, assoc( X ) ==> X }.
% 36.77/37.16 parent0: (12329) {G0,W18,D4,L3,V1,M3} { assoc( X ) = X, z( proj1( X ),
% 36.77/37.16 proj2( X ) ) = X, x2( proj12( X ), proj22( X ) ) = X }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 2
% 36.77/37.16 1 ==> 0
% 36.77/37.16 2 ==> 1
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12366) {G0,W17,D4,L2,V2,M2} { z( assoc( X ), assoc( Y ) ) = assoc
% 36.77/37.16 ( z( X, Y ) ), X = z( proj1( X ), proj2( X ) ) }.
% 36.77/37.16 parent0[1]: (12160) {G0,W17,D4,L2,V2,M2} { X = z( proj1( X ), proj2( X ) )
% 36.77/37.16 , assoc( z( X, Y ) ) = z( assoc( X ), assoc( Y ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12367) {G0,W17,D4,L2,V2,M2} { z( proj1( X ), proj2( X ) ) = X, z
% 36.77/37.16 ( assoc( X ), assoc( Y ) ) = assoc( z( X, Y ) ) }.
% 36.77/37.16 parent0[1]: (12366) {G0,W17,D4,L2,V2,M2} { z( assoc( X ), assoc( Y ) ) =
% 36.77/37.16 assoc( z( X, Y ) ), X = z( proj1( X ), proj2( X ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (29) {G0,W17,D4,L2,V2,M2} I { z( proj1( X ), proj2( X ) ) ==>
% 36.77/37.16 X, z( assoc( X ), assoc( Y ) ) ==> assoc( z( X, Y ) ) }.
% 36.77/37.16 parent0: (12367) {G0,W17,D4,L2,V2,M2} { z( proj1( X ), proj2( X ) ) = X, z
% 36.77/37.16 ( assoc( X ), assoc( Y ) ) = assoc( z( X, Y ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 1 ==> 1
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12407) {G0,W10,D4,L1,V2,M1} { x2( assoc( X ), assoc( Y ) ) =
% 36.77/37.16 assoc( x2( X, Y ) ) }.
% 36.77/37.16 parent0[0]: (12162) {G0,W10,D4,L1,V2,M1} { assoc( x2( X, Y ) ) = x2( assoc
% 36.77/37.16 ( X ), assoc( Y ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (31) {G0,W10,D4,L1,V2,M1} I { x2( assoc( X ), assoc( Y ) ) ==>
% 36.77/37.16 assoc( x2( X, Y ) ) }.
% 36.77/37.16 parent0: (12407) {G0,W10,D4,L1,V2,M1} { x2( assoc( X ), assoc( Y ) ) =
% 36.77/37.16 assoc( x2( X, Y ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (32) {G0,W5,D3,L1,V1,M1} I { append( nil, X ) ==> X }.
% 36.77/37.16 parent0: (12163) {G0,W5,D3,L1,V1,M1} { append( nil, X ) = X }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (33) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==>
% 36.77/37.16 cons( Y, append( Z, X ) ) }.
% 36.77/37.16 parent0: (12164) {G0,W11,D4,L1,V3,M1} { append( cons( Y, Z ), X ) = cons(
% 36.77/37.16 Y, append( Z, X ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 Z := Z
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12534) {G0,W12,D4,L2,V1,M2} { lin( X ) = linTerm( X ), X = x2(
% 36.77/37.16 proj12( X ), proj22( X ) ) }.
% 36.77/37.16 parent0[1]: (12165) {G0,W12,D4,L2,V1,M2} { X = x2( proj12( X ), proj22( X
% 36.77/37.16 ) ), linTerm( X ) = lin( X ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12535) {G0,W12,D4,L2,V1,M2} { x2( proj12( X ), proj22( X ) ) = X
% 36.77/37.16 , lin( X ) = linTerm( X ) }.
% 36.77/37.16 parent0[1]: (12534) {G0,W12,D4,L2,V1,M2} { lin( X ) = linTerm( X ), X = x2
% 36.77/37.16 ( proj12( X ), proj22( X ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (34) {G0,W12,D4,L2,V1,M2} I { x2( proj12( X ), proj22( X ) )
% 36.77/37.16 ==> X, lin( X ) ==> linTerm( X ) }.
% 36.77/37.16 parent0: (12535) {G0,W12,D4,L2,V1,M2} { x2( proj12( X ), proj22( X ) ) = X
% 36.77/37.16 , lin( X ) = linTerm( X ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 1 ==> 1
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 paramod: (12674) {G1,W14,D6,L1,V2,M1} { lin( x2( X, Y ) ) = append( lin( X
% 36.77/37.16 ), cons( mul, append( nil, lin( Y ) ) ) ) }.
% 36.77/37.16 parent0[0]: (33) {G0,W11,D4,L1,V3,M1} I { append( cons( Y, Z ), X ) ==>
% 36.77/37.16 cons( Y, append( Z, X ) ) }.
% 36.77/37.16 parent1[0; 8]: (12168) {G0,W14,D5,L1,V2,M1} { lin( x2( X, Y ) ) = append(
% 36.77/37.16 lin( X ), append( cons( mul, nil ), lin( Y ) ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := lin( Y )
% 36.77/37.16 Y := mul
% 36.77/37.16 Z := nil
% 36.77/37.16 end
% 36.77/37.16 substitution1:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 paramod: (12675) {G1,W12,D5,L1,V2,M1} { lin( x2( X, Y ) ) = append( lin( X
% 36.77/37.16 ), cons( mul, lin( Y ) ) ) }.
% 36.77/37.16 parent0[0]: (32) {G0,W5,D3,L1,V1,M1} I { append( nil, X ) ==> X }.
% 36.77/37.16 parent1[0; 10]: (12674) {G1,W14,D6,L1,V2,M1} { lin( x2( X, Y ) ) = append
% 36.77/37.16 ( lin( X ), cons( mul, append( nil, lin( Y ) ) ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := lin( Y )
% 36.77/37.16 end
% 36.77/37.16 substitution1:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12676) {G1,W12,D5,L1,V2,M1} { append( lin( X ), cons( mul, lin( Y
% 36.77/37.16 ) ) ) = lin( x2( X, Y ) ) }.
% 36.77/37.16 parent0[0]: (12675) {G1,W12,D5,L1,V2,M1} { lin( x2( X, Y ) ) = append( lin
% 36.77/37.16 ( X ), cons( mul, lin( Y ) ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (37) {G1,W12,D5,L1,V2,M1} I;d(33);d(32) { append( lin( X ),
% 36.77/37.16 cons( mul, lin( Y ) ) ) ==> lin( x2( X, Y ) ) }.
% 36.77/37.16 parent0: (12676) {G1,W12,D5,L1,V2,M1} { append( lin( X ), cons( mul, lin(
% 36.77/37.16 Y ) ) ) = lin( x2( X, Y ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12725) {G0,W6,D3,L1,V0,M1} { cons( x, nil ) = lin( eX ) }.
% 36.77/37.16 parent0[0]: (12169) {G0,W6,D3,L1,V0,M1} { lin( eX ) = cons( x, nil ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (38) {G0,W6,D3,L1,V0,M1} I { cons( x, nil ) ==> lin( eX ) }.
% 36.77/37.16 parent0: (12725) {G0,W6,D3,L1,V0,M1} { cons( x, nil ) = lin( eX ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (40) {G0,W10,D3,L2,V2,M2} I { ! lin( X ) = lin( Y ), assoc( X
% 36.77/37.16 ) = assoc( Y ) }.
% 36.77/37.16 parent0: (12171) {G0,W10,D3,L2,V2,M2} { ! lin( X ) = lin( Y ), assoc( X )
% 36.77/37.16 = assoc( Y ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 1 ==> 1
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12778) {G0,W7,D3,L1,V4,M1} { ! x2( Z, T ) = z( X, Y ) }.
% 36.77/37.16 parent0[0]: (22) {G0,W7,D3,L1,V4,M1} I { ! z( X, Y ) = x2( Z, T ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 Z := Z
% 36.77/37.16 T := T
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 paramod: (12779) {G1,W8,D4,L1,V4,M1} { ! assoc( x2( X, Y ) ) = z( Z, T )
% 36.77/37.16 }.
% 36.77/37.16 parent0[0]: (31) {G0,W10,D4,L1,V2,M1} I { x2( assoc( X ), assoc( Y ) ) ==>
% 36.77/37.16 assoc( x2( X, Y ) ) }.
% 36.77/37.16 parent1[0; 2]: (12778) {G0,W7,D3,L1,V4,M1} { ! x2( Z, T ) = z( X, Y ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16 substitution1:
% 36.77/37.16 X := Z
% 36.77/37.16 Y := T
% 36.77/37.16 Z := assoc( X )
% 36.77/37.16 T := assoc( Y )
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12780) {G1,W8,D4,L1,V4,M1} { ! z( Z, T ) = assoc( x2( X, Y ) )
% 36.77/37.16 }.
% 36.77/37.16 parent0[0]: (12779) {G1,W8,D4,L1,V4,M1} { ! assoc( x2( X, Y ) ) = z( Z, T
% 36.77/37.16 ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 Z := Z
% 36.77/37.16 T := T
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (50) {G1,W8,D4,L1,V4,M1} P(31,22) { ! z( Z, T ) = assoc( x2( X
% 36.77/37.16 , Y ) ) }.
% 36.77/37.16 parent0: (12780) {G1,W8,D4,L1,V4,M1} { ! z( Z, T ) = assoc( x2( X, Y ) )
% 36.77/37.16 }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 Z := Z
% 36.77/37.16 T := T
% 36.77/37.16 end
% 36.77/37.16 permutation0:
% 36.77/37.16 0 ==> 0
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12782) {G0,W6,D4,L1,V2,M1} { Y ==> proj22( x2( X, Y ) ) }.
% 36.77/37.16 parent0[0]: (21) {G0,W6,D4,L1,V2,M1} I { proj22( x2( X, Y ) ) ==> Y }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 paramod: (12783) {G1,W8,D5,L1,V2,M1} { assoc( X ) ==> proj22( assoc( x2( Y
% 36.77/37.16 , X ) ) ) }.
% 36.77/37.16 parent0[0]: (31) {G0,W10,D4,L1,V2,M1} I { x2( assoc( X ), assoc( Y ) ) ==>
% 36.77/37.16 assoc( x2( X, Y ) ) }.
% 36.77/37.16 parent1[0; 4]: (12782) {G0,W6,D4,L1,V2,M1} { Y ==> proj22( x2( X, Y ) )
% 36.77/37.16 }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := Y
% 36.77/37.16 Y := X
% 36.77/37.16 end
% 36.77/37.16 substitution1:
% 36.77/37.16 X := assoc( Y )
% 36.77/37.16 Y := assoc( X )
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 eqswap: (12784) {G1,W8,D5,L1,V2,M1} { proj22( assoc( x2( Y, X ) ) ) ==>
% 36.77/37.16 assoc( X ) }.
% 36.77/37.16 parent0[0]: (12783) {G1,W8,D5,L1,V2,M1} { assoc( X ) ==> proj22( assoc( x2
% 36.77/37.16 ( Y, X ) ) ) }.
% 36.77/37.16 substitution0:
% 36.77/37.16 X := X
% 36.77/37.16 Y := Y
% 36.77/37.16 end
% 36.77/37.16
% 36.77/37.16 subsumption: (51) {G1,W8,D5,L1,V2,M1} P(31,21) { proj22( Terminated
% 299.68/300.03 Bliksem ended
%------------------------------------------------------------------------------