%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP660+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n028.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 : Sat Jul 16 07:38:29 EDT 2022
% Result : Theorem 0.78s 1.51s
% Output : Refutation 0.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.13 % Problem : GRP660+1 : TPTP v8.1.0. Released v4.0.0.
% 0.05/0.14 % Command : bliksem %s
% 0.13/0.36 % Computer : n028.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % DateTime : Mon Jun 13 19:12:38 EDT 2022
% 0.13/0.36 % CPUTime :
% 0.78/1.51 *** allocated 10000 integers for termspace/termends
% 0.78/1.51 *** allocated 10000 integers for clauses
% 0.78/1.51 *** allocated 10000 integers for justifications
% 0.78/1.51 Bliksem 1.12
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51 Automatic Strategy Selection
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51 Clauses:
% 0.78/1.51
% 0.78/1.51 { mult( Y, ld( Y, X ) ) = X }.
% 0.78/1.51 { ld( Y, mult( Y, X ) ) = X }.
% 0.78/1.51 { mult( rd( Y, X ), X ) = Y }.
% 0.78/1.51 { rd( mult( Y, X ), X ) = Y }.
% 0.78/1.51 { mult( mult( mult( Z, Y ), X ), Z ) = mult( Z, mult( Y, mult( X, Z ) ) ) }
% 0.78/1.51 .
% 0.78/1.51 { ! mult( skol1( X ), X ) = skol1( X ), ! mult( X, skol1( X ) ) = skol1( X
% 0.78/1.51 ) }.
% 0.78/1.51
% 0.78/1.51 percentage equality = 1.000000, percentage horn = 1.000000
% 0.78/1.51 This is a pure equality problem
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51 Options Used:
% 0.78/1.51
% 0.78/1.51 useres = 1
% 0.78/1.51 useparamod = 1
% 0.78/1.51 useeqrefl = 1
% 0.78/1.51 useeqfact = 1
% 0.78/1.51 usefactor = 1
% 0.78/1.51 usesimpsplitting = 0
% 0.78/1.51 usesimpdemod = 5
% 0.78/1.51 usesimpres = 3
% 0.78/1.51
% 0.78/1.51 resimpinuse = 1000
% 0.78/1.51 resimpclauses = 20000
% 0.78/1.51 substype = eqrewr
% 0.78/1.51 backwardsubs = 1
% 0.78/1.51 selectoldest = 5
% 0.78/1.51
% 0.78/1.51 litorderings [0] = split
% 0.78/1.51 litorderings [1] = extend the termordering, first sorting on arguments
% 0.78/1.51
% 0.78/1.51 termordering = kbo
% 0.78/1.51
% 0.78/1.51 litapriori = 0
% 0.78/1.51 termapriori = 1
% 0.78/1.51 litaposteriori = 0
% 0.78/1.51 termaposteriori = 0
% 0.78/1.51 demodaposteriori = 0
% 0.78/1.51 ordereqreflfact = 0
% 0.78/1.51
% 0.78/1.51 litselect = negord
% 0.78/1.51
% 0.78/1.51 maxweight = 15
% 0.78/1.51 maxdepth = 30000
% 0.78/1.51 maxlength = 115
% 0.78/1.51 maxnrvars = 195
% 0.78/1.51 excuselevel = 1
% 0.78/1.51 increasemaxweight = 1
% 0.78/1.51
% 0.78/1.51 maxselected = 10000000
% 0.78/1.51 maxnrclauses = 10000000
% 0.78/1.51
% 0.78/1.51 showgenerated = 0
% 0.78/1.51 showkept = 0
% 0.78/1.51 showselected = 0
% 0.78/1.51 showdeleted = 0
% 0.78/1.51 showresimp = 1
% 0.78/1.51 showstatus = 2000
% 0.78/1.51
% 0.78/1.51 prologoutput = 0
% 0.78/1.51 nrgoals = 5000000
% 0.78/1.51 totalproof = 1
% 0.78/1.51
% 0.78/1.51 Symbols occurring in the translation:
% 0.78/1.51
% 0.78/1.51 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.78/1.51 . [1, 2] (w:1, o:17, a:1, s:1, b:0),
% 0.78/1.51 ! [4, 1] (w:0, o:11, a:1, s:1, b:0),
% 0.78/1.51 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.78/1.51 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.78/1.51 ld [37, 2] (w:1, o:41, a:1, s:1, b:0),
% 0.78/1.51 mult [38, 2] (w:1, o:42, a:1, s:1, b:0),
% 0.78/1.51 rd [39, 2] (w:1, o:43, a:1, s:1, b:0),
% 0.78/1.51 skol1 [43, 1] (w:1, o:16, a:1, s:1, b:1).
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51 Starting Search:
% 0.78/1.51
% 0.78/1.51 *** allocated 15000 integers for clauses
% 0.78/1.51 *** allocated 22500 integers for clauses
% 0.78/1.51 *** allocated 33750 integers for clauses
% 0.78/1.51 Resimplifying inuse:
% 0.78/1.51 Done
% 0.78/1.51
% 0.78/1.51 Resimplifying inuse:
% 0.78/1.51 Done
% 0.78/1.51
% 0.78/1.51 Failed to find proof!
% 0.78/1.51 maxweight = 15
% 0.78/1.51 maxnrclauses = 10000000
% 0.78/1.51 Generated: 12706
% 0.78/1.51 Kept: 231
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51 The strategy used was not complete!
% 0.78/1.51
% 0.78/1.51 Increased maxweight to 16
% 0.78/1.51
% 0.78/1.51 Starting Search:
% 0.78/1.51
% 0.78/1.51 Resimplifying inuse:
% 0.78/1.51 Done
% 0.78/1.51
% 0.78/1.51 Resimplifying inuse:
% 0.78/1.51 Done
% 0.78/1.51
% 0.78/1.51 Failed to find proof!
% 0.78/1.51 maxweight = 16
% 0.78/1.51 maxnrclauses = 10000000
% 0.78/1.51 Generated: 12706
% 0.78/1.51 Kept: 231
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51 The strategy used was not complete!
% 0.78/1.51
% 0.78/1.51 Increased maxweight to 17
% 0.78/1.51
% 0.78/1.51 Starting Search:
% 0.78/1.51
% 0.78/1.51 Resimplifying inuse:
% 0.78/1.51 Done
% 0.78/1.51
% 0.78/1.51 Resimplifying inuse:
% 0.78/1.51 Done
% 0.78/1.51
% 0.78/1.51 Failed to find proof!
% 0.78/1.51 maxweight = 17
% 0.78/1.51 maxnrclauses = 10000000
% 0.78/1.51 Generated: 12706
% 0.78/1.51 Kept: 231
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51 The strategy used was not complete!
% 0.78/1.51
% 0.78/1.51 Increased maxweight to 18
% 0.78/1.51
% 0.78/1.51 Starting Search:
% 0.78/1.51
% 0.78/1.51 Resimplifying inuse:
% 0.78/1.51 Done
% 0.78/1.51
% 0.78/1.51 Resimplifying inuse:
% 0.78/1.51 Done
% 0.78/1.51
% 0.78/1.51 Failed to find proof!
% 0.78/1.51 maxweight = 18
% 0.78/1.51 maxnrclauses = 10000000
% 0.78/1.51 Generated: 12706
% 0.78/1.51 Kept: 231
% 0.78/1.51
% 0.78/1.51
% 0.78/1.51 The strategy used was not complete!
% 0.78/1.51
% 0.78/1.51 Increased maxweight to 19
% 0.78/1.51
% 0.78/1.51 Starting Search:
% 0.78/1.51
% 0.78/1.51 *** allocated 50625 integers for clauses
% 0.78/1.51 *** allocated 75937 integers for clauses
% 0.78/1.51 *** allocated 113905 integers for clauses
% 0.78/1.51 *** allocated 15000 integers for termspace/termends
% 0.78/1.51
% 0.78/1.51 Bliksems!, er is een bewijs:
% 0.78/1.51 % SZS status Theorem
% 0.78/1.51 % SZS output start Refutation
% 0.78/1.51
% 0.78/1.51 (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.51 (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.78/1.51 (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.51 (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.78/1.51 (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) ) ==> mult(
% 0.78/1.51 mult( mult( Z, Y ), X ), Z ) }.
% 0.78/1.51 (5) {G0,W14,D4,L2,V1,M2} I { ! mult( skol1( X ), X ) ==> skol1( X ), ! mult
% 0.78/1.51 ( X, skol1( X ) ) ==> skol1( X ) }.
% 0.78/1.51 (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.78/1.51 (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.51 (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y ), Z ), X ),
% 0.78/1.51 ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 0.78/1.51 (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd( X, Y ) ),
% 0.78/1.51 Y ) ==> mult( Y, mult( Z, X ) ) }.
% 0.78/1.51 (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 0.78/1.51 mult( mult( Y, rd( Z, X ) ), X ) }.
% 0.78/1.51 (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 0.78/1.51 mult( mult( X, Y ), rd( Z, X ) ) }.
% 0.78/1.51 (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z, X ) ), X )
% 0.78/1.51 ) ==> mult( ld( X, Y ), Z ) }.
% 0.78/1.51 (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld( X, Y ), Z )
% 0.78/1.51 ) ==> rd( mult( Z, Y ), Z ) }.
% 0.78/1.51 (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) ), rd( Y, Z )
% 0.78/1.51 ) ==> rd( mult( Z, X ), Z ) }.
% 0.78/1.51 (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult( X, Z ), X )
% 0.78/1.51 ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.51 (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X ) ==> ld( Y
% 0.78/1.51 , rd( mult( X, Z ), X ) ) }.
% 0.78/1.51 (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X ) ==> ld(
% 0.78/1.51 mult( X, Z ), rd( Y, X ) ) }.
% 0.78/1.51 (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld( mult( X, Y
% 0.78/1.51 ), X ) }.
% 0.78/1.51 (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ), ld( X, Y ) )
% 0.78/1.51 ==> Y }.
% 0.78/1.51 (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X, Y ), X ) )
% 0.78/1.51 ==> X }.
% 0.78/1.51 (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==> ld( ld( Y, X
% 0.78/1.51 ), Y ) }.
% 0.78/1.51 (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd( Z, Y ) ), ld
% 0.78/1.51 ( X, ld( Y, Z ) ) ) ==> Y }.
% 0.78/1.51 (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) ), ld( ld( X, Y
% 0.78/1.51 ), ld( X, Z ) ) ) ==> X }.
% 0.78/1.51 (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) ), Z ) ==> ld
% 0.78/1.51 ( ld( Z, X ), ld( Z, Y ) ) }.
% 0.78/1.51 (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y, mult( X, Y ) )
% 0.78/1.51 ) ==> mult( ld( Z, X ), Y ) }.
% 0.78/1.51 (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X ) ), mult( ld
% 0.78/1.51 ( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 0.78/1.51 (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z ) ), mult( Y,
% 0.78/1.51 Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 0.78/1.51 (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X ), X ), mult(
% 0.78/1.51 Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 0.78/1.51 (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z, Y ) ) ==>
% 0.78/1.51 ld( Y, rd( rd( X, Y ), Z ) ) }.
% 0.78/1.51 (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y ) ), X ) ==>
% 0.78/1.51 ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 0.78/1.51 (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ), rd( X, Y ) )
% 0.78/1.51 ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.51 (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y, rd( Z, ld( Y
% 0.78/1.51 , X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 0.78/1.51 (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z, X ) ) ==>
% 0.78/1.51 mult( X, rd( ld( X, Y ), Z ) ) }.
% 0.78/1.51 (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z ), ld( Y, X )
% 0.78/1.51 ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 0.78/1.51 (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X ), rd( X, X
% 0.78/1.51 ) ) ==> rd( X, X ) }.
% 0.78/1.51 (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X ), rd( X, X )
% 0.78/1.51 ) ==> rd( X, X ) }.
% 0.78/1.51 (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X, X ), ld( X,
% 0.78/1.51 X ) ) ==> ld( X, X ) }.
% 0.78/1.51 (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd( X, X ) ) ==>
% 0.78/1.51 ld( mult( X, X ), X ) }.
% 0.78/1.51 (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X ), ld( X, X )
% 0.78/1.51 ) ==> ld( X, X ) }.
% 0.78/1.51 (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld( X, X ), ld( X
% 0.78/1.51 , X ) ) ==> ld( X, X ) }.
% 0.78/1.51 (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld( ld( X, X ),
% 0.78/1.51 X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 0.78/1.51 (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld( ld( X, X ), X
% 0.78/1.51 ), ld( X, X ) ) ==> X }.
% 0.78/1.51 (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld( ld( X, X ),
% 0.78/1.51 X ) ==> X }.
% 0.78/1.51 (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y, ld( X, X ) )
% 0.78/1.51 ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 0.78/1.51 (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld( X, X ) }.
% 0.78/1.51 (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld( X, Y ), ld( X
% 0.78/1.51 , X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 0.78/1.51 (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) ) ==> ld( mult(
% 0.78/1.51 X, X ), X ) }.
% 0.78/1.51 (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X, X ) ) ==>
% 0.78/1.52 mult( X, rd( ld( X, Y ), X ) ) }.
% 0.78/1.52 (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd( X, Y ), rd( X
% 0.78/1.52 , Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 0.78/1.52 (321) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y, Y ) ) = ld(
% 0.78/1.52 mult( X, ld( Y, X ) ), X ) }.
% 0.78/1.52 (363) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd( X, Y ) ), X
% 0.78/1.52 ) ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X, X ) ) ==>
% 0.78/1.52 ld( ld( ld( X, X ), Y ), X ) }.
% 0.78/1.52 (539) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld( X, X ) )
% 0.78/1.52 ==> mult( ld( mult( X, X ), X ), Y ) }.
% 0.78/1.52 (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(212) { rd( ld(
% 0.78/1.52 ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 0.78/1.52 (553) {G23,W15,D5,L1,V2,M1} P(543,270);d(212);d(194);d(38);d(366);d(242);d(
% 0.78/1.52 0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y, ld( X, X ) )
% 0.78/1.52 }.
% 0.78/1.52 (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld( ld( X, X ),
% 0.78/1.52 rd( Y, ld( X, X ) ) ) ==> Y }.
% 0.78/1.52 (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y ) ==> Y }.
% 0.78/1.52 (583) {G25,W7,D4,L1,V2,M1} P(557,129);d(564);d(564) { mult( Y, ld( X, X ) )
% 0.78/1.52 ==> Y }.
% 0.78/1.52 (590) {G25,W11,D5,L1,V3,M1} P(37,557);d(564);d(194);d(553);d(564) { ld( Y,
% 0.78/1.52 rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 0.78/1.52 (594) {G26,W7,D4,L1,V2,M1} P(557,43);d(590);d(583);d(6);d(564) { rd( Y, ld
% 0.78/1.52 ( X, X ) ) ==> Y }.
% 0.78/1.52 (598) {G27,W7,D4,L1,V2,M1} P(557,0);d(594) { mult( ld( X, X ), Y ) ==> Y
% 0.78/1.52 }.
% 0.78/1.52 (649) {G28,W0,D0,L0,V0,M0} R(583,5);d(598);q { }.
% 0.78/1.52
% 0.78/1.52
% 0.78/1.52 % SZS output end Refutation
% 0.78/1.52 found a proof!
% 0.78/1.52
% 0.78/1.52
% 0.78/1.52 Unprocessed initial clauses:
% 0.78/1.52
% 0.78/1.52 (651) {G0,W7,D4,L1,V2,M1} { mult( Y, ld( Y, X ) ) = X }.
% 0.78/1.52 (652) {G0,W7,D4,L1,V2,M1} { ld( Y, mult( Y, X ) ) = X }.
% 0.78/1.52 (653) {G0,W7,D4,L1,V2,M1} { mult( rd( Y, X ), X ) = Y }.
% 0.78/1.52 (654) {G0,W7,D4,L1,V2,M1} { rd( mult( Y, X ), X ) = Y }.
% 0.78/1.52 (655) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( Z, Y ), X ), Z ) = mult( Z
% 0.78/1.52 , mult( Y, mult( X, Z ) ) ) }.
% 0.78/1.52 (656) {G0,W14,D4,L2,V1,M2} { ! mult( skol1( X ), X ) = skol1( X ), ! mult
% 0.78/1.52 ( X, skol1( X ) ) = skol1( X ) }.
% 0.78/1.52
% 0.78/1.52
% 0.78/1.52 Total Proof:
% 0.78/1.52
% 0.78/1.52 subsumption: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent0: (651) {G0,W7,D4,L1,V2,M1} { mult( Y, ld( Y, X ) ) = X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.78/1.52 parent0: (652) {G0,W7,D4,L1,V2,M1} { ld( Y, mult( Y, X ) ) = X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent0: (653) {G0,W7,D4,L1,V2,M1} { mult( rd( Y, X ), X ) = Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent0: (654) {G0,W7,D4,L1,V2,M1} { rd( mult( Y, X ), X ) = Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (671) {G0,W15,D5,L1,V3,M1} { mult( X, mult( Y, mult( Z, X ) ) ) =
% 0.78/1.52 mult( mult( mult( X, Y ), Z ), X ) }.
% 0.78/1.52 parent0[0]: (655) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( Z, Y ), X ), Z
% 0.78/1.52 ) = mult( Z, mult( Y, mult( X, Z ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) )
% 0.78/1.52 ) ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 0.78/1.52 parent0: (671) {G0,W15,D5,L1,V3,M1} { mult( X, mult( Y, mult( Z, X ) ) ) =
% 0.78/1.52 mult( mult( mult( X, Y ), Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (5) {G0,W14,D4,L2,V1,M2} I { ! mult( skol1( X ), X ) ==> skol1
% 0.78/1.52 ( X ), ! mult( X, skol1( X ) ) ==> skol1( X ) }.
% 0.78/1.52 parent0: (656) {G0,W14,D4,L2,V1,M2} { ! mult( skol1( X ), X ) = skol1( X )
% 0.78/1.52 , ! mult( X, skol1( X ) ) = skol1( X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 1 ==> 1
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (681) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (682) {G1,W7,D4,L1,V2,M1} { X ==> ld( rd( Y, X ), Y ) }.
% 0.78/1.52 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 6]: (681) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := rd( Y, X )
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (683) {G1,W7,D4,L1,V2,M1} { ld( rd( Y, X ), Y ) ==> X }.
% 0.78/1.52 parent0[0]: (682) {G1,W7,D4,L1,V2,M1} { X ==> ld( rd( Y, X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.78/1.52 parent0: (683) {G1,W7,D4,L1,V2,M1} { ld( rd( Y, X ), Y ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (685) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 0.78/1.52 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (686) {G1,W7,D4,L1,V2,M1} { X ==> rd( Y, ld( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 3]: (685) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( X, Y )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (687) {G1,W7,D4,L1,V2,M1} { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 parent0[0]: (686) {G1,W7,D4,L1,V2,M1} { X ==> rd( Y, ld( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 parent0: (687) {G1,W7,D4,L1,V2,M1} { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (689) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z ), X )
% 0.78/1.52 ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 0.78/1.52 parent0[0]: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) )
% 0.78/1.52 ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (692) {G1,W19,D6,L1,V3,M1} { mult( mult( mult( ld( X, Y ), Z ), X
% 0.78/1.52 ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 18]: (689) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z )
% 0.78/1.52 , X ) ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, Y )
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y
% 0.78/1.52 ), Z ), X ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 0.78/1.52 parent0: (692) {G1,W19,D6,L1,V3,M1} { mult( mult( mult( ld( X, Y ), Z ), X
% 0.78/1.52 ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (697) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z ), X )
% 0.78/1.52 ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 0.78/1.52 parent0[0]: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) )
% 0.78/1.52 ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (700) {G1,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), rd( Z, X )
% 0.78/1.52 ), X ) ==> mult( X, mult( Y, Z ) ) }.
% 0.78/1.52 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 14]: (697) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z )
% 0.78/1.52 , X ) ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := rd( Z, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ),
% 0.78/1.52 rd( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 0.78/1.52 parent0: (700) {G1,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), rd( Z, X )
% 0.78/1.52 ), X ) ==> mult( X, mult( Y, Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (705) {G1,W15,D5,L1,V3,M1} { mult( X, mult( Y, Z ) ) ==> mult(
% 0.78/1.52 mult( mult( X, Y ), rd( Z, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd
% 0.78/1.52 ( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (707) {G1,W15,D5,L1,V3,M1} { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 0.78/1.52 mult( mult( Y, rd( Z, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 10]: (705) {G1,W15,D5,L1,V3,M1} { mult( X, mult( Y, Z ) ) ==>
% 0.78/1.52 mult( mult( mult( X, Y ), rd( Z, X ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( X, Y )
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y )
% 0.78/1.52 , Z ) ) ==> mult( mult( Y, rd( Z, X ) ), X ) }.
% 0.78/1.52 parent0: (707) {G1,W15,D5,L1,V3,M1} { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 0.78/1.52 mult( mult( Y, rd( Z, X ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (711) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 0.78/1.52 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (714) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 0.78/1.52 rd( mult( X, mult( Y, Z ) ), X ) }.
% 0.78/1.52 parent0[0]: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd
% 0.78/1.52 ( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 0.78/1.52 parent1[0; 9]: (711) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := mult( mult( X, Y ), rd( Z, X ) )
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (715) {G1,W15,D5,L1,V3,M1} { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 0.78/1.52 mult( mult( X, Y ), rd( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (714) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) )
% 0.78/1.52 ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z )
% 0.78/1.52 ), X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 0.78/1.52 parent0: (715) {G1,W15,D5,L1,V3,M1} { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 0.78/1.52 mult( mult( X, Y ), rd( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (717) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (720) {G1,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X,
% 0.78/1.52 mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 0.78/1.52 parent0[0]: (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y ),
% 0.78/1.52 Z ) ) ==> mult( mult( Y, rd( Z, X ) ), X ) }.
% 0.78/1.52 parent1[0; 8]: (717) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := mult( ld( X, Y ), Z )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (721) {G1,W15,D6,L1,V3,M1} { ld( X, mult( mult( Y, rd( Z, X ) ), X
% 0.78/1.52 ) ) ==> mult( ld( X, Y ), Z ) }.
% 0.78/1.52 parent0[0]: (720) {G1,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X,
% 0.78/1.52 mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd(
% 0.78/1.52 Z, X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 0.78/1.52 parent0: (721) {G1,W15,D6,L1,V3,M1} { ld( X, mult( mult( Y, rd( Z, X ) ),
% 0.78/1.52 X ) ) ==> mult( ld( X, Y ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (723) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 0.78/1.52 rd( mult( X, mult( Y, Z ) ), X ) }.
% 0.78/1.52 parent0[0]: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) )
% 0.78/1.52 , X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (725) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( ld( Y, Z ),
% 0.78/1.52 X ) ) ==> rd( mult( X, Z ), X ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 13]: (723) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X
% 0.78/1.52 ) ) ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := ld( Y, Z )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 0.78/1.52 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 0.78/1.52 parent0: (725) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( ld( Y, Z ),
% 0.78/1.52 X ) ) ==> rd( mult( X, Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (729) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 0.78/1.52 rd( mult( X, mult( Y, Z ) ), X ) }.
% 0.78/1.52 parent0[0]: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) )
% 0.78/1.52 , X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (734) {G1,W15,D5,L1,V3,M1} { mult( mult( X, rd( Y, Z ) ), rd( Z,
% 0.78/1.52 X ) ) ==> rd( mult( X, Y ), X ) }.
% 0.78/1.52 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 13]: (729) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X
% 0.78/1.52 ) ) ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := rd( Y, Z )
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y )
% 0.78/1.52 ), rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 0.78/1.52 parent0: (734) {G1,W15,D5,L1,V3,M1} { mult( mult( X, rd( Y, Z ) ), rd( Z,
% 0.78/1.52 X ) ) ==> rd( mult( X, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (739) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (742) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( mult( Z
% 0.78/1.52 , X ), rd( mult( Z, Y ), Z ) ) }.
% 0.78/1.52 parent0[0]: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 0.78/1.52 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 0.78/1.52 parent1[0; 10]: (739) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := mult( Z, X )
% 0.78/1.52 Y := rd( ld( X, Y ), Z )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (743) {G1,W15,D5,L1,V3,M1} { ld( mult( Z, X ), rd( mult( Z, Y ), Z
% 0.78/1.52 ) ) ==> rd( ld( X, Y ), Z ) }.
% 0.78/1.52 parent0[0]: (742) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( mult
% 0.78/1.52 ( Z, X ), rd( mult( Z, Y ), Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 0.78/1.52 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.52 parent0: (743) {G1,W15,D5,L1,V3,M1} { ld( mult( Z, X ), rd( mult( Z, Y ),
% 0.78/1.52 Z ) ) ==> rd( ld( X, Y ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (745) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 0.78/1.52 Y ), rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 0.78/1.52 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (748) {G1,W15,D5,L1,V3,M1} { rd( ld( ld( X, Y ), Z ), X ) ==> ld
% 0.78/1.52 ( Y, rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 9]: (745) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 0.78/1.52 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( X, Y )
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 0.78/1.52 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 parent0: (748) {G1,W15,D5,L1,V3,M1} { rd( ld( ld( X, Y ), Z ), X ) ==> ld
% 0.78/1.52 ( Y, rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (753) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 0.78/1.52 Y ), rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 0.78/1.52 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (757) {G1,W15,D5,L1,V3,M1} { rd( ld( X, ld( Y, Z ) ), Y ) ==> ld
% 0.78/1.52 ( mult( Y, X ), rd( Z, Y ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 13]: (753) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 0.78/1.52 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := ld( Y, Z )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 0.78/1.52 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 0.78/1.52 parent0: (757) {G1,W15,D5,L1,V3,M1} { rd( ld( X, ld( Y, Z ) ), Y ) ==> ld
% 0.78/1.52 ( mult( Y, X ), rd( Z, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (761) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 0.78/1.52 Y ), rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 0.78/1.52 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (762) {G1,W11,D4,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( mult( Y
% 0.78/1.52 , X ), Y ) }.
% 0.78/1.52 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 10]: (761) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 0.78/1.52 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 0.78/1.52 ( mult( X, Y ), X ) }.
% 0.78/1.52 parent0: (762) {G1,W11,D4,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( mult( Y
% 0.78/1.52 , X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (765) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 0.78/1.52 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (768) {G2,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld
% 0.78/1.52 ( Y, X ) ) }.
% 0.78/1.52 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 0.78/1.52 ( mult( X, Y ), X ) }.
% 0.78/1.52 parent1[0; 3]: (765) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( Y, X )
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (769) {G2,W11,D5,L1,V2,M1} { ld( ld( mult( X, Y ), X ), ld( Y, X )
% 0.78/1.52 ) ==> X }.
% 0.78/1.52 parent0[0]: (768) {G2,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ),
% 0.78/1.52 ld( Y, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y )
% 0.78/1.52 , ld( X, Y ) ) ==> Y }.
% 0.78/1.52 parent0: (769) {G2,W11,D5,L1,V2,M1} { ld( ld( mult( X, Y ), X ), ld( Y, X
% 0.78/1.52 ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (771) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld(
% 0.78/1.52 Y, X ) ) }.
% 0.78/1.52 parent0[0]: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ),
% 0.78/1.52 ld( X, Y ) ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (774) {G1,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, X ), ld( ld( X, Y )
% 0.78/1.52 , X ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 4]: (771) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X
% 0.78/1.52 ), ld( Y, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( X, Y )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (775) {G1,W11,D5,L1,V2,M1} { ld( ld( Y, X ), ld( ld( X, Y ), X ) )
% 0.78/1.52 ==> X }.
% 0.78/1.52 parent0[0]: (774) {G1,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, X ), ld( ld( X,
% 0.78/1.52 Y ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X
% 0.78/1.52 , Y ), X ) ) ==> X }.
% 0.78/1.52 parent0: (775) {G1,W11,D5,L1,V2,M1} { ld( ld( Y, X ), ld( ld( X, Y ), X )
% 0.78/1.52 ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (777) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (778) {G1,W11,D4,L1,V2,M1} { ld( ld( X, Y ), X ) ==> mult( ld( Y
% 0.78/1.52 , X ), X ) }.
% 0.78/1.52 parent0[0]: (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X,
% 0.78/1.52 Y ), X ) ) ==> X }.
% 0.78/1.52 parent1[0; 10]: (777) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( Y, X )
% 0.78/1.52 Y := ld( ld( X, Y ), X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (779) {G1,W11,D4,L1,V2,M1} { mult( ld( Y, X ), X ) ==> ld( ld( X,
% 0.78/1.52 Y ), X ) }.
% 0.78/1.52 parent0[0]: (778) {G1,W11,D4,L1,V2,M1} { ld( ld( X, Y ), X ) ==> mult( ld
% 0.78/1.52 ( Y, X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 0.78/1.52 ld( ld( Y, X ), Y ) }.
% 0.78/1.52 parent0: (779) {G1,W11,D4,L1,V2,M1} { mult( ld( Y, X ), X ) ==> ld( ld( X
% 0.78/1.52 , Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (781) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 0.78/1.52 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (786) {G2,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z, X
% 0.78/1.52 ) ), ld( Y, ld( X, Z ) ) ) }.
% 0.78/1.52 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 0.78/1.52 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 0.78/1.52 parent1[0; 3]: (781) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( Y, ld( X, Z ) )
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (787) {G2,W15,D5,L1,V3,M1} { ld( ld( mult( X, Y ), rd( Z, X ) ),
% 0.78/1.52 ld( Y, ld( X, Z ) ) ) ==> X }.
% 0.78/1.52 parent0[0]: (786) {G2,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z
% 0.78/1.52 , X ) ), ld( Y, ld( X, Z ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd
% 0.78/1.52 ( Z, Y ) ), ld( X, ld( Y, Z ) ) ) ==> Y }.
% 0.78/1.52 parent0: (787) {G2,W15,D5,L1,V3,M1} { ld( ld( mult( X, Y ), rd( Z, X ) ),
% 0.78/1.52 ld( Y, ld( X, Z ) ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (789) {G6,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z, X
% 0.78/1.52 ) ), ld( Y, ld( X, Z ) ) ) }.
% 0.78/1.52 parent0[0]: (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd(
% 0.78/1.52 Z, Y ) ), ld( X, ld( Y, Z ) ) ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (792) {G1,W15,D5,L1,V3,M1} { X ==> ld( ld( Y, rd( Z, X ) ), ld(
% 0.78/1.52 ld( X, Y ), ld( X, Z ) ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 4]: (789) {G6,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd
% 0.78/1.52 ( Z, X ) ), ld( Y, ld( X, Z ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( X, Y )
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (793) {G1,W15,D5,L1,V3,M1} { ld( ld( Y, rd( Z, X ) ), ld( ld( X, Y
% 0.78/1.52 ), ld( X, Z ) ) ) ==> X }.
% 0.78/1.52 parent0[0]: (792) {G1,W15,D5,L1,V3,M1} { X ==> ld( ld( Y, rd( Z, X ) ), ld
% 0.78/1.52 ( ld( X, Y ), ld( X, Z ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) )
% 0.78/1.52 , ld( ld( X, Y ), ld( X, Z ) ) ) ==> X }.
% 0.78/1.52 parent0: (793) {G1,W15,D5,L1,V3,M1} { ld( ld( Y, rd( Z, X ) ), ld( ld( X,
% 0.78/1.52 Y ), ld( X, Z ) ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (795) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (796) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, Z ) ) ==>
% 0.78/1.52 mult( ld( Y, rd( Z, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) ),
% 0.78/1.52 ld( ld( X, Y ), ld( X, Z ) ) ) ==> X }.
% 0.78/1.52 parent1[0; 14]: (795) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( Y, rd( Z, X ) )
% 0.78/1.52 Y := ld( ld( X, Y ), ld( X, Z ) )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (797) {G1,W15,D5,L1,V3,M1} { mult( ld( Y, rd( Z, X ) ), X ) ==> ld
% 0.78/1.52 ( ld( X, Y ), ld( X, Z ) ) }.
% 0.78/1.52 parent0[0]: (796) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, Z ) ) ==>
% 0.78/1.52 mult( ld( Y, rd( Z, X ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z )
% 0.78/1.52 ), Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 0.78/1.52 parent0: (797) {G1,W15,D5,L1,V3,M1} { mult( ld( Y, rd( Z, X ) ), X ) ==>
% 0.78/1.52 ld( ld( X, Y ), ld( X, Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (799) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) ) ==> mult
% 0.78/1.52 ( ld( X, rd( Y, Z ) ), Z ) }.
% 0.78/1.52 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 0.78/1.52 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (802) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, mult( Z, X )
% 0.78/1.52 ) ) ==> mult( ld( Y, Z ), X ) }.
% 0.78/1.52 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 13]: (799) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) )
% 0.78/1.52 ==> mult( ld( X, rd( Y, Z ) ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := mult( Z, X )
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y,
% 0.78/1.52 mult( X, Y ) ) ) ==> mult( ld( Z, X ), Y ) }.
% 0.78/1.52 parent0: (802) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, mult( Z, X )
% 0.78/1.52 ) ) ==> mult( ld( Y, Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (805) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 0.78/1.52 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (806) {G2,W15,D5,L1,V3,M1} { ld( X, Y ) ==> rd( ld( X, mult( Z, X
% 0.78/1.52 ) ), mult( ld( Y, Z ), X ) ) }.
% 0.78/1.52 parent0[0]: (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y,
% 0.78/1.52 mult( X, Y ) ) ) ==> mult( ld( Z, X ), Y ) }.
% 0.78/1.52 parent1[0; 10]: (805) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, mult( Z, X ) )
% 0.78/1.52 Y := ld( X, Y )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (807) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Z, X ) ), mult( ld(
% 0.78/1.52 Y, Z ), X ) ) ==> ld( X, Y ) }.
% 0.78/1.52 parent0[0]: (806) {G2,W15,D5,L1,V3,M1} { ld( X, Y ) ==> rd( ld( X, mult( Z
% 0.78/1.52 , X ) ), mult( ld( Y, Z ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 0.78/1.52 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 0.78/1.52 parent0: (807) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Z, X ) ), mult( ld
% 0.78/1.52 ( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (809) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X, mult( Y, X
% 0.78/1.52 ) ), mult( ld( Z, Y ), X ) ) }.
% 0.78/1.52 parent0[0]: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 0.78/1.52 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (813) {G2,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 0.78/1.52 mult( Y, X ) ), mult( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 13]: (809) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X,
% 0.78/1.52 mult( Y, X ) ), mult( ld( Z, Y ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := rd( Y, Z )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (815) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), mult( Z, X
% 0.78/1.52 ) ) ==> ld( X, rd( Y, Z ) ) }.
% 0.78/1.52 parent0[0]: (813) {G2,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X
% 0.78/1.52 , mult( Y, X ) ), mult( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 0.78/1.52 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 0.78/1.52 parent0: (815) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), mult( Z,
% 0.78/1.52 X ) ) ==> ld( X, rd( Y, Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (816) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 0.78/1.52 mult( Y, X ) ), mult( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 0.78/1.52 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (819) {G6,W15,D5,L1,V2,M1} { ld( X, rd( Y, Y ) ) ==> ld( mult(
% 0.78/1.52 mult( Y, X ), X ), mult( Y, X ) ) }.
% 0.78/1.52 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 0.78/1.52 ( mult( X, Y ), X ) }.
% 0.78/1.52 parent1[0; 6]: (816) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 0.78/1.52 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := mult( Y, X )
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (821) {G6,W15,D5,L1,V2,M1} { ld( mult( mult( Y, X ), X ), mult( Y
% 0.78/1.52 , X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 0.78/1.52 parent0[0]: (819) {G6,W15,D5,L1,V2,M1} { ld( X, rd( Y, Y ) ) ==> ld( mult
% 0.78/1.52 ( mult( Y, X ), X ), mult( Y, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X )
% 0.78/1.52 , X ), mult( Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 0.78/1.52 parent0: (821) {G6,W15,D5,L1,V2,M1} { ld( mult( mult( Y, X ), X ), mult( Y
% 0.78/1.52 , X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (823) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 0.78/1.52 mult( Y, X ) ), mult( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 0.78/1.52 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (826) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 0.78/1.52 ( ld( X, Y ), mult( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 11]: (823) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 0.78/1.52 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := rd( Y, X )
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (828) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), mult( Z, X ) ) ==> ld
% 0.78/1.52 ( X, rd( rd( Y, X ), Z ) ) }.
% 0.78/1.52 parent0[0]: (826) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==>
% 0.78/1.52 rd( ld( X, Y ), mult( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 0.78/1.52 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 0.78/1.52 parent0: (828) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), mult( Z, X ) ) ==>
% 0.78/1.52 ld( X, rd( rd( Y, X ), Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (831) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 0.78/1.52 mult( Y, X ) ), mult( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 0.78/1.52 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (835) {G1,W15,D5,L1,V3,M1} { ld( X, rd( Y, rd( Z, X ) ) ) ==> rd
% 0.78/1.52 ( ld( X, mult( Y, X ) ), Z ) }.
% 0.78/1.52 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 14]: (831) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 0.78/1.52 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := rd( Z, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (837) {G1,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), Z ) ==> ld
% 0.78/1.52 ( X, rd( Y, rd( Z, X ) ) ) }.
% 0.78/1.52 parent0[0]: (835) {G1,W15,D5,L1,V3,M1} { ld( X, rd( Y, rd( Z, X ) ) ) ==>
% 0.78/1.52 rd( ld( X, mult( Y, X ) ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y )
% 0.78/1.52 ), X ) ==> ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 0.78/1.52 parent0: (837) {G1,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), Z ) ==>
% 0.78/1.52 ld( X, rd( Y, rd( Z, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (839) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 0.78/1.52 ( ld( X, Y ), mult( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 0.78/1.52 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (842) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), rd( Z, X ) )
% 0.78/1.52 ) ==> rd( ld( X, Y ), Z ) }.
% 0.78/1.52 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 14]: (839) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) )
% 0.78/1.52 ==> rd( ld( X, Y ), mult( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := rd( Z, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 0.78/1.52 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.52 parent0: (842) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), rd( Z, X ) )
% 0.78/1.52 ) ==> rd( ld( X, Y ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (845) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X, rd(
% 0.78/1.52 rd( Y, X ), rd( Z, X ) ) ) }.
% 0.78/1.52 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 0.78/1.52 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (849) {G2,W19,D6,L1,V3,M1} { rd( ld( ld( X, Y ), Y ), Z ) ==> ld
% 0.78/1.52 ( ld( X, Y ), rd( X, rd( Z, ld( X, Y ) ) ) ) }.
% 0.78/1.52 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 parent1[0; 13]: (845) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld(
% 0.78/1.52 X, rd( rd( Y, X ), rd( Z, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, Y )
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (852) {G2,W19,D6,L1,V3,M1} { ld( ld( X, Y ), rd( X, rd( Z, ld( X,
% 0.78/1.52 Y ) ) ) ) ==> rd( ld( ld( X, Y ), Y ), Z ) }.
% 0.78/1.52 parent0[0]: (849) {G2,W19,D6,L1,V3,M1} { rd( ld( ld( X, Y ), Y ), Z ) ==>
% 0.78/1.52 ld( ld( X, Y ), rd( X, rd( Z, ld( X, Y ) ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y,
% 0.78/1.52 rd( Z, ld( Y, X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 0.78/1.52 parent0: (852) {G2,W19,D6,L1,V3,M1} { ld( ld( X, Y ), rd( X, rd( Z, ld( X
% 0.78/1.52 , Y ) ) ) ) ==> rd( ld( ld( X, Y ), Y ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (855) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (856) {G1,W15,D5,L1,V3,M1} { rd( rd( X, Y ), rd( Z, Y ) ) ==>
% 0.78/1.52 mult( Y, rd( ld( Y, X ), Z ) ) }.
% 0.78/1.52 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 0.78/1.52 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.52 parent1[0; 10]: (855) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := rd( rd( X, Y ), rd( Z, Y ) )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z,
% 0.78/1.52 X ) ) ==> mult( X, rd( ld( X, Y ), Z ) ) }.
% 0.78/1.52 parent0: (856) {G1,W15,D5,L1,V3,M1} { rd( rd( X, Y ), rd( Z, Y ) ) ==>
% 0.78/1.52 mult( Y, rd( ld( Y, X ), Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (859) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Y ), X ) ==> mult( mult
% 0.78/1.52 ( X, rd( Y, Z ) ), rd( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) )
% 0.78/1.52 , rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (861) {G2,W19,D5,L1,V3,M1} { rd( mult( ld( X, Y ), Z ), ld( X, Y
% 0.78/1.52 ) ) ==> mult( mult( ld( X, Y ), rd( Z, Y ) ), X ) }.
% 0.78/1.52 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 parent1[0; 18]: (859) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Y ), X ) ==>
% 0.78/1.52 mult( mult( X, rd( Y, Z ) ), rd( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, Y )
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 0.78/1.52 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 0.78/1.52 parent0: (861) {G2,W19,D5,L1,V3,M1} { rd( mult( ld( X, Y ), Z ), ld( X, Y
% 0.78/1.52 ) ) ==> mult( mult( ld( X, Y ), rd( Z, Y ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (865) {G12,W15,D5,L1,V2,M1} { ld( Y, rd( X, X ) ) ==> ld( mult(
% 0.78/1.52 mult( X, Y ), Y ), mult( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X )
% 0.78/1.52 , X ), mult( Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (868) {G4,W19,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> ld
% 0.78/1.52 ( rd( mult( X, X ), X ), mult( X, rd( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) )
% 0.78/1.52 , rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 0.78/1.52 parent1[0; 9]: (865) {G12,W15,D5,L1,V2,M1} { ld( Y, rd( X, X ) ) ==> ld(
% 0.78/1.52 mult( mult( X, Y ), Y ), mult( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := rd( X, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (872) {G1,W15,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> ld
% 0.78/1.52 ( X, mult( X, rd( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 9]: (868) {G4,W19,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 0.78/1.52 ==> ld( rd( mult( X, X ), X ), mult( X, rd( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (873) {G1,W11,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> rd
% 0.78/1.52 ( X, X ) }.
% 0.78/1.52 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 8]: (872) {G1,W15,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 0.78/1.52 ==> ld( X, mult( X, rd( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := rd( X, X )
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 0.78/1.52 ), rd( X, X ) ) ==> rd( X, X ) }.
% 0.78/1.52 parent0: (873) {G1,W11,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> rd
% 0.78/1.52 ( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (876) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult( ld( X,
% 0.78/1.52 Y ), Y ) }.
% 0.78/1.52 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 0.78/1.52 ld( ld( Y, X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (879) {G9,W19,D5,L1,V1,M1} { ld( ld( rd( X, X ), rd( X, X ) ), rd
% 0.78/1.52 ( X, X ) ) ==> mult( rd( X, X ), rd( X, X ) ) }.
% 0.78/1.52 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 0.78/1.52 ), rd( X, X ) ) ==> rd( X, X ) }.
% 0.78/1.52 parent1[0; 13]: (876) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult
% 0.78/1.52 ( ld( X, Y ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := rd( X, X )
% 0.78/1.52 Y := rd( X, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (883) {G10,W15,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==>
% 0.78/1.52 mult( rd( X, X ), rd( X, X ) ) }.
% 0.78/1.52 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 0.78/1.52 ), rd( X, X ) ) ==> rd( X, X ) }.
% 0.78/1.52 parent1[0; 2]: (879) {G9,W19,D5,L1,V1,M1} { ld( ld( rd( X, X ), rd( X, X )
% 0.78/1.52 ), rd( X, X ) ) ==> mult( rd( X, X ), rd( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (884) {G11,W11,D4,L1,V1,M1} { rd( X, X ) ==> mult( rd( X, X ), rd
% 0.78/1.52 ( X, X ) ) }.
% 0.78/1.52 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 0.78/1.52 ), rd( X, X ) ) ==> rd( X, X ) }.
% 0.78/1.52 parent1[0; 1]: (883) {G10,W15,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 0.78/1.52 ==> mult( rd( X, X ), rd( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (885) {G11,W11,D4,L1,V1,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 0.78/1.52 rd( X, X ) }.
% 0.78/1.52 parent0[0]: (884) {G11,W11,D4,L1,V1,M1} { rd( X, X ) ==> mult( rd( X, X )
% 0.78/1.52 , rd( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X
% 0.78/1.52 ), rd( X, X ) ) ==> rd( X, X ) }.
% 0.78/1.52 parent0: (885) {G11,W11,D4,L1,V1,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 0.78/1.52 rd( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (888) {G3,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X, mult
% 0.78/1.52 ( mult( Y, rd( Z, X ) ), X ) ) }.
% 0.78/1.52 parent0[0]: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z
% 0.78/1.52 , X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (891) {G4,W15,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X ) ==>
% 0.78/1.52 ld( X, mult( rd( X, X ), X ) ) }.
% 0.78/1.52 parent0[0]: (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X )
% 0.78/1.52 , rd( X, X ) ) ==> rd( X, X ) }.
% 0.78/1.52 parent1[0; 11]: (888) {G3,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld
% 0.78/1.52 ( X, mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := rd( X, X )
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (892) {G1,W11,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X ) ==>
% 0.78/1.52 ld( X, X ) }.
% 0.78/1.52 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 10]: (891) {G4,W15,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X
% 0.78/1.52 ) ==> ld( X, mult( rd( X, X ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (893) {G2,W11,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> ld
% 0.78/1.52 ( X, X ) }.
% 0.78/1.52 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 0.78/1.52 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 0.78/1.52 parent1[0; 1]: (892) {G1,W11,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X )
% 0.78/1.52 ==> ld( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X
% 0.78/1.52 , X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent0: (893) {G2,W11,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> ld
% 0.78/1.52 ( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (896) {G5,W15,D5,L1,V3,M1} { ld( mult( Y, X ), rd( Z, Y ) ) ==> rd
% 0.78/1.52 ( ld( X, ld( Y, Z ) ), Y ) }.
% 0.78/1.52 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 0.78/1.52 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (899) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd( X, X
% 0.78/1.52 ) ) ==> rd( ld( X, X ), X ) }.
% 0.78/1.52 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 0.78/1.52 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 11]: (896) {G5,W15,D5,L1,V3,M1} { ld( mult( Y, X ), rd( Z, Y )
% 0.78/1.52 ) ==> rd( ld( X, ld( Y, Z ) ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := X
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (902) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd( X, X
% 0.78/1.52 ) ) ==> ld( mult( X, X ), X ) }.
% 0.78/1.52 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 0.78/1.52 ( mult( X, Y ), X ) }.
% 0.78/1.52 parent1[0; 10]: (899) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd
% 0.78/1.52 ( X, X ) ) ==> rd( ld( X, X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (903) {G1,W11,D4,L1,V1,M1} { ld( X, rd( X, X ) ) ==> ld( mult( X
% 0.78/1.52 , X ), X ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 2]: (902) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd
% 0.78/1.52 ( X, X ) ) ==> ld( mult( X, X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd(
% 0.78/1.52 X, X ) ) ==> ld( mult( X, X ), X ) }.
% 0.78/1.52 parent0: (903) {G1,W11,D4,L1,V1,M1} { ld( X, rd( X, X ) ) ==> ld( mult( X
% 0.78/1.52 , X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (906) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult( ld( X,
% 0.78/1.52 Y ), Y ) }.
% 0.78/1.52 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 0.78/1.52 ld( ld( Y, X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (909) {G9,W19,D5,L1,V1,M1} { ld( ld( ld( X, X ), ld( X, X ) ), ld
% 0.78/1.52 ( X, X ) ) ==> mult( ld( X, X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 0.78/1.52 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 13]: (906) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult
% 0.78/1.52 ( ld( X, Y ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (913) {G10,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==>
% 0.78/1.52 mult( ld( X, X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 0.78/1.52 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 2]: (909) {G9,W19,D5,L1,V1,M1} { ld( ld( ld( X, X ), ld( X, X )
% 0.78/1.52 ), ld( X, X ) ) ==> mult( ld( X, X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (914) {G11,W11,D4,L1,V1,M1} { ld( X, X ) ==> mult( ld( X, X ), ld
% 0.78/1.52 ( X, X ) ) }.
% 0.78/1.52 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 0.78/1.52 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 1]: (913) {G10,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) )
% 0.78/1.52 ==> mult( ld( X, X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (915) {G11,W11,D4,L1,V1,M1} { mult( ld( X, X ), ld( X, X ) ) ==>
% 0.78/1.52 ld( X, X ) }.
% 0.78/1.52 parent0[0]: (914) {G11,W11,D4,L1,V1,M1} { ld( X, X ) ==> mult( ld( X, X )
% 0.78/1.52 , ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X
% 0.78/1.52 ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent0: (915) {G11,W11,D4,L1,V1,M1} { mult( ld( X, X ), ld( X, X ) ) ==>
% 0.78/1.52 ld( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (918) {G5,W11,D4,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> rd( ld( X,
% 0.78/1.52 Y ), Y ) }.
% 0.78/1.52 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 0.78/1.52 ( mult( X, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (921) {G6,W19,D5,L1,V1,M1} { ld( mult( ld( X, X ), ld( X, X ) ),
% 0.78/1.52 ld( X, X ) ) ==> rd( ld( X, X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 0.78/1.52 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 13]: (918) {G5,W11,D4,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> rd
% 0.78/1.52 ( ld( X, Y ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (922) {G7,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> rd
% 0.78/1.52 ( ld( X, X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 0.78/1.52 , ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 2]: (921) {G6,W19,D5,L1,V1,M1} { ld( mult( ld( X, X ), ld( X, X
% 0.78/1.52 ) ), ld( X, X ) ) ==> rd( ld( X, X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (923) {G8,W11,D4,L1,V1,M1} { ld( X, X ) ==> rd( ld( X, X ), ld( X
% 0.78/1.52 , X ) ) }.
% 0.78/1.52 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 0.78/1.52 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 1]: (922) {G7,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) )
% 0.78/1.52 ==> rd( ld( X, X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (924) {G8,W11,D4,L1,V1,M1} { rd( ld( X, X ), ld( X, X ) ) ==> ld(
% 0.78/1.52 X, X ) }.
% 0.78/1.52 parent0[0]: (923) {G8,W11,D4,L1,V1,M1} { ld( X, X ) ==> rd( ld( X, X ), ld
% 0.78/1.52 ( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld(
% 0.78/1.52 X, X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent0: (924) {G8,W11,D4,L1,V1,M1} { rd( ld( X, X ), ld( X, X ) ) ==> ld
% 0.78/1.52 ( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (926) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X, mult( Y, X
% 0.78/1.52 ) ), mult( ld( Z, Y ), X ) ) }.
% 0.78/1.52 parent0[0]: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 0.78/1.52 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (930) {G11,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld( ld
% 0.78/1.52 ( X, X ), mult( X, ld( X, X ) ) ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 0.78/1.52 , ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 16]: (926) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X,
% 0.78/1.52 mult( Y, X ) ), mult( ld( Z, Y ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := X
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (931) {G12,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> ld( ld( X,
% 0.78/1.52 X ), rd( X, rd( ld( X, X ), ld( X, X ) ) ) ) }.
% 0.78/1.52 parent0[0]: (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y )
% 0.78/1.52 ), X ) ==> ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 0.78/1.52 parent1[0; 6]: (930) {G11,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd(
% 0.78/1.52 ld( ld( X, X ), mult( X, ld( X, X ) ) ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (932) {G13,W15,D5,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld( ld
% 0.78/1.52 ( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y,
% 0.78/1.52 rd( Z, ld( Y, X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 0.78/1.52 parent1[0; 6]: (931) {G12,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> ld(
% 0.78/1.52 ld( X, X ), rd( X, rd( ld( X, X ), ld( X, X ) ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 Z := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (933) {G13,W15,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 0.78/1.52 ) ==> ld( ld( X, X ), X ) }.
% 0.78/1.52 parent0[0]: (932) {G13,W15,D5,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld(
% 0.78/1.52 ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld
% 0.78/1.52 ( ld( X, X ), X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 0.78/1.52 parent0: (933) {G13,W15,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 0.78/1.52 ) ==> ld( ld( X, X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (935) {G1,W19,D6,L1,V3,M1} { mult( ld( X, Y ), mult( Z, Y ) ) ==>
% 0.78/1.52 mult( mult( mult( ld( X, Y ), Z ), X ), ld( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y )
% 0.78/1.52 , Z ), X ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (939) {G2,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X, X ),
% 0.78/1.52 X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 0.78/1.52 , ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 12]: (935) {G1,W19,D6,L1,V3,M1} { mult( ld( X, Y ), mult( Z, Y
% 0.78/1.52 ) ) ==> mult( mult( mult( ld( X, Y ), Z ), X ), ld( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 Z := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (941) {G3,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X, X ),
% 0.78/1.52 X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 0.78/1.52 ld( ld( Y, X ), Y ) }.
% 0.78/1.52 parent1[0; 11]: (939) {G2,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X
% 0.78/1.52 , X ), X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (942) {G4,W19,D5,L1,V1,M1} { mult( ld( X, X ), ld( ld( X, X ), X
% 0.78/1.52 ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 0.78/1.52 ld( ld( Y, X ), Y ) }.
% 0.78/1.52 parent1[0; 5]: (941) {G3,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X
% 0.78/1.52 , X ), X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (943) {G1,W11,D5,L1,V1,M1} { X ==> mult( ld( ld( X, X ), X ), ld
% 0.78/1.52 ( X, X ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 1]: (942) {G4,W19,D5,L1,V1,M1} { mult( ld( X, X ), ld( ld( X, X
% 0.78/1.52 ), X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (944) {G1,W11,D5,L1,V1,M1} { mult( ld( ld( X, X ), X ), ld( X, X )
% 0.78/1.52 ) ==> X }.
% 0.78/1.52 parent0[0]: (943) {G1,W11,D5,L1,V1,M1} { X ==> mult( ld( ld( X, X ), X ),
% 0.78/1.52 ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld(
% 0.78/1.52 ld( X, X ), X ), ld( X, X ) ) ==> X }.
% 0.78/1.52 parent0: (944) {G1,W11,D5,L1,V1,M1} { mult( ld( ld( X, X ), X ), ld( X, X
% 0.78/1.52 ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (946) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Z ), X ) ==> mult( mult
% 0.78/1.52 ( X, Y ), rd( ld( Y, Z ), X ) ) }.
% 0.78/1.52 parent0[0]: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 0.78/1.52 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (950) {G4,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld( X, X
% 0.78/1.52 ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld( X
% 0.78/1.52 , X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 16]: (946) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Z ), X ) ==>
% 0.78/1.52 mult( mult( X, Y ), rd( ld( Y, Z ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := X
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (952) {G5,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld( X, X
% 0.78/1.52 ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 0.78/1.52 ld( ld( Y, X ), Y ) }.
% 0.78/1.52 parent1[0; 11]: (950) {G4,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld
% 0.78/1.52 ( X, X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (953) {G6,W19,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 0.78/1.52 ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 0.78/1.52 ld( ld( Y, X ), Y ) }.
% 0.78/1.52 parent1[0; 2]: (952) {G5,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld
% 0.78/1.52 ( X, X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (955) {G7,W11,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 0.78/1.52 ) ==> X }.
% 0.78/1.52 parent0[0]: (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld( ld
% 0.78/1.52 ( X, X ), X ), ld( X, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 10]: (953) {G6,W19,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld(
% 0.78/1.52 X, X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (956) {G8,W7,D4,L1,V1,M1} { ld( ld( X, X ), X ) ==> X }.
% 0.78/1.52 parent0[0]: (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld(
% 0.78/1.52 ld( X, X ), X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 0.78/1.52 parent1[0; 1]: (955) {G7,W11,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X
% 0.78/1.52 , X ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld
% 0.78/1.52 ( ld( X, X ), X ) ==> X }.
% 0.78/1.52 parent0: (956) {G8,W7,D4,L1,V1,M1} { ld( ld( X, X ), X ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (959) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 0.78/1.52 ( ld( X, Y ), mult( Z, X ) ) }.
% 0.78/1.52 parent0[0]: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 0.78/1.52 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (961) {G13,W19,D6,L1,V2,M1} { ld( ld( X, X ), rd( rd( X, ld( X, X
% 0.78/1.52 ) ), Y ) ) ==> rd( X, mult( Y, ld( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 0.78/1.52 ld( X, X ), X ) ==> X }.
% 0.78/1.52 parent1[0; 13]: (959) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) )
% 0.78/1.52 ==> rd( ld( X, Y ), mult( Z, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (962) {G2,W15,D5,L1,V2,M1} { ld( ld( X, X ), rd( X, Y ) ) ==> rd
% 0.78/1.52 ( X, mult( Y, ld( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 parent1[0; 6]: (961) {G13,W19,D6,L1,V2,M1} { ld( ld( X, X ), rd( rd( X, ld
% 0.78/1.52 ( X, X ) ), Y ) ) ==> rd( X, mult( Y, ld( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (963) {G2,W15,D5,L1,V2,M1} { rd( X, mult( Y, ld( X, X ) ) ) ==> ld
% 0.78/1.52 ( ld( X, X ), rd( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (962) {G2,W15,D5,L1,V2,M1} { ld( ld( X, X ), rd( X, Y ) ) ==>
% 0.78/1.52 rd( X, mult( Y, ld( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y,
% 0.78/1.52 ld( X, X ) ) ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 0.78/1.52 parent0: (963) {G2,W15,D5,L1,V2,M1} { rd( X, mult( Y, ld( X, X ) ) ) ==>
% 0.78/1.52 ld( ld( X, X ), rd( X, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (965) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) ) ==> rd
% 0.78/1.52 ( ld( ld( X, Y ), Z ), X ) }.
% 0.78/1.52 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 0.78/1.52 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (968) {G6,W11,D5,L1,V1,M1} { ld( X, rd( mult( X, X ), X ) ) ==>
% 0.78/1.52 rd( X, X ) }.
% 0.78/1.52 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 0.78/1.52 ld( X, X ), X ) ==> X }.
% 0.78/1.52 parent1[0; 9]: (965) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) )
% 0.78/1.52 ==> rd( ld( ld( X, Y ), Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (970) {G1,W7,D3,L1,V1,M1} { ld( X, X ) ==> rd( X, X ) }.
% 0.78/1.52 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 3]: (968) {G6,W11,D5,L1,V1,M1} { ld( X, rd( mult( X, X ), X ) )
% 0.78/1.52 ==> rd( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (971) {G1,W7,D3,L1,V1,M1} { rd( X, X ) ==> ld( X, X ) }.
% 0.78/1.52 parent0[0]: (970) {G1,W7,D3,L1,V1,M1} { ld( X, X ) ==> rd( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld
% 0.78/1.52 ( X, X ) }.
% 0.78/1.52 parent0: (971) {G1,W7,D3,L1,V1,M1} { rd( X, X ) ==> ld( X, X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (973) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) ) ==> rd
% 0.78/1.52 ( ld( ld( X, Y ), Z ), X ) }.
% 0.78/1.52 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 0.78/1.52 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (978) {G6,W19,D6,L1,V2,M1} { ld( X, rd( mult( ld( X, X ), Y ), ld
% 0.78/1.52 ( X, X ) ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 0.78/1.52 ld( X, X ), X ) ==> X }.
% 0.78/1.52 parent1[0; 14]: (973) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X )
% 0.78/1.52 ) ==> rd( ld( ld( X, Y ), Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (979) {G5,W19,D6,L1,V2,M1} { ld( X, mult( mult( ld( X, X ), rd( Y
% 0.78/1.52 , X ) ), X ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 0.78/1.52 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 0.78/1.52 parent1[0; 3]: (978) {G6,W19,D6,L1,V2,M1} { ld( X, rd( mult( ld( X, X ), Y
% 0.78/1.52 ), ld( X, X ) ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (980) {G4,W15,D5,L1,V2,M1} { mult( ld( X, ld( X, X ) ), Y ) ==>
% 0.78/1.52 rd( ld( X, Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z
% 0.78/1.52 , X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 0.78/1.52 parent1[0; 1]: (979) {G5,W19,D6,L1,V2,M1} { ld( X, mult( mult( ld( X, X )
% 0.78/1.52 , rd( Y, X ) ), X ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (981) {G4,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==> mult
% 0.78/1.52 ( ld( X, ld( X, X ) ), Y ) }.
% 0.78/1.52 parent0[0]: (980) {G4,W15,D5,L1,V2,M1} { mult( ld( X, ld( X, X ) ), Y )
% 0.78/1.52 ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld( X
% 0.78/1.52 , Y ), ld( X, X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 0.78/1.52 parent0: (981) {G4,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 0.78/1.52 mult( ld( X, ld( X, X ) ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (983) {G16,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X, rd
% 0.78/1.52 ( X, X ) ) }.
% 0.78/1.52 parent0[0]: (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd( X
% 0.78/1.52 , X ) ) ==> ld( mult( X, X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (984) {G17,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X, ld
% 0.78/1.52 ( X, X ) ) }.
% 0.78/1.52 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 0.78/1.52 X, X ) }.
% 0.78/1.52 parent1[0; 8]: (983) {G16,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld
% 0.78/1.52 ( X, rd( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (985) {G17,W11,D4,L1,V1,M1} { ld( X, ld( X, X ) ) ==> ld( mult( X
% 0.78/1.52 , X ), X ) }.
% 0.78/1.52 parent0[0]: (984) {G17,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X
% 0.78/1.52 , ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) )
% 0.78/1.52 ==> ld( mult( X, X ), X ) }.
% 0.78/1.52 parent0: (985) {G17,W11,D4,L1,V1,M1} { ld( X, ld( X, X ) ) ==> ld( mult( X
% 0.78/1.52 , X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 *** allocated 22500 integers for termspace/termends
% 0.78/1.52 eqswap: (987) {G14,W15,D5,L1,V3,M1} { mult( Y, rd( ld( Y, X ), Z ) ) ==>
% 0.78/1.52 rd( rd( X, Y ), rd( Z, Y ) ) }.
% 0.78/1.52 parent0[0]: (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z, X
% 0.78/1.52 ) ) ==> mult( X, rd( ld( X, Y ), Z ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (993) {G15,W15,D5,L1,V2,M1} { mult( X, rd( ld( X, Y ), X ) ) ==>
% 0.78/1.52 rd( rd( Y, X ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 0.78/1.52 X, X ) }.
% 0.78/1.52 parent1[0; 12]: (987) {G14,W15,D5,L1,V3,M1} { mult( Y, rd( ld( Y, X ), Z )
% 0.78/1.52 ) ==> rd( rd( X, Y ), rd( Z, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (997) {G15,W15,D5,L1,V2,M1} { rd( rd( Y, X ), ld( X, X ) ) ==>
% 0.78/1.52 mult( X, rd( ld( X, Y ), X ) ) }.
% 0.78/1.52 parent0[0]: (993) {G15,W15,D5,L1,V2,M1} { mult( X, rd( ld( X, Y ), X ) )
% 0.78/1.52 ==> rd( rd( Y, X ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X
% 0.78/1.52 , X ) ) ==> mult( X, rd( ld( X, Y ), X ) ) }.
% 0.78/1.52 parent0: (997) {G15,W15,D5,L1,V2,M1} { rd( rd( Y, X ), ld( X, X ) ) ==>
% 0.78/1.52 mult( X, rd( ld( X, Y ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (999) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X, rd(
% 0.78/1.52 rd( Y, X ), rd( Z, X ) ) ) }.
% 0.78/1.52 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 0.78/1.52 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1002) {G14,W15,D5,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( X, ld
% 0.78/1.52 ( rd( Y, X ), rd( Y, X ) ) ) }.
% 0.78/1.52 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 0.78/1.52 X, X ) }.
% 0.78/1.52 parent1[0; 8]: (999) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X
% 0.78/1.52 , rd( rd( Y, X ), rd( Z, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := rd( Y, X )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1005) {G6,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X, ld
% 0.78/1.52 ( rd( Y, X ), rd( Y, X ) ) ) }.
% 0.78/1.52 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 0.78/1.52 ( mult( X, Y ), X ) }.
% 0.78/1.52 parent1[0; 1]: (1002) {G14,W15,D5,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld(
% 0.78/1.52 X, ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1006) {G6,W15,D5,L1,V2,M1} { ld( Y, ld( rd( X, Y ), rd( X, Y ) )
% 0.78/1.52 ) ==> ld( mult( X, Y ), X ) }.
% 0.78/1.52 parent0[0]: (1005) {G6,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X
% 0.78/1.52 , ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd(
% 0.78/1.52 X, Y ), rd( X, Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 0.78/1.52 parent0: (1006) {G6,W15,D5,L1,V2,M1} { ld( Y, ld( rd( X, Y ), rd( X, Y ) )
% 0.78/1.52 ) ==> ld( mult( X, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1008) {G20,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X, ld
% 0.78/1.52 ( rd( Y, X ), rd( Y, X ) ) ) }.
% 0.78/1.52 parent0[0]: (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd( X
% 0.78/1.52 , Y ), rd( X, Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1012) {G2,W19,D6,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X ) ==>
% 0.78/1.52 ld( ld( Y, X ), ld( rd( X, ld( Y, X ) ), Y ) ) }.
% 0.78/1.52 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 parent1[0; 18]: (1008) {G20,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==>
% 0.78/1.52 ld( X, ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( Y, X )
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1013) {G2,W15,D5,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X ) ==>
% 0.78/1.52 ld( ld( Y, X ), ld( Y, Y ) ) }.
% 0.78/1.52 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 parent1[0; 13]: (1012) {G2,W19,D6,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X
% 0.78/1.52 ) ==> ld( ld( Y, X ), ld( rd( X, ld( Y, X ) ), Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1015) {G2,W15,D5,L1,V2,M1} { ld( ld( Y, X ), ld( Y, Y ) ) ==> ld
% 0.78/1.52 ( mult( X, ld( Y, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (1013) {G2,W15,D5,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X )
% 0.78/1.52 ==> ld( ld( Y, X ), ld( Y, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (321) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y,
% 0.78/1.52 Y ) ) = ld( mult( X, ld( Y, X ) ), X ) }.
% 0.78/1.52 parent0: (1015) {G2,W15,D5,L1,V2,M1} { ld( ld( Y, X ), ld( Y, Y ) ) ==> ld
% 0.78/1.52 ( mult( X, ld( Y, X ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1018) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 0.78/1.52 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1019) {G2,W15,D5,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> ld( ld(
% 0.78/1.52 ld( Y, Y ), rd( Y, X ) ), Y ) }.
% 0.78/1.52 parent0[0]: (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y,
% 0.78/1.52 ld( X, X ) ) ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 0.78/1.52 parent1[0; 7]: (1018) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := mult( X, ld( Y, Y ) )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1020) {G2,W15,D5,L1,V2,M1} { ld( ld( ld( Y, Y ), rd( Y, X ) ), Y
% 0.78/1.52 ) ==> mult( X, ld( Y, Y ) ) }.
% 0.78/1.52 parent0[0]: (1019) {G2,W15,D5,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> ld( ld
% 0.78/1.52 ( ld( Y, Y ), rd( Y, X ) ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (363) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd
% 0.78/1.52 ( X, Y ) ), X ) ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 parent0: (1020) {G2,W15,D5,L1,V2,M1} { ld( ld( ld( Y, Y ), rd( Y, X ) ), Y
% 0.78/1.52 ) ==> mult( X, ld( Y, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1022) {G20,W15,D5,L1,V2,M1} { mult( Y, ld( X, X ) ) ==> ld( ld(
% 0.78/1.52 ld( X, X ), rd( X, Y ) ), X ) }.
% 0.78/1.52 parent0[0]: (363) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd(
% 0.78/1.52 X, Y ) ), X ) ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1025) {G2,W15,D5,L1,V2,M1} { mult( ld( X, Y ), ld( Y, Y ) ) ==>
% 0.78/1.52 ld( ld( ld( Y, Y ), X ), Y ) }.
% 0.78/1.52 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.78/1.52 parent1[0; 13]: (1022) {G20,W15,D5,L1,V2,M1} { mult( Y, ld( X, X ) ) ==>
% 0.78/1.52 ld( ld( ld( X, X ), rd( X, Y ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := ld( X, Y )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X
% 0.78/1.52 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 0.78/1.52 parent0: (1025) {G2,W15,D5,L1,V2,M1} { mult( ld( X, Y ), ld( Y, Y ) ) ==>
% 0.78/1.52 ld( ld( ld( Y, Y ), X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1029) {G20,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 0.78/1.52 mult( ld( mult( X, X ), X ), Y ) }.
% 0.78/1.52 parent0[0]: (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) )
% 0.78/1.52 ==> ld( mult( X, X ), X ) }.
% 0.78/1.52 parent1[0; 9]: (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld
% 0.78/1.52 ( X, Y ), ld( X, X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (539) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld
% 0.78/1.52 ( X, X ) ) ==> mult( ld( mult( X, X ), X ), Y ) }.
% 0.78/1.52 parent0: (1029) {G20,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 0.78/1.52 mult( ld( mult( X, X ), X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1032) {G21,W15,D5,L1,V2,M1} { mult( ld( mult( X, X ), X ), Y )
% 0.78/1.52 ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (539) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld
% 0.78/1.52 ( X, X ) ) ==> mult( ld( mult( X, X ), X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1040) {G22,W27,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ), ld( X
% 0.78/1.52 , X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( mult( X, ld(
% 0.78/1.52 X, X ) ), X ) ) }.
% 0.78/1.52 parent0[0]: (321) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y, Y
% 0.78/1.52 ) ) = ld( mult( X, ld( Y, X ) ), X ) }.
% 0.78/1.52 parent1[0; 20]: (1032) {G21,W15,D5,L1,V2,M1} { mult( ld( mult( X, X ), X )
% 0.78/1.52 , Y ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1041) {G1,W23,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ), ld( X,
% 0.78/1.52 X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 21]: (1040) {G22,W27,D6,L1,V2,M1} { mult( ld( mult( ld( X, X )
% 0.78/1.52 , ld( X, X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( mult(
% 0.78/1.52 X, ld( X, X ) ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1042) {G2,W23,D7,L1,V2,M1} { mult( ld( ld( ld( ld( X, X ), X ),
% 0.78/1.52 X ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X
% 0.78/1.52 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 0.78/1.52 parent1[0; 3]: (1041) {G1,W23,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ),
% 0.78/1.52 ld( X, X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1043) {G3,W19,D5,L1,V2,M1} { mult( ld( ld( X, X ), ld( X, X ) )
% 0.78/1.52 , Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 0.78/1.52 ld( X, X ), X ) ==> X }.
% 0.78/1.52 parent1[0; 4]: (1042) {G2,W23,D7,L1,V2,M1} { mult( ld( ld( ld( ld( X, X )
% 0.78/1.52 , X ), X ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1044) {G4,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld(
% 0.78/1.52 ld( X, X ), Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 0.78/1.52 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 2]: (1043) {G3,W19,D5,L1,V2,M1} { mult( ld( ld( X, X ), ld( X,
% 0.78/1.52 X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1045) {G4,W15,D5,L1,V2,M1} { rd( ld( ld( X, X ), Y ), ld( X, X )
% 0.78/1.52 ) ==> mult( ld( X, X ), Y ) }.
% 0.78/1.52 parent0[0]: (1044) {G4,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld
% 0.78/1.52 ( ld( X, X ), Y ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(
% 0.78/1.52 212) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y )
% 0.78/1.52 }.
% 0.78/1.52 parent0: (1045) {G4,W15,D5,L1,V2,M1} { rd( ld( ld( X, X ), Y ), ld( X, X )
% 0.78/1.52 ) ==> mult( ld( X, X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1047) {G20,W15,D5,L1,V2,M1} { mult( Y, rd( ld( Y, X ), Y ) ) ==>
% 0.78/1.52 rd( rd( X, Y ), ld( Y, Y ) ) }.
% 0.78/1.52 parent0[0]: (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X
% 0.78/1.52 , X ) ) ==> mult( X, rd( ld( X, Y ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1055) {G21,W31,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 0.78/1.52 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X ), Y ),
% 0.78/1.52 ld( ld( X, X ), ld( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(212
% 0.78/1.52 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 0.78/1.52 parent1[0; 19]: (1047) {G20,W15,D5,L1,V2,M1} { mult( Y, rd( ld( Y, X ), Y
% 0.78/1.52 ) ) ==> rd( rd( X, Y ), ld( Y, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( ld( X, X ), Y )
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1057) {G16,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 0.78/1.52 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X ), Y ),
% 0.78/1.52 ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 0.78/1.52 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 0.78/1.52 parent1[0; 24]: (1055) {G21,W31,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld(
% 0.78/1.52 ld( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X
% 0.78/1.52 ), Y ), ld( ld( X, X ), ld( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1058) {G5,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 0.78/1.52 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> mult( mult( ld( X, X ), rd
% 0.78/1.52 ( Y, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 0.78/1.52 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 0.78/1.52 parent1[0; 18]: (1057) {G16,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld(
% 0.78/1.52 ld( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X
% 0.78/1.52 ), Y ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1059) {G6,W27,D6,L1,V2,M1} { mult( ld( X, X ), ld( mult( ld( X,
% 0.78/1.52 X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd
% 0.78/1.52 ( Y, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 0.78/1.52 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 0.78/1.52 parent1[0; 5]: (1058) {G5,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld
% 0.78/1.52 ( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> mult( mult( ld( X, X
% 0.78/1.52 ), rd( Y, X ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1060) {G7,W27,D7,L1,V2,M1} { mult( ld( X, X ), ld( ld( ld( ld( X
% 0.78/1.52 , X ), X ), X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd(
% 0.78/1.52 Y, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X
% 0.78/1.52 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 0.78/1.52 parent1[0; 6]: (1059) {G6,W27,D6,L1,V2,M1} { mult( ld( X, X ), ld( mult(
% 0.78/1.52 ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X,
% 0.78/1.52 X ), rd( Y, X ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1061) {G8,W23,D6,L1,V2,M1} { mult( ld( X, X ), ld( ld( X, X ),
% 0.78/1.52 rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd( Y, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 0.78/1.52 ld( X, X ), X ) ==> X }.
% 0.78/1.52 parent1[0; 7]: (1060) {G7,W27,D7,L1,V2,M1} { mult( ld( X, X ), ld( ld( ld
% 0.78/1.52 ( ld( X, X ), X ), X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X
% 0.78/1.52 ), rd( Y, X ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1062) {G1,W15,D5,L1,V2,M1} { rd( Y, ld( X, X ) ) ==> mult( mult
% 0.78/1.52 ( ld( X, X ), rd( Y, X ) ), X ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 1]: (1061) {G8,W23,D6,L1,V2,M1} { mult( ld( X, X ), ld( ld( X,
% 0.78/1.52 X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd( Y, X ) ), X
% 0.78/1.52 ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := rd( Y, ld( X, X ) )
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1063) {G1,W15,D5,L1,V2,M1} { mult( mult( ld( Y, Y ), rd( X, Y ) )
% 0.78/1.52 , Y ) ==> rd( X, ld( Y, Y ) ) }.
% 0.78/1.52 parent0[0]: (1062) {G1,W15,D5,L1,V2,M1} { rd( Y, ld( X, X ) ) ==> mult(
% 0.78/1.52 mult( ld( X, X ), rd( Y, X ) ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (553) {G23,W15,D5,L1,V2,M1} P(543,270);d(212);d(194);d(38);d(
% 0.78/1.52 366);d(242);d(0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y,
% 0.78/1.52 ld( X, X ) ) }.
% 0.78/1.52 parent0: (1063) {G1,W15,D5,L1,V2,M1} { mult( mult( ld( Y, Y ), rd( X, Y )
% 0.78/1.52 ), Y ) ==> rd( X, ld( Y, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1064) {G22,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld(
% 0.78/1.52 ld( X, X ), Y ), ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(212
% 0.78/1.52 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1069) {G6,W23,D5,L1,V2,M1} { mult( ld( X, X ), ld( ld( X, X ), Y
% 0.78/1.52 ) ) ==> ld( mult( ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 0.78/1.52 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 0.78/1.52 parent1[0; 10]: (1064) {G22,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==>
% 0.78/1.52 rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( ld( X, X ), Y )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1070) {G1,W15,D5,L1,V2,M1} { Y ==> ld( mult( ld( X, X ), ld( X,
% 0.78/1.52 X ) ), rd( Y, ld( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 1]: (1069) {G6,W23,D5,L1,V2,M1} { mult( ld( X, X ), ld( ld( X,
% 0.78/1.52 X ), Y ) ) ==> ld( mult( ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1071) {G2,W15,D6,L1,V2,M1} { X ==> ld( ld( ld( ld( Y, Y ), Y ),
% 0.78/1.52 Y ), rd( X, ld( Y, Y ) ) ) }.
% 0.78/1.52 parent0[0]: (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X
% 0.78/1.52 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 0.78/1.52 parent1[0; 3]: (1070) {G1,W15,D5,L1,V2,M1} { Y ==> ld( mult( ld( X, X ),
% 0.78/1.52 ld( X, X ) ), rd( Y, ld( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1072) {G3,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, Y ), rd( X, ld( Y
% 0.78/1.52 , Y ) ) ) }.
% 0.78/1.52 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 0.78/1.52 ld( X, X ), X ) ==> X }.
% 0.78/1.52 parent1[0; 4]: (1071) {G2,W15,D6,L1,V2,M1} { X ==> ld( ld( ld( ld( Y, Y )
% 0.78/1.52 , Y ), Y ), rd( X, ld( Y, Y ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1073) {G3,W11,D5,L1,V2,M1} { ld( ld( Y, Y ), rd( X, ld( Y, Y ) )
% 0.78/1.52 ) ==> X }.
% 0.78/1.52 parent0[0]: (1072) {G3,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, Y ), rd( X, ld
% 0.78/1.52 ( Y, Y ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld
% 0.78/1.52 ( ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 0.78/1.52 parent0: (1073) {G3,W11,D5,L1,V2,M1} { ld( ld( Y, Y ), rd( X, ld( Y, Y ) )
% 0.78/1.52 ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1075) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y, ld( X
% 0.78/1.52 , X ) ) ) }.
% 0.78/1.52 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 0.78/1.52 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1078) {G23,W15,D5,L1,V2,M1} { ld( ld( X, X ), Y ) ==> ld( ld( X
% 0.78/1.52 , X ), mult( ld( X, X ), Y ) ) }.
% 0.78/1.52 parent0[0]: (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(212
% 0.78/1.52 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 0.78/1.52 parent1[0; 10]: (1075) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y
% 0.78/1.52 , ld( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( ld( X, X ), Y )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1079) {G1,W7,D4,L1,V2,M1} { ld( ld( X, X ), Y ) ==> Y }.
% 0.78/1.52 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.78/1.52 parent1[0; 6]: (1078) {G23,W15,D5,L1,V2,M1} { ld( ld( X, X ), Y ) ==> ld(
% 0.78/1.52 ld( X, X ), mult( ld( X, X ), Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 0.78/1.52 ) ==> Y }.
% 0.78/1.52 parent0: (1079) {G1,W7,D4,L1,V2,M1} { ld( ld( X, X ), Y ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1082) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) ) ==>
% 0.78/1.52 mult( ld( X, rd( Y, Z ) ), Z ) }.
% 0.78/1.52 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 0.78/1.52 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1087) {G9,W19,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X ) ),
% 0.78/1.52 ld( ld( X, X ), Y ) ) ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 0.78/1.52 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 0.78/1.52 parent1[0; 15]: (1082) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) )
% 0.78/1.52 ==> mult( ld( X, rd( Y, Z ) ), Z ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := ld( X, X )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1090) {G10,W15,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X ) ),
% 0.78/1.52 Y ) ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 0.78/1.52 ) ==> Y }.
% 0.78/1.52 parent1[0; 9]: (1087) {G9,W19,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X
% 0.78/1.52 ) ), ld( ld( X, X ), Y ) ) ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1092) {G11,W7,D4,L1,V2,M1} { Y ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 0.78/1.52 ) ==> Y }.
% 0.78/1.52 parent1[0; 1]: (1090) {G10,W15,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X
% 0.78/1.52 ) ), Y ) ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1094) {G11,W7,D4,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> X }.
% 0.78/1.52 parent0[0]: (1092) {G11,W7,D4,L1,V2,M1} { Y ==> mult( Y, ld( X, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (583) {G25,W7,D4,L1,V2,M1} P(557,129);d(564);d(564) { mult( Y
% 0.78/1.52 , ld( X, X ) ) ==> Y }.
% 0.78/1.52 parent0: (1094) {G11,W7,D4,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1097) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y, ld( X
% 0.78/1.52 , X ) ) ) }.
% 0.78/1.52 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 0.78/1.52 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1107) {G6,W23,D7,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 0.78/1.52 ( ld( X, X ), ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) ) }.
% 0.78/1.52 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 0.78/1.52 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 0.78/1.52 parent1[0; 12]: (1097) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y
% 0.78/1.52 , ld( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := ld( X, X )
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( ld( ld( X, X ), Y ), Z )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1109) {G7,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 0.78/1.52 ( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 0.78/1.52 ) ==> Y }.
% 0.78/1.52 parent1[0; 8]: (1107) {G6,W23,D7,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 0.78/1.52 ==> ld( ld( X, X ), ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1111) {G5,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 0.78/1.52 ( Y, mult( mult( ld( X, X ), rd( Z, X ) ), X ) ) }.
% 0.78/1.52 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 0.78/1.52 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 0.78/1.52 parent1[0; 10]: (1109) {G7,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 0.78/1.52 ==> ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1112) {G6,W15,D5,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 0.78/1.52 ( Y, rd( Z, ld( X, X ) ) ) }.
% 0.78/1.52 parent0[0]: (553) {G23,W15,D5,L1,V2,M1} P(543,270);d(212);d(194);d(38);d(
% 0.78/1.52 366);d(242);d(0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y,
% 0.78/1.52 ld( X, X ) ) }.
% 0.78/1.52 parent1[0; 10]: (1111) {G5,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 0.78/1.52 ==> ld( Y, mult( mult( ld( X, X ), rd( Z, X ) ), X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Z
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1113) {G7,W11,D5,L1,V3,M1} { ld( Y, Z ) ==> ld( Y, rd( Z, ld( X
% 0.78/1.52 , X ) ) ) }.
% 0.78/1.52 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 0.78/1.52 ) ==> Y }.
% 0.78/1.52 parent1[0; 2]: (1112) {G6,W15,D5,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 0.78/1.52 ==> ld( Y, rd( Z, ld( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 Z := Z
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1114) {G7,W11,D5,L1,V3,M1} { ld( X, rd( Y, ld( Z, Z ) ) ) ==> ld
% 0.78/1.52 ( X, Y ) }.
% 0.78/1.52 parent0[0]: (1113) {G7,W11,D5,L1,V3,M1} { ld( Y, Z ) ==> ld( Y, rd( Z, ld
% 0.78/1.52 ( X, X ) ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Z
% 0.78/1.52 Y := X
% 0.78/1.52 Z := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (590) {G25,W11,D5,L1,V3,M1} P(37,557);d(564);d(194);d(553);d(
% 0.78/1.52 564) { ld( Y, rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 0.78/1.52 parent0: (1114) {G7,W11,D5,L1,V3,M1} { ld( X, rd( Y, ld( Z, Z ) ) ) ==> ld
% 0.78/1.52 ( X, Y ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := Z
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1116) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld
% 0.78/1.52 ( Y, X ) ) }.
% 0.78/1.52 parent0[0]: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ),
% 0.78/1.52 ld( X, Y ) ) ==> Y }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1121) {G7,W23,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld(
% 0.78/1.52 mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), rd( X, ld( Y, Y ) ) ), X ) }.
% 0.78/1.52 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 0.78/1.52 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 0.78/1.52 parent1[0; 22]: (1116) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ),
% 0.78/1.52 X ), ld( Y, X ) ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := rd( X, ld( Y, Y ) )
% 0.78/1.52 Y := ld( Y, Y )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1122) {G8,W19,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld(
% 0.78/1.52 mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), X ), X ) }.
% 0.78/1.52 parent0[0]: (590) {G25,W11,D5,L1,V3,M1} P(37,557);d(564);d(194);d(553);d(
% 0.78/1.52 564) { ld( Y, rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 0.78/1.52 parent1[0; 7]: (1121) {G7,W23,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 0.78/1.52 ld( mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), rd( X, ld( Y, Y ) ) ), X )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) )
% 0.78/1.52 Z := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1123) {G9,W15,D6,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld( rd
% 0.78/1.52 ( X, ld( Y, Y ) ), X ), X ) }.
% 0.78/1.52 parent0[0]: (583) {G25,W7,D4,L1,V2,M1} P(557,129);d(564);d(564) { mult( Y,
% 0.78/1.52 ld( X, X ) ) ==> Y }.
% 0.78/1.52 parent1[0; 8]: (1122) {G8,W19,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 0.78/1.52 ld( mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := rd( X, ld( Y, Y ) )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1124) {G2,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld( Y,
% 0.78/1.52 Y ), X ) }.
% 0.78/1.52 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.78/1.52 parent1[0; 7]: (1123) {G9,W15,D6,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 0.78/1.52 ld( rd( X, ld( Y, Y ) ), X ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := ld( Y, Y )
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1125) {G3,W7,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> X }.
% 0.78/1.52 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 0.78/1.52 ) ==> Y }.
% 0.78/1.52 parent1[0; 6]: (1124) {G2,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 0.78/1.52 ld( Y, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 subsumption: (594) {G26,W7,D4,L1,V2,M1} P(557,43);d(590);d(583);d(6);d(564)
% 0.78/1.52 { rd( Y, ld( X, X ) ) ==> Y }.
% 0.78/1.52 parent0: (1125) {G3,W7,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 permutation0:
% 0.78/1.52 0 ==> 0
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1128) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 0.78/1.52 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1130) {G1,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> mult( ld( Y
% 0.78/1.52 , Y ), X ) }.
% 0.78/1.52 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 0.78/1.52 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 0.78/1.52 parent1[0; 10]: (1128) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 0.78/1.52 }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := ld( Y, Y )
% 0.78/1.52 Y := rd( X, ld( Y, Y ) )
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 paramod: (1131) {G2,W7,D4,L1,V2,M1} { X ==> mult( ld( Y, Y ), X ) }.
% 0.78/1.52 parent0[0]: (594) {G26,W7,D4,L1,V2,M1} P(557,43);d(590);d(583);d(6);d(564)
% 0.78/1.52 { rd( Y, ld( X, X ) ) ==> Y }.
% 0.78/1.52 parent1[0; 1]: (1130) {G1,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> mult
% 0.78/1.52 ( ld( Y, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := Y
% 0.78/1.52 Y := X
% 0.78/1.52 end
% 0.78/1.52 substitution1:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.52
% 0.78/1.52 eqswap: (1132) {G2,W7,D4,L1,V2,M1} { mult( ld( Y, Y ), X ) ==> X }.
% 0.78/1.52 parent0[0]: (1131) {G2,W7,D4,L1,V2,M1} { X ==> mult( ld( Y, Y ), X ) }.
% 0.78/1.52 substitution0:
% 0.78/1.52 X := X
% 0.78/1.52 Y := Y
% 0.78/1.52 end
% 0.78/1.53
% 0.78/1.53 subsumption: (598) {G27,W7,D4,L1,V2,M1} P(557,0);d(594) { mult( ld( X, X )
% 0.78/1.53 , Y ) ==> Y }.
% 0.78/1.53 parent0: (1132) {G2,W7,D4,L1,V2,M1} { mult( ld( Y, Y ), X ) ==> X }.
% 0.78/1.53 substitution0:
% 0.78/1.53 X := Y
% 0.78/1.53 Y := X
% 0.78/1.53 end
% 0.78/1.53 permutation0:
% 0.78/1.53 0 ==> 0
% 0.78/1.53 end
% 0.78/1.53
% 0.78/1.53 eqswap: (1133) {G25,W7,D4,L1,V2,M1} { X ==> mult( X, ld( Y, Y ) ) }.
% 0.78/1.53 parent0[0]: (583) {G25,W7,D4,L1,V2,M1} P(557,129);d(564);d(564) { mult( Y,
% 0.78/1.53 ld( X, X ) ) ==> Y }.
% 0.78/1.53 substitution0:
% 0.78/1.53 X := Y
% 0.78/1.53 Y := X
% 0.78/1.53 end
% 0.78/1.53
% 0.78/1.53 eqswap: (1134) {G0,W14,D4,L2,V1,M2} { ! skol1( X ) ==> mult( skol1( X ), X
% 0.78/1.53 ), ! mult( X, skol1( X ) ) ==> skol1( X ) }.
% 0.78/1.53 parent0[0]: (5) {G0,W14,D4,L2,V1,M2} I { ! mult( skol1( X ), X ) ==> skol1
% 0.78/1.53 ( X ), ! mult( X, skol1( X ) ) ==> skol1( X ) }.
% 0.78/1.53 substitution0:
% 0.78/1.53 X := X
% 0.78/1.53 end
% 0.78/1.53
% 0.78/1.53 resolution: (1138) {G1,W13,D5,L1,V1,M1} { ! mult( ld( X, X ), skol1( ld( X
% 0.78/1.53 , X ) ) ) ==> skol1( ld( X, X ) ) }.
% 0.78/1.53 parent0[0]: (1134) {G0,W14,D4,L2,V1,M2} { ! skol1( X ) ==> mult( skol1( X
% 0.78/1.53 ), X ), ! mult( X, skol1( X ) ) ==> skol1( X ) }.
% 0.78/1.53 parent1[0]: (1133) {G25,W7,D4,L1,V2,M1} { X ==> mult( X, ld( Y, Y ) ) }.
% 0.78/1.53 substitution0:
% 0.78/1.53 X := ld( X, X )
% 0.78/1.53 end
% 0.78/1.53 substitution1:
% 0.78/1.53 X := skol1( ld( X, X ) )
% 0.78/1.53 Y := X
% 0.78/1.53 end
% 0.78/1.53
% 0.78/1.53 paramod: (1139) {G2,W9,D4,L1,V1,M1} { ! skol1( ld( X, X ) ) ==> skol1( ld
% 0.78/1.53 ( X, X ) ) }.
% 0.78/1.53 parent0[0]: (598) {G27,W7,D4,L1,V2,M1} P(557,0);d(594) { mult( ld( X, X ),
% 0.78/1.53 Y ) ==> Y }.
% 0.78/1.53 parent1[0; 2]: (1138) {G1,W13,D5,L1,V1,M1} { ! mult( ld( X, X ), skol1( ld
% 0.78/1.53 ( X, X ) ) ) ==> skol1( ld( X, X ) ) }.
% 0.78/1.53 substitution0:
% 0.78/1.53 X := X
% 0.78/1.53 Y := skol1( ld( X, X ) )
% 0.78/1.53 end
% 0.78/1.53 substitution1:
% 0.78/1.53 X := X
% 0.78/1.53 end
% 0.78/1.53
% 0.78/1.53 eqrefl: (1140) {G0,W0,D0,L0,V0,M0} { }.
% 0.78/1.53 parent0[0]: (1139) {G2,W9,D4,L1,V1,M1} { ! skol1( ld( X, X ) ) ==> skol1(
% 0.78/1.53 ld( X, X ) ) }.
% 0.78/1.53 substitution0:
% 0.78/1.53 X := X
% 0.78/1.53 end
% 0.78/1.53
% 0.78/1.53 subsumption: (649) {G28,W0,D0,L0,V0,M0} R(583,5);d(598);q { }.
% 0.78/1.53 parent0: (1140) {G0,W0,D0,L0,V0,M0} { }.
% 0.78/1.53 substitution0:
% 0.78/1.53 end
% 0.78/1.53 permutation0:
% 0.78/1.53 end
% 0.78/1.53
% 0.78/1.53 Proof check complete!
% 0.78/1.53
% 0.78/1.53 Memory use:
% 0.78/1.53
% 0.78/1.53 space for terms: 10954
% 0.78/1.53 space for clauses: 101079
% 0.78/1.53
% 0.78/1.53
% 0.78/1.53 clauses generated: 7582
% 0.78/1.53 clauses kept: 650
% 0.78/1.53 clauses selected: 121
% 0.78/1.53 clauses deleted: 22
% 0.78/1.53 clauses inuse deleted: 0
% 0.78/1.53
% 0.78/1.53 subsentry: 1364
% 0.78/1.53 literals s-matched: 477
% 0.78/1.53 literals matched: 460
% 0.78/1.53 full subsumption: 0
% 0.78/1.53
% 0.78/1.53 checksum: -1042006349
% 0.78/1.53
% 0.78/1.53
% 0.78/1.53 Bliksem ended
%------------------------------------------------------------------------------