%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP660+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n012.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 1.17s 1.53s
% Output : Refutation 1.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GRP660+3 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n012.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Mon Jun 13 12:10:25 EDT 2022
% 0.13/0.34 % CPUTime :
% 1.17/1.53 *** allocated 10000 integers for termspace/termends
% 1.17/1.53 *** allocated 10000 integers for clauses
% 1.17/1.53 *** allocated 10000 integers for justifications
% 1.17/1.53 Bliksem 1.12
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 Automatic Strategy Selection
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 Clauses:
% 1.17/1.53
% 1.17/1.53 { mult( Y, ld( Y, X ) ) = X }.
% 1.17/1.53 { ld( Y, mult( Y, X ) ) = X }.
% 1.17/1.53 { mult( rd( Y, X ), X ) = Y }.
% 1.17/1.53 { rd( mult( Y, X ), X ) = Y }.
% 1.17/1.53 { mult( mult( mult( Z, Y ), X ), Z ) = mult( Z, mult( Y, mult( X, Z ) ) ) }
% 1.17/1.53 .
% 1.17/1.53 { ! mult( skol1, ld( skol2, skol2 ) ) = skol1, ! mult( ld( skol2, skol2 ),
% 1.17/1.53 skol1 ) = skol1 }.
% 1.17/1.53
% 1.17/1.53 percentage equality = 1.000000, percentage horn = 1.000000
% 1.17/1.53 This is a pure equality problem
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 Options Used:
% 1.17/1.53
% 1.17/1.53 useres = 1
% 1.17/1.53 useparamod = 1
% 1.17/1.53 useeqrefl = 1
% 1.17/1.53 useeqfact = 1
% 1.17/1.53 usefactor = 1
% 1.17/1.53 usesimpsplitting = 0
% 1.17/1.53 usesimpdemod = 5
% 1.17/1.53 usesimpres = 3
% 1.17/1.53
% 1.17/1.53 resimpinuse = 1000
% 1.17/1.53 resimpclauses = 20000
% 1.17/1.53 substype = eqrewr
% 1.17/1.53 backwardsubs = 1
% 1.17/1.53 selectoldest = 5
% 1.17/1.53
% 1.17/1.53 litorderings [0] = split
% 1.17/1.53 litorderings [1] = extend the termordering, first sorting on arguments
% 1.17/1.53
% 1.17/1.53 termordering = kbo
% 1.17/1.53
% 1.17/1.53 litapriori = 0
% 1.17/1.53 termapriori = 1
% 1.17/1.53 litaposteriori = 0
% 1.17/1.53 termaposteriori = 0
% 1.17/1.53 demodaposteriori = 0
% 1.17/1.53 ordereqreflfact = 0
% 1.17/1.53
% 1.17/1.53 litselect = negord
% 1.17/1.53
% 1.17/1.53 maxweight = 15
% 1.17/1.53 maxdepth = 30000
% 1.17/1.53 maxlength = 115
% 1.17/1.53 maxnrvars = 195
% 1.17/1.53 excuselevel = 1
% 1.17/1.53 increasemaxweight = 1
% 1.17/1.53
% 1.17/1.53 maxselected = 10000000
% 1.17/1.53 maxnrclauses = 10000000
% 1.17/1.53
% 1.17/1.53 showgenerated = 0
% 1.17/1.53 showkept = 0
% 1.17/1.53 showselected = 0
% 1.17/1.53 showdeleted = 0
% 1.17/1.53 showresimp = 1
% 1.17/1.53 showstatus = 2000
% 1.17/1.53
% 1.17/1.53 prologoutput = 0
% 1.17/1.53 nrgoals = 5000000
% 1.17/1.53 totalproof = 1
% 1.17/1.53
% 1.17/1.53 Symbols occurring in the translation:
% 1.17/1.53
% 1.17/1.53 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.17/1.53 . [1, 2] (w:1, o:18, a:1, s:1, b:0),
% 1.17/1.53 ! [4, 1] (w:0, o:13, a:1, s:1, b:0),
% 1.17/1.53 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.17/1.53 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.17/1.53 ld [37, 2] (w:1, o:42, a:1, s:1, b:0),
% 1.17/1.53 mult [38, 2] (w:1, o:43, a:1, s:1, b:0),
% 1.17/1.53 rd [39, 2] (w:1, o:44, a:1, s:1, b:0),
% 1.17/1.53 skol1 [43, 0] (w:1, o:11, a:1, s:1, b:1),
% 1.17/1.53 skol2 [44, 0] (w:1, o:12, a:1, s:1, b:1).
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 Starting Search:
% 1.17/1.53
% 1.17/1.53 *** allocated 15000 integers for clauses
% 1.17/1.53 *** allocated 22500 integers for clauses
% 1.17/1.53 *** allocated 33750 integers for clauses
% 1.17/1.53 Resimplifying inuse:
% 1.17/1.53 Done
% 1.17/1.53
% 1.17/1.53 Resimplifying inuse:
% 1.17/1.53 Done
% 1.17/1.53
% 1.17/1.53 Failed to find proof!
% 1.17/1.53 maxweight = 15
% 1.17/1.53 maxnrclauses = 10000000
% 1.17/1.53 Generated: 12706
% 1.17/1.53 Kept: 231
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 The strategy used was not complete!
% 1.17/1.53
% 1.17/1.53 Increased maxweight to 16
% 1.17/1.53
% 1.17/1.53 Starting Search:
% 1.17/1.53
% 1.17/1.53 Resimplifying inuse:
% 1.17/1.53 Done
% 1.17/1.53
% 1.17/1.53 Resimplifying inuse:
% 1.17/1.53 Done
% 1.17/1.53
% 1.17/1.53 Failed to find proof!
% 1.17/1.53 maxweight = 16
% 1.17/1.53 maxnrclauses = 10000000
% 1.17/1.53 Generated: 12706
% 1.17/1.53 Kept: 231
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 The strategy used was not complete!
% 1.17/1.53
% 1.17/1.53 Increased maxweight to 17
% 1.17/1.53
% 1.17/1.53 Starting Search:
% 1.17/1.53
% 1.17/1.53 Resimplifying inuse:
% 1.17/1.53 Done
% 1.17/1.53
% 1.17/1.53 Resimplifying inuse:
% 1.17/1.53 Done
% 1.17/1.53
% 1.17/1.53 Failed to find proof!
% 1.17/1.53 maxweight = 17
% 1.17/1.53 maxnrclauses = 10000000
% 1.17/1.53 Generated: 12706
% 1.17/1.53 Kept: 231
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 The strategy used was not complete!
% 1.17/1.53
% 1.17/1.53 Increased maxweight to 18
% 1.17/1.53
% 1.17/1.53 Starting Search:
% 1.17/1.53
% 1.17/1.53 Resimplifying inuse:
% 1.17/1.53 Done
% 1.17/1.53
% 1.17/1.53 Resimplifying inuse:
% 1.17/1.53 Done
% 1.17/1.53
% 1.17/1.53 Failed to find proof!
% 1.17/1.53 maxweight = 18
% 1.17/1.53 maxnrclauses = 10000000
% 1.17/1.53 Generated: 12706
% 1.17/1.53 Kept: 231
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 The strategy used was not complete!
% 1.17/1.53
% 1.17/1.53 Increased maxweight to 19
% 1.17/1.53
% 1.17/1.53 Starting Search:
% 1.17/1.53
% 1.17/1.53 *** allocated 50625 integers for clauses
% 1.17/1.53 *** allocated 75937 integers for clauses
% 1.17/1.53 *** allocated 113905 integers for clauses
% 1.17/1.53 *** allocated 15000 integers for termspace/termends
% 1.17/1.53
% 1.17/1.53 Bliksems!, er is een bewijs:
% 1.17/1.53 % SZS status Theorem
% 1.17/1.53 % SZS output start Refutation
% 1.17/1.53
% 1.17/1.53 (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.17/1.53 (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.53 (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.17/1.53 (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) ) ==> mult(
% 1.17/1.53 mult( mult( Z, Y ), X ), Z ) }.
% 1.17/1.53 (5) {G0,W14,D4,L2,V0,M2} I { ! mult( skol1, ld( skol2, skol2 ) ) ==> skol1
% 1.17/1.53 , ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.17/1.53 (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.17/1.53 (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.53 (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y ), Z ), X ),
% 1.17/1.53 ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.17/1.53 (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd( X, Y ) ),
% 1.17/1.53 Y ) ==> mult( Y, mult( Z, X ) ) }.
% 1.17/1.53 (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 1.17/1.53 mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.17/1.53 (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 1.17/1.53 mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.17/1.53 (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z, X ) ), X )
% 1.17/1.53 ) ==> mult( ld( X, Y ), Z ) }.
% 1.17/1.53 (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld( X, Y ), Z )
% 1.17/1.53 ) ==> rd( mult( Z, Y ), Z ) }.
% 1.17/1.53 (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) ), rd( Y, Z )
% 1.17/1.53 ) ==> rd( mult( Z, X ), Z ) }.
% 1.17/1.53 (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult( X, Z ), X )
% 1.17/1.53 ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.53 (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X ) ==> ld( Y
% 1.17/1.53 , rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X ) ==> ld(
% 1.17/1.53 mult( X, Z ), rd( Y, X ) ) }.
% 1.17/1.53 (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld( mult( X, Y
% 1.17/1.53 ), X ) }.
% 1.17/1.53 (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ), ld( X, Y ) )
% 1.17/1.53 ==> Y }.
% 1.17/1.53 (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X, Y ), X ) )
% 1.17/1.53 ==> X }.
% 1.17/1.53 (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==> ld( ld( Y, X
% 1.17/1.53 ), Y ) }.
% 1.17/1.53 (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd( Z, Y ) ), ld
% 1.17/1.53 ( X, ld( Y, Z ) ) ) ==> Y }.
% 1.17/1.53 (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) ), ld( ld( X, Y
% 1.17/1.53 ), ld( X, Z ) ) ) ==> X }.
% 1.17/1.53 (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) ), Z ) ==> ld
% 1.17/1.53 ( ld( Z, X ), ld( Z, Y ) ) }.
% 1.17/1.53 (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y, mult( X, Y ) )
% 1.17/1.53 ) ==> mult( ld( Z, X ), Y ) }.
% 1.17/1.53 (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X ) ), mult( ld
% 1.17/1.53 ( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.17/1.53 (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z ) ), mult( Y,
% 1.17/1.53 Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.17/1.53 (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X ), X ), mult(
% 1.17/1.53 Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.17/1.53 (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z, Y ) ) ==>
% 1.17/1.53 ld( Y, rd( rd( X, Y ), Z ) ) }.
% 1.17/1.53 (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y ) ), X ) ==>
% 1.17/1.53 ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 1.17/1.53 (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ), rd( X, Y ) )
% 1.17/1.53 ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.53 (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y, rd( Z, ld( Y
% 1.17/1.53 , X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 1.17/1.53 (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z, X ) ) ==>
% 1.17/1.53 mult( X, rd( ld( X, Y ), Z ) ) }.
% 1.17/1.53 (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z ), ld( Y, X )
% 1.17/1.53 ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.17/1.53 (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X ), rd( X, X
% 1.17/1.53 ) ) ==> rd( X, X ) }.
% 1.17/1.53 (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X ), rd( X, X )
% 1.17/1.53 ) ==> rd( X, X ) }.
% 1.17/1.53 (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X, X ), ld( X,
% 1.17/1.53 X ) ) ==> ld( X, X ) }.
% 1.17/1.53 (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd( X, X ) ) ==>
% 1.17/1.53 ld( mult( X, X ), X ) }.
% 1.17/1.53 (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X ), ld( X, X )
% 1.17/1.53 ) ==> ld( X, X ) }.
% 1.17/1.53 (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld( X, X ), ld( X
% 1.17/1.53 , X ) ) ==> ld( X, X ) }.
% 1.17/1.53 (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld( ld( X, X ),
% 1.17/1.53 X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 1.17/1.53 (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld( ld( X, X ), X
% 1.17/1.53 ), ld( X, X ) ) ==> X }.
% 1.17/1.53 (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld( ld( X, X ),
% 1.17/1.53 X ) ==> X }.
% 1.17/1.53 (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y, ld( X, X ) )
% 1.17/1.53 ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 1.17/1.53 (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld( X, X ) }.
% 1.17/1.53 (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld( X, Y ), ld( X
% 1.17/1.53 , X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 1.17/1.53 (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) ) ==> ld( mult(
% 1.17/1.53 X, X ), X ) }.
% 1.17/1.53 (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X, X ) ) ==>
% 1.17/1.53 mult( X, rd( ld( X, Y ), X ) ) }.
% 1.17/1.53 (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd( X, Y ), rd( X
% 1.17/1.53 , Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 1.17/1.53 (321) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y, Y ) ) = ld(
% 1.17/1.53 mult( X, ld( Y, X ) ), X ) }.
% 1.17/1.53 (363) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd( X, Y ) ), X
% 1.17/1.53 ) ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.53 (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X, X ) ) ==>
% 1.17/1.53 ld( ld( ld( X, X ), Y ), X ) }.
% 1.17/1.53 (539) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld( X, X ) )
% 1.17/1.53 ==> mult( ld( mult( X, X ), X ), Y ) }.
% 1.17/1.53 (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(212) { rd( ld(
% 1.17/1.53 ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 1.17/1.53 (553) {G23,W15,D5,L1,V2,M1} P(543,270);d(212);d(194);d(38);d(366);d(242);d(
% 1.17/1.53 0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y, ld( X, X ) )
% 1.17/1.53 }.
% 1.17/1.53 (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld( ld( X, X ),
% 1.17/1.53 rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.17/1.53 (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y ) ==> Y }.
% 1.17/1.53 (583) {G25,W7,D4,L1,V2,M1} P(557,129);d(564);d(564) { mult( Y, ld( X, X ) )
% 1.17/1.53 ==> Y }.
% 1.17/1.53 (584) {G25,W7,D3,L1,V2,M1} P(557,120);d(564);d(564) { ld( Y, Y ) = ld( X, X
% 1.17/1.53 ) }.
% 1.17/1.53 (590) {G25,W11,D5,L1,V3,M1} P(37,557);d(564);d(194);d(553);d(564) { ld( Y,
% 1.17/1.53 rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 1.17/1.53 (594) {G26,W7,D4,L1,V2,M1} P(557,43);d(590);d(583);d(6);d(564) { rd( Y, ld
% 1.17/1.53 ( X, X ) ) ==> Y }.
% 1.17/1.53 (598) {G27,W7,D4,L1,V2,M1} P(557,0);d(594) { mult( ld( X, X ), Y ) ==> Y
% 1.17/1.53 }.
% 1.17/1.53 (635) {G28,W0,D0,L0,V0,M0} P(584,5);d(583);d(598);q;q { }.
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 % SZS output end Refutation
% 1.17/1.53 found a proof!
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 Unprocessed initial clauses:
% 1.17/1.53
% 1.17/1.53 (637) {G0,W7,D4,L1,V2,M1} { mult( Y, ld( Y, X ) ) = X }.
% 1.17/1.53 (638) {G0,W7,D4,L1,V2,M1} { ld( Y, mult( Y, X ) ) = X }.
% 1.17/1.53 (639) {G0,W7,D4,L1,V2,M1} { mult( rd( Y, X ), X ) = Y }.
% 1.17/1.53 (640) {G0,W7,D4,L1,V2,M1} { rd( mult( Y, X ), X ) = Y }.
% 1.17/1.53 (641) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( Z, Y ), X ), Z ) = mult( Z
% 1.17/1.53 , mult( Y, mult( X, Z ) ) ) }.
% 1.17/1.53 (642) {G0,W14,D4,L2,V0,M2} { ! mult( skol1, ld( skol2, skol2 ) ) = skol1,
% 1.17/1.53 ! mult( ld( skol2, skol2 ), skol1 ) = skol1 }.
% 1.17/1.53
% 1.17/1.53
% 1.17/1.53 Total Proof:
% 1.17/1.53
% 1.17/1.53 subsumption: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent0: (637) {G0,W7,D4,L1,V2,M1} { mult( Y, ld( Y, X ) ) = X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.17/1.53 parent0: (638) {G0,W7,D4,L1,V2,M1} { ld( Y, mult( Y, X ) ) = X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.53 parent0: (639) {G0,W7,D4,L1,V2,M1} { mult( rd( Y, X ), X ) = Y }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.17/1.53 parent0: (640) {G0,W7,D4,L1,V2,M1} { rd( mult( Y, X ), X ) = Y }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (657) {G0,W15,D5,L1,V3,M1} { mult( X, mult( Y, mult( Z, X ) ) ) =
% 1.17/1.53 mult( mult( mult( X, Y ), Z ), X ) }.
% 1.17/1.53 parent0[0]: (641) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( Z, Y ), X ), Z
% 1.17/1.53 ) = mult( Z, mult( Y, mult( X, Z ) ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) )
% 1.17/1.53 ) ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 1.17/1.53 parent0: (657) {G0,W15,D5,L1,V3,M1} { mult( X, mult( Y, mult( Z, X ) ) ) =
% 1.17/1.53 mult( mult( mult( X, Y ), Z ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := X
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (5) {G0,W14,D4,L2,V0,M2} I { ! mult( skol1, ld( skol2, skol2 )
% 1.17/1.53 ) ==> skol1, ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.17/1.53 parent0: (642) {G0,W14,D4,L2,V0,M2} { ! mult( skol1, ld( skol2, skol2 ) )
% 1.17/1.53 = skol1, ! mult( ld( skol2, skol2 ), skol1 ) = skol1 }.
% 1.17/1.53 substitution0:
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 1 ==> 1
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (667) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.17/1.53 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (668) {G1,W7,D4,L1,V2,M1} { X ==> ld( rd( Y, X ), Y ) }.
% 1.17/1.53 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.53 parent1[0; 6]: (667) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := rd( Y, X )
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (669) {G1,W7,D4,L1,V2,M1} { ld( rd( Y, X ), Y ) ==> X }.
% 1.17/1.53 parent0[0]: (668) {G1,W7,D4,L1,V2,M1} { X ==> ld( rd( Y, X ), Y ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.17/1.53 parent0: (669) {G1,W7,D4,L1,V2,M1} { ld( rd( Y, X ), Y ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (671) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 1.17/1.53 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (672) {G1,W7,D4,L1,V2,M1} { X ==> rd( Y, ld( X, Y ) ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent1[0; 3]: (671) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := ld( X, Y )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (673) {G1,W7,D4,L1,V2,M1} { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.53 parent0[0]: (672) {G1,W7,D4,L1,V2,M1} { X ==> rd( Y, ld( X, Y ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.53 parent0: (673) {G1,W7,D4,L1,V2,M1} { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (675) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z ), X )
% 1.17/1.53 ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 1.17/1.53 parent0[0]: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) )
% 1.17/1.53 ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (678) {G1,W19,D6,L1,V3,M1} { mult( mult( mult( ld( X, Y ), Z ), X
% 1.17/1.53 ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent1[0; 18]: (675) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z )
% 1.17/1.53 , X ) ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := ld( X, Y )
% 1.17/1.53 Y := Z
% 1.17/1.53 Z := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y
% 1.17/1.53 ), Z ), X ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.17/1.53 parent0: (678) {G1,W19,D6,L1,V3,M1} { mult( mult( mult( ld( X, Y ), Z ), X
% 1.17/1.53 ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (683) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z ), X )
% 1.17/1.53 ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 1.17/1.53 parent0[0]: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) )
% 1.17/1.53 ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (686) {G1,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), rd( Z, X )
% 1.17/1.53 ), X ) ==> mult( X, mult( Y, Z ) ) }.
% 1.17/1.53 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.53 parent1[0; 14]: (683) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z )
% 1.17/1.53 , X ) ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Z
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := rd( Z, X )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ),
% 1.17/1.53 rd( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 1.17/1.53 parent0: (686) {G1,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), rd( Z, X )
% 1.17/1.53 ), X ) ==> mult( X, mult( Y, Z ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := Z
% 1.17/1.53 Z := X
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (691) {G1,W15,D5,L1,V3,M1} { mult( X, mult( Y, Z ) ) ==> mult(
% 1.17/1.53 mult( mult( X, Y ), rd( Z, X ) ), X ) }.
% 1.17/1.53 parent0[0]: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd
% 1.17/1.53 ( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (693) {G1,W15,D5,L1,V3,M1} { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 1.17/1.53 mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent1[0; 10]: (691) {G1,W15,D5,L1,V3,M1} { mult( X, mult( Y, Z ) ) ==>
% 1.17/1.53 mult( mult( mult( X, Y ), rd( Z, X ) ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := ld( X, Y )
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y )
% 1.17/1.53 , Z ) ) ==> mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.17/1.53 parent0: (693) {G1,W15,D5,L1,V3,M1} { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 1.17/1.53 mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (697) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 1.17/1.53 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (700) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 1.17/1.53 rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.17/1.53 parent0[0]: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd
% 1.17/1.53 ( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 1.17/1.53 parent1[0; 9]: (697) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := mult( mult( X, Y ), rd( Z, X ) )
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (701) {G1,W15,D5,L1,V3,M1} { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 1.17/1.53 mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.17/1.53 parent0[0]: (700) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) )
% 1.17/1.53 ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z )
% 1.17/1.53 ), X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.17/1.53 parent0: (701) {G1,W15,D5,L1,V3,M1} { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 1.17/1.53 mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (703) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.17/1.53 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (706) {G1,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X,
% 1.17/1.53 mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 1.17/1.53 parent0[0]: (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y ),
% 1.17/1.53 Z ) ) ==> mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.17/1.53 parent1[0; 8]: (703) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := mult( ld( X, Y ), Z )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (707) {G1,W15,D6,L1,V3,M1} { ld( X, mult( mult( Y, rd( Z, X ) ), X
% 1.17/1.53 ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.17/1.53 parent0[0]: (706) {G1,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X,
% 1.17/1.53 mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd(
% 1.17/1.53 Z, X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.17/1.53 parent0: (707) {G1,W15,D6,L1,V3,M1} { ld( X, mult( mult( Y, rd( Z, X ) ),
% 1.17/1.53 X ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (709) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 1.17/1.53 rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.17/1.53 parent0[0]: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) )
% 1.17/1.53 , X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (711) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( ld( Y, Z ),
% 1.17/1.53 X ) ) ==> rd( mult( X, Z ), X ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent1[0; 13]: (709) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X
% 1.17/1.53 ) ) ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := ld( Y, Z )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 1.17/1.53 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 1.17/1.53 parent0: (711) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( ld( Y, Z ),
% 1.17/1.53 X ) ) ==> rd( mult( X, Z ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (715) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 1.17/1.53 rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.17/1.53 parent0[0]: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) )
% 1.17/1.53 , X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (720) {G1,W15,D5,L1,V3,M1} { mult( mult( X, rd( Y, Z ) ), rd( Z,
% 1.17/1.53 X ) ) ==> rd( mult( X, Y ), X ) }.
% 1.17/1.53 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.53 parent1[0; 13]: (715) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X
% 1.17/1.53 ) ) ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := rd( Y, Z )
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y )
% 1.17/1.53 ), rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 1.17/1.53 parent0: (720) {G1,W15,D5,L1,V3,M1} { mult( mult( X, rd( Y, Z ) ), rd( Z,
% 1.17/1.53 X ) ) ==> rd( mult( X, Y ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (725) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.17/1.53 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (728) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( mult( Z
% 1.17/1.53 , X ), rd( mult( Z, Y ), Z ) ) }.
% 1.17/1.53 parent0[0]: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 1.17/1.53 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 1.17/1.53 parent1[0; 10]: (725) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) )
% 1.17/1.53 }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := mult( Z, X )
% 1.17/1.53 Y := rd( ld( X, Y ), Z )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (729) {G1,W15,D5,L1,V3,M1} { ld( mult( Z, X ), rd( mult( Z, Y ), Z
% 1.17/1.53 ) ) ==> rd( ld( X, Y ), Z ) }.
% 1.17/1.53 parent0[0]: (728) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( mult
% 1.17/1.53 ( Z, X ), rd( mult( Z, Y ), Z ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 1.17/1.53 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.53 parent0: (729) {G1,W15,D5,L1,V3,M1} { ld( mult( Z, X ), rd( mult( Z, Y ),
% 1.17/1.53 Z ) ) ==> rd( ld( X, Y ), Z ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := Z
% 1.17/1.53 Z := X
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (731) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 1.17/1.53 Y ), rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 1.17/1.53 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (734) {G1,W15,D5,L1,V3,M1} { rd( ld( ld( X, Y ), Z ), X ) ==> ld
% 1.17/1.53 ( Y, rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent1[0; 9]: (731) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 1.17/1.53 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := ld( X, Y )
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 1.17/1.53 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 parent0: (734) {G1,W15,D5,L1,V3,M1} { rd( ld( ld( X, Y ), Z ), X ) ==> ld
% 1.17/1.53 ( Y, rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (739) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 1.17/1.53 Y ), rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 1.17/1.53 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (743) {G1,W15,D5,L1,V3,M1} { rd( ld( X, ld( Y, Z ) ), Y ) ==> ld
% 1.17/1.53 ( mult( Y, X ), rd( Z, Y ) ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent1[0; 13]: (739) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 1.17/1.53 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 Z := ld( Y, Z )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.17/1.53 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.17/1.53 parent0: (743) {G1,W15,D5,L1,V3,M1} { rd( ld( X, ld( Y, Z ) ), Y ) ==> ld
% 1.17/1.53 ( mult( Y, X ), rd( Z, Y ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (747) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 1.17/1.53 Y ), rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 1.17/1.53 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (748) {G1,W11,D4,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( mult( Y
% 1.17/1.53 , X ), Y ) }.
% 1.17/1.53 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.17/1.53 parent1[0; 10]: (747) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 1.17/1.53 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.17/1.53 ( mult( X, Y ), X ) }.
% 1.17/1.53 parent0: (748) {G1,W11,D4,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( mult( Y
% 1.17/1.53 , X ), Y ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (751) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.17/1.53 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (754) {G2,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld
% 1.17/1.53 ( Y, X ) ) }.
% 1.17/1.53 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.17/1.53 ( mult( X, Y ), X ) }.
% 1.17/1.53 parent1[0; 3]: (751) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := ld( Y, X )
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (755) {G2,W11,D5,L1,V2,M1} { ld( ld( mult( X, Y ), X ), ld( Y, X )
% 1.17/1.53 ) ==> X }.
% 1.17/1.53 parent0[0]: (754) {G2,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ),
% 1.17/1.53 ld( Y, X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y )
% 1.17/1.53 , ld( X, Y ) ) ==> Y }.
% 1.17/1.53 parent0: (755) {G2,W11,D5,L1,V2,M1} { ld( ld( mult( X, Y ), X ), ld( Y, X
% 1.17/1.53 ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (757) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld(
% 1.17/1.53 Y, X ) ) }.
% 1.17/1.53 parent0[0]: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ),
% 1.17/1.53 ld( X, Y ) ) ==> Y }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (760) {G1,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, X ), ld( ld( X, Y )
% 1.17/1.53 , X ) ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent1[0; 4]: (757) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X
% 1.17/1.53 ), ld( Y, X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := ld( X, Y )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (761) {G1,W11,D5,L1,V2,M1} { ld( ld( Y, X ), ld( ld( X, Y ), X ) )
% 1.17/1.53 ==> X }.
% 1.17/1.53 parent0[0]: (760) {G1,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, X ), ld( ld( X,
% 1.17/1.53 Y ), X ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X
% 1.17/1.53 , Y ), X ) ) ==> X }.
% 1.17/1.53 parent0: (761) {G1,W11,D5,L1,V2,M1} { ld( ld( Y, X ), ld( ld( X, Y ), X )
% 1.17/1.53 ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (763) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (764) {G1,W11,D4,L1,V2,M1} { ld( ld( X, Y ), X ) ==> mult( ld( Y
% 1.17/1.53 , X ), X ) }.
% 1.17/1.53 parent0[0]: (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X,
% 1.17/1.53 Y ), X ) ) ==> X }.
% 1.17/1.53 parent1[0; 10]: (763) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 1.17/1.53 }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := ld( Y, X )
% 1.17/1.53 Y := ld( ld( X, Y ), X )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (765) {G1,W11,D4,L1,V2,M1} { mult( ld( Y, X ), X ) ==> ld( ld( X,
% 1.17/1.53 Y ), X ) }.
% 1.17/1.53 parent0[0]: (764) {G1,W11,D4,L1,V2,M1} { ld( ld( X, Y ), X ) ==> mult( ld
% 1.17/1.53 ( Y, X ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.17/1.53 ld( ld( Y, X ), Y ) }.
% 1.17/1.53 parent0: (765) {G1,W11,D4,L1,V2,M1} { mult( ld( Y, X ), X ) ==> ld( ld( X
% 1.17/1.53 , Y ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (767) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.17/1.53 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (772) {G2,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z, X
% 1.17/1.53 ) ), ld( Y, ld( X, Z ) ) ) }.
% 1.17/1.53 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.17/1.53 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.17/1.53 parent1[0; 3]: (767) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Z
% 1.17/1.53 Z := Y
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := ld( Y, ld( X, Z ) )
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (773) {G2,W15,D5,L1,V3,M1} { ld( ld( mult( X, Y ), rd( Z, X ) ),
% 1.17/1.53 ld( Y, ld( X, Z ) ) ) ==> X }.
% 1.17/1.53 parent0[0]: (772) {G2,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z
% 1.17/1.53 , X ) ), ld( Y, ld( X, Z ) ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd
% 1.17/1.53 ( Z, Y ) ), ld( X, ld( Y, Z ) ) ) ==> Y }.
% 1.17/1.53 parent0: (773) {G2,W15,D5,L1,V3,M1} { ld( ld( mult( X, Y ), rd( Z, X ) ),
% 1.17/1.53 ld( Y, ld( X, Z ) ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (775) {G6,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z, X
% 1.17/1.53 ) ), ld( Y, ld( X, Z ) ) ) }.
% 1.17/1.53 parent0[0]: (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd(
% 1.17/1.53 Z, Y ) ), ld( X, ld( Y, Z ) ) ) ==> Y }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (778) {G1,W15,D5,L1,V3,M1} { X ==> ld( ld( Y, rd( Z, X ) ), ld(
% 1.17/1.53 ld( X, Y ), ld( X, Z ) ) ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 parent1[0; 4]: (775) {G6,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd
% 1.17/1.53 ( Z, X ) ), ld( Y, ld( X, Z ) ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := X
% 1.17/1.53 Y := ld( X, Y )
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (779) {G1,W15,D5,L1,V3,M1} { ld( ld( Y, rd( Z, X ) ), ld( ld( X, Y
% 1.17/1.53 ), ld( X, Z ) ) ) ==> X }.
% 1.17/1.53 parent0[0]: (778) {G1,W15,D5,L1,V3,M1} { X ==> ld( ld( Y, rd( Z, X ) ), ld
% 1.17/1.53 ( ld( X, Y ), ld( X, Z ) ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) )
% 1.17/1.53 , ld( ld( X, Y ), ld( X, Z ) ) ) ==> X }.
% 1.17/1.53 parent0: (779) {G1,W15,D5,L1,V3,M1} { ld( ld( Y, rd( Z, X ) ), ld( ld( X,
% 1.17/1.53 Y ), ld( X, Z ) ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (781) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 1.17/1.53 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Y
% 1.17/1.53 Y := X
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (782) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, Z ) ) ==>
% 1.17/1.53 mult( ld( Y, rd( Z, X ) ), X ) }.
% 1.17/1.53 parent0[0]: (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) ),
% 1.17/1.53 ld( ld( X, Y ), ld( X, Z ) ) ) ==> X }.
% 1.17/1.53 parent1[0; 14]: (781) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 1.17/1.53 }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53 substitution1:
% 1.17/1.53 X := ld( Y, rd( Z, X ) )
% 1.17/1.53 Y := ld( ld( X, Y ), ld( X, Z ) )
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (783) {G1,W15,D5,L1,V3,M1} { mult( ld( Y, rd( Z, X ) ), X ) ==> ld
% 1.17/1.53 ( ld( X, Y ), ld( X, Z ) ) }.
% 1.17/1.53 parent0[0]: (782) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, Z ) ) ==>
% 1.17/1.53 mult( ld( Y, rd( Z, X ) ), X ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 subsumption: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z )
% 1.17/1.53 ), Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 1.17/1.53 parent0: (783) {G1,W15,D5,L1,V3,M1} { mult( ld( Y, rd( Z, X ) ), X ) ==>
% 1.17/1.53 ld( ld( X, Y ), ld( X, Z ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := Z
% 1.17/1.53 Y := X
% 1.17/1.53 Z := Y
% 1.17/1.53 end
% 1.17/1.53 permutation0:
% 1.17/1.53 0 ==> 0
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 eqswap: (785) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) ) ==> mult
% 1.17/1.53 ( ld( X, rd( Y, Z ) ), Z ) }.
% 1.17/1.53 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 1.17/1.53 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 1.17/1.53 substitution0:
% 1.17/1.53 X := X
% 1.17/1.53 Y := Y
% 1.17/1.53 Z := Z
% 1.17/1.53 end
% 1.17/1.53
% 1.17/1.53 paramod: (788) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, mult( Z, X )
% 1.17/1.53 ) ) ==> mult( ld( Y, Z ), X ) }.
% 1.17/1.53 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.17/1.53 parent1[0; 13]: (785) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) )
% 1.17/1.54 ==> mult( ld( X, rd( Y, Z ) ), Z ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Z
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := mult( Z, X )
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y,
% 1.17/1.54 mult( X, Y ) ) ) ==> mult( ld( Z, X ), Y ) }.
% 1.17/1.54 parent0: (788) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, mult( Z, X )
% 1.17/1.54 ) ) ==> mult( ld( Y, Z ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (791) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 1.17/1.54 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (792) {G2,W15,D5,L1,V3,M1} { ld( X, Y ) ==> rd( ld( X, mult( Z, X
% 1.17/1.54 ) ), mult( ld( Y, Z ), X ) ) }.
% 1.17/1.54 parent0[0]: (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y,
% 1.17/1.54 mult( X, Y ) ) ) ==> mult( ld( Z, X ), Y ) }.
% 1.17/1.54 parent1[0; 10]: (791) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Z
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, mult( Z, X ) )
% 1.17/1.54 Y := ld( X, Y )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (793) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Z, X ) ), mult( ld(
% 1.17/1.54 Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.17/1.54 parent0[0]: (792) {G2,W15,D5,L1,V3,M1} { ld( X, Y ) ==> rd( ld( X, mult( Z
% 1.17/1.54 , X ) ), mult( ld( Y, Z ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 1.17/1.54 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.17/1.54 parent0: (793) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Z, X ) ), mult( ld
% 1.17/1.54 ( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (795) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X, mult( Y, X
% 1.17/1.54 ) ), mult( ld( Z, Y ), X ) ) }.
% 1.17/1.54 parent0[0]: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 1.17/1.54 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (799) {G2,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 1.17/1.54 mult( Y, X ) ), mult( Z, X ) ) }.
% 1.17/1.54 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.17/1.54 parent1[0; 13]: (795) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X,
% 1.17/1.54 mult( Y, X ) ), mult( ld( Z, Y ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := rd( Y, Z )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (801) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), mult( Z, X
% 1.17/1.54 ) ) ==> ld( X, rd( Y, Z ) ) }.
% 1.17/1.54 parent0[0]: (799) {G2,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X
% 1.17/1.54 , mult( Y, X ) ), mult( Z, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 1.17/1.54 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.17/1.54 parent0: (801) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), mult( Z,
% 1.17/1.54 X ) ) ==> ld( X, rd( Y, Z ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Z
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (802) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 1.17/1.54 mult( Y, X ) ), mult( Z, X ) ) }.
% 1.17/1.54 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 1.17/1.54 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (805) {G6,W15,D5,L1,V2,M1} { ld( X, rd( Y, Y ) ) ==> ld( mult(
% 1.17/1.54 mult( Y, X ), X ), mult( Y, X ) ) }.
% 1.17/1.54 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.17/1.54 ( mult( X, Y ), X ) }.
% 1.17/1.54 parent1[0; 6]: (802) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 1.17/1.54 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := mult( Y, X )
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (807) {G6,W15,D5,L1,V2,M1} { ld( mult( mult( Y, X ), X ), mult( Y
% 1.17/1.54 , X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.17/1.54 parent0[0]: (805) {G6,W15,D5,L1,V2,M1} { ld( X, rd( Y, Y ) ) ==> ld( mult
% 1.17/1.54 ( mult( Y, X ), X ), mult( Y, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X )
% 1.17/1.54 , X ), mult( Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.17/1.54 parent0: (807) {G6,W15,D5,L1,V2,M1} { ld( mult( mult( Y, X ), X ), mult( Y
% 1.17/1.54 , X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (809) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 1.17/1.54 mult( Y, X ) ), mult( Z, X ) ) }.
% 1.17/1.54 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 1.17/1.54 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (812) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 1.17/1.54 ( ld( X, Y ), mult( Z, X ) ) }.
% 1.17/1.54 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.54 parent1[0; 11]: (809) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 1.17/1.54 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := rd( Y, X )
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (814) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), mult( Z, X ) ) ==> ld
% 1.17/1.54 ( X, rd( rd( Y, X ), Z ) ) }.
% 1.17/1.54 parent0[0]: (812) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==>
% 1.17/1.54 rd( ld( X, Y ), mult( Z, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 1.17/1.54 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 1.17/1.54 parent0: (814) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), mult( Z, X ) ) ==>
% 1.17/1.54 ld( X, rd( rd( Y, X ), Z ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (817) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 1.17/1.54 mult( Y, X ) ), mult( Z, X ) ) }.
% 1.17/1.54 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 1.17/1.54 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (821) {G1,W15,D5,L1,V3,M1} { ld( X, rd( Y, rd( Z, X ) ) ) ==> rd
% 1.17/1.54 ( ld( X, mult( Y, X ) ), Z ) }.
% 1.17/1.54 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.54 parent1[0; 14]: (817) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 1.17/1.54 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Z
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := rd( Z, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (823) {G1,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), Z ) ==> ld
% 1.17/1.54 ( X, rd( Y, rd( Z, X ) ) ) }.
% 1.17/1.54 parent0[0]: (821) {G1,W15,D5,L1,V3,M1} { ld( X, rd( Y, rd( Z, X ) ) ) ==>
% 1.17/1.54 rd( ld( X, mult( Y, X ) ), Z ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y )
% 1.17/1.54 ), X ) ==> ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 1.17/1.54 parent0: (823) {G1,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), Z ) ==>
% 1.17/1.54 ld( X, rd( Y, rd( Z, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (825) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 1.17/1.54 ( ld( X, Y ), mult( Z, X ) ) }.
% 1.17/1.54 parent0[0]: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 1.17/1.54 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (828) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), rd( Z, X ) )
% 1.17/1.54 ) ==> rd( ld( X, Y ), Z ) }.
% 1.17/1.54 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.54 parent1[0; 14]: (825) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) )
% 1.17/1.54 ==> rd( ld( X, Y ), mult( Z, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Z
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := rd( Z, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 1.17/1.54 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.54 parent0: (828) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), rd( Z, X ) )
% 1.17/1.54 ) ==> rd( ld( X, Y ), Z ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (831) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X, rd(
% 1.17/1.54 rd( Y, X ), rd( Z, X ) ) ) }.
% 1.17/1.54 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 1.17/1.54 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Z
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (835) {G2,W19,D6,L1,V3,M1} { rd( ld( ld( X, Y ), Y ), Z ) ==> ld
% 1.17/1.54 ( ld( X, Y ), rd( X, rd( Z, ld( X, Y ) ) ) ) }.
% 1.17/1.54 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.54 parent1[0; 13]: (831) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld(
% 1.17/1.54 X, rd( rd( Y, X ), rd( Z, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, Y )
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (838) {G2,W19,D6,L1,V3,M1} { ld( ld( X, Y ), rd( X, rd( Z, ld( X,
% 1.17/1.54 Y ) ) ) ) ==> rd( ld( ld( X, Y ), Y ), Z ) }.
% 1.17/1.54 parent0[0]: (835) {G2,W19,D6,L1,V3,M1} { rd( ld( ld( X, Y ), Y ), Z ) ==>
% 1.17/1.54 ld( ld( X, Y ), rd( X, rd( Z, ld( X, Y ) ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y,
% 1.17/1.54 rd( Z, ld( Y, X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 1.17/1.54 parent0: (838) {G2,W19,D6,L1,V3,M1} { ld( ld( X, Y ), rd( X, rd( Z, ld( X
% 1.17/1.54 , Y ) ) ) ) ==> rd( ld( ld( X, Y ), Y ), Z ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (841) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 1.17/1.54 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (842) {G1,W15,D5,L1,V3,M1} { rd( rd( X, Y ), rd( Z, Y ) ) ==>
% 1.17/1.54 mult( Y, rd( ld( Y, X ), Z ) ) }.
% 1.17/1.54 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 1.17/1.54 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.54 parent1[0; 10]: (841) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 1.17/1.54 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Z
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := rd( rd( X, Y ), rd( Z, Y ) )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z,
% 1.17/1.54 X ) ) ==> mult( X, rd( ld( X, Y ), Z ) ) }.
% 1.17/1.54 parent0: (842) {G1,W15,D5,L1,V3,M1} { rd( rd( X, Y ), rd( Z, Y ) ) ==>
% 1.17/1.54 mult( Y, rd( ld( Y, X ), Z ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (845) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Y ), X ) ==> mult( mult
% 1.17/1.54 ( X, rd( Y, Z ) ), rd( Z, X ) ) }.
% 1.17/1.54 parent0[0]: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) )
% 1.17/1.54 , rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (847) {G2,W19,D5,L1,V3,M1} { rd( mult( ld( X, Y ), Z ), ld( X, Y
% 1.17/1.54 ) ) ==> mult( mult( ld( X, Y ), rd( Z, Y ) ), X ) }.
% 1.17/1.54 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.54 parent1[0; 18]: (845) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Y ), X ) ==>
% 1.17/1.54 mult( mult( X, rd( Y, Z ) ), rd( Z, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, Y )
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 1.17/1.54 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.17/1.54 parent0: (847) {G2,W19,D5,L1,V3,M1} { rd( mult( ld( X, Y ), Z ), ld( X, Y
% 1.17/1.54 ) ) ==> mult( mult( ld( X, Y ), rd( Z, Y ) ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (851) {G12,W15,D5,L1,V2,M1} { ld( Y, rd( X, X ) ) ==> ld( mult(
% 1.17/1.54 mult( X, Y ), Y ), mult( X, Y ) ) }.
% 1.17/1.54 parent0[0]: (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X )
% 1.17/1.54 , X ), mult( Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (854) {G4,W19,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> ld
% 1.17/1.54 ( rd( mult( X, X ), X ), mult( X, rd( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) )
% 1.17/1.54 , rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 1.17/1.54 parent1[0; 9]: (851) {G12,W15,D5,L1,V2,M1} { ld( Y, rd( X, X ) ) ==> ld(
% 1.17/1.54 mult( mult( X, Y ), Y ), mult( X, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := rd( X, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (858) {G1,W15,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> ld
% 1.17/1.54 ( X, mult( X, rd( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.17/1.54 parent1[0; 9]: (854) {G4,W19,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 1.17/1.54 ==> ld( rd( mult( X, X ), X ), mult( X, rd( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (859) {G1,W11,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> rd
% 1.17/1.54 ( X, X ) }.
% 1.17/1.54 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.17/1.54 parent1[0; 8]: (858) {G1,W15,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 1.17/1.54 ==> ld( X, mult( X, rd( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := rd( X, X )
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 1.17/1.54 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.17/1.54 parent0: (859) {G1,W11,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> rd
% 1.17/1.54 ( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (862) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult( ld( X,
% 1.17/1.54 Y ), Y ) }.
% 1.17/1.54 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.17/1.54 ld( ld( Y, X ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (865) {G9,W19,D5,L1,V1,M1} { ld( ld( rd( X, X ), rd( X, X ) ), rd
% 1.17/1.54 ( X, X ) ) ==> mult( rd( X, X ), rd( X, X ) ) }.
% 1.17/1.54 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 1.17/1.54 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.17/1.54 parent1[0; 13]: (862) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult
% 1.17/1.54 ( ld( X, Y ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := rd( X, X )
% 1.17/1.54 Y := rd( X, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (869) {G10,W15,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==>
% 1.17/1.54 mult( rd( X, X ), rd( X, X ) ) }.
% 1.17/1.54 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 1.17/1.54 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.17/1.54 parent1[0; 2]: (865) {G9,W19,D5,L1,V1,M1} { ld( ld( rd( X, X ), rd( X, X )
% 1.17/1.54 ), rd( X, X ) ) ==> mult( rd( X, X ), rd( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (870) {G11,W11,D4,L1,V1,M1} { rd( X, X ) ==> mult( rd( X, X ), rd
% 1.17/1.54 ( X, X ) ) }.
% 1.17/1.54 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 1.17/1.54 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.17/1.54 parent1[0; 1]: (869) {G10,W15,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 1.17/1.54 ==> mult( rd( X, X ), rd( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (871) {G11,W11,D4,L1,V1,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 1.17/1.54 rd( X, X ) }.
% 1.17/1.54 parent0[0]: (870) {G11,W11,D4,L1,V1,M1} { rd( X, X ) ==> mult( rd( X, X )
% 1.17/1.54 , rd( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X
% 1.17/1.54 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.17/1.54 parent0: (871) {G11,W11,D4,L1,V1,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 1.17/1.54 rd( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (874) {G3,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X, mult
% 1.17/1.54 ( mult( Y, rd( Z, X ) ), X ) ) }.
% 1.17/1.54 parent0[0]: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z
% 1.17/1.54 , X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (877) {G4,W15,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X ) ==>
% 1.17/1.54 ld( X, mult( rd( X, X ), X ) ) }.
% 1.17/1.54 parent0[0]: (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X )
% 1.17/1.54 , rd( X, X ) ) ==> rd( X, X ) }.
% 1.17/1.54 parent1[0; 11]: (874) {G3,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld
% 1.17/1.54 ( X, mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := rd( X, X )
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (878) {G1,W11,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X ) ==>
% 1.17/1.54 ld( X, X ) }.
% 1.17/1.54 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.17/1.54 parent1[0; 10]: (877) {G4,W15,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X
% 1.17/1.54 ) ==> ld( X, mult( rd( X, X ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (879) {G2,W11,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> ld
% 1.17/1.54 ( X, X ) }.
% 1.17/1.54 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 1.17/1.54 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 1.17/1.54 parent1[0; 1]: (878) {G1,W11,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X )
% 1.17/1.54 ==> ld( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X
% 1.17/1.54 , X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent0: (879) {G2,W11,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> ld
% 1.17/1.54 ( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (882) {G5,W15,D5,L1,V3,M1} { ld( mult( Y, X ), rd( Z, Y ) ) ==> rd
% 1.17/1.54 ( ld( X, ld( Y, Z ) ), Y ) }.
% 1.17/1.54 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.17/1.54 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (885) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd( X, X
% 1.17/1.54 ) ) ==> rd( ld( X, X ), X ) }.
% 1.17/1.54 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.17/1.54 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 11]: (882) {G5,W15,D5,L1,V3,M1} { ld( mult( Y, X ), rd( Z, Y )
% 1.17/1.54 ) ==> rd( ld( X, ld( Y, Z ) ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := X
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (888) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd( X, X
% 1.17/1.54 ) ) ==> ld( mult( X, X ), X ) }.
% 1.17/1.54 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.17/1.54 ( mult( X, Y ), X ) }.
% 1.17/1.54 parent1[0; 10]: (885) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd
% 1.17/1.54 ( X, X ) ) ==> rd( ld( X, X ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (889) {G1,W11,D4,L1,V1,M1} { ld( X, rd( X, X ) ) ==> ld( mult( X
% 1.17/1.54 , X ), X ) }.
% 1.17/1.54 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.54 parent1[0; 2]: (888) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd
% 1.17/1.54 ( X, X ) ) ==> ld( mult( X, X ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd(
% 1.17/1.54 X, X ) ) ==> ld( mult( X, X ), X ) }.
% 1.17/1.54 parent0: (889) {G1,W11,D4,L1,V1,M1} { ld( X, rd( X, X ) ) ==> ld( mult( X
% 1.17/1.54 , X ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (892) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult( ld( X,
% 1.17/1.54 Y ), Y ) }.
% 1.17/1.54 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.17/1.54 ld( ld( Y, X ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (895) {G9,W19,D5,L1,V1,M1} { ld( ld( ld( X, X ), ld( X, X ) ), ld
% 1.17/1.54 ( X, X ) ) ==> mult( ld( X, X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.17/1.54 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 13]: (892) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult
% 1.17/1.54 ( ld( X, Y ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (899) {G10,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==>
% 1.17/1.54 mult( ld( X, X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.17/1.54 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 2]: (895) {G9,W19,D5,L1,V1,M1} { ld( ld( ld( X, X ), ld( X, X )
% 1.17/1.54 ), ld( X, X ) ) ==> mult( ld( X, X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (900) {G11,W11,D4,L1,V1,M1} { ld( X, X ) ==> mult( ld( X, X ), ld
% 1.17/1.54 ( X, X ) ) }.
% 1.17/1.54 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.17/1.54 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 1]: (899) {G10,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) )
% 1.17/1.54 ==> mult( ld( X, X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (901) {G11,W11,D4,L1,V1,M1} { mult( ld( X, X ), ld( X, X ) ) ==>
% 1.17/1.54 ld( X, X ) }.
% 1.17/1.54 parent0[0]: (900) {G11,W11,D4,L1,V1,M1} { ld( X, X ) ==> mult( ld( X, X )
% 1.17/1.54 , ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X
% 1.17/1.54 ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent0: (901) {G11,W11,D4,L1,V1,M1} { mult( ld( X, X ), ld( X, X ) ) ==>
% 1.17/1.54 ld( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (904) {G5,W11,D4,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> rd( ld( X,
% 1.17/1.54 Y ), Y ) }.
% 1.17/1.54 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.17/1.54 ( mult( X, Y ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (907) {G6,W19,D5,L1,V1,M1} { ld( mult( ld( X, X ), ld( X, X ) ),
% 1.17/1.54 ld( X, X ) ) ==> rd( ld( X, X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.17/1.54 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 13]: (904) {G5,W11,D4,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> rd
% 1.17/1.54 ( ld( X, Y ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (908) {G7,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> rd
% 1.17/1.54 ( ld( X, X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 1.17/1.54 , ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 2]: (907) {G6,W19,D5,L1,V1,M1} { ld( mult( ld( X, X ), ld( X, X
% 1.17/1.54 ) ), ld( X, X ) ) ==> rd( ld( X, X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (909) {G8,W11,D4,L1,V1,M1} { ld( X, X ) ==> rd( ld( X, X ), ld( X
% 1.17/1.54 , X ) ) }.
% 1.17/1.54 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.17/1.54 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 1]: (908) {G7,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) )
% 1.17/1.54 ==> rd( ld( X, X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (910) {G8,W11,D4,L1,V1,M1} { rd( ld( X, X ), ld( X, X ) ) ==> ld(
% 1.17/1.54 X, X ) }.
% 1.17/1.54 parent0[0]: (909) {G8,W11,D4,L1,V1,M1} { ld( X, X ) ==> rd( ld( X, X ), ld
% 1.17/1.54 ( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld(
% 1.17/1.54 X, X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent0: (910) {G8,W11,D4,L1,V1,M1} { rd( ld( X, X ), ld( X, X ) ) ==> ld
% 1.17/1.54 ( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (912) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X, mult( Y, X
% 1.17/1.54 ) ), mult( ld( Z, Y ), X ) ) }.
% 1.17/1.54 parent0[0]: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 1.17/1.54 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (916) {G11,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld( ld
% 1.17/1.54 ( X, X ), mult( X, ld( X, X ) ) ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 1.17/1.54 , ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 16]: (912) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X,
% 1.17/1.54 mult( Y, X ) ), mult( ld( Z, Y ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := X
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (917) {G12,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> ld( ld( X,
% 1.17/1.54 X ), rd( X, rd( ld( X, X ), ld( X, X ) ) ) ) }.
% 1.17/1.54 parent0[0]: (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y )
% 1.17/1.54 ), X ) ==> ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 1.17/1.54 parent1[0; 6]: (916) {G11,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd(
% 1.17/1.54 ld( ld( X, X ), mult( X, ld( X, X ) ) ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (918) {G13,W15,D5,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld( ld
% 1.17/1.54 ( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y,
% 1.17/1.54 rd( Z, ld( Y, X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 1.17/1.54 parent1[0; 6]: (917) {G12,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> ld(
% 1.17/1.54 ld( X, X ), rd( X, rd( ld( X, X ), ld( X, X ) ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 Z := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (919) {G13,W15,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 1.17/1.54 ) ==> ld( ld( X, X ), X ) }.
% 1.17/1.54 parent0[0]: (918) {G13,W15,D5,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld(
% 1.17/1.54 ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld
% 1.17/1.54 ( ld( X, X ), X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 1.17/1.54 parent0: (919) {G13,W15,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 1.17/1.54 ) ==> ld( ld( X, X ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (921) {G1,W19,D6,L1,V3,M1} { mult( ld( X, Y ), mult( Z, Y ) ) ==>
% 1.17/1.54 mult( mult( mult( ld( X, Y ), Z ), X ), ld( X, Y ) ) }.
% 1.17/1.54 parent0[0]: (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y )
% 1.17/1.54 , Z ), X ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (925) {G2,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X, X ),
% 1.17/1.54 X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 1.17/1.54 , ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 12]: (921) {G1,W19,D6,L1,V3,M1} { mult( ld( X, Y ), mult( Z, Y
% 1.17/1.54 ) ) ==> mult( mult( mult( ld( X, Y ), Z ), X ), ld( X, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 Z := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (927) {G3,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X, X ),
% 1.17/1.54 X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.17/1.54 ld( ld( Y, X ), Y ) }.
% 1.17/1.54 parent1[0; 11]: (925) {G2,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X
% 1.17/1.54 , X ), X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (928) {G4,W19,D5,L1,V1,M1} { mult( ld( X, X ), ld( ld( X, X ), X
% 1.17/1.54 ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.17/1.54 ld( ld( Y, X ), Y ) }.
% 1.17/1.54 parent1[0; 5]: (927) {G3,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X
% 1.17/1.54 , X ), X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (929) {G1,W11,D5,L1,V1,M1} { X ==> mult( ld( ld( X, X ), X ), ld
% 1.17/1.54 ( X, X ) ) }.
% 1.17/1.54 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.54 parent1[0; 1]: (928) {G4,W19,D5,L1,V1,M1} { mult( ld( X, X ), ld( ld( X, X
% 1.17/1.54 ), X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (930) {G1,W11,D5,L1,V1,M1} { mult( ld( ld( X, X ), X ), ld( X, X )
% 1.17/1.54 ) ==> X }.
% 1.17/1.54 parent0[0]: (929) {G1,W11,D5,L1,V1,M1} { X ==> mult( ld( ld( X, X ), X ),
% 1.17/1.54 ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld(
% 1.17/1.54 ld( X, X ), X ), ld( X, X ) ) ==> X }.
% 1.17/1.54 parent0: (930) {G1,W11,D5,L1,V1,M1} { mult( ld( ld( X, X ), X ), ld( X, X
% 1.17/1.54 ) ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (932) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Z ), X ) ==> mult( mult
% 1.17/1.54 ( X, Y ), rd( ld( Y, Z ), X ) ) }.
% 1.17/1.54 parent0[0]: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 1.17/1.54 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (936) {G4,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld( X, X
% 1.17/1.54 ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld( X
% 1.17/1.54 , X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 16]: (932) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Z ), X ) ==>
% 1.17/1.54 mult( mult( X, Y ), rd( ld( Y, Z ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := X
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (938) {G5,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld( X, X
% 1.17/1.54 ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.17/1.54 ld( ld( Y, X ), Y ) }.
% 1.17/1.54 parent1[0; 11]: (936) {G4,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld
% 1.17/1.54 ( X, X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (939) {G6,W19,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 1.17/1.54 ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.17/1.54 ld( ld( Y, X ), Y ) }.
% 1.17/1.54 parent1[0; 2]: (938) {G5,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld
% 1.17/1.54 ( X, X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (941) {G7,W11,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 1.17/1.54 ) ==> X }.
% 1.17/1.54 parent0[0]: (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld( ld
% 1.17/1.54 ( X, X ), X ), ld( X, X ) ) ==> X }.
% 1.17/1.54 parent1[0; 10]: (939) {G6,W19,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld(
% 1.17/1.54 X, X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (942) {G8,W7,D4,L1,V1,M1} { ld( ld( X, X ), X ) ==> X }.
% 1.17/1.54 parent0[0]: (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld(
% 1.17/1.54 ld( X, X ), X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 1.17/1.54 parent1[0; 1]: (941) {G7,W11,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X
% 1.17/1.54 , X ) ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld
% 1.17/1.54 ( ld( X, X ), X ) ==> X }.
% 1.17/1.54 parent0: (942) {G8,W7,D4,L1,V1,M1} { ld( ld( X, X ), X ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (945) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 1.17/1.54 ( ld( X, Y ), mult( Z, X ) ) }.
% 1.17/1.54 parent0[0]: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 1.17/1.54 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (947) {G13,W19,D6,L1,V2,M1} { ld( ld( X, X ), rd( rd( X, ld( X, X
% 1.17/1.54 ) ), Y ) ) ==> rd( X, mult( Y, ld( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.17/1.54 ld( X, X ), X ) ==> X }.
% 1.17/1.54 parent1[0; 13]: (945) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) )
% 1.17/1.54 ==> rd( ld( X, Y ), mult( Z, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (948) {G2,W15,D5,L1,V2,M1} { ld( ld( X, X ), rd( X, Y ) ) ==> rd
% 1.17/1.54 ( X, mult( Y, ld( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.54 parent1[0; 6]: (947) {G13,W19,D6,L1,V2,M1} { ld( ld( X, X ), rd( rd( X, ld
% 1.17/1.54 ( X, X ) ), Y ) ) ==> rd( X, mult( Y, ld( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (949) {G2,W15,D5,L1,V2,M1} { rd( X, mult( Y, ld( X, X ) ) ) ==> ld
% 1.17/1.54 ( ld( X, X ), rd( X, Y ) ) }.
% 1.17/1.54 parent0[0]: (948) {G2,W15,D5,L1,V2,M1} { ld( ld( X, X ), rd( X, Y ) ) ==>
% 1.17/1.54 rd( X, mult( Y, ld( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y,
% 1.17/1.54 ld( X, X ) ) ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 1.17/1.54 parent0: (949) {G2,W15,D5,L1,V2,M1} { rd( X, mult( Y, ld( X, X ) ) ) ==>
% 1.17/1.54 ld( ld( X, X ), rd( X, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (951) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) ) ==> rd
% 1.17/1.54 ( ld( ld( X, Y ), Z ), X ) }.
% 1.17/1.54 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 1.17/1.54 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (954) {G6,W11,D5,L1,V1,M1} { ld( X, rd( mult( X, X ), X ) ) ==>
% 1.17/1.54 rd( X, X ) }.
% 1.17/1.54 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.17/1.54 ld( X, X ), X ) ==> X }.
% 1.17/1.54 parent1[0; 9]: (951) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) )
% 1.17/1.54 ==> rd( ld( ld( X, Y ), Z ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (956) {G1,W7,D3,L1,V1,M1} { ld( X, X ) ==> rd( X, X ) }.
% 1.17/1.54 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.17/1.54 parent1[0; 3]: (954) {G6,W11,D5,L1,V1,M1} { ld( X, rd( mult( X, X ), X ) )
% 1.17/1.54 ==> rd( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (957) {G1,W7,D3,L1,V1,M1} { rd( X, X ) ==> ld( X, X ) }.
% 1.17/1.54 parent0[0]: (956) {G1,W7,D3,L1,V1,M1} { ld( X, X ) ==> rd( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld
% 1.17/1.54 ( X, X ) }.
% 1.17/1.54 parent0: (957) {G1,W7,D3,L1,V1,M1} { rd( X, X ) ==> ld( X, X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (959) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) ) ==> rd
% 1.17/1.54 ( ld( ld( X, Y ), Z ), X ) }.
% 1.17/1.54 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 1.17/1.54 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (964) {G6,W19,D6,L1,V2,M1} { ld( X, rd( mult( ld( X, X ), Y ), ld
% 1.17/1.54 ( X, X ) ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.17/1.54 ld( X, X ), X ) ==> X }.
% 1.17/1.54 parent1[0; 14]: (959) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X )
% 1.17/1.54 ) ==> rd( ld( ld( X, Y ), Z ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (965) {G5,W19,D6,L1,V2,M1} { ld( X, mult( mult( ld( X, X ), rd( Y
% 1.17/1.54 , X ) ), X ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 1.17/1.54 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.17/1.54 parent1[0; 3]: (964) {G6,W19,D6,L1,V2,M1} { ld( X, rd( mult( ld( X, X ), Y
% 1.17/1.54 ), ld( X, X ) ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (966) {G4,W15,D5,L1,V2,M1} { mult( ld( X, ld( X, X ) ), Y ) ==>
% 1.17/1.54 rd( ld( X, Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z
% 1.17/1.54 , X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.17/1.54 parent1[0; 1]: (965) {G5,W19,D6,L1,V2,M1} { ld( X, mult( mult( ld( X, X )
% 1.17/1.54 , rd( Y, X ) ), X ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (967) {G4,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==> mult
% 1.17/1.54 ( ld( X, ld( X, X ) ), Y ) }.
% 1.17/1.54 parent0[0]: (966) {G4,W15,D5,L1,V2,M1} { mult( ld( X, ld( X, X ) ), Y )
% 1.17/1.54 ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld( X
% 1.17/1.54 , Y ), ld( X, X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 1.17/1.54 parent0: (967) {G4,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 1.17/1.54 mult( ld( X, ld( X, X ) ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (969) {G16,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X, rd
% 1.17/1.54 ( X, X ) ) }.
% 1.17/1.54 parent0[0]: (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd( X
% 1.17/1.54 , X ) ) ==> ld( mult( X, X ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (970) {G17,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X, ld
% 1.17/1.54 ( X, X ) ) }.
% 1.17/1.54 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 1.17/1.54 X, X ) }.
% 1.17/1.54 parent1[0; 8]: (969) {G16,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld
% 1.17/1.54 ( X, rd( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (971) {G17,W11,D4,L1,V1,M1} { ld( X, ld( X, X ) ) ==> ld( mult( X
% 1.17/1.54 , X ), X ) }.
% 1.17/1.54 parent0[0]: (970) {G17,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X
% 1.17/1.54 , ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) )
% 1.17/1.54 ==> ld( mult( X, X ), X ) }.
% 1.17/1.54 parent0: (971) {G17,W11,D4,L1,V1,M1} { ld( X, ld( X, X ) ) ==> ld( mult( X
% 1.17/1.54 , X ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (973) {G14,W15,D5,L1,V3,M1} { mult( Y, rd( ld( Y, X ), Z ) ) ==>
% 1.17/1.54 rd( rd( X, Y ), rd( Z, Y ) ) }.
% 1.17/1.54 parent0[0]: (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z, X
% 1.17/1.54 ) ) ==> mult( X, rd( ld( X, Y ), Z ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (979) {G15,W15,D5,L1,V2,M1} { mult( X, rd( ld( X, Y ), X ) ) ==>
% 1.17/1.54 rd( rd( Y, X ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 1.17/1.54 X, X ) }.
% 1.17/1.54 parent1[0; 12]: (973) {G14,W15,D5,L1,V3,M1} { mult( Y, rd( ld( Y, X ), Z )
% 1.17/1.54 ) ==> rd( rd( X, Y ), rd( Z, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (983) {G15,W15,D5,L1,V2,M1} { rd( rd( Y, X ), ld( X, X ) ) ==>
% 1.17/1.54 mult( X, rd( ld( X, Y ), X ) ) }.
% 1.17/1.54 parent0[0]: (979) {G15,W15,D5,L1,V2,M1} { mult( X, rd( ld( X, Y ), X ) )
% 1.17/1.54 ==> rd( rd( Y, X ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X
% 1.17/1.54 , X ) ) ==> mult( X, rd( ld( X, Y ), X ) ) }.
% 1.17/1.54 parent0: (983) {G15,W15,D5,L1,V2,M1} { rd( rd( Y, X ), ld( X, X ) ) ==>
% 1.17/1.54 mult( X, rd( ld( X, Y ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 *** allocated 22500 integers for termspace/termends
% 1.17/1.54 eqswap: (985) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X, rd(
% 1.17/1.54 rd( Y, X ), rd( Z, X ) ) ) }.
% 1.17/1.54 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 1.17/1.54 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Z
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (988) {G14,W15,D5,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( X, ld(
% 1.17/1.54 rd( Y, X ), rd( Y, X ) ) ) }.
% 1.17/1.54 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 1.17/1.54 X, X ) }.
% 1.17/1.54 parent1[0; 8]: (985) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X
% 1.17/1.54 , rd( rd( Y, X ), rd( Z, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := rd( Y, X )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (991) {G6,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X, ld
% 1.17/1.54 ( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.17/1.54 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.17/1.54 ( mult( X, Y ), X ) }.
% 1.17/1.54 parent1[0; 1]: (988) {G14,W15,D5,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( X
% 1.17/1.54 , ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (992) {G6,W15,D5,L1,V2,M1} { ld( Y, ld( rd( X, Y ), rd( X, Y ) ) )
% 1.17/1.54 ==> ld( mult( X, Y ), X ) }.
% 1.17/1.54 parent0[0]: (991) {G6,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X,
% 1.17/1.54 ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd(
% 1.17/1.54 X, Y ), rd( X, Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 1.17/1.54 parent0: (992) {G6,W15,D5,L1,V2,M1} { ld( Y, ld( rd( X, Y ), rd( X, Y ) )
% 1.17/1.54 ) ==> ld( mult( X, Y ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (994) {G20,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X, ld
% 1.17/1.54 ( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.17/1.54 parent0[0]: (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd( X
% 1.17/1.54 , Y ), rd( X, Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (998) {G2,W19,D6,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X ) ==>
% 1.17/1.54 ld( ld( Y, X ), ld( rd( X, ld( Y, X ) ), Y ) ) }.
% 1.17/1.54 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.54 parent1[0; 18]: (994) {G20,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld
% 1.17/1.54 ( X, ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( Y, X )
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (999) {G2,W15,D5,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X ) ==>
% 1.17/1.54 ld( ld( Y, X ), ld( Y, Y ) ) }.
% 1.17/1.54 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.54 parent1[0; 13]: (998) {G2,W19,D6,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X
% 1.17/1.54 ) ==> ld( ld( Y, X ), ld( rd( X, ld( Y, X ) ), Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1001) {G2,W15,D5,L1,V2,M1} { ld( ld( Y, X ), ld( Y, Y ) ) ==> ld
% 1.17/1.54 ( mult( X, ld( Y, X ) ), X ) }.
% 1.17/1.54 parent0[0]: (999) {G2,W15,D5,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X )
% 1.17/1.54 ==> ld( ld( Y, X ), ld( Y, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (321) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y,
% 1.17/1.54 Y ) ) = ld( mult( X, ld( Y, X ) ), X ) }.
% 1.17/1.54 parent0: (1001) {G2,W15,D5,L1,V2,M1} { ld( ld( Y, X ), ld( Y, Y ) ) ==> ld
% 1.17/1.54 ( mult( X, ld( Y, X ) ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1004) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.17/1.54 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1005) {G2,W15,D5,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> ld( ld(
% 1.17/1.54 ld( Y, Y ), rd( Y, X ) ), Y ) }.
% 1.17/1.54 parent0[0]: (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y,
% 1.17/1.54 ld( X, X ) ) ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 1.17/1.54 parent1[0; 7]: (1004) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := mult( X, ld( Y, Y ) )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1006) {G2,W15,D5,L1,V2,M1} { ld( ld( ld( Y, Y ), rd( Y, X ) ), Y
% 1.17/1.54 ) ==> mult( X, ld( Y, Y ) ) }.
% 1.17/1.54 parent0[0]: (1005) {G2,W15,D5,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> ld( ld
% 1.17/1.54 ( ld( Y, Y ), rd( Y, X ) ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (363) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd
% 1.17/1.54 ( X, Y ) ), X ) ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.54 parent0: (1006) {G2,W15,D5,L1,V2,M1} { ld( ld( ld( Y, Y ), rd( Y, X ) ), Y
% 1.17/1.54 ) ==> mult( X, ld( Y, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1008) {G20,W15,D5,L1,V2,M1} { mult( Y, ld( X, X ) ) ==> ld( ld(
% 1.17/1.54 ld( X, X ), rd( X, Y ) ), X ) }.
% 1.17/1.54 parent0[0]: (363) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd(
% 1.17/1.54 X, Y ) ), X ) ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1011) {G2,W15,D5,L1,V2,M1} { mult( ld( X, Y ), ld( Y, Y ) ) ==>
% 1.17/1.54 ld( ld( ld( Y, Y ), X ), Y ) }.
% 1.17/1.54 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.17/1.54 parent1[0; 13]: (1008) {G20,W15,D5,L1,V2,M1} { mult( Y, ld( X, X ) ) ==>
% 1.17/1.54 ld( ld( ld( X, X ), rd( X, Y ) ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := ld( X, Y )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X
% 1.17/1.54 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 1.17/1.54 parent0: (1011) {G2,W15,D5,L1,V2,M1} { mult( ld( X, Y ), ld( Y, Y ) ) ==>
% 1.17/1.54 ld( ld( ld( Y, Y ), X ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1015) {G20,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 1.17/1.54 mult( ld( mult( X, X ), X ), Y ) }.
% 1.17/1.54 parent0[0]: (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) )
% 1.17/1.54 ==> ld( mult( X, X ), X ) }.
% 1.17/1.54 parent1[0; 9]: (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld
% 1.17/1.54 ( X, Y ), ld( X, X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (539) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld
% 1.17/1.54 ( X, X ) ) ==> mult( ld( mult( X, X ), X ), Y ) }.
% 1.17/1.54 parent0: (1015) {G20,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 1.17/1.54 mult( ld( mult( X, X ), X ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1018) {G21,W15,D5,L1,V2,M1} { mult( ld( mult( X, X ), X ), Y )
% 1.17/1.54 ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (539) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld
% 1.17/1.54 ( X, X ) ) ==> mult( ld( mult( X, X ), X ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1026) {G22,W27,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ), ld( X
% 1.17/1.54 , X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( mult( X, ld(
% 1.17/1.54 X, X ) ), X ) ) }.
% 1.17/1.54 parent0[0]: (321) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y, Y
% 1.17/1.54 ) ) = ld( mult( X, ld( Y, X ) ), X ) }.
% 1.17/1.54 parent1[0; 20]: (1018) {G21,W15,D5,L1,V2,M1} { mult( ld( mult( X, X ), X )
% 1.17/1.54 , Y ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1027) {G1,W23,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ), ld( X,
% 1.17/1.54 X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.54 parent1[0; 21]: (1026) {G22,W27,D6,L1,V2,M1} { mult( ld( mult( ld( X, X )
% 1.17/1.54 , ld( X, X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( mult(
% 1.17/1.54 X, ld( X, X ) ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1028) {G2,W23,D7,L1,V2,M1} { mult( ld( ld( ld( ld( X, X ), X ),
% 1.17/1.54 X ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X
% 1.17/1.54 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 1.17/1.54 parent1[0; 3]: (1027) {G1,W23,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ),
% 1.17/1.54 ld( X, X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) )
% 1.17/1.54 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1029) {G3,W19,D5,L1,V2,M1} { mult( ld( ld( X, X ), ld( X, X ) )
% 1.17/1.54 , Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.17/1.54 ld( X, X ), X ) ==> X }.
% 1.17/1.54 parent1[0; 4]: (1028) {G2,W23,D7,L1,V2,M1} { mult( ld( ld( ld( ld( X, X )
% 1.17/1.54 , X ), X ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) )
% 1.17/1.54 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1030) {G4,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld(
% 1.17/1.54 ld( X, X ), Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.17/1.54 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 2]: (1029) {G3,W19,D5,L1,V2,M1} { mult( ld( ld( X, X ), ld( X,
% 1.17/1.54 X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1031) {G4,W15,D5,L1,V2,M1} { rd( ld( ld( X, X ), Y ), ld( X, X )
% 1.17/1.54 ) ==> mult( ld( X, X ), Y ) }.
% 1.17/1.54 parent0[0]: (1030) {G4,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld
% 1.17/1.54 ( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(
% 1.17/1.54 212) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y )
% 1.17/1.54 }.
% 1.17/1.54 parent0: (1031) {G4,W15,D5,L1,V2,M1} { rd( ld( ld( X, X ), Y ), ld( X, X )
% 1.17/1.54 ) ==> mult( ld( X, X ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1033) {G20,W15,D5,L1,V2,M1} { mult( Y, rd( ld( Y, X ), Y ) ) ==>
% 1.17/1.54 rd( rd( X, Y ), ld( Y, Y ) ) }.
% 1.17/1.54 parent0[0]: (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X
% 1.17/1.54 , X ) ) ==> mult( X, rd( ld( X, Y ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1041) {G21,W31,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 1.17/1.54 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X ), Y ),
% 1.17/1.54 ld( ld( X, X ), ld( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(212
% 1.17/1.54 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 1.17/1.54 parent1[0; 19]: (1033) {G20,W15,D5,L1,V2,M1} { mult( Y, rd( ld( Y, X ), Y
% 1.17/1.54 ) ) ==> rd( rd( X, Y ), ld( Y, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( ld( X, X ), Y )
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1043) {G16,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 1.17/1.54 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X ), Y ),
% 1.17/1.54 ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.17/1.54 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.17/1.54 parent1[0; 24]: (1041) {G21,W31,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld(
% 1.17/1.54 ld( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X
% 1.17/1.54 ), Y ), ld( ld( X, X ), ld( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1044) {G5,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 1.17/1.54 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> mult( mult( ld( X, X ), rd
% 1.17/1.54 ( Y, X ) ), X ) }.
% 1.17/1.54 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 1.17/1.54 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.17/1.54 parent1[0; 18]: (1043) {G16,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld(
% 1.17/1.54 ld( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X
% 1.17/1.54 ), Y ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1045) {G6,W27,D6,L1,V2,M1} { mult( ld( X, X ), ld( mult( ld( X,
% 1.17/1.54 X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd
% 1.17/1.54 ( Y, X ) ), X ) }.
% 1.17/1.54 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.17/1.54 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.17/1.54 parent1[0; 5]: (1044) {G5,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld
% 1.17/1.54 ( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> mult( mult( ld( X, X
% 1.17/1.54 ), rd( Y, X ) ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1046) {G7,W27,D7,L1,V2,M1} { mult( ld( X, X ), ld( ld( ld( ld( X
% 1.17/1.54 , X ), X ), X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd(
% 1.17/1.54 Y, X ) ), X ) }.
% 1.17/1.54 parent0[0]: (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X
% 1.17/1.54 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 1.17/1.54 parent1[0; 6]: (1045) {G6,W27,D6,L1,V2,M1} { mult( ld( X, X ), ld( mult(
% 1.17/1.54 ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X,
% 1.17/1.54 X ), rd( Y, X ) ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1047) {G8,W23,D6,L1,V2,M1} { mult( ld( X, X ), ld( ld( X, X ),
% 1.17/1.54 rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd( Y, X ) ), X ) }.
% 1.17/1.54 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.17/1.54 ld( X, X ), X ) ==> X }.
% 1.17/1.54 parent1[0; 7]: (1046) {G7,W27,D7,L1,V2,M1} { mult( ld( X, X ), ld( ld( ld
% 1.17/1.54 ( ld( X, X ), X ), X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X
% 1.17/1.54 ), rd( Y, X ) ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1048) {G1,W15,D5,L1,V2,M1} { rd( Y, ld( X, X ) ) ==> mult( mult
% 1.17/1.54 ( ld( X, X ), rd( Y, X ) ), X ) }.
% 1.17/1.54 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.54 parent1[0; 1]: (1047) {G8,W23,D6,L1,V2,M1} { mult( ld( X, X ), ld( ld( X,
% 1.17/1.54 X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd( Y, X ) ), X
% 1.17/1.54 ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := rd( Y, ld( X, X ) )
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1049) {G1,W15,D5,L1,V2,M1} { mult( mult( ld( Y, Y ), rd( X, Y ) )
% 1.17/1.54 , Y ) ==> rd( X, ld( Y, Y ) ) }.
% 1.17/1.54 parent0[0]: (1048) {G1,W15,D5,L1,V2,M1} { rd( Y, ld( X, X ) ) ==> mult(
% 1.17/1.54 mult( ld( X, X ), rd( Y, X ) ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (553) {G23,W15,D5,L1,V2,M1} P(543,270);d(212);d(194);d(38);d(
% 1.17/1.54 366);d(242);d(0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y,
% 1.17/1.54 ld( X, X ) ) }.
% 1.17/1.54 parent0: (1049) {G1,W15,D5,L1,V2,M1} { mult( mult( ld( Y, Y ), rd( X, Y )
% 1.17/1.54 ), Y ) ==> rd( X, ld( Y, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1050) {G22,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld(
% 1.17/1.54 ld( X, X ), Y ), ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(212
% 1.17/1.54 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1055) {G6,W23,D5,L1,V2,M1} { mult( ld( X, X ), ld( ld( X, X ), Y
% 1.17/1.54 ) ) ==> ld( mult( ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.17/1.54 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.17/1.54 parent1[0; 10]: (1050) {G22,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==>
% 1.17/1.54 rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := ld( ld( X, X ), Y )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1056) {G1,W15,D5,L1,V2,M1} { Y ==> ld( mult( ld( X, X ), ld( X,
% 1.17/1.54 X ) ), rd( Y, ld( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.54 parent1[0; 1]: (1055) {G6,W23,D5,L1,V2,M1} { mult( ld( X, X ), ld( ld( X,
% 1.17/1.54 X ), Y ) ) ==> ld( mult( ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) )
% 1.17/1.54 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1057) {G2,W15,D6,L1,V2,M1} { X ==> ld( ld( ld( ld( Y, Y ), Y ),
% 1.17/1.54 Y ), rd( X, ld( Y, Y ) ) ) }.
% 1.17/1.54 parent0[0]: (366) {G21,W15,D5,L1,V2,M1} P(7,363) { mult( ld( Y, X ), ld( X
% 1.17/1.54 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 1.17/1.54 parent1[0; 3]: (1056) {G1,W15,D5,L1,V2,M1} { Y ==> ld( mult( ld( X, X ),
% 1.17/1.54 ld( X, X ) ), rd( Y, ld( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1058) {G3,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, Y ), rd( X, ld( Y
% 1.17/1.54 , Y ) ) ) }.
% 1.17/1.54 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.17/1.54 ld( X, X ), X ) ==> X }.
% 1.17/1.54 parent1[0; 4]: (1057) {G2,W15,D6,L1,V2,M1} { X ==> ld( ld( ld( ld( Y, Y )
% 1.17/1.54 , Y ), Y ), rd( X, ld( Y, Y ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1059) {G3,W11,D5,L1,V2,M1} { ld( ld( Y, Y ), rd( X, ld( Y, Y ) )
% 1.17/1.54 ) ==> X }.
% 1.17/1.54 parent0[0]: (1058) {G3,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, Y ), rd( X, ld
% 1.17/1.54 ( Y, Y ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld
% 1.17/1.54 ( ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.17/1.54 parent0: (1059) {G3,W11,D5,L1,V2,M1} { ld( ld( Y, Y ), rd( X, ld( Y, Y ) )
% 1.17/1.54 ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1061) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y, ld( X
% 1.17/1.54 , X ) ) ) }.
% 1.17/1.54 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 1.17/1.54 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1064) {G23,W15,D5,L1,V2,M1} { ld( ld( X, X ), Y ) ==> ld( ld( X
% 1.17/1.54 , X ), mult( ld( X, X ), Y ) ) }.
% 1.17/1.54 parent0[0]: (543) {G22,W15,D5,L1,V2,M1} P(321,539);d(0);d(366);d(242);d(212
% 1.17/1.54 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 1.17/1.54 parent1[0; 10]: (1061) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y
% 1.17/1.54 , ld( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := ld( ld( X, X ), Y )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1065) {G1,W7,D4,L1,V2,M1} { ld( ld( X, X ), Y ) ==> Y }.
% 1.17/1.54 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.17/1.54 parent1[0; 6]: (1064) {G23,W15,D5,L1,V2,M1} { ld( ld( X, X ), Y ) ==> ld(
% 1.17/1.54 ld( X, X ), mult( ld( X, X ), Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 1.17/1.54 ) ==> Y }.
% 1.17/1.54 parent0: (1065) {G1,W7,D4,L1,V2,M1} { ld( ld( X, X ), Y ) ==> Y }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1068) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) ) ==>
% 1.17/1.54 mult( ld( X, rd( Y, Z ) ), Z ) }.
% 1.17/1.54 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 1.17/1.54 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1073) {G9,W19,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X ) ),
% 1.17/1.54 ld( ld( X, X ), Y ) ) ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 1.17/1.54 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.17/1.54 parent1[0; 15]: (1068) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) )
% 1.17/1.54 ==> mult( ld( X, rd( Y, Z ) ), Z ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1076) {G10,W15,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X ) ),
% 1.17/1.54 Y ) ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 1.17/1.54 ) ==> Y }.
% 1.17/1.54 parent1[0; 9]: (1073) {G9,W19,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X
% 1.17/1.54 ) ), ld( ld( X, X ), Y ) ) ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1078) {G11,W7,D4,L1,V2,M1} { Y ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.54 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 1.17/1.54 ) ==> Y }.
% 1.17/1.54 parent1[0; 1]: (1076) {G10,W15,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X
% 1.17/1.54 ) ), Y ) ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1080) {G11,W7,D4,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> X }.
% 1.17/1.54 parent0[0]: (1078) {G11,W7,D4,L1,V2,M1} { Y ==> mult( Y, ld( X, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (583) {G25,W7,D4,L1,V2,M1} P(557,129);d(564);d(564) { mult( Y
% 1.17/1.54 , ld( X, X ) ) ==> Y }.
% 1.17/1.54 parent0: (1080) {G11,W7,D4,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1083) {G7,W15,D5,L1,V3,M1} { Z ==> ld( ld( X, rd( Y, Z ) ), ld(
% 1.17/1.54 ld( Z, X ), ld( Z, Y ) ) ) }.
% 1.17/1.54 parent0[0]: (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) ),
% 1.17/1.54 ld( ld( X, Y ), ld( X, Z ) ) ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Z
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1086) {G8,W19,D6,L1,V2,M1} { ld( X, X ) ==> ld( Y, ld( ld( ld( X
% 1.17/1.54 , X ), ld( X, X ) ), ld( ld( X, X ), Y ) ) ) }.
% 1.17/1.54 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 1.17/1.54 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.17/1.54 parent1[0; 5]: (1083) {G7,W15,D5,L1,V3,M1} { Z ==> ld( ld( X, rd( Y, Z ) )
% 1.17/1.54 , ld( ld( Z, X ), ld( Z, Y ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := ld( X, X )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1093) {G9,W15,D6,L1,V2,M1} { ld( X, X ) ==> ld( Y, ld( ld( ld( X
% 1.17/1.54 , X ), ld( X, X ) ), Y ) ) }.
% 1.17/1.54 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 1.17/1.54 ) ==> Y }.
% 1.17/1.54 parent1[0; 14]: (1086) {G8,W19,D6,L1,V2,M1} { ld( X, X ) ==> ld( Y, ld( ld
% 1.17/1.54 ( ld( X, X ), ld( X, X ) ), ld( ld( X, X ), Y ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1095) {G10,W7,D3,L1,V2,M1} { ld( X, X ) ==> ld( Y, Y ) }.
% 1.17/1.54 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 1.17/1.54 ) ==> Y }.
% 1.17/1.54 parent1[0; 6]: (1093) {G9,W15,D6,L1,V2,M1} { ld( X, X ) ==> ld( Y, ld( ld
% 1.17/1.54 ( ld( X, X ), ld( X, X ) ), Y ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (584) {G25,W7,D3,L1,V2,M1} P(557,120);d(564);d(564) { ld( Y, Y
% 1.17/1.54 ) = ld( X, X ) }.
% 1.17/1.54 parent0: (1095) {G10,W7,D3,L1,V2,M1} { ld( X, X ) ==> ld( Y, Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1099) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y, ld( X
% 1.17/1.54 , X ) ) ) }.
% 1.17/1.54 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 1.17/1.54 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1109) {G6,W23,D7,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 1.17/1.54 ( ld( X, X ), ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) ) }.
% 1.17/1.54 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 1.17/1.54 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 1.17/1.54 parent1[0; 12]: (1099) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y
% 1.17/1.54 , ld( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := ld( X, X )
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := ld( ld( ld( X, X ), Y ), Z )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1111) {G7,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 1.17/1.54 ( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 1.17/1.54 ) ==> Y }.
% 1.17/1.54 parent1[0; 8]: (1109) {G6,W23,D7,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 1.17/1.54 ==> ld( ld( X, X ), ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) )
% 1.17/1.54 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1113) {G5,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 1.17/1.54 ( Y, mult( mult( ld( X, X ), rd( Z, X ) ), X ) ) }.
% 1.17/1.54 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 1.17/1.54 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.17/1.54 parent1[0; 10]: (1111) {G7,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 1.17/1.54 ==> ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1114) {G6,W15,D5,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 1.17/1.54 ( Y, rd( Z, ld( X, X ) ) ) }.
% 1.17/1.54 parent0[0]: (553) {G23,W15,D5,L1,V2,M1} P(543,270);d(212);d(194);d(38);d(
% 1.17/1.54 366);d(242);d(0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y,
% 1.17/1.54 ld( X, X ) ) }.
% 1.17/1.54 parent1[0; 10]: (1113) {G5,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 1.17/1.54 ==> ld( Y, mult( mult( ld( X, X ), rd( Z, X ) ), X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Z
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1115) {G7,W11,D5,L1,V3,M1} { ld( Y, Z ) ==> ld( Y, rd( Z, ld( X
% 1.17/1.54 , X ) ) ) }.
% 1.17/1.54 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 1.17/1.54 ) ==> Y }.
% 1.17/1.54 parent1[0; 2]: (1114) {G6,W15,D5,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 1.17/1.54 ==> ld( Y, rd( Z, ld( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 Z := Z
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1116) {G7,W11,D5,L1,V3,M1} { ld( X, rd( Y, ld( Z, Z ) ) ) ==> ld
% 1.17/1.54 ( X, Y ) }.
% 1.17/1.54 parent0[0]: (1115) {G7,W11,D5,L1,V3,M1} { ld( Y, Z ) ==> ld( Y, rd( Z, ld
% 1.17/1.54 ( X, X ) ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Z
% 1.17/1.54 Y := X
% 1.17/1.54 Z := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (590) {G25,W11,D5,L1,V3,M1} P(37,557);d(564);d(194);d(553);d(
% 1.17/1.54 564) { ld( Y, rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 1.17/1.54 parent0: (1116) {G7,W11,D5,L1,V3,M1} { ld( X, rd( Y, ld( Z, Z ) ) ) ==> ld
% 1.17/1.54 ( X, Y ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := Z
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1118) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld
% 1.17/1.54 ( Y, X ) ) }.
% 1.17/1.54 parent0[0]: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ),
% 1.17/1.54 ld( X, Y ) ) ==> Y }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1123) {G7,W23,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld(
% 1.17/1.54 mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), rd( X, ld( Y, Y ) ) ), X ) }.
% 1.17/1.54 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 1.17/1.54 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.17/1.54 parent1[0; 22]: (1118) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ),
% 1.17/1.54 X ), ld( Y, X ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := rd( X, ld( Y, Y ) )
% 1.17/1.54 Y := ld( Y, Y )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1124) {G8,W19,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld(
% 1.17/1.54 mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), X ), X ) }.
% 1.17/1.54 parent0[0]: (590) {G25,W11,D5,L1,V3,M1} P(37,557);d(564);d(194);d(553);d(
% 1.17/1.54 564) { ld( Y, rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 1.17/1.54 parent1[0; 7]: (1123) {G7,W23,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 1.17/1.54 ld( mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), rd( X, ld( Y, Y ) ) ), X )
% 1.17/1.54 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) )
% 1.17/1.54 Z := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1125) {G9,W15,D6,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld( rd
% 1.17/1.54 ( X, ld( Y, Y ) ), X ), X ) }.
% 1.17/1.54 parent0[0]: (583) {G25,W7,D4,L1,V2,M1} P(557,129);d(564);d(564) { mult( Y,
% 1.17/1.54 ld( X, X ) ) ==> Y }.
% 1.17/1.54 parent1[0; 8]: (1124) {G8,W19,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 1.17/1.54 ld( mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), X ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := rd( X, ld( Y, Y ) )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1126) {G2,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld( Y,
% 1.17/1.54 Y ), X ) }.
% 1.17/1.54 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.17/1.54 parent1[0; 7]: (1125) {G9,W15,D6,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 1.17/1.54 ld( rd( X, ld( Y, Y ) ), X ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := ld( Y, Y )
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1127) {G3,W7,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> X }.
% 1.17/1.54 parent0[0]: (564) {G24,W7,D4,L1,V2,M1} P(543,557);d(1) { ld( ld( X, X ), Y
% 1.17/1.54 ) ==> Y }.
% 1.17/1.54 parent1[0; 6]: (1126) {G2,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 1.17/1.54 ld( Y, Y ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (594) {G26,W7,D4,L1,V2,M1} P(557,43);d(590);d(583);d(6);d(564)
% 1.17/1.54 { rd( Y, ld( X, X ) ) ==> Y }.
% 1.17/1.54 parent0: (1127) {G3,W7,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1130) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 1.17/1.54 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1132) {G1,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> mult( ld( Y
% 1.17/1.54 , Y ), X ) }.
% 1.17/1.54 parent0[0]: (557) {G23,W11,D5,L1,V2,M1} P(543,38);d(0);d(366);d(242) { ld(
% 1.17/1.54 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.17/1.54 parent1[0; 10]: (1130) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 1.17/1.54 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := ld( Y, Y )
% 1.17/1.54 Y := rd( X, ld( Y, Y ) )
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1133) {G2,W7,D4,L1,V2,M1} { X ==> mult( ld( Y, Y ), X ) }.
% 1.17/1.54 parent0[0]: (594) {G26,W7,D4,L1,V2,M1} P(557,43);d(590);d(583);d(6);d(564)
% 1.17/1.54 { rd( Y, ld( X, X ) ) ==> Y }.
% 1.17/1.54 parent1[0; 1]: (1132) {G1,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> mult
% 1.17/1.54 ( ld( Y, Y ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1134) {G2,W7,D4,L1,V2,M1} { mult( ld( Y, Y ), X ) ==> X }.
% 1.17/1.54 parent0[0]: (1133) {G2,W7,D4,L1,V2,M1} { X ==> mult( ld( Y, Y ), X ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := Y
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (598) {G27,W7,D4,L1,V2,M1} P(557,0);d(594) { mult( ld( X, X )
% 1.17/1.54 , Y ) ==> Y }.
% 1.17/1.54 parent0: (1134) {G2,W7,D4,L1,V2,M1} { mult( ld( Y, Y ), X ) ==> X }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := Y
% 1.17/1.54 Y := X
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 0 ==> 0
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqswap: (1135) {G0,W14,D4,L2,V0,M2} { ! skol1 ==> mult( skol1, ld( skol2,
% 1.17/1.54 skol2 ) ), ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.17/1.54 parent0[0]: (5) {G0,W14,D4,L2,V0,M2} I { ! mult( skol1, ld( skol2, skol2 )
% 1.17/1.54 ) ==> skol1, ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1141) {G1,W14,D4,L2,V1,M2} { ! mult( ld( X, X ), skol1 ) ==>
% 1.17/1.54 skol1, ! skol1 ==> mult( skol1, ld( skol2, skol2 ) ) }.
% 1.17/1.54 parent0[0]: (584) {G25,W7,D3,L1,V2,M1} P(557,120);d(564);d(564) { ld( Y, Y
% 1.17/1.54 ) = ld( X, X ) }.
% 1.17/1.54 parent1[1; 3]: (1135) {G0,W14,D4,L2,V0,M2} { ! skol1 ==> mult( skol1, ld(
% 1.17/1.54 skol2, skol2 ) ), ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := skol2
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1143) {G2,W10,D4,L2,V1,M2} { ! skol1 ==> skol1, ! mult( ld( X, X
% 1.17/1.54 ), skol1 ) ==> skol1 }.
% 1.17/1.54 parent0[0]: (583) {G25,W7,D4,L1,V2,M1} P(557,129);d(564);d(564) { mult( Y,
% 1.17/1.54 ld( X, X ) ) ==> Y }.
% 1.17/1.54 parent1[1; 3]: (1141) {G1,W14,D4,L2,V1,M2} { ! mult( ld( X, X ), skol1 )
% 1.17/1.54 ==> skol1, ! skol1 ==> mult( skol1, ld( skol2, skol2 ) ) }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := skol2
% 1.17/1.54 Y := skol1
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 paramod: (1144) {G3,W6,D2,L2,V0,M2} { ! skol1 ==> skol1, ! skol1 ==> skol1
% 1.17/1.54 }.
% 1.17/1.54 parent0[0]: (598) {G27,W7,D4,L1,V2,M1} P(557,0);d(594) { mult( ld( X, X ),
% 1.17/1.54 Y ) ==> Y }.
% 1.17/1.54 parent1[1; 2]: (1143) {G2,W10,D4,L2,V1,M2} { ! skol1 ==> skol1, ! mult( ld
% 1.17/1.54 ( X, X ), skol1 ) ==> skol1 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 X := X
% 1.17/1.54 Y := skol1
% 1.17/1.54 end
% 1.17/1.54 substitution1:
% 1.17/1.54 X := X
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqrefl: (1147) {G0,W3,D2,L1,V0,M1} { ! skol1 ==> skol1 }.
% 1.17/1.54 parent0[0]: (1144) {G3,W6,D2,L2,V0,M2} { ! skol1 ==> skol1, ! skol1 ==>
% 1.17/1.54 skol1 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 eqrefl: (1148) {G0,W0,D0,L0,V0,M0} { }.
% 1.17/1.54 parent0[0]: (1147) {G0,W3,D2,L1,V0,M1} { ! skol1 ==> skol1 }.
% 1.17/1.54 substitution0:
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 subsumption: (635) {G28,W0,D0,L0,V0,M0} P(584,5);d(583);d(598);q;q { }.
% 1.17/1.54 parent0: (1148) {G0,W0,D0,L0,V0,M0} { }.
% 1.17/1.54 substitution0:
% 1.17/1.54 end
% 1.17/1.54 permutation0:
% 1.17/1.54 end
% 1.17/1.54
% 1.17/1.54 Proof check complete!
% 1.17/1.54
% 1.17/1.54 Memory use:
% 1.17/1.54
% 1.17/1.54 space for terms: 10784
% 1.17/1.54 space for clauses: 99706
% 1.17/1.54
% 1.17/1.54
% 1.17/1.54 clauses generated: 7410
% 1.17/1.54 clauses kept: 636
% 1.17/1.54 clauses selected: 119
% 1.17/1.54 clauses deleted: 21
% 1.17/1.54 clauses inuse deleted: 0
% 1.17/1.54
% 1.17/1.54 subsentry: 1403
% 1.17/1.54 literals s-matched: 485
% 1.17/1.54 literals matched: 461
% 1.17/1.54 full subsumption: 0
% 1.17/1.54
% 1.17/1.54 checksum: 1484155447
% 1.17/1.54
% 1.17/1.54
% 1.17/1.54 Bliksem ended
%------------------------------------------------------------------------------