%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : RNG083+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n029.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 : Mon Jul 18 20:16:19 EDT 2022
% Result : Theorem 7.38s 7.78s
% Output : Refutation 7.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : RNG083+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Mon May 30 22:33:29 EDT 2022
% 0.12/0.33 % CPUTime :
% 7.38/7.78 *** allocated 10000 integers for termspace/termends
% 7.38/7.78 *** allocated 10000 integers for clauses
% 7.38/7.78 *** allocated 10000 integers for justifications
% 7.38/7.78 Bliksem 1.12
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Automatic Strategy Selection
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Clauses:
% 7.38/7.78
% 7.38/7.78 { && }.
% 7.38/7.78 { aElement0( sz00 ) }.
% 7.38/7.78 { aElement0( sz10 ) }.
% 7.38/7.78 { ! aElement0( X ), aElement0( smndt0( X ) ) }.
% 7.38/7.78 { ! aElement0( X ), ! aElement0( Y ), aElement0( sdtpldt0( X, Y ) ) }.
% 7.38/7.78 { ! aElement0( X ), ! aElement0( Y ), aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.78 { ! aElement0( X ), ! aElement0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }
% 7.38/7.78 .
% 7.38/7.78 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), sdtpldt0( sdtpldt0
% 7.38/7.78 ( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 7.38/7.78 { ! aElement0( X ), sdtpldt0( X, sz00 ) = X }.
% 7.38/7.78 { ! aElement0( X ), X = sdtpldt0( sz00, X ) }.
% 7.38/7.78 { ! aElement0( X ), sdtpldt0( X, smndt0( X ) ) = sz00 }.
% 7.38/7.78 { ! aElement0( X ), sz00 = sdtpldt0( smndt0( X ), X ) }.
% 7.38/7.78 { ! aElement0( X ), ! aElement0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }
% 7.38/7.78 .
% 7.38/7.78 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), sdtasdt0( sdtasdt0
% 7.38/7.78 ( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 7.38/7.78 { ! aElement0( X ), sdtasdt0( X, sz10 ) = X }.
% 7.38/7.78 { ! aElement0( X ), X = sdtasdt0( sz10, X ) }.
% 7.38/7.78 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), sdtasdt0( X,
% 7.38/7.78 sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 7.38/7.78 { ! aElement0( X ), ! aElement0( Y ), ! aElement0( Z ), sdtasdt0( sdtpldt0
% 7.38/7.78 ( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 7.38/7.78 { ! aElement0( X ), sdtasdt0( smndt0( sz10 ), X ) = smndt0( X ) }.
% 7.38/7.78 { ! aElement0( X ), smndt0( X ) = sdtasdt0( X, smndt0( sz10 ) ) }.
% 7.38/7.78 { aElement0( xx ) }.
% 7.38/7.78 { ! sdtasdt0( xx, sz00 ) = sz00, ! sz00 = sdtasdt0( sz00, xx ) }.
% 7.38/7.78
% 7.38/7.78 percentage equality = 0.307692, percentage horn = 1.000000
% 7.38/7.78 This is a problem with some equality
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Options Used:
% 7.38/7.78
% 7.38/7.78 useres = 1
% 7.38/7.78 useparamod = 1
% 7.38/7.78 useeqrefl = 1
% 7.38/7.78 useeqfact = 1
% 7.38/7.78 usefactor = 1
% 7.38/7.78 usesimpsplitting = 0
% 7.38/7.78 usesimpdemod = 5
% 7.38/7.78 usesimpres = 3
% 7.38/7.78
% 7.38/7.78 resimpinuse = 1000
% 7.38/7.78 resimpclauses = 20000
% 7.38/7.78 substype = eqrewr
% 7.38/7.78 backwardsubs = 1
% 7.38/7.78 selectoldest = 5
% 7.38/7.78
% 7.38/7.78 litorderings [0] = split
% 7.38/7.78 litorderings [1] = extend the termordering, first sorting on arguments
% 7.38/7.78
% 7.38/7.78 termordering = kbo
% 7.38/7.78
% 7.38/7.78 litapriori = 0
% 7.38/7.78 termapriori = 1
% 7.38/7.78 litaposteriori = 0
% 7.38/7.78 termaposteriori = 0
% 7.38/7.78 demodaposteriori = 0
% 7.38/7.78 ordereqreflfact = 0
% 7.38/7.78
% 7.38/7.78 litselect = negord
% 7.38/7.78
% 7.38/7.78 maxweight = 15
% 7.38/7.78 maxdepth = 30000
% 7.38/7.78 maxlength = 115
% 7.38/7.78 maxnrvars = 195
% 7.38/7.78 excuselevel = 1
% 7.38/7.78 increasemaxweight = 1
% 7.38/7.78
% 7.38/7.78 maxselected = 10000000
% 7.38/7.78 maxnrclauses = 10000000
% 7.38/7.78
% 7.38/7.78 showgenerated = 0
% 7.38/7.78 showkept = 0
% 7.38/7.78 showselected = 0
% 7.38/7.78 showdeleted = 0
% 7.38/7.78 showresimp = 1
% 7.38/7.78 showstatus = 2000
% 7.38/7.78
% 7.38/7.78 prologoutput = 0
% 7.38/7.78 nrgoals = 5000000
% 7.38/7.78 totalproof = 1
% 7.38/7.78
% 7.38/7.78 Symbols occurring in the translation:
% 7.38/7.78
% 7.38/7.78 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 7.38/7.78 . [1, 2] (w:1, o:19, a:1, s:1, b:0),
% 7.38/7.78 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 7.38/7.78 ! [4, 1] (w:0, o:12, a:1, s:1, b:0),
% 7.38/7.78 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.38/7.78 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.38/7.78 aElement0 [36, 1] (w:1, o:17, a:1, s:1, b:0),
% 7.38/7.78 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 7.38/7.78 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 7.38/7.78 smndt0 [39, 1] (w:1, o:18, a:1, s:1, b:0),
% 7.38/7.78 sdtpldt0 [41, 2] (w:1, o:43, a:1, s:1, b:0),
% 7.38/7.78 sdtasdt0 [42, 2] (w:1, o:44, a:1, s:1, b:0),
% 7.38/7.78 xx [44, 0] (w:1, o:11, a:1, s:1, b:0).
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Starting Search:
% 7.38/7.78
% 7.38/7.78 *** allocated 15000 integers for clauses
% 7.38/7.78 *** allocated 22500 integers for clauses
% 7.38/7.78 *** allocated 33750 integers for clauses
% 7.38/7.78 *** allocated 50625 integers for clauses
% 7.38/7.78 *** allocated 75937 integers for clauses
% 7.38/7.78 *** allocated 15000 integers for termspace/termends
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 *** allocated 113905 integers for clauses
% 7.38/7.78 *** allocated 22500 integers for termspace/termends
% 7.38/7.78 *** allocated 170857 integers for clauses
% 7.38/7.78
% 7.38/7.78 Intermediate Status:
% 7.38/7.78 Generated: 4819
% 7.38/7.78 Kept: 2019
% 7.38/7.78 Inuse: 112
% 7.38/7.78 Deleted: 12
% 7.38/7.78 Deletedinuse: 11
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 *** allocated 33750 integers for termspace/termends
% 7.38/7.78 *** allocated 256285 integers for clauses
% 7.38/7.78 *** allocated 50625 integers for termspace/termends
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 *** allocated 384427 integers for clauses
% 7.38/7.78
% 7.38/7.78 Intermediate Status:
% 7.38/7.78 Generated: 10574
% 7.38/7.78 Kept: 4248
% 7.38/7.78 Inuse: 166
% 7.38/7.78 Deleted: 37
% 7.38/7.78 Deletedinuse: 17
% 7.38/7.78
% 7.38/7.78 *** allocated 75937 integers for termspace/termends
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 *** allocated 576640 integers for clauses
% 7.38/7.78
% 7.38/7.78 Intermediate Status:
% 7.38/7.78 Generated: 15597
% 7.38/7.78 Kept: 6351
% 7.38/7.78 Inuse: 204
% 7.38/7.78 Deleted: 49
% 7.38/7.78 Deletedinuse: 17
% 7.38/7.78
% 7.38/7.78 *** allocated 113905 integers for termspace/termends
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Intermediate Status:
% 7.38/7.78 Generated: 18988
% 7.38/7.78 Kept: 8565
% 7.38/7.78 Inuse: 221
% 7.38/7.78 Deleted: 57
% 7.38/7.78 Deletedinuse: 17
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 *** allocated 864960 integers for clauses
% 7.38/7.78 *** allocated 170857 integers for termspace/termends
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Intermediate Status:
% 7.38/7.78 Generated: 22671
% 7.38/7.78 Kept: 10602
% 7.38/7.78 Inuse: 250
% 7.38/7.78 Deleted: 61
% 7.38/7.78 Deletedinuse: 18
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Intermediate Status:
% 7.38/7.78 Generated: 26372
% 7.38/7.78 Kept: 13290
% 7.38/7.78 Inuse: 258
% 7.38/7.78 Deleted: 61
% 7.38/7.78 Deletedinuse: 18
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 *** allocated 256285 integers for termspace/termends
% 7.38/7.78 *** allocated 1297440 integers for clauses
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Intermediate Status:
% 7.38/7.78 Generated: 30469
% 7.38/7.78 Kept: 16243
% 7.38/7.78 Inuse: 268
% 7.38/7.78 Deleted: 61
% 7.38/7.78 Deletedinuse: 18
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Intermediate Status:
% 7.38/7.78 Generated: 34215
% 7.38/7.78 Kept: 18519
% 7.38/7.78 Inuse: 294
% 7.38/7.78 Deleted: 67
% 7.38/7.78 Deletedinuse: 18
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 Resimplifying inuse:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78 Resimplifying clauses:
% 7.38/7.78 Done
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Bliksems!, er is een bewijs:
% 7.38/7.78 % SZS status Theorem
% 7.38/7.78 % SZS output start Refutation
% 7.38/7.78
% 7.38/7.78 (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.78 (2) {G0,W2,D2,L1,V0,M1} I { aElement0( sz10 ) }.
% 7.38/7.78 (3) {G0,W5,D3,L2,V1,M2} I { ! aElement0( X ), aElement0( smndt0( X ) ) }.
% 7.38/7.78 (4) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y ), aElement0(
% 7.38/7.78 sdtpldt0( X, Y ) ) }.
% 7.38/7.78 (5) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y ), aElement0(
% 7.38/7.78 sdtasdt0( X, Y ) ) }.
% 7.38/7.78 (6) {G0,W11,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y ), sdtpldt0(
% 7.38/7.78 X, Y ) = sdtpldt0( Y, X ) }.
% 7.38/7.78 (8) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( X, sz00 ) ==> X }.
% 7.38/7.78 (9) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( sz00, X ) ==> X }.
% 7.38/7.78 (10) {G0,W8,D4,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( X, smndt0( X ) )
% 7.38/7.78 ==> sz00 }.
% 7.38/7.78 (11) {G0,W8,D4,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( smndt0( X ), X )
% 7.38/7.78 ==> sz00 }.
% 7.38/7.78 (12) {G0,W11,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y ), sdtasdt0
% 7.38/7.78 ( X, Y ) = sdtasdt0( Y, X ) }.
% 7.38/7.78 (13) {G0,W17,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) ==> sdtasdt0( sdtasdt0( X
% 7.38/7.78 , Y ), Z ) }.
% 7.38/7.78 (14) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( X, sz10 ) ==> X
% 7.38/7.78 }.
% 7.38/7.78 (15) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( sz10, X ) ==> X
% 7.38/7.78 }.
% 7.38/7.78 (16) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ), sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) ==>
% 7.38/7.78 sdtasdt0( X, sdtpldt0( Y, Z ) ) }.
% 7.38/7.78 (17) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ), sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) ==>
% 7.38/7.78 sdtasdt0( sdtpldt0( Y, Z ), X ) }.
% 7.38/7.78 (18) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( smndt0( sz10 ), X
% 7.38/7.78 ) ==> smndt0( X ) }.
% 7.38/7.78 (19) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( X, smndt0( sz10 )
% 7.38/7.78 ) ==> smndt0( X ) }.
% 7.38/7.78 (20) {G0,W2,D2,L1,V0,M1} I { aElement0( xx ) }.
% 7.38/7.78 (21) {G0,W10,D3,L2,V0,M2} I { ! sdtasdt0( xx, sz00 ) ==> sz00, ! sdtasdt0(
% 7.38/7.78 sz00, xx ) ==> sz00 }.
% 7.38/7.78 (34) {G1,W17,D4,L3,V2,M3} F(16) { ! aElement0( X ), ! aElement0( Y ),
% 7.38/7.78 sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Y ) ) ==> sdtasdt0( X, sdtpldt0
% 7.38/7.78 ( Y, Y ) ) }.
% 7.38/7.78 (37) {G1,W17,D4,L3,V2,M3} F(17) { ! aElement0( X ), ! aElement0( Y ),
% 7.38/7.78 sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( X, X ) ) ==> sdtasdt0( sdtpldt0( Y
% 7.38/7.78 , X ), X ) }.
% 7.38/7.78 (41) {G1,W3,D3,L1,V0,M1} R(3,1) { aElement0( smndt0( sz00 ) ) }.
% 7.38/7.78 (42) {G1,W3,D3,L1,V0,M1} R(3,2) { aElement0( smndt0( sz10 ) ) }.
% 7.38/7.78 (48) {G1,W6,D3,L2,V1,M2} R(4,2) { ! aElement0( X ), aElement0( sdtpldt0(
% 7.38/7.78 sz10, X ) ) }.
% 7.38/7.78 (59) {G2,W4,D4,L1,V0,M1} R(41,3) { aElement0( smndt0( smndt0( sz00 ) ) )
% 7.38/7.78 }.
% 7.38/7.78 (83) {G1,W6,D3,L2,V1,M2} R(5,1) { ! aElement0( X ), aElement0( sdtasdt0(
% 7.38/7.78 sz00, X ) ) }.
% 7.38/7.78 (84) {G1,W6,D3,L2,V1,M2} R(5,1) { ! aElement0( X ), aElement0( sdtasdt0( X
% 7.38/7.78 , sz00 ) ) }.
% 7.38/7.78 (118) {G3,W5,D5,L1,V0,M1} R(59,3) { aElement0( smndt0( smndt0( smndt0( sz00
% 7.38/7.78 ) ) ) ) }.
% 7.38/7.78 (133) {G1,W17,D4,L4,V3,M4} R(6,5) { ! aElement0( X ), sdtpldt0( sdtasdt0( Y
% 7.38/7.78 , Z ), X ) = sdtpldt0( X, sdtasdt0( Y, Z ) ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ) }.
% 7.38/7.78 (145) {G2,W15,D4,L3,V2,M3} F(133) { ! aElement0( X ), sdtpldt0( X, sdtasdt0
% 7.38/7.78 ( X, Y ) ) ==> sdtpldt0( sdtasdt0( X, Y ), X ), ! aElement0( Y ) }.
% 7.38/7.78 (175) {G2,W4,D3,L1,V0,M1} R(83,2) { aElement0( sdtasdt0( sz00, sz10 ) ) }.
% 7.38/7.78 (197) {G3,W5,D4,L1,V0,M1} R(175,3) { aElement0( smndt0( sdtasdt0( sz00,
% 7.38/7.78 sz10 ) ) ) }.
% 7.38/7.78 (269) {G1,W13,D4,L3,V2,M3} R(8,5) { sdtpldt0( sdtasdt0( X, Y ), sz00 ) ==>
% 7.38/7.78 sdtasdt0( X, Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.78 (275) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 7.38/7.78 (304) {G2,W7,D4,L1,V0,M1} R(9,41) { sdtpldt0( sz00, smndt0( sz00 ) ) ==>
% 7.38/7.78 smndt0( sz00 ) }.
% 7.38/7.78 (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==> sz00 }.
% 7.38/7.78 (377) {G2,W5,D4,L1,V0,M1} R(84,42) { aElement0( sdtasdt0( smndt0( sz10 ),
% 7.38/7.78 sz00 ) ) }.
% 7.38/7.78 (416) {G2,W12,D5,L2,V1,M2} R(11,84) { sdtpldt0( smndt0( sdtasdt0( X, sz00 )
% 7.38/7.78 ), sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X ) }.
% 7.38/7.78 (512) {G1,W17,D4,L4,V3,M4} R(12,4) { ! aElement0( X ), sdtasdt0( sdtpldt0(
% 7.38/7.78 Y, Z ), X ) = sdtasdt0( X, sdtpldt0( Y, Z ) ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ) }.
% 7.38/7.78 (516) {G2,W15,D4,L3,V2,M3} F(512) { ! aElement0( X ), sdtasdt0( X, sdtpldt0
% 7.38/7.78 ( X, Y ) ) ==> sdtasdt0( sdtpldt0( X, Y ), X ), ! aElement0( Y ) }.
% 7.38/7.78 (620) {G2,W15,D4,L3,V2,M3} R(13,42);d(18) { ! aElement0( X ), ! aElement0(
% 7.38/7.78 Y ), sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ) ==> sdtasdt0( smndt0( X
% 7.38/7.78 ), Y ) }.
% 7.38/7.78 (621) {G2,W13,D4,L3,V2,M3} R(13,42);d(18);d(19) { ! aElement0( X ), !
% 7.38/7.78 aElement0( Y ), sdtasdt0( X, smndt0( Y ) ) ==> sdtasdt0( smndt0( X ), Y )
% 7.38/7.78 }.
% 7.38/7.78 (622) {G3,W15,D4,L3,V2,M3} R(13,42);d(19);d(621) { ! aElement0( X ), !
% 7.38/7.78 aElement0( Y ), sdtasdt0( sdtasdt0( X, Y ), smndt0( sz10 ) ) ==> sdtasdt0
% 7.38/7.78 ( smndt0( X ), Y ) }.
% 7.38/7.78 (765) {G4,W5,D3,L1,V0,M1} R(14,118);d(349);d(349);d(349) { sdtasdt0( sz00,
% 7.38/7.78 sz10 ) ==> sz00 }.
% 7.38/7.78 (811) {G5,W5,D3,L1,V0,M1} R(15,197);d(765);d(349) { sdtasdt0( sz10, sz00 )
% 7.38/7.78 ==> sz00 }.
% 7.38/7.78 (937) {G2,W4,D3,L1,V0,M1} R(48,2) { aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.78 (989) {G1,W17,D4,L3,V2,M3} R(17,1) { ! aElement0( X ), ! aElement0( Y ),
% 7.38/7.78 sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( Y, sz00 ) ) ==> sdtasdt0(
% 7.38/7.78 sdtpldt0( X, Y ), sz00 ) }.
% 7.38/7.78 (996) {G6,W13,D4,L3,V1,M3} P(811,17);d(269);r(1) { ! aElement0( X ), !
% 7.38/7.78 aElement0( sz10 ), sdtasdt0( sdtpldt0( X, sz10 ), sz00 ) ==> sdtasdt0( X
% 7.38/7.78 , sz00 ) }.
% 7.38/7.78 (1002) {G7,W7,D4,L1,V0,M1} F(996);d(811);r(2) { sdtasdt0( sdtpldt0( sz10,
% 7.38/7.78 sz10 ), sz00 ) ==> sz00 }.
% 7.38/7.78 (1008) {G2,W15,D4,L2,V1,M2} F(989) { ! aElement0( X ), sdtpldt0( sdtasdt0(
% 7.38/7.78 X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0( sdtpldt0( X, X ), sz00 )
% 7.38/7.78 }.
% 7.38/7.78 (1115) {G3,W13,D4,L3,V2,M3} R(18,5);d(620) { ! aElement0( X ), ! aElement0
% 7.38/7.78 ( Y ), sdtasdt0( smndt0( X ), Y ) ==> smndt0( sdtasdt0( X, Y ) ) }.
% 7.38/7.78 (1121) {G4,W6,D4,L1,V0,M1} R(18,1);d(349) { sdtasdt0( smndt0( sz10 ), sz00
% 7.38/7.78 ) ==> sz00 }.
% 7.38/7.78 (1264) {G5,W6,D4,L1,V0,M1} R(19,377);d(1121);d(349) { sdtasdt0( sz00,
% 7.38/7.78 smndt0( sz10 ) ) ==> sz00 }.
% 7.38/7.78 (1455) {G1,W7,D3,L2,V0,M2} P(12,21);f;r(20) { ! sdtasdt0( sz00, xx ) ==>
% 7.38/7.78 sz00, ! aElement0( sz00 ) }.
% 7.38/7.78 (2022) {G6,W13,D4,L3,V1,M3} P(1264,13);d(622);d(1115);r(1) { ! aElement0( X
% 7.38/7.78 ), ! aElement0( smndt0( sz10 ) ), smndt0( sdtasdt0( X, sz00 ) ) ==>
% 7.38/7.78 sdtasdt0( X, sz00 ) }.
% 7.38/7.78 (2453) {G3,W11,D4,L2,V1,M2} R(34,1);d(1008);d(275) { ! aElement0( X ),
% 7.38/7.78 sdtasdt0( sdtpldt0( X, X ), sz00 ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.78 (7533) {G2,W5,D3,L1,V0,M1} S(1455);r(1) { ! sdtasdt0( sz00, xx ) ==> sz00
% 7.38/7.78 }.
% 7.38/7.78 (17532) {G8,W9,D3,L2,V0,M2} P(1002,37);d(145);d(269);d(8);d(1002);r(1) { !
% 7.38/7.78 aElement0( sdtpldt0( sz10, sz10 ) ), sdtasdt0( sz00, sz00 ) ==> sz00 }.
% 7.38/7.78 (20048) {G9,W5,D3,L1,V0,M1} S(17532);r(937) { sdtasdt0( sz00, sz00 ) ==>
% 7.38/7.78 sz00 }.
% 7.38/7.78 (20057) {G7,W10,D4,L2,V1,M2} S(2022);r(42) { ! aElement0( X ), smndt0(
% 7.38/7.78 sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.78 (20062) {G4,W13,D4,L2,V1,M2} S(1008);d(2453) { ! aElement0( X ), sdtpldt0(
% 7.38/7.78 sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.78 (20086) {G8,W7,D3,L2,V1,M2} S(416);d(20057);d(20062) { ! aElement0( X ),
% 7.38/7.78 sdtasdt0( X, sz00 ) ==> sz00 }.
% 7.38/7.78 (20090) {G10,W7,D3,L2,V1,M2} P(20048,16);f;d(145);d(269);d(516);d(9);d(
% 7.38/7.78 20086);r(1) { ! aElement0( X ), sdtasdt0( sz00, X ) ==> sz00 }.
% 7.38/7.78 (20153) {G11,W0,D0,L0,V0,M0} R(20090,7533);r(20) { }.
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 % SZS output end Refutation
% 7.38/7.78 found a proof!
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Unprocessed initial clauses:
% 7.38/7.78
% 7.38/7.78 (20155) {G0,W1,D1,L1,V0,M1} { && }.
% 7.38/7.78 (20156) {G0,W2,D2,L1,V0,M1} { aElement0( sz00 ) }.
% 7.38/7.78 (20157) {G0,W2,D2,L1,V0,M1} { aElement0( sz10 ) }.
% 7.38/7.78 (20158) {G0,W5,D3,L2,V1,M2} { ! aElement0( X ), aElement0( smndt0( X ) )
% 7.38/7.78 }.
% 7.38/7.78 (20159) {G0,W8,D3,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y ),
% 7.38/7.78 aElement0( sdtpldt0( X, Y ) ) }.
% 7.38/7.78 (20160) {G0,W8,D3,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y ),
% 7.38/7.78 aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.78 (20161) {G0,W11,D3,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y ),
% 7.38/7.78 sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 7.38/7.78 (20162) {G0,W17,D4,L4,V3,M4} { ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0(
% 7.38/7.78 Y, Z ) ) }.
% 7.38/7.78 (20163) {G0,W7,D3,L2,V1,M2} { ! aElement0( X ), sdtpldt0( X, sz00 ) = X
% 7.38/7.78 }.
% 7.38/7.78 (20164) {G0,W7,D3,L2,V1,M2} { ! aElement0( X ), X = sdtpldt0( sz00, X )
% 7.38/7.78 }.
% 7.38/7.78 (20165) {G0,W8,D4,L2,V1,M2} { ! aElement0( X ), sdtpldt0( X, smndt0( X ) )
% 7.38/7.78 = sz00 }.
% 7.38/7.78 (20166) {G0,W8,D4,L2,V1,M2} { ! aElement0( X ), sz00 = sdtpldt0( smndt0( X
% 7.38/7.78 ), X ) }.
% 7.38/7.78 (20167) {G0,W11,D3,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y ),
% 7.38/7.78 sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 7.38/7.78 (20168) {G0,W17,D4,L4,V3,M4} { ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0(
% 7.38/7.78 Y, Z ) ) }.
% 7.38/7.78 (20169) {G0,W7,D3,L2,V1,M2} { ! aElement0( X ), sdtasdt0( X, sz10 ) = X
% 7.38/7.78 }.
% 7.38/7.78 (20170) {G0,W7,D3,L2,V1,M2} { ! aElement0( X ), X = sdtasdt0( sz10, X )
% 7.38/7.78 }.
% 7.38/7.78 (20171) {G0,W19,D4,L4,V3,M4} { ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X,
% 7.38/7.78 Y ), sdtasdt0( X, Z ) ) }.
% 7.38/7.78 (20172) {G0,W19,D4,L4,V3,M4} { ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y,
% 7.38/7.78 X ), sdtasdt0( Z, X ) ) }.
% 7.38/7.78 (20173) {G0,W9,D4,L2,V1,M2} { ! aElement0( X ), sdtasdt0( smndt0( sz10 ),
% 7.38/7.78 X ) = smndt0( X ) }.
% 7.38/7.78 (20174) {G0,W9,D4,L2,V1,M2} { ! aElement0( X ), smndt0( X ) = sdtasdt0( X
% 7.38/7.78 , smndt0( sz10 ) ) }.
% 7.38/7.78 (20175) {G0,W2,D2,L1,V0,M1} { aElement0( xx ) }.
% 7.38/7.78 (20176) {G0,W10,D3,L2,V0,M2} { ! sdtasdt0( xx, sz00 ) = sz00, ! sz00 =
% 7.38/7.78 sdtasdt0( sz00, xx ) }.
% 7.38/7.78
% 7.38/7.78
% 7.38/7.78 Total Proof:
% 7.38/7.78
% 7.38/7.78 subsumption: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.78 parent0: (20156) {G0,W2,D2,L1,V0,M1} { aElement0( sz00 ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (2) {G0,W2,D2,L1,V0,M1} I { aElement0( sz10 ) }.
% 7.38/7.78 parent0: (20157) {G0,W2,D2,L1,V0,M1} { aElement0( sz10 ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (3) {G0,W5,D3,L2,V1,M2} I { ! aElement0( X ), aElement0(
% 7.38/7.78 smndt0( X ) ) }.
% 7.38/7.78 parent0: (20158) {G0,W5,D3,L2,V1,M2} { ! aElement0( X ), aElement0( smndt0
% 7.38/7.78 ( X ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (4) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , aElement0( sdtpldt0( X, Y ) ) }.
% 7.38/7.78 parent0: (20159) {G0,W8,D3,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , aElement0( sdtpldt0( X, Y ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 2 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (5) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.78 parent0: (20160) {G0,W8,D3,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 2 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (6) {G0,W11,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.78 ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 7.38/7.78 parent0: (20161) {G0,W11,D3,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 2 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (8) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( X,
% 7.38/7.78 sz00 ) ==> X }.
% 7.38/7.78 parent0: (20163) {G0,W7,D3,L2,V1,M2} { ! aElement0( X ), sdtpldt0( X, sz00
% 7.38/7.78 ) = X }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 eqswap: (20209) {G0,W7,D3,L2,V1,M2} { sdtpldt0( sz00, X ) = X, ! aElement0
% 7.38/7.78 ( X ) }.
% 7.38/7.78 parent0[1]: (20164) {G0,W7,D3,L2,V1,M2} { ! aElement0( X ), X = sdtpldt0(
% 7.38/7.78 sz00, X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (9) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( sz00,
% 7.38/7.78 X ) ==> X }.
% 7.38/7.78 parent0: (20209) {G0,W7,D3,L2,V1,M2} { sdtpldt0( sz00, X ) = X, !
% 7.38/7.78 aElement0( X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 1
% 7.38/7.78 1 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (10) {G0,W8,D4,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( X,
% 7.38/7.78 smndt0( X ) ) ==> sz00 }.
% 7.38/7.78 parent0: (20165) {G0,W8,D4,L2,V1,M2} { ! aElement0( X ), sdtpldt0( X,
% 7.38/7.78 smndt0( X ) ) = sz00 }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 eqswap: (20240) {G0,W8,D4,L2,V1,M2} { sdtpldt0( smndt0( X ), X ) = sz00, !
% 7.38/7.78 aElement0( X ) }.
% 7.38/7.78 parent0[1]: (20166) {G0,W8,D4,L2,V1,M2} { ! aElement0( X ), sz00 =
% 7.38/7.78 sdtpldt0( smndt0( X ), X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (11) {G0,W8,D4,L2,V1,M2} I { ! aElement0( X ), sdtpldt0(
% 7.38/7.78 smndt0( X ), X ) ==> sz00 }.
% 7.38/7.78 parent0: (20240) {G0,W8,D4,L2,V1,M2} { sdtpldt0( smndt0( X ), X ) = sz00,
% 7.38/7.78 ! aElement0( X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 1
% 7.38/7.78 1 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 *** allocated 384427 integers for termspace/termends
% 7.38/7.78 subsumption: (12) {G0,W11,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.78 ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 7.38/7.78 parent0: (20167) {G0,W11,D3,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 2 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 eqswap: (20275) {G0,W17,D4,L4,V3,M4} { sdtasdt0( X, sdtasdt0( Y, Z ) ) =
% 7.38/7.78 sdtasdt0( sdtasdt0( X, Y ), Z ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ) }.
% 7.38/7.78 parent0[3]: (20168) {G0,W17,D4,L4,V3,M4} { ! aElement0( X ), ! aElement0(
% 7.38/7.78 Y ), ! aElement0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X,
% 7.38/7.78 sdtasdt0( Y, Z ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 Z := Z
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (13) {G0,W17,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.78 ), ! aElement0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) ==> sdtasdt0(
% 7.38/7.78 sdtasdt0( X, Y ), Z ) }.
% 7.38/7.78 parent0: (20275) {G0,W17,D4,L4,V3,M4} { sdtasdt0( X, sdtasdt0( Y, Z ) ) =
% 7.38/7.78 sdtasdt0( sdtasdt0( X, Y ), Z ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.78 aElement0( Z ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 Z := Z
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 3
% 7.38/7.78 1 ==> 0
% 7.38/7.78 2 ==> 1
% 7.38/7.78 3 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (14) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( X,
% 7.38/7.78 sz10 ) ==> X }.
% 7.38/7.78 parent0: (20169) {G0,W7,D3,L2,V1,M2} { ! aElement0( X ), sdtasdt0( X, sz10
% 7.38/7.78 ) = X }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 eqswap: (20338) {G0,W7,D3,L2,V1,M2} { sdtasdt0( sz10, X ) = X, ! aElement0
% 7.38/7.78 ( X ) }.
% 7.38/7.78 parent0[1]: (20170) {G0,W7,D3,L2,V1,M2} { ! aElement0( X ), X = sdtasdt0(
% 7.38/7.78 sz10, X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (15) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( sz10
% 7.38/7.78 , X ) ==> X }.
% 7.38/7.78 parent0: (20338) {G0,W7,D3,L2,V1,M2} { sdtasdt0( sz10, X ) = X, !
% 7.38/7.78 aElement0( X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 1
% 7.38/7.78 1 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 eqswap: (20367) {G0,W19,D4,L4,V3,M4} { sdtpldt0( sdtasdt0( X, Y ),
% 7.38/7.78 sdtasdt0( X, Z ) ) = sdtasdt0( X, sdtpldt0( Y, Z ) ), ! aElement0( X ), !
% 7.38/7.78 aElement0( Y ), ! aElement0( Z ) }.
% 7.38/7.78 parent0[3]: (20171) {G0,W19,D4,L4,V3,M4} { ! aElement0( X ), ! aElement0(
% 7.38/7.78 Y ), ! aElement0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0(
% 7.38/7.78 sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 Z := Z
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (16) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.78 ), ! aElement0( Z ), sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) ==>
% 7.38/7.78 sdtasdt0( X, sdtpldt0( Y, Z ) ) }.
% 7.38/7.78 parent0: (20367) {G0,W19,D4,L4,V3,M4} { sdtpldt0( sdtasdt0( X, Y ),
% 7.38/7.78 sdtasdt0( X, Z ) ) = sdtasdt0( X, sdtpldt0( Y, Z ) ), ! aElement0( X ), !
% 7.38/7.78 aElement0( Y ), ! aElement0( Z ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 Z := Z
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 3
% 7.38/7.78 1 ==> 0
% 7.38/7.78 2 ==> 1
% 7.38/7.78 3 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 eqswap: (20413) {G0,W19,D4,L4,V3,M4} { sdtpldt0( sdtasdt0( X, Z ),
% 7.38/7.78 sdtasdt0( Y, Z ) ) = sdtasdt0( sdtpldt0( X, Y ), Z ), ! aElement0( Z ), !
% 7.38/7.78 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.78 parent0[3]: (20172) {G0,W19,D4,L4,V3,M4} { ! aElement0( X ), ! aElement0(
% 7.38/7.78 Y ), ! aElement0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0(
% 7.38/7.78 sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := Z
% 7.38/7.78 Y := X
% 7.38/7.78 Z := Y
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (17) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.78 ), ! aElement0( Z ), sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) ==>
% 7.38/7.78 sdtasdt0( sdtpldt0( Y, Z ), X ) }.
% 7.38/7.78 parent0: (20413) {G0,W19,D4,L4,V3,M4} { sdtpldt0( sdtasdt0( X, Z ),
% 7.38/7.78 sdtasdt0( Y, Z ) ) = sdtasdt0( sdtpldt0( X, Y ), Z ), ! aElement0( Z ), !
% 7.38/7.78 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := Y
% 7.38/7.78 Y := Z
% 7.38/7.78 Z := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 3
% 7.38/7.78 1 ==> 0
% 7.38/7.78 2 ==> 1
% 7.38/7.78 3 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (18) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0(
% 7.38/7.78 smndt0( sz10 ), X ) ==> smndt0( X ) }.
% 7.38/7.78 parent0: (20173) {G0,W9,D4,L2,V1,M2} { ! aElement0( X ), sdtasdt0( smndt0
% 7.38/7.78 ( sz10 ), X ) = smndt0( X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 eqswap: (20516) {G0,W9,D4,L2,V1,M2} { sdtasdt0( X, smndt0( sz10 ) ) =
% 7.38/7.78 smndt0( X ), ! aElement0( X ) }.
% 7.38/7.78 parent0[1]: (20174) {G0,W9,D4,L2,V1,M2} { ! aElement0( X ), smndt0( X ) =
% 7.38/7.78 sdtasdt0( X, smndt0( sz10 ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (19) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( X,
% 7.38/7.78 smndt0( sz10 ) ) ==> smndt0( X ) }.
% 7.38/7.78 parent0: (20516) {G0,W9,D4,L2,V1,M2} { sdtasdt0( X, smndt0( sz10 ) ) =
% 7.38/7.78 smndt0( X ), ! aElement0( X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 1
% 7.38/7.78 1 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (20) {G0,W2,D2,L1,V0,M1} I { aElement0( xx ) }.
% 7.38/7.78 parent0: (20175) {G0,W2,D2,L1,V0,M1} { aElement0( xx ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 eqswap: (20614) {G0,W10,D3,L2,V0,M2} { ! sdtasdt0( sz00, xx ) = sz00, !
% 7.38/7.78 sdtasdt0( xx, sz00 ) = sz00 }.
% 7.38/7.78 parent0[1]: (20176) {G0,W10,D3,L2,V0,M2} { ! sdtasdt0( xx, sz00 ) = sz00,
% 7.38/7.78 ! sz00 = sdtasdt0( sz00, xx ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (21) {G0,W10,D3,L2,V0,M2} I { ! sdtasdt0( xx, sz00 ) ==> sz00
% 7.38/7.78 , ! sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.78 parent0: (20614) {G0,W10,D3,L2,V0,M2} { ! sdtasdt0( sz00, xx ) = sz00, !
% 7.38/7.78 sdtasdt0( xx, sz00 ) = sz00 }.
% 7.38/7.78 substitution0:
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 1
% 7.38/7.78 1 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 factor: (20619) {G0,W17,D4,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Y ) ) ==> sdtasdt0( X,
% 7.38/7.78 sdtpldt0( Y, Y ) ) }.
% 7.38/7.78 parent0[1, 2]: (16) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0
% 7.38/7.78 ( Y ), ! aElement0( Z ), sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) )
% 7.38/7.78 ==> sdtasdt0( X, sdtpldt0( Y, Z ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 Z := Y
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (34) {G1,W17,D4,L3,V2,M3} F(16) { ! aElement0( X ), !
% 7.38/7.78 aElement0( Y ), sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Y ) ) ==>
% 7.38/7.78 sdtasdt0( X, sdtpldt0( Y, Y ) ) }.
% 7.38/7.78 parent0: (20619) {G0,W17,D4,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Y ) ) ==> sdtasdt0( X,
% 7.38/7.78 sdtpldt0( Y, Y ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 2 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 factor: (20627) {G0,W17,D4,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( X, X ) ) ==> sdtasdt0( sdtpldt0(
% 7.38/7.78 Y, X ), X ) }.
% 7.38/7.78 parent0[0, 2]: (17) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0
% 7.38/7.78 ( Y ), ! aElement0( Z ), sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) )
% 7.38/7.78 ==> sdtasdt0( sdtpldt0( Y, Z ), X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 Z := X
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (37) {G1,W17,D4,L3,V2,M3} F(17) { ! aElement0( X ), !
% 7.38/7.78 aElement0( Y ), sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( X, X ) ) ==>
% 7.38/7.78 sdtasdt0( sdtpldt0( Y, X ), X ) }.
% 7.38/7.78 parent0: (20627) {G0,W17,D4,L3,V2,M3} { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( X, X ) ) ==> sdtasdt0( sdtpldt0(
% 7.38/7.78 Y, X ), X ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := X
% 7.38/7.78 Y := Y
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 1 ==> 1
% 7.38/7.78 2 ==> 2
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 resolution: (20634) {G1,W3,D3,L1,V0,M1} { aElement0( smndt0( sz00 ) ) }.
% 7.38/7.78 parent0[0]: (3) {G0,W5,D3,L2,V1,M2} I { ! aElement0( X ), aElement0( smndt0
% 7.38/7.78 ( X ) ) }.
% 7.38/7.78 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := sz00
% 7.38/7.78 end
% 7.38/7.78 substitution1:
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (41) {G1,W3,D3,L1,V0,M1} R(3,1) { aElement0( smndt0( sz00 ) )
% 7.38/7.78 }.
% 7.38/7.78 parent0: (20634) {G1,W3,D3,L1,V0,M1} { aElement0( smndt0( sz00 ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 resolution: (20635) {G1,W3,D3,L1,V0,M1} { aElement0( smndt0( sz10 ) ) }.
% 7.38/7.78 parent0[0]: (3) {G0,W5,D3,L2,V1,M2} I { ! aElement0( X ), aElement0( smndt0
% 7.38/7.78 ( X ) ) }.
% 7.38/7.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aElement0( sz10 ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := sz10
% 7.38/7.78 end
% 7.38/7.78 substitution1:
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (42) {G1,W3,D3,L1,V0,M1} R(3,2) { aElement0( smndt0( sz10 ) )
% 7.38/7.78 }.
% 7.38/7.78 parent0: (20635) {G1,W3,D3,L1,V0,M1} { aElement0( smndt0( sz10 ) ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 end
% 7.38/7.78 permutation0:
% 7.38/7.78 0 ==> 0
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 resolution: (20636) {G1,W6,D3,L2,V1,M2} { ! aElement0( X ), aElement0(
% 7.38/7.78 sdtpldt0( sz10, X ) ) }.
% 7.38/7.78 parent0[0]: (4) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.78 , aElement0( sdtpldt0( X, Y ) ) }.
% 7.38/7.78 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aElement0( sz10 ) }.
% 7.38/7.78 substitution0:
% 7.38/7.78 X := sz10
% 7.38/7.78 Y := X
% 7.38/7.78 end
% 7.38/7.78 substitution1:
% 7.38/7.78 end
% 7.38/7.78
% 7.38/7.78 subsumption: (48) {G1,W6,D3,L2,V1,M2} R(4,2) { ! aElement0( X ), aElement0
% 7.38/7.78 ( sdtpldt0( sz10, X ) ) }.
% 7.38/7.79 parent0: (20636) {G1,W6,D3,L2,V1,M2} { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtpldt0( sz10, X ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 1 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20638) {G1,W4,D4,L1,V0,M1} { aElement0( smndt0( smndt0( sz00
% 7.38/7.79 ) ) ) }.
% 7.38/7.79 parent0[0]: (3) {G0,W5,D3,L2,V1,M2} I { ! aElement0( X ), aElement0( smndt0
% 7.38/7.79 ( X ) ) }.
% 7.38/7.79 parent1[0]: (41) {G1,W3,D3,L1,V0,M1} R(3,1) { aElement0( smndt0( sz00 ) )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := smndt0( sz00 )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (59) {G2,W4,D4,L1,V0,M1} R(41,3) { aElement0( smndt0( smndt0(
% 7.38/7.79 sz00 ) ) ) }.
% 7.38/7.79 parent0: (20638) {G1,W4,D4,L1,V0,M1} { aElement0( smndt0( smndt0( sz00 ) )
% 7.38/7.79 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20639) {G1,W6,D3,L2,V1,M2} { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtasdt0( sz00, X ) ) }.
% 7.38/7.79 parent0[0]: (5) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.79 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sz00
% 7.38/7.79 Y := X
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (83) {G1,W6,D3,L2,V1,M2} R(5,1) { ! aElement0( X ), aElement0
% 7.38/7.79 ( sdtasdt0( sz00, X ) ) }.
% 7.38/7.79 parent0: (20639) {G1,W6,D3,L2,V1,M2} { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtasdt0( sz00, X ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 1 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20642) {G1,W6,D3,L2,V1,M2} { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtasdt0( X, sz00 ) ) }.
% 7.38/7.79 parent0[1]: (5) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.79 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := sz00
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (84) {G1,W6,D3,L2,V1,M2} R(5,1) { ! aElement0( X ), aElement0
% 7.38/7.79 ( sdtasdt0( X, sz00 ) ) }.
% 7.38/7.79 parent0: (20642) {G1,W6,D3,L2,V1,M2} { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtasdt0( X, sz00 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 1 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20643) {G1,W5,D5,L1,V0,M1} { aElement0( smndt0( smndt0(
% 7.38/7.79 smndt0( sz00 ) ) ) ) }.
% 7.38/7.79 parent0[0]: (3) {G0,W5,D3,L2,V1,M2} I { ! aElement0( X ), aElement0( smndt0
% 7.38/7.79 ( X ) ) }.
% 7.38/7.79 parent1[0]: (59) {G2,W4,D4,L1,V0,M1} R(41,3) { aElement0( smndt0( smndt0(
% 7.38/7.79 sz00 ) ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := smndt0( smndt0( sz00 ) )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (118) {G3,W5,D5,L1,V0,M1} R(59,3) { aElement0( smndt0( smndt0
% 7.38/7.79 ( smndt0( sz00 ) ) ) ) }.
% 7.38/7.79 parent0: (20643) {G1,W5,D5,L1,V0,M1} { aElement0( smndt0( smndt0( smndt0(
% 7.38/7.79 sz00 ) ) ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20644) {G1,W17,D4,L4,V3,M4} { ! aElement0( Z ), sdtpldt0(
% 7.38/7.79 sdtasdt0( X, Y ), Z ) = sdtpldt0( Z, sdtasdt0( X, Y ) ), ! aElement0( X )
% 7.38/7.79 , ! aElement0( Y ) }.
% 7.38/7.79 parent0[0]: (6) {G0,W11,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 7.38/7.79 parent1[2]: (5) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sdtasdt0( X, Y )
% 7.38/7.79 Y := Z
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (133) {G1,W17,D4,L4,V3,M4} R(6,5) { ! aElement0( X ), sdtpldt0
% 7.38/7.79 ( sdtasdt0( Y, Z ), X ) = sdtpldt0( X, sdtasdt0( Y, Z ) ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( Z ) }.
% 7.38/7.79 parent0: (20644) {G1,W17,D4,L4,V3,M4} { ! aElement0( Z ), sdtpldt0(
% 7.38/7.79 sdtasdt0( X, Y ), Z ) = sdtpldt0( Z, sdtasdt0( X, Y ) ), ! aElement0( X )
% 7.38/7.79 , ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := Y
% 7.38/7.79 Y := Z
% 7.38/7.79 Z := X
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 1 ==> 1
% 7.38/7.79 2 ==> 2
% 7.38/7.79 3 ==> 3
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20654) {G1,W17,D4,L4,V3,M4} { sdtpldt0( Z, sdtasdt0( X, Y ) ) =
% 7.38/7.79 sdtpldt0( sdtasdt0( X, Y ), Z ), ! aElement0( Z ), ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (133) {G1,W17,D4,L4,V3,M4} R(6,5) { ! aElement0( X ), sdtpldt0
% 7.38/7.79 ( sdtasdt0( Y, Z ), X ) = sdtpldt0( X, sdtasdt0( Y, Z ) ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( Z ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := Z
% 7.38/7.79 Y := X
% 7.38/7.79 Z := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (20659) {G1,W15,D4,L3,V2,M3} { sdtpldt0( X, sdtasdt0( X, Y ) ) =
% 7.38/7.79 sdtpldt0( sdtasdt0( X, Y ), X ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1, 2]: (20654) {G1,W17,D4,L4,V3,M4} { sdtpldt0( Z, sdtasdt0( X, Y
% 7.38/7.79 ) ) = sdtpldt0( sdtasdt0( X, Y ), Z ), ! aElement0( Z ), ! aElement0( X
% 7.38/7.79 ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 Z := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (145) {G2,W15,D4,L3,V2,M3} F(133) { ! aElement0( X ), sdtpldt0
% 7.38/7.79 ( X, sdtasdt0( X, Y ) ) ==> sdtpldt0( sdtasdt0( X, Y ), X ), ! aElement0
% 7.38/7.79 ( Y ) }.
% 7.38/7.79 parent0: (20659) {G1,W15,D4,L3,V2,M3} { sdtpldt0( X, sdtasdt0( X, Y ) ) =
% 7.38/7.79 sdtpldt0( sdtasdt0( X, Y ), X ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 1
% 7.38/7.79 1 ==> 0
% 7.38/7.79 2 ==> 2
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20663) {G1,W4,D3,L1,V0,M1} { aElement0( sdtasdt0( sz00, sz10
% 7.38/7.79 ) ) }.
% 7.38/7.79 parent0[0]: (83) {G1,W6,D3,L2,V1,M2} R(5,1) { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtasdt0( sz00, X ) ) }.
% 7.38/7.79 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aElement0( sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sz10
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (175) {G2,W4,D3,L1,V0,M1} R(83,2) { aElement0( sdtasdt0( sz00
% 7.38/7.79 , sz10 ) ) }.
% 7.38/7.79 parent0: (20663) {G1,W4,D3,L1,V0,M1} { aElement0( sdtasdt0( sz00, sz10 ) )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20664) {G1,W5,D4,L1,V0,M1} { aElement0( smndt0( sdtasdt0(
% 7.38/7.79 sz00, sz10 ) ) ) }.
% 7.38/7.79 parent0[0]: (3) {G0,W5,D3,L2,V1,M2} I { ! aElement0( X ), aElement0( smndt0
% 7.38/7.79 ( X ) ) }.
% 7.38/7.79 parent1[0]: (175) {G2,W4,D3,L1,V0,M1} R(83,2) { aElement0( sdtasdt0( sz00,
% 7.38/7.79 sz10 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sdtasdt0( sz00, sz10 )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (197) {G3,W5,D4,L1,V0,M1} R(175,3) { aElement0( smndt0(
% 7.38/7.79 sdtasdt0( sz00, sz10 ) ) ) }.
% 7.38/7.79 parent0: (20664) {G1,W5,D4,L1,V0,M1} { aElement0( smndt0( sdtasdt0( sz00,
% 7.38/7.79 sz10 ) ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20665) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( X, sz00 ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent0[1]: (8) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( X, sz00
% 7.38/7.79 ) ==> X }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20666) {G1,W13,D4,L3,V2,M3} { sdtasdt0( X, Y ) ==> sdtpldt0(
% 7.38/7.79 sdtasdt0( X, Y ), sz00 ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (20665) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( X, sz00 ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent1[2]: (5) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sdtasdt0( X, Y )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20667) {G1,W13,D4,L3,V2,M3} { sdtpldt0( sdtasdt0( X, Y ), sz00 )
% 7.38/7.79 ==> sdtasdt0( X, Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[0]: (20666) {G1,W13,D4,L3,V2,M3} { sdtasdt0( X, Y ) ==> sdtpldt0(
% 7.38/7.79 sdtasdt0( X, Y ), sz00 ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (269) {G1,W13,D4,L3,V2,M3} R(8,5) { sdtpldt0( sdtasdt0( X, Y )
% 7.38/7.79 , sz00 ) ==> sdtasdt0( X, Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0: (20667) {G1,W13,D4,L3,V2,M3} { sdtpldt0( sdtasdt0( X, Y ), sz00 )
% 7.38/7.79 ==> sdtasdt0( X, Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 1 ==> 1
% 7.38/7.79 2 ==> 2
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20670) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( X, sz00 ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent0[1]: (8) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( X, sz00
% 7.38/7.79 ) ==> X }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20671) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtpldt0( sz00, sz00 )
% 7.38/7.79 }.
% 7.38/7.79 parent0[1]: (20670) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( X, sz00 ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sz00
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20672) {G1,W5,D3,L1,V0,M1} { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 7.38/7.79 parent0[0]: (20671) {G1,W5,D3,L1,V0,M1} { sz00 ==> sdtpldt0( sz00, sz00 )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (275) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent0: (20672) {G1,W5,D3,L1,V0,M1} { sdtpldt0( sz00, sz00 ) ==> sz00 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20673) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( sz00, X ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent0[1]: (9) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( sz00, X
% 7.38/7.79 ) ==> X }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20674) {G1,W7,D4,L1,V0,M1} { smndt0( sz00 ) ==> sdtpldt0(
% 7.38/7.79 sz00, smndt0( sz00 ) ) }.
% 7.38/7.79 parent0[1]: (20673) {G0,W7,D3,L2,V1,M2} { X ==> sdtpldt0( sz00, X ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent1[0]: (41) {G1,W3,D3,L1,V0,M1} R(3,1) { aElement0( smndt0( sz00 ) )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := smndt0( sz00 )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20675) {G1,W7,D4,L1,V0,M1} { sdtpldt0( sz00, smndt0( sz00 ) ) ==>
% 7.38/7.79 smndt0( sz00 ) }.
% 7.38/7.79 parent0[0]: (20674) {G1,W7,D4,L1,V0,M1} { smndt0( sz00 ) ==> sdtpldt0(
% 7.38/7.79 sz00, smndt0( sz00 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (304) {G2,W7,D4,L1,V0,M1} R(9,41) { sdtpldt0( sz00, smndt0(
% 7.38/7.79 sz00 ) ) ==> smndt0( sz00 ) }.
% 7.38/7.79 parent0: (20675) {G1,W7,D4,L1,V0,M1} { sdtpldt0( sz00, smndt0( sz00 ) )
% 7.38/7.79 ==> smndt0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20676) {G0,W8,D4,L2,V1,M2} { sz00 ==> sdtpldt0( X, smndt0( X ) )
% 7.38/7.79 , ! aElement0( X ) }.
% 7.38/7.79 parent0[1]: (10) {G0,W8,D4,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( X,
% 7.38/7.79 smndt0( X ) ) ==> sz00 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20678) {G1,W6,D4,L1,V0,M1} { sz00 ==> sdtpldt0( sz00, smndt0
% 7.38/7.79 ( sz00 ) ) }.
% 7.38/7.79 parent0[1]: (20676) {G0,W8,D4,L2,V1,M2} { sz00 ==> sdtpldt0( X, smndt0( X
% 7.38/7.79 ) ), ! aElement0( X ) }.
% 7.38/7.79 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sz00
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (20679) {G2,W4,D3,L1,V0,M1} { sz00 ==> smndt0( sz00 ) }.
% 7.38/7.79 parent0[0]: (304) {G2,W7,D4,L1,V0,M1} R(9,41) { sdtpldt0( sz00, smndt0(
% 7.38/7.79 sz00 ) ) ==> smndt0( sz00 ) }.
% 7.38/7.79 parent1[0; 2]: (20678) {G1,W6,D4,L1,V0,M1} { sz00 ==> sdtpldt0( sz00,
% 7.38/7.79 smndt0( sz00 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20680) {G2,W4,D3,L1,V0,M1} { smndt0( sz00 ) ==> sz00 }.
% 7.38/7.79 parent0[0]: (20679) {G2,W4,D3,L1,V0,M1} { sz00 ==> smndt0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent0: (20680) {G2,W4,D3,L1,V0,M1} { smndt0( sz00 ) ==> sz00 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20681) {G2,W5,D4,L1,V0,M1} { aElement0( sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), sz00 ) ) }.
% 7.38/7.79 parent0[0]: (84) {G1,W6,D3,L2,V1,M2} R(5,1) { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtasdt0( X, sz00 ) ) }.
% 7.38/7.79 parent1[0]: (42) {G1,W3,D3,L1,V0,M1} R(3,2) { aElement0( smndt0( sz10 ) )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := smndt0( sz10 )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (377) {G2,W5,D4,L1,V0,M1} R(84,42) { aElement0( sdtasdt0(
% 7.38/7.79 smndt0( sz10 ), sz00 ) ) }.
% 7.38/7.79 parent0: (20681) {G2,W5,D4,L1,V0,M1} { aElement0( sdtasdt0( smndt0( sz10 )
% 7.38/7.79 , sz00 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20682) {G0,W8,D4,L2,V1,M2} { sz00 ==> sdtpldt0( smndt0( X ), X )
% 7.38/7.79 , ! aElement0( X ) }.
% 7.38/7.79 parent0[1]: (11) {G0,W8,D4,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( smndt0
% 7.38/7.79 ( X ), X ) ==> sz00 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20683) {G1,W12,D5,L2,V1,M2} { sz00 ==> sdtpldt0( smndt0(
% 7.38/7.79 sdtasdt0( X, sz00 ) ), sdtasdt0( X, sz00 ) ), ! aElement0( X ) }.
% 7.38/7.79 parent0[1]: (20682) {G0,W8,D4,L2,V1,M2} { sz00 ==> sdtpldt0( smndt0( X ),
% 7.38/7.79 X ), ! aElement0( X ) }.
% 7.38/7.79 parent1[1]: (84) {G1,W6,D3,L2,V1,M2} R(5,1) { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtasdt0( X, sz00 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sdtasdt0( X, sz00 )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20684) {G1,W12,D5,L2,V1,M2} { sdtpldt0( smndt0( sdtasdt0( X, sz00
% 7.38/7.79 ) ), sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X ) }.
% 7.38/7.79 parent0[0]: (20683) {G1,W12,D5,L2,V1,M2} { sz00 ==> sdtpldt0( smndt0(
% 7.38/7.79 sdtasdt0( X, sz00 ) ), sdtasdt0( X, sz00 ) ), ! aElement0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (416) {G2,W12,D5,L2,V1,M2} R(11,84) { sdtpldt0( smndt0(
% 7.38/7.79 sdtasdt0( X, sz00 ) ), sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X )
% 7.38/7.79 }.
% 7.38/7.79 parent0: (20684) {G1,W12,D5,L2,V1,M2} { sdtpldt0( smndt0( sdtasdt0( X,
% 7.38/7.79 sz00 ) ), sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 1 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20685) {G1,W17,D4,L4,V3,M4} { ! aElement0( Z ), sdtasdt0(
% 7.38/7.79 sdtpldt0( X, Y ), Z ) = sdtasdt0( Z, sdtpldt0( X, Y ) ), ! aElement0( X )
% 7.38/7.79 , ! aElement0( Y ) }.
% 7.38/7.79 parent0[0]: (12) {G0,W11,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.79 ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 7.38/7.79 parent1[2]: (4) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , aElement0( sdtpldt0( X, Y ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sdtpldt0( X, Y )
% 7.38/7.79 Y := Z
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (512) {G1,W17,D4,L4,V3,M4} R(12,4) { ! aElement0( X ),
% 7.38/7.79 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtasdt0( X, sdtpldt0( Y, Z ) ), !
% 7.38/7.79 aElement0( Y ), ! aElement0( Z ) }.
% 7.38/7.79 parent0: (20685) {G1,W17,D4,L4,V3,M4} { ! aElement0( Z ), sdtasdt0(
% 7.38/7.79 sdtpldt0( X, Y ), Z ) = sdtasdt0( Z, sdtpldt0( X, Y ) ), ! aElement0( X )
% 7.38/7.79 , ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := Y
% 7.38/7.79 Y := Z
% 7.38/7.79 Z := X
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 1 ==> 1
% 7.38/7.79 2 ==> 2
% 7.38/7.79 3 ==> 3
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20695) {G1,W17,D4,L4,V3,M4} { sdtasdt0( Z, sdtpldt0( X, Y ) ) =
% 7.38/7.79 sdtasdt0( sdtpldt0( X, Y ), Z ), ! aElement0( Z ), ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (512) {G1,W17,D4,L4,V3,M4} R(12,4) { ! aElement0( X ), sdtasdt0
% 7.38/7.79 ( sdtpldt0( Y, Z ), X ) = sdtasdt0( X, sdtpldt0( Y, Z ) ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( Z ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := Z
% 7.38/7.79 Y := X
% 7.38/7.79 Z := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (20700) {G1,W15,D4,L3,V2,M3} { sdtasdt0( X, sdtpldt0( X, Y ) ) =
% 7.38/7.79 sdtasdt0( sdtpldt0( X, Y ), X ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1, 2]: (20695) {G1,W17,D4,L4,V3,M4} { sdtasdt0( Z, sdtpldt0( X, Y
% 7.38/7.79 ) ) = sdtasdt0( sdtpldt0( X, Y ), Z ), ! aElement0( Z ), ! aElement0( X
% 7.38/7.79 ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 Z := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (516) {G2,W15,D4,L3,V2,M3} F(512) { ! aElement0( X ), sdtasdt0
% 7.38/7.79 ( X, sdtpldt0( X, Y ) ) ==> sdtasdt0( sdtpldt0( X, Y ), X ), ! aElement0
% 7.38/7.79 ( Y ) }.
% 7.38/7.79 parent0: (20700) {G1,W15,D4,L3,V2,M3} { sdtasdt0( X, sdtpldt0( X, Y ) ) =
% 7.38/7.79 sdtasdt0( sdtpldt0( X, Y ), X ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 1
% 7.38/7.79 1 ==> 0
% 7.38/7.79 2 ==> 2
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20704) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z ) ==>
% 7.38/7.79 sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( Z ) }.
% 7.38/7.79 parent0[3]: (13) {G0,W17,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) ==> sdtasdt0(
% 7.38/7.79 sdtasdt0( X, Y ), Z ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 Z := Z
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20706) {G1,W17,D5,L3,V2,M3} { sdtasdt0( sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), X ), Y ) ==> sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (20704) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z )
% 7.38/7.79 ==> sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , ! aElement0( Z ) }.
% 7.38/7.79 parent1[0]: (42) {G1,W3,D3,L1,V0,M1} R(3,2) { aElement0( smndt0( sz10 ) )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := smndt0( sz10 )
% 7.38/7.79 Y := X
% 7.38/7.79 Z := Y
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (20722) {G1,W17,D4,L4,V2,M4} { sdtasdt0( smndt0( X ), Y ) ==>
% 7.38/7.79 sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ), ! aElement0( X ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (18) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( smndt0
% 7.38/7.79 ( sz10 ), X ) ==> smndt0( X ) }.
% 7.38/7.79 parent1[0; 2]: (20706) {G1,W17,D5,L3,V2,M3} { sdtasdt0( sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), X ), Y ) ==> sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20725) {G1,W17,D4,L4,V2,M4} { sdtasdt0( smndt0( sz10 ), sdtasdt0
% 7.38/7.79 ( X, Y ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0
% 7.38/7.79 ( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[0]: (20722) {G1,W17,D4,L4,V2,M4} { sdtasdt0( smndt0( X ), Y ) ==>
% 7.38/7.79 sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ), ! aElement0( X ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (20734) {G1,W15,D4,L3,V2,M3} { sdtasdt0( smndt0( sz10 ), sdtasdt0
% 7.38/7.79 ( X, Y ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0
% 7.38/7.79 ( Y ) }.
% 7.38/7.79 parent0[1, 2]: (20725) {G1,W17,D4,L4,V2,M4} { sdtasdt0( smndt0( sz10 ),
% 7.38/7.79 sdtasdt0( X, Y ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (620) {G2,W15,D4,L3,V2,M3} R(13,42);d(18) { ! aElement0( X ),
% 7.38/7.79 ! aElement0( Y ), sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( X ), Y ) }.
% 7.38/7.79 parent0: (20734) {G1,W15,D4,L3,V2,M3} { sdtasdt0( smndt0( sz10 ), sdtasdt0
% 7.38/7.79 ( X, Y ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0
% 7.38/7.79 ( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 2
% 7.38/7.79 1 ==> 0
% 7.38/7.79 2 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20738) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z ) ==>
% 7.38/7.79 sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( Z ) }.
% 7.38/7.79 parent0[3]: (13) {G0,W17,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) ==> sdtasdt0(
% 7.38/7.79 sdtasdt0( X, Y ), Z ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 Z := Z
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20742) {G1,W17,D5,L3,V2,M3} { sdtasdt0( sdtasdt0( X, smndt0(
% 7.38/7.79 sz10 ) ), Y ) ==> sdtasdt0( X, sdtasdt0( smndt0( sz10 ), Y ) ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[2]: (20738) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z )
% 7.38/7.79 ==> sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , ! aElement0( Z ) }.
% 7.38/7.79 parent1[0]: (42) {G1,W3,D3,L1,V0,M1} R(3,2) { aElement0( smndt0( sz10 ) )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := smndt0( sz10 )
% 7.38/7.79 Z := Y
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (20772) {G1,W17,D5,L4,V2,M4} { sdtasdt0( sdtasdt0( X, smndt0(
% 7.38/7.79 sz10 ) ), Y ) ==> sdtasdt0( X, smndt0( Y ) ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (18) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( smndt0
% 7.38/7.79 ( sz10 ), X ) ==> smndt0( X ) }.
% 7.38/7.79 parent1[0; 9]: (20742) {G1,W17,D5,L3,V2,M3} { sdtasdt0( sdtasdt0( X,
% 7.38/7.79 smndt0( sz10 ) ), Y ) ==> sdtasdt0( X, sdtasdt0( smndt0( sz10 ), Y ) ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := Y
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (20774) {G1,W15,D5,L3,V2,M3} { sdtasdt0( sdtasdt0( X, smndt0( sz10
% 7.38/7.79 ) ), Y ) ==> sdtasdt0( X, smndt0( Y ) ), ! aElement0( Y ), ! aElement0(
% 7.38/7.79 X ) }.
% 7.38/7.79 parent0[1, 3]: (20772) {G1,W17,D5,L4,V2,M4} { sdtasdt0( sdtasdt0( X,
% 7.38/7.79 smndt0( sz10 ) ), Y ) ==> sdtasdt0( X, smndt0( Y ) ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (20786) {G1,W15,D4,L4,V2,M4} { sdtasdt0( smndt0( X ), Y ) ==>
% 7.38/7.79 sdtasdt0( X, smndt0( Y ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent0[1]: (19) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( X,
% 7.38/7.79 smndt0( sz10 ) ) ==> smndt0( X ) }.
% 7.38/7.79 parent1[0; 2]: (20774) {G1,W15,D5,L3,V2,M3} { sdtasdt0( sdtasdt0( X,
% 7.38/7.79 smndt0( sz10 ) ), Y ) ==> sdtasdt0( X, smndt0( Y ) ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20787) {G1,W15,D4,L4,V2,M4} { sdtasdt0( X, smndt0( Y ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent0[0]: (20786) {G1,W15,D4,L4,V2,M4} { sdtasdt0( smndt0( X ), Y ) ==>
% 7.38/7.79 sdtasdt0( X, smndt0( Y ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (20789) {G1,W13,D4,L3,V2,M3} { sdtasdt0( X, smndt0( Y ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1, 3]: (20787) {G1,W15,D4,L4,V2,M4} { sdtasdt0( X, smndt0( Y ) )
% 7.38/7.79 ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (621) {G2,W13,D4,L3,V2,M3} R(13,42);d(18);d(19) { ! aElement0
% 7.38/7.79 ( X ), ! aElement0( Y ), sdtasdt0( X, smndt0( Y ) ) ==> sdtasdt0( smndt0
% 7.38/7.79 ( X ), Y ) }.
% 7.38/7.79 parent0: (20789) {G1,W13,D4,L3,V2,M3} { sdtasdt0( X, smndt0( Y ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 2
% 7.38/7.79 1 ==> 0
% 7.38/7.79 2 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (20794) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z ) ==>
% 7.38/7.79 sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( Z ) }.
% 7.38/7.79 parent0[3]: (13) {G0,W17,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) ==> sdtasdt0(
% 7.38/7.79 sdtasdt0( X, Y ), Z ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 Z := Z
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (20799) {G1,W17,D5,L3,V2,M3} { sdtasdt0( sdtasdt0( X, Y ),
% 7.38/7.79 smndt0( sz10 ) ) ==> sdtasdt0( X, sdtasdt0( Y, smndt0( sz10 ) ) ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[3]: (20794) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z )
% 7.38/7.79 ==> sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , ! aElement0( Z ) }.
% 7.38/7.79 parent1[0]: (42) {G1,W3,D3,L1,V0,M1} R(3,2) { aElement0( smndt0( sz10 ) )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 Z := smndt0( sz10 )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (20890) {G1,W17,D4,L4,V2,M4} { sdtasdt0( sdtasdt0( X, Y ), smndt0
% 7.38/7.79 ( sz10 ) ) ==> sdtasdt0( X, smndt0( Y ) ), ! aElement0( Y ), ! aElement0
% 7.38/7.79 ( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (19) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( X,
% 7.38/7.79 smndt0( sz10 ) ) ==> smndt0( X ) }.
% 7.38/7.79 parent1[0; 9]: (20799) {G1,W17,D5,L3,V2,M3} { sdtasdt0( sdtasdt0( X, Y ),
% 7.38/7.79 smndt0( sz10 ) ) ==> sdtasdt0( X, sdtasdt0( Y, smndt0( sz10 ) ) ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := Y
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (20897) {G1,W15,D4,L3,V2,M3} { sdtasdt0( sdtasdt0( X, Y ), smndt0
% 7.38/7.79 ( sz10 ) ) ==> sdtasdt0( X, smndt0( Y ) ), ! aElement0( Y ), ! aElement0
% 7.38/7.79 ( X ) }.
% 7.38/7.79 parent0[1, 3]: (20890) {G1,W17,D4,L4,V2,M4} { sdtasdt0( sdtasdt0( X, Y ),
% 7.38/7.79 smndt0( sz10 ) ) ==> sdtasdt0( X, smndt0( Y ) ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (20954) {G2,W19,D4,L5,V2,M5} { sdtasdt0( sdtasdt0( X, Y ), smndt0
% 7.38/7.79 ( sz10 ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0
% 7.38/7.79 ( Y ), ! aElement0( Y ), ! aElement0( X ) }.
% 7.38/7.79 parent0[2]: (621) {G2,W13,D4,L3,V2,M3} R(13,42);d(18);d(19) { ! aElement0(
% 7.38/7.79 X ), ! aElement0( Y ), sdtasdt0( X, smndt0( Y ) ) ==> sdtasdt0( smndt0( X
% 7.38/7.79 ), Y ) }.
% 7.38/7.79 parent1[0; 7]: (20897) {G1,W15,D4,L3,V2,M3} { sdtasdt0( sdtasdt0( X, Y ),
% 7.38/7.79 smndt0( sz10 ) ) ==> sdtasdt0( X, smndt0( Y ) ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (20965) {G2,W17,D4,L4,V2,M4} { sdtasdt0( sdtasdt0( X, Y ), smndt0
% 7.38/7.79 ( sz10 ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0
% 7.38/7.79 ( Y ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1, 4]: (20954) {G2,W19,D4,L5,V2,M5} { sdtasdt0( sdtasdt0( X, Y ),
% 7.38/7.79 smndt0( sz10 ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ), ! aElement0( Y ), ! aElement0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (20967) {G2,W15,D4,L3,V2,M3} { sdtasdt0( sdtasdt0( X, Y ), smndt0
% 7.38/7.79 ( sz10 ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0
% 7.38/7.79 ( Y ) }.
% 7.38/7.79 parent0[2, 3]: (20965) {G2,W17,D4,L4,V2,M4} { sdtasdt0( sdtasdt0( X, Y ),
% 7.38/7.79 smndt0( sz10 ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (622) {G3,W15,D4,L3,V2,M3} R(13,42);d(19);d(621) { ! aElement0
% 7.38/7.79 ( X ), ! aElement0( Y ), sdtasdt0( sdtasdt0( X, Y ), smndt0( sz10 ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( X ), Y ) }.
% 7.38/7.79 parent0: (20967) {G2,W15,D4,L3,V2,M3} { sdtasdt0( sdtasdt0( X, Y ), smndt0
% 7.38/7.79 ( sz10 ) ) ==> sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0
% 7.38/7.79 ( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 2
% 7.38/7.79 1 ==> 0
% 7.38/7.79 2 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21001) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( X, sz10 ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent0[1]: (14) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( X,
% 7.38/7.79 sz10 ) ==> X }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21005) {G1,W11,D6,L1,V0,M1} { smndt0( smndt0( smndt0( sz00 )
% 7.38/7.79 ) ) ==> sdtasdt0( smndt0( smndt0( smndt0( sz00 ) ) ), sz10 ) }.
% 7.38/7.79 parent0[1]: (21001) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( X, sz10 ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent1[0]: (118) {G3,W5,D5,L1,V0,M1} R(59,3) { aElement0( smndt0( smndt0(
% 7.38/7.79 smndt0( sz00 ) ) ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := smndt0( smndt0( smndt0( sz00 ) ) )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21007) {G2,W10,D5,L1,V0,M1} { smndt0( smndt0( smndt0( sz00 ) ) )
% 7.38/7.79 ==> sdtasdt0( smndt0( smndt0( sz00 ) ), sz10 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 8]: (21005) {G1,W11,D6,L1,V0,M1} { smndt0( smndt0( smndt0( sz00
% 7.38/7.79 ) ) ) ==> sdtasdt0( smndt0( smndt0( smndt0( sz00 ) ) ), sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21019) {G3,W9,D5,L1,V0,M1} { smndt0( smndt0( smndt0( sz00 ) ) )
% 7.38/7.79 ==> sdtasdt0( smndt0( sz00 ), sz10 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 7]: (21007) {G2,W10,D5,L1,V0,M1} { smndt0( smndt0( smndt0( sz00
% 7.38/7.79 ) ) ) ==> sdtasdt0( smndt0( smndt0( sz00 ) ), sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21030) {G4,W8,D5,L1,V0,M1} { smndt0( smndt0( smndt0( sz00 ) ) )
% 7.38/7.79 ==> sdtasdt0( sz00, sz10 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 6]: (21019) {G3,W9,D5,L1,V0,M1} { smndt0( smndt0( smndt0( sz00
% 7.38/7.79 ) ) ) ==> sdtasdt0( smndt0( sz00 ), sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21031) {G4,W7,D4,L1,V0,M1} { smndt0( smndt0( sz00 ) ) ==>
% 7.38/7.79 sdtasdt0( sz00, sz10 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 3]: (21030) {G4,W8,D5,L1,V0,M1} { smndt0( smndt0( smndt0( sz00
% 7.38/7.79 ) ) ) ==> sdtasdt0( sz00, sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21032) {G4,W6,D3,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0( sz00,
% 7.38/7.79 sz10 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 2]: (21031) {G4,W7,D4,L1,V0,M1} { smndt0( smndt0( sz00 ) ) ==>
% 7.38/7.79 sdtasdt0( sz00, sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21033) {G4,W5,D3,L1,V0,M1} { sz00 ==> sdtasdt0( sz00, sz10 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 1]: (21032) {G4,W6,D3,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0(
% 7.38/7.79 sz00, sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21039) {G4,W5,D3,L1,V0,M1} { sdtasdt0( sz00, sz10 ) ==> sz00 }.
% 7.38/7.79 parent0[0]: (21033) {G4,W5,D3,L1,V0,M1} { sz00 ==> sdtasdt0( sz00, sz10 )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (765) {G4,W5,D3,L1,V0,M1} R(14,118);d(349);d(349);d(349) {
% 7.38/7.79 sdtasdt0( sz00, sz10 ) ==> sz00 }.
% 7.38/7.79 parent0: (21039) {G4,W5,D3,L1,V0,M1} { sdtasdt0( sz00, sz10 ) ==> sz00 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21043) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( sz10, X ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent0[1]: (15) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( sz10,
% 7.38/7.79 X ) ==> X }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21046) {G1,W11,D5,L1,V0,M1} { smndt0( sdtasdt0( sz00, sz10 )
% 7.38/7.79 ) ==> sdtasdt0( sz10, smndt0( sdtasdt0( sz00, sz10 ) ) ) }.
% 7.38/7.79 parent0[1]: (21043) {G0,W7,D3,L2,V1,M2} { X ==> sdtasdt0( sz10, X ), !
% 7.38/7.79 aElement0( X ) }.
% 7.38/7.79 parent1[0]: (197) {G3,W5,D4,L1,V0,M1} R(175,3) { aElement0( smndt0(
% 7.38/7.79 sdtasdt0( sz00, sz10 ) ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := smndt0( sdtasdt0( sz00, sz10 ) )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21048) {G2,W9,D4,L1,V0,M1} { smndt0( sdtasdt0( sz00, sz10 ) )
% 7.38/7.79 ==> sdtasdt0( sz10, smndt0( sz00 ) ) }.
% 7.38/7.79 parent0[0]: (765) {G4,W5,D3,L1,V0,M1} R(14,118);d(349);d(349);d(349) {
% 7.38/7.79 sdtasdt0( sz00, sz10 ) ==> sz00 }.
% 7.38/7.79 parent1[0; 8]: (21046) {G1,W11,D5,L1,V0,M1} { smndt0( sdtasdt0( sz00, sz10
% 7.38/7.79 ) ) ==> sdtasdt0( sz10, smndt0( sdtasdt0( sz00, sz10 ) ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21049) {G3,W7,D4,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0( sz10,
% 7.38/7.79 smndt0( sz00 ) ) }.
% 7.38/7.79 parent0[0]: (765) {G4,W5,D3,L1,V0,M1} R(14,118);d(349);d(349);d(349) {
% 7.38/7.79 sdtasdt0( sz00, sz10 ) ==> sz00 }.
% 7.38/7.79 parent1[0; 2]: (21048) {G2,W9,D4,L1,V0,M1} { smndt0( sdtasdt0( sz00, sz10
% 7.38/7.79 ) ) ==> sdtasdt0( sz10, smndt0( sz00 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21053) {G4,W6,D3,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0( sz10,
% 7.38/7.79 sz00 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 5]: (21049) {G3,W7,D4,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0(
% 7.38/7.79 sz10, smndt0( sz00 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21054) {G4,W5,D3,L1,V0,M1} { sz00 ==> sdtasdt0( sz10, sz00 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 1]: (21053) {G4,W6,D3,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0(
% 7.38/7.79 sz10, sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21056) {G4,W5,D3,L1,V0,M1} { sdtasdt0( sz10, sz00 ) ==> sz00 }.
% 7.38/7.79 parent0[0]: (21054) {G4,W5,D3,L1,V0,M1} { sz00 ==> sdtasdt0( sz10, sz00 )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (811) {G5,W5,D3,L1,V0,M1} R(15,197);d(765);d(349) { sdtasdt0(
% 7.38/7.79 sz10, sz00 ) ==> sz00 }.
% 7.38/7.79 parent0: (21056) {G4,W5,D3,L1,V0,M1} { sdtasdt0( sz10, sz00 ) ==> sz00 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21058) {G1,W4,D3,L1,V0,M1} { aElement0( sdtpldt0( sz10, sz10
% 7.38/7.79 ) ) }.
% 7.38/7.79 parent0[0]: (48) {G1,W6,D3,L2,V1,M2} R(4,2) { ! aElement0( X ), aElement0(
% 7.38/7.79 sdtpldt0( sz10, X ) ) }.
% 7.38/7.79 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aElement0( sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sz10
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (937) {G2,W4,D3,L1,V0,M1} R(48,2) { aElement0( sdtpldt0( sz10
% 7.38/7.79 , sz10 ) ) }.
% 7.38/7.79 parent0: (21058) {G1,W4,D3,L1,V0,M1} { aElement0( sdtpldt0( sz10, sz10 ) )
% 7.38/7.79 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21059) {G0,W19,D4,L4,V3,M4} { sdtasdt0( sdtpldt0( X, Z ), Y ) ==>
% 7.38/7.79 sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( Z, Y ) ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Z ) }.
% 7.38/7.79 parent0[3]: (17) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( Z ), sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) ==>
% 7.38/7.79 sdtasdt0( sdtpldt0( Y, Z ), X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := Y
% 7.38/7.79 Y := X
% 7.38/7.79 Z := Z
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21060) {G1,W17,D4,L3,V2,M3} { sdtasdt0( sdtpldt0( X, Y ),
% 7.38/7.79 sz00 ) ==> sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( Y, sz00 ) ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (21059) {G0,W19,D4,L4,V3,M4} { sdtasdt0( sdtpldt0( X, Z ), Y )
% 7.38/7.79 ==> sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( Z, Y ) ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Z ) }.
% 7.38/7.79 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := sz00
% 7.38/7.79 Z := Y
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21065) {G1,W17,D4,L3,V2,M3} { sdtpldt0( sdtasdt0( X, sz00 ),
% 7.38/7.79 sdtasdt0( Y, sz00 ) ) ==> sdtasdt0( sdtpldt0( X, Y ), sz00 ), ! aElement0
% 7.38/7.79 ( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[0]: (21060) {G1,W17,D4,L3,V2,M3} { sdtasdt0( sdtpldt0( X, Y ),
% 7.38/7.79 sz00 ) ==> sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( Y, sz00 ) ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (989) {G1,W17,D4,L3,V2,M3} R(17,1) { ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ), sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( Y, sz00 ) ) ==>
% 7.38/7.79 sdtasdt0( sdtpldt0( X, Y ), sz00 ) }.
% 7.38/7.79 parent0: (21065) {G1,W17,D4,L3,V2,M3} { sdtpldt0( sdtasdt0( X, sz00 ),
% 7.38/7.79 sdtasdt0( Y, sz00 ) ) ==> sdtasdt0( sdtpldt0( X, Y ), sz00 ), ! aElement0
% 7.38/7.79 ( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 2
% 7.38/7.79 1 ==> 0
% 7.38/7.79 2 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21073) {G0,W19,D4,L4,V3,M4} { sdtasdt0( sdtpldt0( X, Z ), Y ) ==>
% 7.38/7.79 sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( Z, Y ) ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Z ) }.
% 7.38/7.79 parent0[3]: (17) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( Z ), sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) ==>
% 7.38/7.79 sdtasdt0( sdtpldt0( Y, Z ), X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := Y
% 7.38/7.79 Y := X
% 7.38/7.79 Z := Z
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21076) {G1,W17,D4,L4,V1,M4} { sdtasdt0( sdtpldt0( X, sz10 ),
% 7.38/7.79 sz00 ) ==> sdtpldt0( sdtasdt0( X, sz00 ), sz00 ), ! aElement0( sz00 ), !
% 7.38/7.79 aElement0( X ), ! aElement0( sz10 ) }.
% 7.38/7.79 parent0[0]: (811) {G5,W5,D3,L1,V0,M1} R(15,197);d(765);d(349) { sdtasdt0(
% 7.38/7.79 sz10, sz00 ) ==> sz00 }.
% 7.38/7.79 parent1[0; 10]: (21073) {G0,W19,D4,L4,V3,M4} { sdtasdt0( sdtpldt0( X, Z )
% 7.38/7.79 , Y ) ==> sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( Z, Y ) ), ! aElement0( Y
% 7.38/7.79 ), ! aElement0( X ), ! aElement0( Z ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := sz00
% 7.38/7.79 Z := sz10
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21103) {G2,W19,D4,L6,V1,M6} { sdtasdt0( sdtpldt0( X, sz10 ),
% 7.38/7.79 sz00 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.79 aElement0( sz00 ), ! aElement0( X ), ! aElement0( sz10 ) }.
% 7.38/7.79 parent0[0]: (269) {G1,W13,D4,L3,V2,M3} R(8,5) { sdtpldt0( sdtasdt0( X, Y )
% 7.38/7.79 , sz00 ) ==> sdtasdt0( X, Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent1[0; 6]: (21076) {G1,W17,D4,L4,V1,M4} { sdtasdt0( sdtpldt0( X, sz10
% 7.38/7.79 ), sz00 ) ==> sdtpldt0( sdtasdt0( X, sz00 ), sz00 ), ! aElement0( sz00 )
% 7.38/7.79 , ! aElement0( X ), ! aElement0( sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := sz00
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (21105) {G2,W17,D4,L5,V1,M5} { sdtasdt0( sdtpldt0( X, sz10 ), sz00
% 7.38/7.79 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.79 aElement0( sz00 ), ! aElement0( sz10 ) }.
% 7.38/7.79 parent0[1, 4]: (21103) {G2,W19,D4,L6,V1,M6} { sdtasdt0( sdtpldt0( X, sz10
% 7.38/7.79 ), sz00 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 )
% 7.38/7.79 , ! aElement0( sz00 ), ! aElement0( X ), ! aElement0( sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (21108) {G2,W15,D4,L4,V1,M4} { sdtasdt0( sdtpldt0( X, sz10 ), sz00
% 7.38/7.79 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.79 aElement0( sz10 ) }.
% 7.38/7.79 parent0[2, 3]: (21105) {G2,W17,D4,L5,V1,M5} { sdtasdt0( sdtpldt0( X, sz10
% 7.38/7.79 ), sz00 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 )
% 7.38/7.79 , ! aElement0( sz00 ), ! aElement0( sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21123) {G1,W13,D4,L3,V1,M3} { sdtasdt0( sdtpldt0( X, sz10 ),
% 7.38/7.79 sz00 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz10 ) }.
% 7.38/7.79 parent0[2]: (21108) {G2,W15,D4,L4,V1,M4} { sdtasdt0( sdtpldt0( X, sz10 ),
% 7.38/7.79 sz00 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.79 aElement0( sz10 ) }.
% 7.38/7.79 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (996) {G6,W13,D4,L3,V1,M3} P(811,17);d(269);r(1) { ! aElement0
% 7.38/7.79 ( X ), ! aElement0( sz10 ), sdtasdt0( sdtpldt0( X, sz10 ), sz00 ) ==>
% 7.38/7.79 sdtasdt0( X, sz00 ) }.
% 7.38/7.79 parent0: (21123) {G1,W13,D4,L3,V1,M3} { sdtasdt0( sdtpldt0( X, sz10 ),
% 7.38/7.79 sz00 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 2
% 7.38/7.79 1 ==> 0
% 7.38/7.79 2 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (21130) {G6,W11,D4,L2,V0,M2} { ! aElement0( sz10 ), sdtasdt0(
% 7.38/7.79 sdtpldt0( sz10, sz10 ), sz00 ) ==> sdtasdt0( sz10, sz00 ) }.
% 7.38/7.79 parent0[0, 1]: (996) {G6,W13,D4,L3,V1,M3} P(811,17);d(269);r(1) { !
% 7.38/7.79 aElement0( X ), ! aElement0( sz10 ), sdtasdt0( sdtpldt0( X, sz10 ), sz00
% 7.38/7.79 ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sz10
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21131) {G6,W9,D4,L2,V0,M2} { sdtasdt0( sdtpldt0( sz10, sz10 ),
% 7.38/7.79 sz00 ) ==> sz00, ! aElement0( sz10 ) }.
% 7.38/7.79 parent0[0]: (811) {G5,W5,D3,L1,V0,M1} R(15,197);d(765);d(349) { sdtasdt0(
% 7.38/7.79 sz10, sz00 ) ==> sz00 }.
% 7.38/7.79 parent1[1; 6]: (21130) {G6,W11,D4,L2,V0,M2} { ! aElement0( sz10 ),
% 7.38/7.79 sdtasdt0( sdtpldt0( sz10, sz10 ), sz00 ) ==> sdtasdt0( sz10, sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21132) {G1,W7,D4,L1,V0,M1} { sdtasdt0( sdtpldt0( sz10, sz10 )
% 7.38/7.79 , sz00 ) ==> sz00 }.
% 7.38/7.79 parent0[1]: (21131) {G6,W9,D4,L2,V0,M2} { sdtasdt0( sdtpldt0( sz10, sz10 )
% 7.38/7.79 , sz00 ) ==> sz00, ! aElement0( sz10 ) }.
% 7.38/7.79 parent1[0]: (2) {G0,W2,D2,L1,V0,M1} I { aElement0( sz10 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (1002) {G7,W7,D4,L1,V0,M1} F(996);d(811);r(2) { sdtasdt0(
% 7.38/7.79 sdtpldt0( sz10, sz10 ), sz00 ) ==> sz00 }.
% 7.38/7.79 parent0: (21132) {G1,W7,D4,L1,V0,M1} { sdtasdt0( sdtpldt0( sz10, sz10 ),
% 7.38/7.79 sz00 ) ==> sz00 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (21135) {G1,W15,D4,L2,V1,M2} { ! aElement0( X ), sdtpldt0(
% 7.38/7.79 sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0( sdtpldt0( X, X )
% 7.38/7.79 , sz00 ) }.
% 7.38/7.79 parent0[0, 1]: (989) {G1,W17,D4,L3,V2,M3} R(17,1) { ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ), sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( Y, sz00 ) ) ==>
% 7.38/7.79 sdtasdt0( sdtpldt0( X, Y ), sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (1008) {G2,W15,D4,L2,V1,M2} F(989) { ! aElement0( X ),
% 7.38/7.79 sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0(
% 7.38/7.79 sdtpldt0( X, X ), sz00 ) }.
% 7.38/7.79 parent0: (21135) {G1,W15,D4,L2,V1,M2} { ! aElement0( X ), sdtpldt0(
% 7.38/7.79 sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0( sdtpldt0( X, X )
% 7.38/7.79 , sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 1 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21137) {G0,W9,D4,L2,V1,M2} { smndt0( X ) ==> sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), X ), ! aElement0( X ) }.
% 7.38/7.79 parent0[1]: (18) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( smndt0
% 7.38/7.79 ( sz10 ), X ) ==> smndt0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21139) {G1,W15,D4,L3,V2,M3} { smndt0( sdtasdt0( X, Y ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ), ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ) }.
% 7.38/7.79 parent0[1]: (21137) {G0,W9,D4,L2,V1,M2} { smndt0( X ) ==> sdtasdt0( smndt0
% 7.38/7.79 ( sz10 ), X ), ! aElement0( X ) }.
% 7.38/7.79 parent1[2]: (5) {G0,W8,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y )
% 7.38/7.79 , aElement0( sdtasdt0( X, Y ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sdtasdt0( X, Y )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21147) {G2,W17,D4,L5,V2,M5} { smndt0( sdtasdt0( X, Y ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[2]: (620) {G2,W15,D4,L3,V2,M3} R(13,42);d(18) { ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ), sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( X ), Y ) }.
% 7.38/7.79 parent1[0; 5]: (21139) {G1,W15,D4,L3,V2,M3} { smndt0( sdtasdt0( X, Y ) )
% 7.38/7.79 ==> sdtasdt0( smndt0( sz10 ), sdtasdt0( X, Y ) ), ! aElement0( X ), !
% 7.38/7.79 aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21148) {G2,W17,D4,L5,V2,M5} { sdtasdt0( smndt0( X ), Y ) ==>
% 7.38/7.79 smndt0( sdtasdt0( X, Y ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[0]: (21147) {G2,W17,D4,L5,V2,M5} { smndt0( sdtasdt0( X, Y ) ) ==>
% 7.38/7.79 sdtasdt0( smndt0( X ), Y ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (21150) {G2,W15,D4,L4,V2,M4} { sdtasdt0( smndt0( X ), Y ) ==>
% 7.38/7.79 smndt0( sdtasdt0( X, Y ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( Y ) }.
% 7.38/7.79 parent0[1, 3]: (21148) {G2,W17,D4,L5,V2,M5} { sdtasdt0( smndt0( X ), Y )
% 7.38/7.79 ==> smndt0( sdtasdt0( X, Y ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 factor: (21152) {G2,W13,D4,L3,V2,M3} { sdtasdt0( smndt0( X ), Y ) ==>
% 7.38/7.79 smndt0( sdtasdt0( X, Y ) ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 parent0[2, 3]: (21150) {G2,W15,D4,L4,V2,M4} { sdtasdt0( smndt0( X ), Y )
% 7.38/7.79 ==> smndt0( sdtasdt0( X, Y ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.79 aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (1115) {G3,W13,D4,L3,V2,M3} R(18,5);d(620) { ! aElement0( X )
% 7.38/7.79 , ! aElement0( Y ), sdtasdt0( smndt0( X ), Y ) ==> smndt0( sdtasdt0( X, Y
% 7.38/7.79 ) ) }.
% 7.38/7.79 parent0: (21152) {G2,W13,D4,L3,V2,M3} { sdtasdt0( smndt0( X ), Y ) ==>
% 7.38/7.79 smndt0( sdtasdt0( X, Y ) ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 Y := Y
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 2
% 7.38/7.79 1 ==> 0
% 7.38/7.79 2 ==> 1
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21159) {G0,W9,D4,L2,V1,M2} { smndt0( X ) ==> sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), X ), ! aElement0( X ) }.
% 7.38/7.79 parent0[1]: (18) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( smndt0
% 7.38/7.79 ( sz10 ), X ) ==> smndt0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21161) {G1,W7,D4,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0(
% 7.38/7.79 smndt0( sz10 ), sz00 ) }.
% 7.38/7.79 parent0[1]: (21159) {G0,W9,D4,L2,V1,M2} { smndt0( X ) ==> sdtasdt0( smndt0
% 7.38/7.79 ( sz10 ), X ), ! aElement0( X ) }.
% 7.38/7.79 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sz00
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21162) {G2,W6,D4,L1,V0,M1} { sz00 ==> sdtasdt0( smndt0( sz10 ),
% 7.38/7.79 sz00 ) }.
% 7.38/7.79 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent1[0; 1]: (21161) {G1,W7,D4,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0(
% 7.38/7.79 smndt0( sz10 ), sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21163) {G2,W6,D4,L1,V0,M1} { sdtasdt0( smndt0( sz10 ), sz00 ) ==>
% 7.38/7.79 sz00 }.
% 7.38/7.79 parent0[0]: (21162) {G2,W6,D4,L1,V0,M1} { sz00 ==> sdtasdt0( smndt0( sz10
% 7.38/7.79 ), sz00 ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 subsumption: (1121) {G4,W6,D4,L1,V0,M1} R(18,1);d(349) { sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), sz00 ) ==> sz00 }.
% 7.38/7.79 parent0: (21163) {G2,W6,D4,L1,V0,M1} { sdtasdt0( smndt0( sz10 ), sz00 )
% 7.38/7.79 ==> sz00 }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 permutation0:
% 7.38/7.79 0 ==> 0
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 eqswap: (21164) {G0,W9,D4,L2,V1,M2} { smndt0( X ) ==> sdtasdt0( X, smndt0
% 7.38/7.79 ( sz10 ) ), ! aElement0( X ) }.
% 7.38/7.79 parent0[1]: (19) {G0,W9,D4,L2,V1,M2} I { ! aElement0( X ), sdtasdt0( X,
% 7.38/7.79 smndt0( sz10 ) ) ==> smndt0( X ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := X
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 resolution: (21167) {G1,W13,D5,L1,V0,M1} { smndt0( sdtasdt0( smndt0( sz10
% 7.38/7.79 ), sz00 ) ) ==> sdtasdt0( sdtasdt0( smndt0( sz10 ), sz00 ), smndt0( sz10
% 7.38/7.79 ) ) }.
% 7.38/7.79 parent0[1]: (21164) {G0,W9,D4,L2,V1,M2} { smndt0( X ) ==> sdtasdt0( X,
% 7.38/7.79 smndt0( sz10 ) ), ! aElement0( X ) }.
% 7.38/7.79 parent1[0]: (377) {G2,W5,D4,L1,V0,M1} R(84,42) { aElement0( sdtasdt0(
% 7.38/7.79 smndt0( sz10 ), sz00 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 X := sdtasdt0( smndt0( sz10 ), sz00 )
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21169) {G2,W10,D5,L1,V0,M1} { smndt0( sdtasdt0( smndt0( sz10 ),
% 7.38/7.79 sz00 ) ) ==> sdtasdt0( sz00, smndt0( sz10 ) ) }.
% 7.38/7.79 parent0[0]: (1121) {G4,W6,D4,L1,V0,M1} R(18,1);d(349) { sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), sz00 ) ==> sz00 }.
% 7.38/7.79 parent1[0; 7]: (21167) {G1,W13,D5,L1,V0,M1} { smndt0( sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), sz00 ) ) ==> sdtasdt0( sdtasdt0( smndt0( sz10 ), sz00 ), smndt0(
% 7.38/7.79 sz10 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.79 substitution1:
% 7.38/7.79 end
% 7.38/7.79
% 7.38/7.79 paramod: (21170) {G3,W7,D4,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0( sz00,
% 7.38/7.79 smndt0( sz10 ) ) }.
% 7.38/7.79 parent0[0]: (1121) {G4,W6,D4,L1,V0,M1} R(18,1);d(349) { sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), sz00 ) ==> sz00 }.
% 7.38/7.79 parent1[0; 2]: (21169) {G2,W10,D5,L1,V0,M1} { smndt0( sdtasdt0( smndt0(
% 7.38/7.79 sz10 ), sz00 ) ) ==> sdtasdt0( sz00, smndt0( sz10 ) ) }.
% 7.38/7.79 substitution0:
% 7.38/7.79 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (21171) {G4,W6,D4,L1,V0,M1} { sz00 ==> sdtasdt0( sz00, smndt0(
% 7.38/7.80 sz10 ) ) }.
% 7.38/7.80 parent0[0]: (349) {G3,W4,D3,L1,V0,M1} R(10,1);d(304) { smndt0( sz00 ) ==>
% 7.38/7.80 sz00 }.
% 7.38/7.80 parent1[0; 1]: (21170) {G3,W7,D4,L1,V0,M1} { smndt0( sz00 ) ==> sdtasdt0(
% 7.38/7.80 sz00, smndt0( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 eqswap: (21172) {G4,W6,D4,L1,V0,M1} { sdtasdt0( sz00, smndt0( sz10 ) ) ==>
% 7.38/7.80 sz00 }.
% 7.38/7.80 parent0[0]: (21171) {G4,W6,D4,L1,V0,M1} { sz00 ==> sdtasdt0( sz00, smndt0
% 7.38/7.80 ( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (1264) {G5,W6,D4,L1,V0,M1} R(19,377);d(1121);d(349) { sdtasdt0
% 7.38/7.80 ( sz00, smndt0( sz10 ) ) ==> sz00 }.
% 7.38/7.80 parent0: (21172) {G4,W6,D4,L1,V0,M1} { sdtasdt0( sz00, smndt0( sz10 ) )
% 7.38/7.80 ==> sz00 }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 0
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 eqswap: (21173) {G0,W10,D3,L2,V0,M2} { ! sz00 ==> sdtasdt0( xx, sz00 ), !
% 7.38/7.80 sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.80 parent0[0]: (21) {G0,W10,D3,L2,V0,M2} I { ! sdtasdt0( xx, sz00 ) ==> sz00,
% 7.38/7.80 ! sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (21176) {G1,W14,D3,L4,V0,M4} { ! sz00 ==> sdtasdt0( sz00, xx ), !
% 7.38/7.80 aElement0( xx ), ! aElement0( sz00 ), ! sdtasdt0( sz00, xx ) ==> sz00
% 7.38/7.80 }.
% 7.38/7.80 parent0[2]: (12) {G0,W11,D3,L3,V2,M3} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.80 ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 7.38/7.80 parent1[0; 3]: (21173) {G0,W10,D3,L2,V0,M2} { ! sz00 ==> sdtasdt0( xx,
% 7.38/7.80 sz00 ), ! sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := xx
% 7.38/7.80 Y := sz00
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 resolution: (21256) {G1,W12,D3,L3,V0,M3} { ! sz00 ==> sdtasdt0( sz00, xx )
% 7.38/7.80 , ! aElement0( sz00 ), ! sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.80 parent0[1]: (21176) {G1,W14,D3,L4,V0,M4} { ! sz00 ==> sdtasdt0( sz00, xx )
% 7.38/7.80 , ! aElement0( xx ), ! aElement0( sz00 ), ! sdtasdt0( sz00, xx ) ==> sz00
% 7.38/7.80 }.
% 7.38/7.80 parent1[0]: (20) {G0,W2,D2,L1,V0,M1} I { aElement0( xx ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 eqswap: (21257) {G1,W12,D3,L3,V0,M3} { ! sdtasdt0( sz00, xx ) ==> sz00, !
% 7.38/7.80 aElement0( sz00 ), ! sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.80 parent0[0]: (21256) {G1,W12,D3,L3,V0,M3} { ! sz00 ==> sdtasdt0( sz00, xx )
% 7.38/7.80 , ! aElement0( sz00 ), ! sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (21259) {G1,W7,D3,L2,V0,M2} { ! sdtasdt0( sz00, xx ) ==> sz00, !
% 7.38/7.80 aElement0( sz00 ) }.
% 7.38/7.80 parent0[0, 2]: (21257) {G1,W12,D3,L3,V0,M3} { ! sdtasdt0( sz00, xx ) ==>
% 7.38/7.80 sz00, ! aElement0( sz00 ), ! sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (1455) {G1,W7,D3,L2,V0,M2} P(12,21);f;r(20) { ! sdtasdt0( sz00
% 7.38/7.80 , xx ) ==> sz00, ! aElement0( sz00 ) }.
% 7.38/7.80 parent0: (21259) {G1,W7,D3,L2,V0,M2} { ! sdtasdt0( sz00, xx ) ==> sz00, !
% 7.38/7.80 aElement0( sz00 ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 0
% 7.38/7.80 1 ==> 1
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 eqswap: (21262) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z ) ==>
% 7.38/7.80 sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aElement0( X ), ! aElement0( Y ), !
% 7.38/7.80 aElement0( Z ) }.
% 7.38/7.80 parent0[3]: (13) {G0,W17,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.38/7.80 ), ! aElement0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) ==> sdtasdt0(
% 7.38/7.80 sdtasdt0( X, Y ), Z ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 Y := Y
% 7.38/7.80 Z := Z
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (21266) {G1,W17,D4,L4,V1,M4} { sdtasdt0( sdtasdt0( X, sz00 ),
% 7.38/7.80 smndt0( sz10 ) ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0(
% 7.38/7.80 sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 parent0[0]: (1264) {G5,W6,D4,L1,V0,M1} R(19,377);d(1121);d(349) { sdtasdt0
% 7.38/7.80 ( sz00, smndt0( sz10 ) ) ==> sz00 }.
% 7.38/7.80 parent1[0; 9]: (21262) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ),
% 7.38/7.80 Z ) ==> sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aElement0( X ), ! aElement0( Y
% 7.38/7.80 ), ! aElement0( Z ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 X := X
% 7.38/7.80 Y := sz00
% 7.38/7.80 Z := smndt0( sz10 )
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (21832) {G2,W19,D4,L6,V1,M6} { sdtasdt0( smndt0( X ), sz00 ) ==>
% 7.38/7.80 sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0(
% 7.38/7.80 X ), ! aElement0( sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 parent0[2]: (622) {G3,W15,D4,L3,V2,M3} R(13,42);d(19);d(621) { ! aElement0
% 7.38/7.80 ( X ), ! aElement0( Y ), sdtasdt0( sdtasdt0( X, Y ), smndt0( sz10 ) ) ==>
% 7.38/7.80 sdtasdt0( smndt0( X ), Y ) }.
% 7.38/7.80 parent1[0; 1]: (21266) {G1,W17,D4,L4,V1,M4} { sdtasdt0( sdtasdt0( X, sz00
% 7.38/7.80 ), smndt0( sz10 ) ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), !
% 7.38/7.80 aElement0( sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 Y := sz00
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (21834) {G2,W17,D4,L5,V1,M5} { sdtasdt0( smndt0( X ), sz00 ) ==>
% 7.38/7.80 sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0(
% 7.38/7.80 sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 parent0[1, 3]: (21832) {G2,W19,D4,L6,V1,M6} { sdtasdt0( smndt0( X ), sz00
% 7.38/7.80 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.80 aElement0( X ), ! aElement0( sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (21837) {G2,W15,D4,L4,V1,M4} { sdtasdt0( smndt0( X ), sz00 ) ==>
% 7.38/7.80 sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0(
% 7.38/7.80 smndt0( sz10 ) ) }.
% 7.38/7.80 parent0[2, 3]: (21834) {G2,W17,D4,L5,V1,M5} { sdtasdt0( smndt0( X ), sz00
% 7.38/7.80 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.80 aElement0( sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22157) {G3,W19,D4,L6,V1,M6} { smndt0( sdtasdt0( X, sz00 ) ) ==>
% 7.38/7.80 sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0(
% 7.38/7.80 X ), ! aElement0( sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 parent0[2]: (1115) {G3,W13,D4,L3,V2,M3} R(18,5);d(620) { ! aElement0( X ),
% 7.38/7.80 ! aElement0( Y ), sdtasdt0( smndt0( X ), Y ) ==> smndt0( sdtasdt0( X, Y )
% 7.38/7.80 ) }.
% 7.38/7.80 parent1[0; 1]: (21837) {G2,W15,D4,L4,V1,M4} { sdtasdt0( smndt0( X ), sz00
% 7.38/7.80 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.80 aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 Y := sz00
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22159) {G3,W17,D4,L5,V1,M5} { smndt0( sdtasdt0( X, sz00 ) ) ==>
% 7.38/7.80 sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0(
% 7.38/7.80 sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 parent0[1, 3]: (22157) {G3,W19,D4,L6,V1,M6} { smndt0( sdtasdt0( X, sz00 )
% 7.38/7.80 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.80 aElement0( X ), ! aElement0( sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22162) {G3,W15,D4,L4,V1,M4} { smndt0( sdtasdt0( X, sz00 ) ) ==>
% 7.38/7.80 sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0(
% 7.38/7.80 smndt0( sz10 ) ) }.
% 7.38/7.80 parent0[2, 3]: (22159) {G3,W17,D4,L5,V1,M5} { smndt0( sdtasdt0( X, sz00 )
% 7.38/7.80 ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.80 aElement0( sz00 ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 resolution: (22177) {G1,W13,D4,L3,V1,M3} { smndt0( sdtasdt0( X, sz00 ) )
% 7.38/7.80 ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( smndt0( sz10 ) )
% 7.38/7.80 }.
% 7.38/7.80 parent0[2]: (22162) {G3,W15,D4,L4,V1,M4} { smndt0( sdtasdt0( X, sz00 ) )
% 7.38/7.80 ==> sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( sz00 ), !
% 7.38/7.80 aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (2022) {G6,W13,D4,L3,V1,M3} P(1264,13);d(622);d(1115);r(1) { !
% 7.38/7.80 aElement0( X ), ! aElement0( smndt0( sz10 ) ), smndt0( sdtasdt0( X, sz00
% 7.38/7.80 ) ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.80 parent0: (22177) {G1,W13,D4,L3,V1,M3} { smndt0( sdtasdt0( X, sz00 ) ) ==>
% 7.38/7.80 sdtasdt0( X, sz00 ), ! aElement0( X ), ! aElement0( smndt0( sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 2
% 7.38/7.80 1 ==> 0
% 7.38/7.80 2 ==> 1
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 eqswap: (22181) {G1,W17,D4,L3,V2,M3} { sdtasdt0( X, sdtpldt0( Y, Y ) ) ==>
% 7.38/7.80 sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Y ) ), ! aElement0( X ), !
% 7.38/7.80 aElement0( Y ) }.
% 7.38/7.80 parent0[2]: (34) {G1,W17,D4,L3,V2,M3} F(16) { ! aElement0( X ), ! aElement0
% 7.38/7.80 ( Y ), sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Y ) ) ==> sdtasdt0( X,
% 7.38/7.80 sdtpldt0( Y, Y ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 Y := Y
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 resolution: (22185) {G1,W15,D4,L2,V1,M2} { sdtasdt0( X, sdtpldt0( sz00,
% 7.38/7.80 sz00 ) ) ==> sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ), !
% 7.38/7.80 aElement0( X ) }.
% 7.38/7.80 parent0[2]: (22181) {G1,W17,D4,L3,V2,M3} { sdtasdt0( X, sdtpldt0( Y, Y ) )
% 7.38/7.80 ==> sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Y ) ), ! aElement0( X ), !
% 7.38/7.80 aElement0( Y ) }.
% 7.38/7.80 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 Y := sz00
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22186) {G2,W15,D4,L3,V1,M3} { sdtasdt0( X, sdtpldt0( sz00, sz00
% 7.38/7.80 ) ) ==> sdtasdt0( sdtpldt0( X, X ), sz00 ), ! aElement0( X ), !
% 7.38/7.80 aElement0( X ) }.
% 7.38/7.80 parent0[1]: (1008) {G2,W15,D4,L2,V1,M2} F(989) { ! aElement0( X ), sdtpldt0
% 7.38/7.80 ( sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0( sdtpldt0( X, X
% 7.38/7.80 ), sz00 ) }.
% 7.38/7.80 parent1[0; 6]: (22185) {G1,W15,D4,L2,V1,M2} { sdtasdt0( X, sdtpldt0( sz00
% 7.38/7.80 , sz00 ) ) ==> sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ), !
% 7.38/7.80 aElement0( X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22187) {G2,W13,D4,L2,V1,M2} { sdtasdt0( X, sdtpldt0( sz00, sz00 )
% 7.38/7.80 ) ==> sdtasdt0( sdtpldt0( X, X ), sz00 ), ! aElement0( X ) }.
% 7.38/7.80 parent0[1, 2]: (22186) {G2,W15,D4,L3,V1,M3} { sdtasdt0( X, sdtpldt0( sz00
% 7.38/7.80 , sz00 ) ) ==> sdtasdt0( sdtpldt0( X, X ), sz00 ), ! aElement0( X ), !
% 7.38/7.80 aElement0( X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22188) {G2,W11,D4,L2,V1,M2} { sdtasdt0( X, sz00 ) ==> sdtasdt0(
% 7.38/7.80 sdtpldt0( X, X ), sz00 ), ! aElement0( X ) }.
% 7.38/7.80 parent0[0]: (275) {G1,W5,D3,L1,V0,M1} R(8,1) { sdtpldt0( sz00, sz00 ) ==>
% 7.38/7.80 sz00 }.
% 7.38/7.80 parent1[0; 3]: (22187) {G2,W13,D4,L2,V1,M2} { sdtasdt0( X, sdtpldt0( sz00
% 7.38/7.80 , sz00 ) ) ==> sdtasdt0( sdtpldt0( X, X ), sz00 ), ! aElement0( X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 eqswap: (22189) {G2,W11,D4,L2,V1,M2} { sdtasdt0( sdtpldt0( X, X ), sz00 )
% 7.38/7.80 ==> sdtasdt0( X, sz00 ), ! aElement0( X ) }.
% 7.38/7.80 parent0[0]: (22188) {G2,W11,D4,L2,V1,M2} { sdtasdt0( X, sz00 ) ==>
% 7.38/7.80 sdtasdt0( sdtpldt0( X, X ), sz00 ), ! aElement0( X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (2453) {G3,W11,D4,L2,V1,M2} R(34,1);d(1008);d(275) { !
% 7.38/7.80 aElement0( X ), sdtasdt0( sdtpldt0( X, X ), sz00 ) ==> sdtasdt0( X, sz00
% 7.38/7.80 ) }.
% 7.38/7.80 parent0: (22189) {G2,W11,D4,L2,V1,M2} { sdtasdt0( sdtpldt0( X, X ), sz00 )
% 7.38/7.80 ==> sdtasdt0( X, sz00 ), ! aElement0( X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 1
% 7.38/7.80 1 ==> 0
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 resolution: (22191) {G1,W5,D3,L1,V0,M1} { ! sdtasdt0( sz00, xx ) ==> sz00
% 7.38/7.80 }.
% 7.38/7.80 parent0[1]: (1455) {G1,W7,D3,L2,V0,M2} P(12,21);f;r(20) { ! sdtasdt0( sz00
% 7.38/7.80 , xx ) ==> sz00, ! aElement0( sz00 ) }.
% 7.38/7.80 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (7533) {G2,W5,D3,L1,V0,M1} S(1455);r(1) { ! sdtasdt0( sz00, xx
% 7.38/7.80 ) ==> sz00 }.
% 7.38/7.80 parent0: (22191) {G1,W5,D3,L1,V0,M1} { ! sdtasdt0( sz00, xx ) ==> sz00 }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 0
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 eqswap: (22194) {G1,W17,D4,L3,V2,M3} { sdtasdt0( sdtpldt0( X, Y ), Y ) ==>
% 7.38/7.80 sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( Y, Y ) ), ! aElement0( Y ), !
% 7.38/7.80 aElement0( X ) }.
% 7.38/7.80 parent0[2]: (37) {G1,W17,D4,L3,V2,M3} F(17) { ! aElement0( X ), ! aElement0
% 7.38/7.80 ( Y ), sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( X, X ) ) ==> sdtasdt0(
% 7.38/7.80 sdtpldt0( Y, X ), X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := Y
% 7.38/7.80 Y := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22199) {G2,W19,D5,L3,V0,M3} { sdtasdt0( sdtpldt0( sdtpldt0( sz10
% 7.38/7.80 , sz10 ), sz00 ), sz00 ) ==> sdtpldt0( sz00, sdtasdt0( sz00, sz00 ) ), !
% 7.38/7.80 aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 parent0[0]: (1002) {G7,W7,D4,L1,V0,M1} F(996);d(811);r(2) { sdtasdt0(
% 7.38/7.80 sdtpldt0( sz10, sz10 ), sz00 ) ==> sz00 }.
% 7.38/7.80 parent1[0; 9]: (22194) {G1,W17,D4,L3,V2,M3} { sdtasdt0( sdtpldt0( X, Y ),
% 7.38/7.80 Y ) ==> sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( Y, Y ) ), ! aElement0( Y )
% 7.38/7.80 , ! aElement0( X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 X := sdtpldt0( sz10, sz10 )
% 7.38/7.80 Y := sz00
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22200) {G3,W23,D5,L5,V0,M5} { sdtasdt0( sdtpldt0( sdtpldt0( sz10
% 7.38/7.80 , sz10 ), sz00 ), sz00 ) ==> sdtpldt0( sdtasdt0( sz00, sz00 ), sz00 ), !
% 7.38/7.80 aElement0( sz00 ), ! aElement0( sz00 ), ! aElement0( sz00 ), ! aElement0
% 7.38/7.80 ( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 parent0[1]: (145) {G2,W15,D4,L3,V2,M3} F(133) { ! aElement0( X ), sdtpldt0
% 7.38/7.80 ( X, sdtasdt0( X, Y ) ) ==> sdtpldt0( sdtasdt0( X, Y ), X ), ! aElement0
% 7.38/7.80 ( Y ) }.
% 7.38/7.80 parent1[0; 8]: (22199) {G2,W19,D5,L3,V0,M3} { sdtasdt0( sdtpldt0( sdtpldt0
% 7.38/7.80 ( sz10, sz10 ), sz00 ), sz00 ) ==> sdtpldt0( sz00, sdtasdt0( sz00, sz00 )
% 7.38/7.80 ), ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := sz00
% 7.38/7.80 Y := sz00
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22201) {G3,W21,D5,L4,V0,M4} { sdtasdt0( sdtpldt0( sdtpldt0( sz10
% 7.38/7.80 , sz10 ), sz00 ), sz00 ) ==> sdtpldt0( sdtasdt0( sz00, sz00 ), sz00 ), !
% 7.38/7.80 aElement0( sz00 ), ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10
% 7.38/7.80 ) ) }.
% 7.38/7.80 parent0[1, 2]: (22200) {G3,W23,D5,L5,V0,M5} { sdtasdt0( sdtpldt0( sdtpldt0
% 7.38/7.80 ( sz10, sz10 ), sz00 ), sz00 ) ==> sdtpldt0( sdtasdt0( sz00, sz00 ), sz00
% 7.38/7.80 ), ! aElement0( sz00 ), ! aElement0( sz00 ), ! aElement0( sz00 ), !
% 7.38/7.80 aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22202) {G3,W19,D5,L3,V0,M3} { sdtasdt0( sdtpldt0( sdtpldt0( sz10
% 7.38/7.80 , sz10 ), sz00 ), sz00 ) ==> sdtpldt0( sdtasdt0( sz00, sz00 ), sz00 ), !
% 7.38/7.80 aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 parent0[1, 2]: (22201) {G3,W21,D5,L4,V0,M4} { sdtasdt0( sdtpldt0( sdtpldt0
% 7.38/7.80 ( sz10, sz10 ), sz00 ), sz00 ) ==> sdtpldt0( sdtasdt0( sz00, sz00 ), sz00
% 7.38/7.80 ), ! aElement0( sz00 ), ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10
% 7.38/7.80 , sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22203) {G2,W21,D5,L5,V0,M5} { sdtasdt0( sdtpldt0( sdtpldt0( sz10
% 7.38/7.80 , sz10 ), sz00 ), sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0( sz00 )
% 7.38/7.80 , ! aElement0( sz00 ), ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10,
% 7.38/7.80 sz10 ) ) }.
% 7.38/7.80 parent0[0]: (269) {G1,W13,D4,L3,V2,M3} R(8,5) { sdtpldt0( sdtasdt0( X, Y )
% 7.38/7.80 , sz00 ) ==> sdtasdt0( X, Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.38/7.80 parent1[0; 8]: (22202) {G3,W19,D5,L3,V0,M3} { sdtasdt0( sdtpldt0( sdtpldt0
% 7.38/7.80 ( sz10, sz10 ), sz00 ), sz00 ) ==> sdtpldt0( sdtasdt0( sz00, sz00 ), sz00
% 7.38/7.80 ), ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := sz00
% 7.38/7.80 Y := sz00
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22204) {G2,W19,D5,L4,V0,M4} { sdtasdt0( sdtpldt0( sdtpldt0( sz10
% 7.38/7.80 , sz10 ), sz00 ), sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0( sz00 )
% 7.38/7.80 , ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 parent0[1, 2]: (22203) {G2,W21,D5,L5,V0,M5} { sdtasdt0( sdtpldt0( sdtpldt0
% 7.38/7.80 ( sz10, sz10 ), sz00 ), sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0(
% 7.38/7.80 sz00 ), ! aElement0( sz00 ), ! aElement0( sz00 ), ! aElement0( sdtpldt0(
% 7.38/7.80 sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22205) {G2,W17,D5,L3,V0,M3} { sdtasdt0( sdtpldt0( sdtpldt0( sz10
% 7.38/7.80 , sz10 ), sz00 ), sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0( sz00 )
% 7.38/7.80 , ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 parent0[1, 2]: (22204) {G2,W19,D5,L4,V0,M4} { sdtasdt0( sdtpldt0( sdtpldt0
% 7.38/7.80 ( sz10, sz10 ), sz00 ), sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0(
% 7.38/7.80 sz00 ), ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22206) {G1,W19,D4,L4,V0,M4} { sdtasdt0( sdtpldt0( sz10, sz10 ),
% 7.38/7.80 sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) )
% 7.38/7.80 , ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 parent0[1]: (8) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( X, sz00
% 7.38/7.80 ) ==> X }.
% 7.38/7.80 parent1[0; 2]: (22205) {G2,W17,D5,L3,V0,M3} { sdtasdt0( sdtpldt0( sdtpldt0
% 7.38/7.80 ( sz10, sz10 ), sz00 ), sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0(
% 7.38/7.80 sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := sdtpldt0( sz10, sz10 )
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22207) {G1,W15,D4,L3,V0,M3} { sdtasdt0( sdtpldt0( sz10, sz10 ),
% 7.38/7.80 sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) )
% 7.38/7.80 , ! aElement0( sz00 ) }.
% 7.38/7.80 parent0[1, 3]: (22206) {G1,W19,D4,L4,V0,M4} { sdtasdt0( sdtpldt0( sz10,
% 7.38/7.80 sz10 ), sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0( sdtpldt0( sz10,
% 7.38/7.80 sz10 ) ), ! aElement0( sz00 ), ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22208) {G2,W11,D3,L3,V0,M3} { sz00 ==> sdtasdt0( sz00, sz00 ), !
% 7.38/7.80 aElement0( sdtpldt0( sz10, sz10 ) ), ! aElement0( sz00 ) }.
% 7.38/7.80 parent0[0]: (1002) {G7,W7,D4,L1,V0,M1} F(996);d(811);r(2) { sdtasdt0(
% 7.38/7.80 sdtpldt0( sz10, sz10 ), sz00 ) ==> sz00 }.
% 7.38/7.80 parent1[0; 1]: (22207) {G1,W15,D4,L3,V0,M3} { sdtasdt0( sdtpldt0( sz10,
% 7.38/7.80 sz10 ), sz00 ) ==> sdtasdt0( sz00, sz00 ), ! aElement0( sdtpldt0( sz10,
% 7.38/7.80 sz10 ) ), ! aElement0( sz00 ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 resolution: (22209) {G1,W9,D3,L2,V0,M2} { sz00 ==> sdtasdt0( sz00, sz00 )
% 7.38/7.80 , ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 parent0[2]: (22208) {G2,W11,D3,L3,V0,M3} { sz00 ==> sdtasdt0( sz00, sz00 )
% 7.38/7.80 , ! aElement0( sdtpldt0( sz10, sz10 ) ), ! aElement0( sz00 ) }.
% 7.38/7.80 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 eqswap: (22210) {G1,W9,D3,L2,V0,M2} { sdtasdt0( sz00, sz00 ) ==> sz00, !
% 7.38/7.80 aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 parent0[0]: (22209) {G1,W9,D3,L2,V0,M2} { sz00 ==> sdtasdt0( sz00, sz00 )
% 7.38/7.80 , ! aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (17532) {G8,W9,D3,L2,V0,M2} P(1002,37);d(145);d(269);d(8);d(
% 7.38/7.80 1002);r(1) { ! aElement0( sdtpldt0( sz10, sz10 ) ), sdtasdt0( sz00, sz00
% 7.38/7.80 ) ==> sz00 }.
% 7.38/7.80 parent0: (22210) {G1,W9,D3,L2,V0,M2} { sdtasdt0( sz00, sz00 ) ==> sz00, !
% 7.38/7.80 aElement0( sdtpldt0( sz10, sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 1
% 7.38/7.80 1 ==> 0
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 resolution: (22212) {G3,W5,D3,L1,V0,M1} { sdtasdt0( sz00, sz00 ) ==> sz00
% 7.38/7.80 }.
% 7.38/7.80 parent0[0]: (17532) {G8,W9,D3,L2,V0,M2} P(1002,37);d(145);d(269);d(8);d(
% 7.38/7.80 1002);r(1) { ! aElement0( sdtpldt0( sz10, sz10 ) ), sdtasdt0( sz00, sz00
% 7.38/7.80 ) ==> sz00 }.
% 7.38/7.80 parent1[0]: (937) {G2,W4,D3,L1,V0,M1} R(48,2) { aElement0( sdtpldt0( sz10,
% 7.38/7.80 sz10 ) ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (20048) {G9,W5,D3,L1,V0,M1} S(17532);r(937) { sdtasdt0( sz00,
% 7.38/7.80 sz00 ) ==> sz00 }.
% 7.38/7.80 parent0: (22212) {G3,W5,D3,L1,V0,M1} { sdtasdt0( sz00, sz00 ) ==> sz00 }.
% 7.38/7.80 substitution0:
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 0
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 resolution: (22219) {G2,W10,D4,L2,V1,M2} { ! aElement0( X ), smndt0(
% 7.38/7.80 sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.80 parent0[1]: (2022) {G6,W13,D4,L3,V1,M3} P(1264,13);d(622);d(1115);r(1) { !
% 7.38/7.80 aElement0( X ), ! aElement0( smndt0( sz10 ) ), smndt0( sdtasdt0( X, sz00
% 7.38/7.80 ) ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.80 parent1[0]: (42) {G1,W3,D3,L1,V0,M1} R(3,2) { aElement0( smndt0( sz10 ) )
% 7.38/7.80 }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (20057) {G7,W10,D4,L2,V1,M2} S(2022);r(42) { ! aElement0( X )
% 7.38/7.80 , smndt0( sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.80 parent0: (22219) {G2,W10,D4,L2,V1,M2} { ! aElement0( X ), smndt0( sdtasdt0
% 7.38/7.80 ( X, sz00 ) ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 0
% 7.38/7.80 1 ==> 1
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22223) {G3,W15,D4,L3,V1,M3} { sdtpldt0( sdtasdt0( X, sz00 ),
% 7.38/7.80 sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), !
% 7.38/7.80 aElement0( X ) }.
% 7.38/7.80 parent0[1]: (2453) {G3,W11,D4,L2,V1,M2} R(34,1);d(1008);d(275) { !
% 7.38/7.80 aElement0( X ), sdtasdt0( sdtpldt0( X, X ), sz00 ) ==> sdtasdt0( X, sz00
% 7.38/7.80 ) }.
% 7.38/7.80 parent1[1; 8]: (1008) {G2,W15,D4,L2,V1,M2} F(989) { ! aElement0( X ),
% 7.38/7.80 sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0(
% 7.38/7.80 sdtpldt0( X, X ), sz00 ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80 substitution1:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 factor: (22226) {G3,W13,D4,L2,V1,M2} { sdtpldt0( sdtasdt0( X, sz00 ),
% 7.38/7.80 sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ) }.
% 7.38/7.80 parent0[1, 2]: (22223) {G3,W15,D4,L3,V1,M3} { sdtpldt0( sdtasdt0( X, sz00
% 7.38/7.80 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ), !
% 7.38/7.80 aElement0( X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 subsumption: (20062) {G4,W13,D4,L2,V1,M2} S(1008);d(2453) { ! aElement0( X
% 7.38/7.80 ), sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X
% 7.38/7.80 , sz00 ) }.
% 7.38/7.80 parent0: (22226) {G3,W13,D4,L2,V1,M2} { sdtpldt0( sdtasdt0( X, sz00 ),
% 7.38/7.80 sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ), ! aElement0( X ) }.
% 7.38/7.80 substitution0:
% 7.38/7.80 X := X
% 7.38/7.80 end
% 7.38/7.80 permutation0:
% 7.38/7.80 0 ==> 1
% 7.38/7.80 1 ==> 0
% 7.38/7.80 end
% 7.38/7.80
% 7.38/7.80 paramod: (22230) {G3,W13,D4,L3,V1,M3} { sdtpldt0( sdtasdt0( X, sz00 ),
% 7.38/7.80 sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X ), ! aElement0( X ) }.
% 7.38/7.80 parent0[1]: (20057) {G7,W10,D4,L2,V1,M2} S(2022);r(42) { ! aElement0( X ),
% 7.38/7.80 smndt0( sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X, sz00 ) }.
% 7.38/7.80 parent1[0; 2]: (416) {G2,W12,D5,L2,V1,M2} R(11,84) { sdtpldt0( smndt0(
% 7.38/7.80 sdtasdt0( X, sz00 ) ), sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X )
% 7.45/7.83 }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (22231) {G3,W11,D4,L2,V1,M2} { sdtpldt0( sdtasdt0( X, sz00 ),
% 7.45/7.83 sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X ) }.
% 7.45/7.83 parent0[1, 2]: (22230) {G3,W13,D4,L3,V1,M3} { sdtpldt0( sdtasdt0( X, sz00
% 7.45/7.83 ), sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X ), ! aElement0( X )
% 7.45/7.83 }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 paramod: (22232) {G4,W9,D3,L3,V1,M3} { sdtasdt0( X, sz00 ) ==> sz00, !
% 7.45/7.83 aElement0( X ), ! aElement0( X ) }.
% 7.45/7.83 parent0[1]: (20062) {G4,W13,D4,L2,V1,M2} S(1008);d(2453) { ! aElement0( X )
% 7.45/7.83 , sdtpldt0( sdtasdt0( X, sz00 ), sdtasdt0( X, sz00 ) ) ==> sdtasdt0( X,
% 7.45/7.83 sz00 ) }.
% 7.45/7.83 parent1[0; 1]: (22231) {G3,W11,D4,L2,V1,M2} { sdtpldt0( sdtasdt0( X, sz00
% 7.45/7.83 ), sdtasdt0( X, sz00 ) ) ==> sz00, ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (22235) {G4,W7,D3,L2,V1,M2} { sdtasdt0( X, sz00 ) ==> sz00, !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 parent0[1, 2]: (22232) {G4,W9,D3,L3,V1,M3} { sdtasdt0( X, sz00 ) ==> sz00
% 7.45/7.83 , ! aElement0( X ), ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 subsumption: (20086) {G8,W7,D3,L2,V1,M2} S(416);d(20057);d(20062) { !
% 7.45/7.83 aElement0( X ), sdtasdt0( X, sz00 ) ==> sz00 }.
% 7.45/7.83 parent0: (22235) {G4,W7,D3,L2,V1,M2} { sdtasdt0( X, sz00 ) ==> sz00, !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83 permutation0:
% 7.45/7.83 0 ==> 1
% 7.45/7.83 1 ==> 0
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 eqswap: (22237) {G0,W19,D4,L4,V3,M4} { sdtasdt0( X, sdtpldt0( Y, Z ) ) ==>
% 7.45/7.83 sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), ! aElement0( X ), !
% 7.45/7.83 aElement0( Y ), ! aElement0( Z ) }.
% 7.45/7.83 parent0[3]: (16) {G0,W19,D4,L4,V3,M4} I { ! aElement0( X ), ! aElement0( Y
% 7.45/7.83 ), ! aElement0( Z ), sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) ==>
% 7.45/7.83 sdtasdt0( X, sdtpldt0( Y, Z ) ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 Y := Y
% 7.45/7.83 Z := Z
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 paramod: (22243) {G1,W17,D4,L4,V1,M4} { sdtasdt0( sz00, sdtpldt0( sz00, X
% 7.45/7.83 ) ) ==> sdtpldt0( sz00, sdtasdt0( sz00, X ) ), ! aElement0( sz00 ), !
% 7.45/7.83 aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 parent0[0]: (20048) {G9,W5,D3,L1,V0,M1} S(17532);r(937) { sdtasdt0( sz00,
% 7.45/7.83 sz00 ) ==> sz00 }.
% 7.45/7.83 parent1[0; 7]: (22237) {G0,W19,D4,L4,V3,M4} { sdtasdt0( X, sdtpldt0( Y, Z
% 7.45/7.83 ) ) ==> sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), ! aElement0( X )
% 7.45/7.83 , ! aElement0( Y ), ! aElement0( Z ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := sz00
% 7.45/7.83 Y := sz00
% 7.45/7.83 Z := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 paramod: (22250) {G2,W21,D4,L6,V1,M6} { sdtasdt0( sz00, sdtpldt0( sz00, X
% 7.45/7.83 ) ) ==> sdtpldt0( sdtasdt0( sz00, X ), sz00 ), ! aElement0( sz00 ), !
% 7.45/7.83 aElement0( X ), ! aElement0( sz00 ), ! aElement0( sz00 ), ! aElement0( X
% 7.45/7.83 ) }.
% 7.45/7.83 parent0[1]: (145) {G2,W15,D4,L3,V2,M3} F(133) { ! aElement0( X ), sdtpldt0
% 7.45/7.83 ( X, sdtasdt0( X, Y ) ) ==> sdtpldt0( sdtasdt0( X, Y ), X ), ! aElement0
% 7.45/7.83 ( Y ) }.
% 7.45/7.83 parent1[0; 6]: (22243) {G1,W17,D4,L4,V1,M4} { sdtasdt0( sz00, sdtpldt0(
% 7.45/7.83 sz00, X ) ) ==> sdtpldt0( sz00, sdtasdt0( sz00, X ) ), ! aElement0( sz00
% 7.45/7.83 ), ! aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := sz00
% 7.45/7.83 Y := X
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (22252) {G2,W19,D4,L5,V1,M5} { sdtasdt0( sz00, sdtpldt0( sz00, X )
% 7.45/7.83 ) ==> sdtpldt0( sdtasdt0( sz00, X ), sz00 ), ! aElement0( sz00 ), !
% 7.45/7.83 aElement0( X ), ! aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 parent0[1, 3]: (22250) {G2,W21,D4,L6,V1,M6} { sdtasdt0( sz00, sdtpldt0(
% 7.45/7.83 sz00, X ) ) ==> sdtpldt0( sdtasdt0( sz00, X ), sz00 ), ! aElement0( sz00
% 7.45/7.83 ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0( sz00 ), !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (22254) {G2,W17,D4,L4,V1,M4} { sdtasdt0( sz00, sdtpldt0( sz00, X )
% 7.45/7.83 ) ==> sdtpldt0( sdtasdt0( sz00, X ), sz00 ), ! aElement0( sz00 ), !
% 7.45/7.83 aElement0( X ), ! aElement0( X ) }.
% 7.45/7.83 parent0[1, 3]: (22252) {G2,W19,D4,L5,V1,M5} { sdtasdt0( sz00, sdtpldt0(
% 7.45/7.83 sz00, X ) ) ==> sdtpldt0( sdtasdt0( sz00, X ), sz00 ), ! aElement0( sz00
% 7.45/7.83 ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (22256) {G2,W15,D4,L3,V1,M3} { sdtasdt0( sz00, sdtpldt0( sz00, X )
% 7.45/7.83 ) ==> sdtpldt0( sdtasdt0( sz00, X ), sz00 ), ! aElement0( sz00 ), !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 parent0[2, 3]: (22254) {G2,W17,D4,L4,V1,M4} { sdtasdt0( sz00, sdtpldt0(
% 7.45/7.83 sz00, X ) ) ==> sdtpldt0( sdtasdt0( sz00, X ), sz00 ), ! aElement0( sz00
% 7.45/7.83 ), ! aElement0( X ), ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 paramod: (44188) {G2,W17,D4,L5,V1,M5} { sdtasdt0( sz00, sdtpldt0( sz00, X
% 7.45/7.83 ) ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X ), !
% 7.45/7.83 aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 parent0[0]: (269) {G1,W13,D4,L3,V2,M3} R(8,5) { sdtpldt0( sdtasdt0( X, Y )
% 7.45/7.83 , sz00 ) ==> sdtasdt0( X, Y ), ! aElement0( X ), ! aElement0( Y ) }.
% 7.45/7.83 parent1[0; 6]: (22256) {G2,W15,D4,L3,V1,M3} { sdtasdt0( sz00, sdtpldt0(
% 7.45/7.83 sz00, X ) ) ==> sdtpldt0( sdtasdt0( sz00, X ), sz00 ), ! aElement0( sz00
% 7.45/7.83 ), ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := sz00
% 7.45/7.83 Y := X
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (44190) {G2,W15,D4,L4,V1,M4} { sdtasdt0( sz00, sdtpldt0( sz00, X )
% 7.45/7.83 ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X ), !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 parent0[1, 3]: (44188) {G2,W17,D4,L5,V1,M5} { sdtasdt0( sz00, sdtpldt0(
% 7.45/7.83 sz00, X ) ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X
% 7.45/7.83 ), ! aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (44192) {G2,W13,D4,L3,V1,M3} { sdtasdt0( sz00, sdtpldt0( sz00, X )
% 7.45/7.83 ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 parent0[2, 3]: (44190) {G2,W15,D4,L4,V1,M4} { sdtasdt0( sz00, sdtpldt0(
% 7.45/7.83 sz00, X ) ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X
% 7.45/7.83 ), ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 paramod: (46251) {G3,W17,D4,L5,V1,M5} { sdtasdt0( sdtpldt0( sz00, X ),
% 7.45/7.83 sz00 ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X ), !
% 7.45/7.83 aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 parent0[1]: (516) {G2,W15,D4,L3,V2,M3} F(512) { ! aElement0( X ), sdtasdt0
% 7.45/7.83 ( X, sdtpldt0( X, Y ) ) ==> sdtasdt0( sdtpldt0( X, Y ), X ), ! aElement0
% 7.45/7.83 ( Y ) }.
% 7.45/7.83 parent1[0; 1]: (44192) {G2,W13,D4,L3,V1,M3} { sdtasdt0( sz00, sdtpldt0(
% 7.45/7.83 sz00, X ) ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X
% 7.45/7.83 ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := sz00
% 7.45/7.83 Y := X
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (46253) {G3,W15,D4,L4,V1,M4} { sdtasdt0( sdtpldt0( sz00, X ), sz00
% 7.45/7.83 ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X ), !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 parent0[1, 3]: (46251) {G3,W17,D4,L5,V1,M5} { sdtasdt0( sdtpldt0( sz00, X
% 7.45/7.83 ), sz00 ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X )
% 7.45/7.83 , ! aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (46255) {G3,W13,D4,L3,V1,M3} { sdtasdt0( sdtpldt0( sz00, X ), sz00
% 7.45/7.83 ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 parent0[2, 3]: (46253) {G3,W15,D4,L4,V1,M4} { sdtasdt0( sdtpldt0( sz00, X
% 7.45/7.83 ), sz00 ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X )
% 7.45/7.83 , ! aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 paramod: (46602) {G1,W13,D3,L4,V1,M4} { sdtasdt0( X, sz00 ) ==> sdtasdt0(
% 7.45/7.83 sz00, X ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0( X ) }.
% 7.45/7.83 parent0[1]: (9) {G0,W7,D3,L2,V1,M2} I { ! aElement0( X ), sdtpldt0( sz00, X
% 7.45/7.83 ) ==> X }.
% 7.45/7.83 parent1[0; 2]: (46255) {G3,W13,D4,L3,V1,M3} { sdtasdt0( sdtpldt0( sz00, X
% 7.45/7.83 ), sz00 ) ==> sdtasdt0( sz00, X ), ! aElement0( sz00 ), ! aElement0( X )
% 7.45/7.83 }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (46604) {G1,W11,D3,L3,V1,M3} { sdtasdt0( X, sz00 ) ==> sdtasdt0(
% 7.45/7.83 sz00, X ), ! aElement0( X ), ! aElement0( sz00 ) }.
% 7.45/7.83 parent0[1, 3]: (46602) {G1,W13,D3,L4,V1,M4} { sdtasdt0( X, sz00 ) ==>
% 7.45/7.83 sdtasdt0( sz00, X ), ! aElement0( X ), ! aElement0( sz00 ), ! aElement0(
% 7.45/7.83 X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 paramod: (46658) {G2,W11,D3,L4,V1,M4} { sz00 ==> sdtasdt0( sz00, X ), !
% 7.45/7.83 aElement0( X ), ! aElement0( X ), ! aElement0( sz00 ) }.
% 7.45/7.83 parent0[1]: (20086) {G8,W7,D3,L2,V1,M2} S(416);d(20057);d(20062) { !
% 7.45/7.83 aElement0( X ), sdtasdt0( X, sz00 ) ==> sz00 }.
% 7.45/7.83 parent1[0; 1]: (46604) {G1,W11,D3,L3,V1,M3} { sdtasdt0( X, sz00 ) ==>
% 7.45/7.83 sdtasdt0( sz00, X ), ! aElement0( X ), ! aElement0( sz00 ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 factor: (46659) {G2,W9,D3,L3,V1,M3} { sz00 ==> sdtasdt0( sz00, X ), !
% 7.45/7.83 aElement0( X ), ! aElement0( sz00 ) }.
% 7.45/7.83 parent0[1, 2]: (46658) {G2,W11,D3,L4,V1,M4} { sz00 ==> sdtasdt0( sz00, X )
% 7.45/7.83 , ! aElement0( X ), ! aElement0( X ), ! aElement0( sz00 ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 resolution: (46663) {G1,W7,D3,L2,V1,M2} { sz00 ==> sdtasdt0( sz00, X ), !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 parent0[2]: (46659) {G2,W9,D3,L3,V1,M3} { sz00 ==> sdtasdt0( sz00, X ), !
% 7.45/7.83 aElement0( X ), ! aElement0( sz00 ) }.
% 7.45/7.83 parent1[0]: (1) {G0,W2,D2,L1,V0,M1} I { aElement0( sz00 ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 eqswap: (46664) {G1,W7,D3,L2,V1,M2} { sdtasdt0( sz00, X ) ==> sz00, !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 parent0[0]: (46663) {G1,W7,D3,L2,V1,M2} { sz00 ==> sdtasdt0( sz00, X ), !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 subsumption: (20090) {G10,W7,D3,L2,V1,M2} P(20048,16);f;d(145);d(269);d(516
% 7.45/7.83 );d(9);d(20086);r(1) { ! aElement0( X ), sdtasdt0( sz00, X ) ==> sz00 }.
% 7.45/7.83 parent0: (46664) {G1,W7,D3,L2,V1,M2} { sdtasdt0( sz00, X ) ==> sz00, !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83 permutation0:
% 7.45/7.83 0 ==> 1
% 7.45/7.83 1 ==> 0
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 eqswap: (46665) {G10,W7,D3,L2,V1,M2} { sz00 ==> sdtasdt0( sz00, X ), !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 parent0[1]: (20090) {G10,W7,D3,L2,V1,M2} P(20048,16);f;d(145);d(269);d(516)
% 7.45/7.83 ;d(9);d(20086);r(1) { ! aElement0( X ), sdtasdt0( sz00, X ) ==> sz00 }.
% 7.45/7.83 substitution0:
% 7.45/7.83 X := X
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 eqswap: (46666) {G2,W5,D3,L1,V0,M1} { ! sz00 ==> sdtasdt0( sz00, xx ) }.
% 7.45/7.83 parent0[0]: (7533) {G2,W5,D3,L1,V0,M1} S(1455);r(1) { ! sdtasdt0( sz00, xx
% 7.45/7.83 ) ==> sz00 }.
% 7.45/7.83 substitution0:
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 resolution: (46667) {G3,W2,D2,L1,V0,M1} { ! aElement0( xx ) }.
% 7.45/7.83 parent0[0]: (46666) {G2,W5,D3,L1,V0,M1} { ! sz00 ==> sdtasdt0( sz00, xx )
% 7.45/7.83 }.
% 7.45/7.83 parent1[0]: (46665) {G10,W7,D3,L2,V1,M2} { sz00 ==> sdtasdt0( sz00, X ), !
% 7.45/7.83 aElement0( X ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 X := xx
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 resolution: (46668) {G1,W0,D0,L0,V0,M0} { }.
% 7.45/7.83 parent0[0]: (46667) {G3,W2,D2,L1,V0,M1} { ! aElement0( xx ) }.
% 7.45/7.83 parent1[0]: (20) {G0,W2,D2,L1,V0,M1} I { aElement0( xx ) }.
% 7.45/7.83 substitution0:
% 7.45/7.83 end
% 7.45/7.83 substitution1:
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 subsumption: (20153) {G11,W0,D0,L0,V0,M0} R(20090,7533);r(20) { }.
% 7.45/7.83 parent0: (46668) {G1,W0,D0,L0,V0,M0} { }.
% 7.45/7.83 substitution0:
% 7.45/7.83 end
% 7.45/7.83 permutation0:
% 7.45/7.83 end
% 7.45/7.83
% 7.45/7.83 Proof check complete!
% 7.45/7.83
% 7.45/7.83 Memory use:
% 7.45/7.83
% 7.45/7.83 space for terms: 255204
% 7.45/7.83 space for clauses: 1169918
% 7.45/7.83
% 7.45/7.83
% 7.45/7.83 clauses generated: 38645
% 7.45/7.83 clauses kept: 20154
% 7.45/7.83 clauses selected: 301
% 7.45/7.83 clauses deleted: 1726
% 7.45/7.83 clauses inuse deleted: 18
% 7.45/7.83
% 7.45/7.83 subsentry: 285988
% 7.45/7.83 literals s-matched: 123683
% 7.45/7.83 literals matched: 123426
% 7.45/7.83 full subsumption: 32068
% 7.45/7.83
% 7.45/7.83 checksum: 2041544325
% 7.45/7.83
% 7.45/7.83
% 7.45/7.83 Bliksem ended
%------------------------------------------------------------------------------