%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP660+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n016.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.09s 1.47s
% Output : Refutation 1.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP660+2 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n016.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Mon Jun 13 21:14:45 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.09/1.47 *** allocated 10000 integers for termspace/termends
% 1.09/1.47 *** allocated 10000 integers for clauses
% 1.09/1.47 *** allocated 10000 integers for justifications
% 1.09/1.47 Bliksem 1.12
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 Automatic Strategy Selection
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 Clauses:
% 1.09/1.47
% 1.09/1.47 { mult( Y, ld( Y, X ) ) = X }.
% 1.09/1.47 { ld( Y, mult( Y, X ) ) = X }.
% 1.09/1.47 { mult( rd( Y, X ), X ) = Y }.
% 1.09/1.47 { rd( mult( Y, X ), X ) = Y }.
% 1.09/1.47 { mult( mult( mult( Z, Y ), X ), Z ) = mult( Z, mult( Y, mult( X, Z ) ) ) }
% 1.09/1.47 .
% 1.09/1.47 { ! mult( skol1, rd( skol2, skol2 ) ) = skol1, ! mult( rd( skol2, skol2 ),
% 1.09/1.47 skol1 ) = skol1 }.
% 1.09/1.47
% 1.09/1.47 percentage equality = 1.000000, percentage horn = 1.000000
% 1.09/1.47 This is a pure equality problem
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 Options Used:
% 1.09/1.47
% 1.09/1.47 useres = 1
% 1.09/1.47 useparamod = 1
% 1.09/1.47 useeqrefl = 1
% 1.09/1.47 useeqfact = 1
% 1.09/1.47 usefactor = 1
% 1.09/1.47 usesimpsplitting = 0
% 1.09/1.47 usesimpdemod = 5
% 1.09/1.47 usesimpres = 3
% 1.09/1.47
% 1.09/1.47 resimpinuse = 1000
% 1.09/1.47 resimpclauses = 20000
% 1.09/1.47 substype = eqrewr
% 1.09/1.47 backwardsubs = 1
% 1.09/1.47 selectoldest = 5
% 1.09/1.47
% 1.09/1.47 litorderings [0] = split
% 1.09/1.47 litorderings [1] = extend the termordering, first sorting on arguments
% 1.09/1.47
% 1.09/1.47 termordering = kbo
% 1.09/1.47
% 1.09/1.47 litapriori = 0
% 1.09/1.47 termapriori = 1
% 1.09/1.47 litaposteriori = 0
% 1.09/1.47 termaposteriori = 0
% 1.09/1.47 demodaposteriori = 0
% 1.09/1.47 ordereqreflfact = 0
% 1.09/1.47
% 1.09/1.47 litselect = negord
% 1.09/1.47
% 1.09/1.47 maxweight = 15
% 1.09/1.47 maxdepth = 30000
% 1.09/1.47 maxlength = 115
% 1.09/1.47 maxnrvars = 195
% 1.09/1.47 excuselevel = 1
% 1.09/1.47 increasemaxweight = 1
% 1.09/1.47
% 1.09/1.47 maxselected = 10000000
% 1.09/1.47 maxnrclauses = 10000000
% 1.09/1.47
% 1.09/1.47 showgenerated = 0
% 1.09/1.47 showkept = 0
% 1.09/1.47 showselected = 0
% 1.09/1.47 showdeleted = 0
% 1.09/1.47 showresimp = 1
% 1.09/1.47 showstatus = 2000
% 1.09/1.47
% 1.09/1.47 prologoutput = 0
% 1.09/1.47 nrgoals = 5000000
% 1.09/1.47 totalproof = 1
% 1.09/1.47
% 1.09/1.47 Symbols occurring in the translation:
% 1.09/1.47
% 1.09/1.47 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.09/1.47 . [1, 2] (w:1, o:18, a:1, s:1, b:0),
% 1.09/1.47 ! [4, 1] (w:0, o:13, a:1, s:1, b:0),
% 1.09/1.47 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.09/1.47 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.09/1.47 ld [37, 2] (w:1, o:42, a:1, s:1, b:0),
% 1.09/1.47 mult [38, 2] (w:1, o:43, a:1, s:1, b:0),
% 1.09/1.47 rd [39, 2] (w:1, o:44, a:1, s:1, b:0),
% 1.09/1.47 skol1 [43, 0] (w:1, o:11, a:1, s:1, b:1),
% 1.09/1.47 skol2 [44, 0] (w:1, o:12, a:1, s:1, b:1).
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 Starting Search:
% 1.09/1.47
% 1.09/1.47 *** allocated 15000 integers for clauses
% 1.09/1.47 *** allocated 22500 integers for clauses
% 1.09/1.47 *** allocated 33750 integers for clauses
% 1.09/1.47 Resimplifying inuse:
% 1.09/1.47 Done
% 1.09/1.47
% 1.09/1.47 Resimplifying inuse:
% 1.09/1.47 Done
% 1.09/1.47
% 1.09/1.47 Failed to find proof!
% 1.09/1.47 maxweight = 15
% 1.09/1.47 maxnrclauses = 10000000
% 1.09/1.47 Generated: 12709
% 1.09/1.47 Kept: 232
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 The strategy used was not complete!
% 1.09/1.47
% 1.09/1.47 Increased maxweight to 16
% 1.09/1.47
% 1.09/1.47 Starting Search:
% 1.09/1.47
% 1.09/1.47 Resimplifying inuse:
% 1.09/1.47 Done
% 1.09/1.47
% 1.09/1.47 Resimplifying inuse:
% 1.09/1.47 Done
% 1.09/1.47
% 1.09/1.47 Failed to find proof!
% 1.09/1.47 maxweight = 16
% 1.09/1.47 maxnrclauses = 10000000
% 1.09/1.47 Generated: 12709
% 1.09/1.47 Kept: 232
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 The strategy used was not complete!
% 1.09/1.47
% 1.09/1.47 Increased maxweight to 17
% 1.09/1.47
% 1.09/1.47 Starting Search:
% 1.09/1.47
% 1.09/1.47 Resimplifying inuse:
% 1.09/1.47 Done
% 1.09/1.47
% 1.09/1.47 Resimplifying inuse:
% 1.09/1.47 Done
% 1.09/1.47
% 1.09/1.47 Failed to find proof!
% 1.09/1.47 maxweight = 17
% 1.09/1.47 maxnrclauses = 10000000
% 1.09/1.47 Generated: 12709
% 1.09/1.47 Kept: 232
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 The strategy used was not complete!
% 1.09/1.47
% 1.09/1.47 Increased maxweight to 18
% 1.09/1.47
% 1.09/1.47 Starting Search:
% 1.09/1.47
% 1.09/1.47 Resimplifying inuse:
% 1.09/1.47 Done
% 1.09/1.47
% 1.09/1.47 Resimplifying inuse:
% 1.09/1.47 Done
% 1.09/1.47
% 1.09/1.47 Failed to find proof!
% 1.09/1.47 maxweight = 18
% 1.09/1.47 maxnrclauses = 10000000
% 1.09/1.47 Generated: 12709
% 1.09/1.47 Kept: 232
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 The strategy used was not complete!
% 1.09/1.47
% 1.09/1.47 Increased maxweight to 19
% 1.09/1.47
% 1.09/1.47 Starting Search:
% 1.09/1.47
% 1.09/1.47 *** allocated 50625 integers for clauses
% 1.09/1.47 *** allocated 75937 integers for clauses
% 1.09/1.47 *** allocated 113905 integers for clauses
% 1.09/1.47 *** allocated 15000 integers for termspace/termends
% 1.09/1.47
% 1.09/1.47 Bliksems!, er is een bewijs:
% 1.09/1.47 % SZS status Theorem
% 1.09/1.47 % SZS output start Refutation
% 1.09/1.47
% 1.09/1.47 (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.09/1.47 (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.09/1.47 (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) ) ==> mult(
% 1.09/1.47 mult( mult( Z, Y ), X ), Z ) }.
% 1.09/1.47 (5) {G0,W14,D4,L2,V0,M2} I { ! mult( skol1, rd( skol2, skol2 ) ) ==> skol1
% 1.09/1.47 , ! mult( rd( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.47 (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.09/1.47 (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.47 (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y ), Z ), X ),
% 1.09/1.47 ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.09/1.47 (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd( X, Y ) ),
% 1.09/1.47 Y ) ==> mult( Y, mult( Z, X ) ) }.
% 1.09/1.47 (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 1.09/1.47 mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.09/1.47 (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 1.09/1.47 mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.09/1.47 (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z, X ) ), X )
% 1.09/1.47 ) ==> mult( ld( X, Y ), Z ) }.
% 1.09/1.47 (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld( X, Y ), Z )
% 1.09/1.47 ) ==> rd( mult( Z, Y ), Z ) }.
% 1.09/1.47 (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) ), rd( Y, Z )
% 1.09/1.47 ) ==> rd( mult( Z, X ), Z ) }.
% 1.09/1.47 (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult( X, Z ), X )
% 1.09/1.47 ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X ) ==> ld( Y
% 1.09/1.47 , rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X ) ==> ld(
% 1.09/1.47 mult( X, Z ), rd( Y, X ) ) }.
% 1.09/1.47 (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld( mult( X, Y
% 1.09/1.47 ), X ) }.
% 1.09/1.47 (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ), ld( X, Y ) )
% 1.09/1.47 ==> Y }.
% 1.09/1.47 (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X, Y ), X ) )
% 1.09/1.47 ==> X }.
% 1.09/1.47 (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==> ld( ld( Y, X
% 1.09/1.47 ), Y ) }.
% 1.09/1.47 (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd( Z, Y ) ), ld
% 1.09/1.47 ( X, ld( Y, Z ) ) ) ==> Y }.
% 1.09/1.47 (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) ), ld( ld( X, Y
% 1.09/1.47 ), ld( X, Z ) ) ) ==> X }.
% 1.09/1.47 (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) ), Z ) ==> ld
% 1.09/1.47 ( ld( Z, X ), ld( Z, Y ) ) }.
% 1.09/1.47 (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y, mult( X, Y ) )
% 1.09/1.47 ) ==> mult( ld( Z, X ), Y ) }.
% 1.09/1.47 (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X ) ), mult( ld
% 1.09/1.47 ( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.09/1.47 (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z ) ), mult( Y,
% 1.09/1.47 Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.09/1.47 (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X ), X ), mult(
% 1.09/1.47 Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.09/1.47 (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z, Y ) ) ==>
% 1.09/1.47 ld( Y, rd( rd( X, Y ), Z ) ) }.
% 1.09/1.47 (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y ) ), X ) ==>
% 1.09/1.47 ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 1.09/1.47 (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ), rd( X, Y ) )
% 1.09/1.47 ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y, rd( Z, ld( Y
% 1.09/1.47 , X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 1.09/1.47 (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z, X ) ) ==>
% 1.09/1.47 mult( X, rd( ld( X, Y ), Z ) ) }.
% 1.09/1.47 (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z ), ld( Y, X )
% 1.09/1.47 ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.09/1.47 (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X ), rd( X, X
% 1.09/1.47 ) ) ==> rd( X, X ) }.
% 1.09/1.47 (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X ), rd( X, X )
% 1.09/1.47 ) ==> rd( X, X ) }.
% 1.09/1.47 (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X, X ), ld( X,
% 1.09/1.47 X ) ) ==> ld( X, X ) }.
% 1.09/1.47 (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd( X, X ) ) ==>
% 1.09/1.47 ld( mult( X, X ), X ) }.
% 1.09/1.47 (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X ), ld( X, X )
% 1.09/1.47 ) ==> ld( X, X ) }.
% 1.09/1.47 (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld( X, X ), ld( X
% 1.09/1.47 , X ) ) ==> ld( X, X ) }.
% 1.09/1.47 (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld( ld( X, X ),
% 1.09/1.47 X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 1.09/1.47 (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld( ld( X, X ), X
% 1.09/1.47 ), ld( X, X ) ) ==> X }.
% 1.09/1.47 (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld( ld( X, X ),
% 1.09/1.47 X ) ==> X }.
% 1.09/1.47 (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y, ld( X, X ) )
% 1.09/1.47 ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 1.09/1.47 (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld( X, X ) }.
% 1.09/1.47 (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld( X, Y ), ld( X
% 1.09/1.47 , X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 1.09/1.47 (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) ) ==> ld( mult(
% 1.09/1.47 X, X ), X ) }.
% 1.09/1.47 (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X, X ) ) ==>
% 1.09/1.47 mult( X, rd( ld( X, Y ), X ) ) }.
% 1.09/1.47 (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd( X, Y ), rd( X
% 1.09/1.47 , Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 1.09/1.47 (278) {G20,W14,D4,L2,V0,M2} P(255,5) { ! mult( skol1, ld( skol2, skol2 ) )
% 1.09/1.47 ==> skol1, ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.47 (322) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y, Y ) ) = ld(
% 1.09/1.47 mult( X, ld( Y, X ) ), X ) }.
% 1.09/1.47 (364) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd( X, Y ) ), X
% 1.09/1.47 ) ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.47 (367) {G21,W15,D5,L1,V2,M1} P(7,364) { mult( ld( Y, X ), ld( X, X ) ) ==>
% 1.09/1.47 ld( ld( ld( X, X ), Y ), X ) }.
% 1.09/1.47 (540) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld( X, X ) )
% 1.09/1.47 ==> mult( ld( mult( X, X ), X ), Y ) }.
% 1.09/1.47 (544) {G22,W15,D5,L1,V2,M1} P(322,540);d(0);d(367);d(242);d(212) { rd( ld(
% 1.09/1.47 ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 1.09/1.47 (554) {G23,W15,D5,L1,V2,M1} P(544,270);d(212);d(194);d(38);d(367);d(242);d(
% 1.09/1.47 0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y, ld( X, X ) )
% 1.09/1.47 }.
% 1.09/1.47 (558) {G23,W11,D5,L1,V2,M1} P(544,38);d(0);d(367);d(242) { ld( ld( X, X ),
% 1.09/1.47 rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.09/1.47 (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y ) ==> Y }.
% 1.09/1.47 (584) {G25,W7,D4,L1,V2,M1} P(558,129);d(565);d(565) { mult( Y, ld( X, X ) )
% 1.09/1.47 ==> Y }.
% 1.09/1.47 (585) {G25,W7,D3,L1,V2,M1} P(558,120);d(565);d(565) { ld( Y, Y ) = ld( X, X
% 1.09/1.47 ) }.
% 1.09/1.47 (591) {G25,W11,D5,L1,V3,M1} P(37,558);d(565);d(194);d(554);d(565) { ld( Y,
% 1.09/1.47 rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 1.09/1.47 (595) {G26,W7,D4,L1,V2,M1} P(558,43);d(591);d(584);d(6);d(565) { rd( Y, ld
% 1.09/1.47 ( X, X ) ) ==> Y }.
% 1.09/1.47 (599) {G27,W7,D4,L1,V2,M1} P(558,0);d(595) { mult( ld( X, X ), Y ) ==> Y
% 1.09/1.47 }.
% 1.09/1.47 (622) {G28,W0,D0,L0,V0,M0} P(585,278);d(584);d(599);q;q { }.
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 % SZS output end Refutation
% 1.09/1.47 found a proof!
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 Unprocessed initial clauses:
% 1.09/1.47
% 1.09/1.47 (624) {G0,W7,D4,L1,V2,M1} { mult( Y, ld( Y, X ) ) = X }.
% 1.09/1.47 (625) {G0,W7,D4,L1,V2,M1} { ld( Y, mult( Y, X ) ) = X }.
% 1.09/1.47 (626) {G0,W7,D4,L1,V2,M1} { mult( rd( Y, X ), X ) = Y }.
% 1.09/1.47 (627) {G0,W7,D4,L1,V2,M1} { rd( mult( Y, X ), X ) = Y }.
% 1.09/1.47 (628) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( Z, Y ), X ), Z ) = mult( Z
% 1.09/1.47 , mult( Y, mult( X, Z ) ) ) }.
% 1.09/1.47 (629) {G0,W14,D4,L2,V0,M2} { ! mult( skol1, rd( skol2, skol2 ) ) = skol1,
% 1.09/1.47 ! mult( rd( skol2, skol2 ), skol1 ) = skol1 }.
% 1.09/1.47
% 1.09/1.47
% 1.09/1.47 Total Proof:
% 1.09/1.47
% 1.09/1.47 subsumption: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent0: (624) {G0,W7,D4,L1,V2,M1} { mult( Y, ld( Y, X ) ) = X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.09/1.47 parent0: (625) {G0,W7,D4,L1,V2,M1} { ld( Y, mult( Y, X ) ) = X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent0: (626) {G0,W7,D4,L1,V2,M1} { mult( rd( Y, X ), X ) = Y }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent0: (627) {G0,W7,D4,L1,V2,M1} { rd( mult( Y, X ), X ) = Y }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (644) {G0,W15,D5,L1,V3,M1} { mult( X, mult( Y, mult( Z, X ) ) ) =
% 1.09/1.47 mult( mult( mult( X, Y ), Z ), X ) }.
% 1.09/1.47 parent0[0]: (628) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( Z, Y ), X ), Z
% 1.09/1.47 ) = mult( Z, mult( Y, mult( X, Z ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) )
% 1.09/1.47 ) ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 1.09/1.47 parent0: (644) {G0,W15,D5,L1,V3,M1} { mult( X, mult( Y, mult( Z, X ) ) ) =
% 1.09/1.47 mult( mult( mult( X, Y ), Z ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (5) {G0,W14,D4,L2,V0,M2} I { ! mult( skol1, rd( skol2, skol2 )
% 1.09/1.47 ) ==> skol1, ! mult( rd( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.47 parent0: (629) {G0,W14,D4,L2,V0,M2} { ! mult( skol1, rd( skol2, skol2 ) )
% 1.09/1.47 = skol1, ! mult( rd( skol2, skol2 ), skol1 ) = skol1 }.
% 1.09/1.47 substitution0:
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 1 ==> 1
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (654) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (655) {G1,W7,D4,L1,V2,M1} { X ==> ld( rd( Y, X ), Y ) }.
% 1.09/1.47 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 6]: (654) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := rd( Y, X )
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (656) {G1,W7,D4,L1,V2,M1} { ld( rd( Y, X ), Y ) ==> X }.
% 1.09/1.47 parent0[0]: (655) {G1,W7,D4,L1,V2,M1} { X ==> ld( rd( Y, X ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.09/1.47 parent0: (656) {G1,W7,D4,L1,V2,M1} { ld( rd( Y, X ), Y ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (658) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 1.09/1.47 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (659) {G1,W7,D4,L1,V2,M1} { X ==> rd( Y, ld( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 3]: (658) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := ld( X, Y )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (660) {G1,W7,D4,L1,V2,M1} { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.47 parent0[0]: (659) {G1,W7,D4,L1,V2,M1} { X ==> rd( Y, ld( X, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.47 parent0: (660) {G1,W7,D4,L1,V2,M1} { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (662) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z ), X )
% 1.09/1.47 ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 1.09/1.47 parent0[0]: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) )
% 1.09/1.47 ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (665) {G1,W19,D6,L1,V3,M1} { mult( mult( mult( ld( X, Y ), Z ), X
% 1.09/1.47 ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 18]: (662) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z )
% 1.09/1.47 , X ) ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, Y )
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y
% 1.09/1.47 ), Z ), X ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.09/1.47 parent0: (665) {G1,W19,D6,L1,V3,M1} { mult( mult( mult( ld( X, Y ), Z ), X
% 1.09/1.47 ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (670) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z ), X )
% 1.09/1.47 ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 1.09/1.47 parent0[0]: (4) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( X, Z ) ) )
% 1.09/1.47 ==> mult( mult( mult( Z, Y ), X ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (673) {G1,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), rd( Z, X )
% 1.09/1.47 ), X ) ==> mult( X, mult( Y, Z ) ) }.
% 1.09/1.47 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 14]: (670) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Z )
% 1.09/1.47 , X ) ==> mult( X, mult( Y, mult( Z, X ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Z
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := rd( Z, X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ),
% 1.09/1.47 rd( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 1.09/1.47 parent0: (673) {G1,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), rd( Z, X )
% 1.09/1.47 ), X ) ==> mult( X, mult( Y, Z ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (678) {G1,W15,D5,L1,V3,M1} { mult( X, mult( Y, Z ) ) ==> mult(
% 1.09/1.47 mult( mult( X, Y ), rd( Z, X ) ), X ) }.
% 1.09/1.47 parent0[0]: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd
% 1.09/1.47 ( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (680) {G1,W15,D5,L1,V3,M1} { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 1.09/1.47 mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 10]: (678) {G1,W15,D5,L1,V3,M1} { mult( X, mult( Y, Z ) ) ==>
% 1.09/1.47 mult( mult( mult( X, Y ), rd( Z, X ) ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := ld( X, Y )
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y )
% 1.09/1.47 , Z ) ) ==> mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.09/1.47 parent0: (680) {G1,W15,D5,L1,V3,M1} { mult( X, mult( ld( X, Y ), Z ) ) ==>
% 1.09/1.47 mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (684) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 1.09/1.47 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (687) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 1.09/1.47 rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.09/1.47 parent0[0]: (13) {G1,W15,D5,L1,V3,M1} P(2,4) { mult( mult( mult( Y, Z ), rd
% 1.09/1.47 ( X, Y ) ), Y ) ==> mult( Y, mult( Z, X ) ) }.
% 1.09/1.47 parent1[0; 9]: (684) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := mult( mult( X, Y ), rd( Z, X ) )
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (688) {G1,W15,D5,L1,V3,M1} { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 1.09/1.47 mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (687) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) )
% 1.09/1.47 ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z )
% 1.09/1.47 ), X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.09/1.47 parent0: (688) {G1,W15,D5,L1,V3,M1} { rd( mult( X, mult( Y, Z ) ), X ) ==>
% 1.09/1.47 mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (690) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (693) {G1,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X,
% 1.09/1.47 mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 1.09/1.47 parent0[0]: (15) {G2,W15,D5,L1,V3,M1} P(0,13) { mult( X, mult( ld( X, Y ),
% 1.09/1.47 Z ) ) ==> mult( mult( Y, rd( Z, X ) ), X ) }.
% 1.09/1.47 parent1[0; 8]: (690) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := mult( ld( X, Y ), Z )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (694) {G1,W15,D6,L1,V3,M1} { ld( X, mult( mult( Y, rd( Z, X ) ), X
% 1.09/1.47 ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.09/1.47 parent0[0]: (693) {G1,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X,
% 1.09/1.47 mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd(
% 1.09/1.47 Z, X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.09/1.47 parent0: (694) {G1,W15,D6,L1,V3,M1} { ld( X, mult( mult( Y, rd( Z, X ) ),
% 1.09/1.47 X ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (696) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 1.09/1.47 rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.09/1.47 parent0[0]: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) )
% 1.09/1.47 , X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (698) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( ld( Y, Z ),
% 1.09/1.47 X ) ) ==> rd( mult( X, Z ), X ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 13]: (696) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X
% 1.09/1.47 ) ) ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := ld( Y, Z )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 1.09/1.47 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 1.09/1.47 parent0: (698) {G1,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( ld( Y, Z ),
% 1.09/1.47 X ) ) ==> rd( mult( X, Z ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (702) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X ) ) ==>
% 1.09/1.47 rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.09/1.47 parent0[0]: (18) {G2,W15,D5,L1,V3,M1} P(13,3) { rd( mult( X, mult( Y, Z ) )
% 1.09/1.47 , X ) ==> mult( mult( X, Y ), rd( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (707) {G1,W15,D5,L1,V3,M1} { mult( mult( X, rd( Y, Z ) ), rd( Z,
% 1.09/1.47 X ) ) ==> rd( mult( X, Y ), X ) }.
% 1.09/1.47 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 13]: (702) {G2,W15,D5,L1,V3,M1} { mult( mult( X, Y ), rd( Z, X
% 1.09/1.47 ) ) ==> rd( mult( X, mult( Y, Z ) ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := rd( Y, Z )
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y )
% 1.09/1.47 ), rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 1.09/1.47 parent0: (707) {G1,W15,D5,L1,V3,M1} { mult( mult( X, rd( Y, Z ) ), rd( Z,
% 1.09/1.47 X ) ) ==> rd( mult( X, Y ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (712) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (715) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( mult( Z
% 1.09/1.47 , X ), rd( mult( Z, Y ), Z ) ) }.
% 1.09/1.47 parent0[0]: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 1.09/1.47 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 1.09/1.47 parent1[0; 10]: (712) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) )
% 1.09/1.47 }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := mult( Z, X )
% 1.09/1.47 Y := rd( ld( X, Y ), Z )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (716) {G1,W15,D5,L1,V3,M1} { ld( mult( Z, X ), rd( mult( Z, Y ), Z
% 1.09/1.47 ) ) ==> rd( ld( X, Y ), Z ) }.
% 1.09/1.47 parent0[0]: (715) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( mult
% 1.09/1.47 ( Z, X ), rd( mult( Z, Y ), Z ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 1.09/1.47 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 parent0: (716) {G1,W15,D5,L1,V3,M1} { ld( mult( Z, X ), rd( mult( Z, Y ),
% 1.09/1.47 Z ) ) ==> rd( ld( X, Y ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (718) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 1.09/1.47 Y ), rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 1.09/1.47 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (721) {G1,W15,D5,L1,V3,M1} { rd( ld( ld( X, Y ), Z ), X ) ==> ld
% 1.09/1.47 ( Y, rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 9]: (718) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 1.09/1.47 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := ld( X, Y )
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 1.09/1.47 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 parent0: (721) {G1,W15,D5,L1,V3,M1} { rd( ld( ld( X, Y ), Z ), X ) ==> ld
% 1.09/1.47 ( Y, rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (726) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 1.09/1.47 Y ), rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 1.09/1.47 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (730) {G1,W15,D5,L1,V3,M1} { rd( ld( X, ld( Y, Z ) ), Y ) ==> ld
% 1.09/1.47 ( mult( Y, X ), rd( Z, Y ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 13]: (726) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 1.09/1.47 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := ld( Y, Z )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.09/1.47 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.09/1.47 parent0: (730) {G1,W15,D5,L1,V3,M1} { rd( ld( X, ld( Y, Z ) ), Y ) ==> ld
% 1.09/1.47 ( mult( Y, X ), rd( Z, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (734) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld( mult( X,
% 1.09/1.47 Y ), rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 parent0[0]: (31) {G4,W15,D5,L1,V3,M1} P(27,1) { ld( mult( X, Y ), rd( mult
% 1.09/1.47 ( X, Z ), X ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (735) {G1,W11,D4,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( mult( Y
% 1.09/1.47 , X ), Y ) }.
% 1.09/1.47 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 10]: (734) {G4,W15,D5,L1,V3,M1} { rd( ld( Y, Z ), X ) ==> ld(
% 1.09/1.47 mult( X, Y ), rd( mult( X, Z ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.09/1.47 ( mult( X, Y ), X ) }.
% 1.09/1.47 parent0: (735) {G1,W11,D4,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( mult( Y
% 1.09/1.47 , X ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (738) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.09/1.47 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (741) {G2,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld
% 1.09/1.47 ( Y, X ) ) }.
% 1.09/1.47 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.09/1.47 ( mult( X, Y ), X ) }.
% 1.09/1.47 parent1[0; 3]: (738) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( Y, X )
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (742) {G2,W11,D5,L1,V2,M1} { ld( ld( mult( X, Y ), X ), ld( Y, X )
% 1.09/1.47 ) ==> X }.
% 1.09/1.47 parent0[0]: (741) {G2,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ),
% 1.09/1.47 ld( Y, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y )
% 1.09/1.47 , ld( X, Y ) ) ==> Y }.
% 1.09/1.47 parent0: (742) {G2,W11,D5,L1,V2,M1} { ld( ld( mult( X, Y ), X ), ld( Y, X
% 1.09/1.47 ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (744) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld(
% 1.09/1.47 Y, X ) ) }.
% 1.09/1.47 parent0[0]: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ),
% 1.09/1.47 ld( X, Y ) ) ==> Y }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (747) {G1,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, X ), ld( ld( X, Y )
% 1.09/1.47 , X ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 4]: (744) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X
% 1.09/1.47 ), ld( Y, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := ld( X, Y )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (748) {G1,W11,D5,L1,V2,M1} { ld( ld( Y, X ), ld( ld( X, Y ), X ) )
% 1.09/1.47 ==> X }.
% 1.09/1.47 parent0[0]: (747) {G1,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, X ), ld( ld( X,
% 1.09/1.47 Y ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X
% 1.09/1.47 , Y ), X ) ) ==> X }.
% 1.09/1.47 parent0: (748) {G1,W11,D5,L1,V2,M1} { ld( ld( Y, X ), ld( ld( X, Y ), X )
% 1.09/1.47 ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (750) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (751) {G1,W11,D4,L1,V2,M1} { ld( ld( X, Y ), X ) ==> mult( ld( Y
% 1.09/1.47 , X ), X ) }.
% 1.09/1.47 parent0[0]: (52) {G7,W11,D5,L1,V2,M1} P(0,43) { ld( ld( Y, X ), ld( ld( X,
% 1.09/1.47 Y ), X ) ) ==> X }.
% 1.09/1.47 parent1[0; 10]: (750) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 1.09/1.47 }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( Y, X )
% 1.09/1.47 Y := ld( ld( X, Y ), X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (752) {G1,W11,D4,L1,V2,M1} { mult( ld( Y, X ), X ) ==> ld( ld( X,
% 1.09/1.47 Y ), X ) }.
% 1.09/1.47 parent0[0]: (751) {G1,W11,D4,L1,V2,M1} { ld( ld( X, Y ), X ) ==> mult( ld
% 1.09/1.47 ( Y, X ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.09/1.47 ld( ld( Y, X ), Y ) }.
% 1.09/1.47 parent0: (752) {G1,W11,D4,L1,V2,M1} { mult( ld( Y, X ), X ) ==> ld( ld( X
% 1.09/1.47 , Y ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (754) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.09/1.47 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (759) {G2,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z, X
% 1.09/1.47 ) ), ld( Y, ld( X, Z ) ) ) }.
% 1.09/1.47 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.09/1.47 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.09/1.47 parent1[0; 3]: (754) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( Y, ld( X, Z ) )
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (760) {G2,W15,D5,L1,V3,M1} { ld( ld( mult( X, Y ), rd( Z, X ) ),
% 1.09/1.47 ld( Y, ld( X, Z ) ) ) ==> X }.
% 1.09/1.47 parent0[0]: (759) {G2,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z
% 1.09/1.47 , X ) ), ld( Y, ld( X, Z ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd
% 1.09/1.47 ( Z, Y ) ), ld( X, ld( Y, Z ) ) ) ==> Y }.
% 1.09/1.47 parent0: (760) {G2,W15,D5,L1,V3,M1} { ld( ld( mult( X, Y ), rd( Z, X ) ),
% 1.09/1.47 ld( Y, ld( X, Z ) ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (762) {G6,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd( Z, X
% 1.09/1.47 ) ), ld( Y, ld( X, Z ) ) ) }.
% 1.09/1.47 parent0[0]: (109) {G6,W15,D5,L1,V3,M1} P(38,6) { ld( ld( mult( Y, X ), rd(
% 1.09/1.47 Z, Y ) ), ld( X, ld( Y, Z ) ) ) ==> Y }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (765) {G1,W15,D5,L1,V3,M1} { X ==> ld( ld( Y, rd( Z, X ) ), ld(
% 1.09/1.47 ld( X, Y ), ld( X, Z ) ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 4]: (762) {G6,W15,D5,L1,V3,M1} { X ==> ld( ld( mult( X, Y ), rd
% 1.09/1.47 ( Z, X ) ), ld( Y, ld( X, Z ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := ld( X, Y )
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (766) {G1,W15,D5,L1,V3,M1} { ld( ld( Y, rd( Z, X ) ), ld( ld( X, Y
% 1.09/1.47 ), ld( X, Z ) ) ) ==> X }.
% 1.09/1.47 parent0[0]: (765) {G1,W15,D5,L1,V3,M1} { X ==> ld( ld( Y, rd( Z, X ) ), ld
% 1.09/1.47 ( ld( X, Y ), ld( X, Z ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) )
% 1.09/1.47 , ld( ld( X, Y ), ld( X, Z ) ) ) ==> X }.
% 1.09/1.47 parent0: (766) {G1,W15,D5,L1,V3,M1} { ld( ld( Y, rd( Z, X ) ), ld( ld( X,
% 1.09/1.47 Y ), ld( X, Z ) ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (768) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (769) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, Z ) ) ==>
% 1.09/1.47 mult( ld( Y, rd( Z, X ) ), X ) }.
% 1.09/1.47 parent0[0]: (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) ),
% 1.09/1.47 ld( ld( X, Y ), ld( X, Z ) ) ) ==> X }.
% 1.09/1.47 parent1[0; 14]: (768) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 1.09/1.47 }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( Y, rd( Z, X ) )
% 1.09/1.47 Y := ld( ld( X, Y ), ld( X, Z ) )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (770) {G1,W15,D5,L1,V3,M1} { mult( ld( Y, rd( Z, X ) ), X ) ==> ld
% 1.09/1.47 ( ld( X, Y ), ld( X, Z ) ) }.
% 1.09/1.47 parent0[0]: (769) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, Z ) ) ==>
% 1.09/1.47 mult( ld( Y, rd( Z, X ) ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z )
% 1.09/1.47 ), Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 1.09/1.47 parent0: (770) {G1,W15,D5,L1,V3,M1} { mult( ld( Y, rd( Z, X ) ), X ) ==>
% 1.09/1.47 ld( ld( X, Y ), ld( X, Z ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (772) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) ) ==> mult
% 1.09/1.47 ( ld( X, rd( Y, Z ) ), Z ) }.
% 1.09/1.47 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 1.09/1.47 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (775) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, mult( Z, X )
% 1.09/1.47 ) ) ==> mult( ld( Y, Z ), X ) }.
% 1.09/1.47 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 13]: (772) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) )
% 1.09/1.47 ==> mult( ld( X, rd( Y, Z ) ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Z
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := mult( Z, X )
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y,
% 1.09/1.47 mult( X, Y ) ) ) ==> mult( ld( Z, X ), Y ) }.
% 1.09/1.47 parent0: (775) {G1,W15,D5,L1,V3,M1} { ld( ld( X, Y ), ld( X, mult( Z, X )
% 1.09/1.47 ) ) ==> mult( ld( Y, Z ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (778) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 1.09/1.47 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (779) {G2,W15,D5,L1,V3,M1} { ld( X, Y ) ==> rd( ld( X, mult( Z, X
% 1.09/1.47 ) ), mult( ld( Y, Z ), X ) ) }.
% 1.09/1.47 parent0[0]: (140) {G9,W15,D5,L1,V3,M1} P(3,129) { ld( ld( Y, Z ), ld( Y,
% 1.09/1.47 mult( X, Y ) ) ) ==> mult( ld( Z, X ), Y ) }.
% 1.09/1.47 parent1[0; 10]: (778) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, mult( Z, X ) )
% 1.09/1.47 Y := ld( X, Y )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (780) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Z, X ) ), mult( ld(
% 1.09/1.47 Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.09/1.47 parent0[0]: (779) {G2,W15,D5,L1,V3,M1} { ld( X, Y ) ==> rd( ld( X, mult( Z
% 1.09/1.47 , X ) ), mult( ld( Y, Z ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 1.09/1.47 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.09/1.47 parent0: (780) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Z, X ) ), mult( ld
% 1.09/1.47 ( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (782) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X, mult( Y, X
% 1.09/1.47 ) ), mult( ld( Z, Y ), X ) ) }.
% 1.09/1.47 parent0[0]: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 1.09/1.47 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (786) {G2,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 1.09/1.47 mult( Y, X ) ), mult( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 13]: (782) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X,
% 1.09/1.47 mult( Y, X ) ), mult( ld( Z, Y ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := rd( Y, Z )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (788) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), mult( Z, X
% 1.09/1.47 ) ) ==> ld( X, rd( Y, Z ) ) }.
% 1.09/1.47 parent0[0]: (786) {G2,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X
% 1.09/1.47 , mult( Y, X ) ), mult( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 1.09/1.47 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.09/1.47 parent0: (788) {G2,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), mult( Z,
% 1.09/1.47 X ) ) ==> ld( X, rd( Y, Z ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (789) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 1.09/1.47 mult( Y, X ) ), mult( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 1.09/1.47 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (792) {G6,W15,D5,L1,V2,M1} { ld( X, rd( Y, Y ) ) ==> ld( mult(
% 1.09/1.47 mult( Y, X ), X ), mult( Y, X ) ) }.
% 1.09/1.47 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.09/1.47 ( mult( X, Y ), X ) }.
% 1.09/1.47 parent1[0; 6]: (789) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 1.09/1.47 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := mult( Y, X )
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (794) {G6,W15,D5,L1,V2,M1} { ld( mult( mult( Y, X ), X ), mult( Y
% 1.09/1.47 , X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.09/1.47 parent0[0]: (792) {G6,W15,D5,L1,V2,M1} { ld( X, rd( Y, Y ) ) ==> ld( mult
% 1.09/1.47 ( mult( Y, X ), X ), mult( Y, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X )
% 1.09/1.47 , X ), mult( Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.09/1.47 parent0: (794) {G6,W15,D5,L1,V2,M1} { ld( mult( mult( Y, X ), X ), mult( Y
% 1.09/1.47 , X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (796) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 1.09/1.47 mult( Y, X ) ), mult( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 1.09/1.47 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (799) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 1.09/1.47 ( ld( X, Y ), mult( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 11]: (796) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 1.09/1.47 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := rd( Y, X )
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (801) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), mult( Z, X ) ) ==> ld
% 1.09/1.47 ( X, rd( rd( Y, X ), Z ) ) }.
% 1.09/1.47 parent0[0]: (799) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==>
% 1.09/1.47 rd( ld( X, Y ), mult( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 1.09/1.47 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 1.09/1.47 parent0: (801) {G1,W15,D5,L1,V3,M1} { rd( ld( X, Y ), mult( Z, X ) ) ==>
% 1.09/1.47 ld( X, rd( rd( Y, X ), Z ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (804) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd( ld( X,
% 1.09/1.47 mult( Y, X ) ), mult( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (156) {G11,W15,D5,L1,V3,M1} P(6,144) { rd( ld( Z, mult( X, Z )
% 1.09/1.47 ), mult( Y, Z ) ) ==> ld( Z, rd( X, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (808) {G1,W15,D5,L1,V3,M1} { ld( X, rd( Y, rd( Z, X ) ) ) ==> rd
% 1.09/1.47 ( ld( X, mult( Y, X ) ), Z ) }.
% 1.09/1.47 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 14]: (804) {G11,W15,D5,L1,V3,M1} { ld( X, rd( Y, Z ) ) ==> rd(
% 1.09/1.47 ld( X, mult( Y, X ) ), mult( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Z
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := rd( Z, X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (810) {G1,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), Z ) ==> ld
% 1.09/1.47 ( X, rd( Y, rd( Z, X ) ) ) }.
% 1.09/1.47 parent0[0]: (808) {G1,W15,D5,L1,V3,M1} { ld( X, rd( Y, rd( Z, X ) ) ) ==>
% 1.09/1.47 rd( ld( X, mult( Y, X ) ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y )
% 1.09/1.47 ), X ) ==> ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 1.09/1.47 parent0: (810) {G1,W15,D5,L1,V3,M1} { rd( ld( X, mult( Y, X ) ), Z ) ==>
% 1.09/1.47 ld( X, rd( Y, rd( Z, X ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (812) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 1.09/1.47 ( ld( X, Y ), mult( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 1.09/1.47 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (815) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), rd( Z, X ) )
% 1.09/1.47 ) ==> rd( ld( X, Y ), Z ) }.
% 1.09/1.47 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 14]: (812) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) )
% 1.09/1.47 ==> rd( ld( X, Y ), mult( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Z
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := rd( Z, X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 1.09/1.47 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 parent0: (815) {G1,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), rd( Z, X ) )
% 1.09/1.47 ) ==> rd( ld( X, Y ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (818) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X, rd(
% 1.09/1.47 rd( Y, X ), rd( Z, X ) ) ) }.
% 1.09/1.47 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 1.09/1.47 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (822) {G2,W19,D6,L1,V3,M1} { rd( ld( ld( X, Y ), Y ), Z ) ==> ld
% 1.09/1.47 ( ld( X, Y ), rd( X, rd( Z, ld( X, Y ) ) ) ) }.
% 1.09/1.47 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.47 parent1[0; 13]: (818) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld(
% 1.09/1.47 X, rd( rd( Y, X ), rd( Z, X ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, Y )
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (825) {G2,W19,D6,L1,V3,M1} { ld( ld( X, Y ), rd( X, rd( Z, ld( X,
% 1.09/1.47 Y ) ) ) ) ==> rd( ld( ld( X, Y ), Y ), Z ) }.
% 1.09/1.47 parent0[0]: (822) {G2,W19,D6,L1,V3,M1} { rd( ld( ld( X, Y ), Y ), Z ) ==>
% 1.09/1.47 ld( ld( X, Y ), rd( X, rd( Z, ld( X, Y ) ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y,
% 1.09/1.47 rd( Z, ld( Y, X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 1.09/1.47 parent0: (825) {G2,W19,D6,L1,V3,M1} { ld( ld( X, Y ), rd( X, rd( Z, ld( X
% 1.09/1.47 , Y ) ) ) ) ==> rd( ld( ld( X, Y ), Y ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (828) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (829) {G1,W15,D5,L1,V3,M1} { rd( rd( X, Y ), rd( Z, Y ) ) ==>
% 1.09/1.47 mult( Y, rd( ld( Y, X ), Z ) ) }.
% 1.09/1.47 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 1.09/1.47 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.47 parent1[0; 10]: (828) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 1.09/1.47 }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Z
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := rd( rd( X, Y ), rd( Z, Y ) )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z,
% 1.09/1.47 X ) ) ==> mult( X, rd( ld( X, Y ), Z ) ) }.
% 1.09/1.47 parent0: (829) {G1,W15,D5,L1,V3,M1} { rd( rd( X, Y ), rd( Z, Y ) ) ==>
% 1.09/1.47 mult( Y, rd( ld( Y, X ), Z ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (832) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Y ), X ) ==> mult( mult
% 1.09/1.47 ( X, rd( Y, Z ) ), rd( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) )
% 1.09/1.47 , rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (834) {G2,W19,D5,L1,V3,M1} { rd( mult( ld( X, Y ), Z ), ld( X, Y
% 1.09/1.47 ) ) ==> mult( mult( ld( X, Y ), rd( Z, Y ) ), X ) }.
% 1.09/1.47 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.47 parent1[0; 18]: (832) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Y ), X ) ==>
% 1.09/1.47 mult( mult( X, rd( Y, Z ) ), rd( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, Y )
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 1.09/1.47 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.09/1.47 parent0: (834) {G2,W19,D5,L1,V3,M1} { rd( mult( ld( X, Y ), Z ), ld( X, Y
% 1.09/1.47 ) ) ==> mult( mult( ld( X, Y ), rd( Z, Y ) ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (838) {G12,W15,D5,L1,V2,M1} { ld( Y, rd( X, X ) ) ==> ld( mult(
% 1.09/1.47 mult( X, Y ), Y ), mult( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (162) {G12,W15,D5,L1,V2,M1} P(156,40) { ld( mult( mult( Y, X )
% 1.09/1.47 , X ), mult( Y, X ) ) ==> ld( X, rd( Y, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (841) {G4,W19,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> ld
% 1.09/1.47 ( rd( mult( X, X ), X ), mult( X, rd( X, X ) ) ) }.
% 1.09/1.47 parent0[0]: (28) {G3,W15,D5,L1,V3,M1} P(2,18) { mult( mult( Z, rd( X, Y ) )
% 1.09/1.47 , rd( Y, Z ) ) ==> rd( mult( Z, X ), Z ) }.
% 1.09/1.47 parent1[0; 9]: (838) {G12,W15,D5,L1,V2,M1} { ld( Y, rd( X, X ) ) ==> ld(
% 1.09/1.47 mult( mult( X, Y ), Y ), mult( X, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := rd( X, X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (845) {G1,W15,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> ld
% 1.09/1.47 ( X, mult( X, rd( X, X ) ) ) }.
% 1.09/1.47 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 9]: (841) {G4,W19,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 1.09/1.47 ==> ld( rd( mult( X, X ), X ), mult( X, rd( X, X ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (846) {G1,W11,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> rd
% 1.09/1.47 ( X, X ) }.
% 1.09/1.47 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 8]: (845) {G1,W15,D5,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 1.09/1.47 ==> ld( X, mult( X, rd( X, X ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := rd( X, X )
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 1.09/1.47 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.09/1.47 parent0: (846) {G1,W11,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==> rd
% 1.09/1.47 ( X, X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (849) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult( ld( X,
% 1.09/1.47 Y ), Y ) }.
% 1.09/1.47 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.09/1.47 ld( ld( Y, X ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (852) {G9,W19,D5,L1,V1,M1} { ld( ld( rd( X, X ), rd( X, X ) ), rd
% 1.09/1.47 ( X, X ) ) ==> mult( rd( X, X ), rd( X, X ) ) }.
% 1.09/1.47 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 1.09/1.47 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.09/1.47 parent1[0; 13]: (849) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult
% 1.09/1.47 ( ld( X, Y ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := rd( X, X )
% 1.09/1.47 Y := rd( X, X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (856) {G10,W15,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) ) ==>
% 1.09/1.47 mult( rd( X, X ), rd( X, X ) ) }.
% 1.09/1.47 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 1.09/1.47 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.09/1.47 parent1[0; 2]: (852) {G9,W19,D5,L1,V1,M1} { ld( ld( rd( X, X ), rd( X, X )
% 1.09/1.47 ), rd( X, X ) ) ==> mult( rd( X, X ), rd( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (857) {G11,W11,D4,L1,V1,M1} { rd( X, X ) ==> mult( rd( X, X ), rd
% 1.09/1.47 ( X, X ) ) }.
% 1.09/1.47 parent0[0]: (195) {G13,W11,D4,L1,V1,M1} P(28,162);d(3);d(1) { ld( rd( X, X
% 1.09/1.47 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.09/1.47 parent1[0; 1]: (856) {G10,W15,D4,L1,V1,M1} { ld( rd( X, X ), rd( X, X ) )
% 1.09/1.47 ==> mult( rd( X, X ), rd( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (858) {G11,W11,D4,L1,V1,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 1.09/1.47 rd( X, X ) }.
% 1.09/1.47 parent0[0]: (857) {G11,W11,D4,L1,V1,M1} { rd( X, X ) ==> mult( rd( X, X )
% 1.09/1.47 , rd( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X
% 1.09/1.47 ), rd( X, X ) ) ==> rd( X, X ) }.
% 1.09/1.47 parent0: (858) {G11,W11,D4,L1,V1,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 1.09/1.47 rd( X, X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (861) {G3,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld( X, mult
% 1.09/1.47 ( mult( Y, rd( Z, X ) ), X ) ) }.
% 1.09/1.47 parent0[0]: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z
% 1.09/1.47 , X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (864) {G4,W15,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X ) ==>
% 1.09/1.47 ld( X, mult( rd( X, X ), X ) ) }.
% 1.09/1.47 parent0[0]: (209) {G14,W11,D4,L1,V1,M1} P(195,58);d(195) { mult( rd( X, X )
% 1.09/1.47 , rd( X, X ) ) ==> rd( X, X ) }.
% 1.09/1.47 parent1[0; 11]: (861) {G3,W15,D6,L1,V3,M1} { mult( ld( X, Y ), Z ) ==> ld
% 1.09/1.47 ( X, mult( mult( Y, rd( Z, X ) ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := rd( X, X )
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (865) {G1,W11,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X ) ==>
% 1.09/1.47 ld( X, X ) }.
% 1.09/1.47 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 1.09/1.47 parent1[0; 10]: (864) {G4,W15,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X
% 1.09/1.47 ) ==> ld( X, mult( rd( X, X ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (866) {G2,W11,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> ld
% 1.09/1.47 ( X, X ) }.
% 1.09/1.47 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 1.09/1.47 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 1.09/1.47 parent1[0; 1]: (865) {G1,W11,D5,L1,V1,M1} { mult( ld( X, rd( X, X ) ), X )
% 1.09/1.47 ==> ld( X, X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X
% 1.09/1.47 , X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent0: (866) {G2,W11,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> ld
% 1.09/1.47 ( X, X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (869) {G5,W15,D5,L1,V3,M1} { ld( mult( Y, X ), rd( Z, Y ) ) ==> rd
% 1.09/1.47 ( ld( X, ld( Y, Z ) ), Y ) }.
% 1.09/1.47 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.09/1.47 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (872) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd( X, X
% 1.09/1.47 ) ) ==> rd( ld( X, X ), X ) }.
% 1.09/1.47 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.09/1.47 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 11]: (869) {G5,W15,D5,L1,V3,M1} { ld( mult( Y, X ), rd( Z, Y )
% 1.09/1.47 ) ==> rd( ld( X, ld( Y, Z ) ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, X )
% 1.09/1.47 Y := X
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (875) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd( X, X
% 1.09/1.47 ) ) ==> ld( mult( X, X ), X ) }.
% 1.09/1.47 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.09/1.47 ( mult( X, Y ), X ) }.
% 1.09/1.47 parent1[0; 10]: (872) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd
% 1.09/1.47 ( X, X ) ) ==> rd( ld( X, X ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (876) {G1,W11,D4,L1,V1,M1} { ld( X, rd( X, X ) ) ==> ld( mult( X
% 1.09/1.47 , X ), X ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 2]: (875) {G6,W15,D5,L1,V1,M1} { ld( mult( X, ld( X, X ) ), rd
% 1.09/1.47 ( X, X ) ) ==> ld( mult( X, X ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd(
% 1.09/1.47 X, X ) ) ==> ld( mult( X, X ), X ) }.
% 1.09/1.47 parent0: (876) {G1,W11,D4,L1,V1,M1} { ld( X, rd( X, X ) ) ==> ld( mult( X
% 1.09/1.47 , X ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (879) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult( ld( X,
% 1.09/1.47 Y ), Y ) }.
% 1.09/1.47 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.09/1.47 ld( ld( Y, X ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (882) {G9,W19,D5,L1,V1,M1} { ld( ld( ld( X, X ), ld( X, X ) ), ld
% 1.09/1.47 ( X, X ) ) ==> mult( ld( X, X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.09/1.47 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 13]: (879) {G8,W11,D4,L1,V2,M1} { ld( ld( Y, X ), Y ) ==> mult
% 1.09/1.47 ( ld( X, Y ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, X )
% 1.09/1.47 Y := ld( X, X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (886) {G10,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==>
% 1.09/1.47 mult( ld( X, X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.09/1.47 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 2]: (882) {G9,W19,D5,L1,V1,M1} { ld( ld( ld( X, X ), ld( X, X )
% 1.09/1.47 ), ld( X, X ) ) ==> mult( ld( X, X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (887) {G11,W11,D4,L1,V1,M1} { ld( X, X ) ==> mult( ld( X, X ), ld
% 1.09/1.47 ( X, X ) ) }.
% 1.09/1.47 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.09/1.47 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 1]: (886) {G10,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) )
% 1.09/1.47 ==> mult( ld( X, X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (888) {G11,W11,D4,L1,V1,M1} { mult( ld( X, X ), ld( X, X ) ) ==>
% 1.09/1.47 ld( X, X ) }.
% 1.09/1.47 parent0[0]: (887) {G11,W11,D4,L1,V1,M1} { ld( X, X ) ==> mult( ld( X, X )
% 1.09/1.47 , ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X
% 1.09/1.47 ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent0: (888) {G11,W11,D4,L1,V1,M1} { mult( ld( X, X ), ld( X, X ) ) ==>
% 1.09/1.47 ld( X, X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (891) {G5,W11,D4,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> rd( ld( X,
% 1.09/1.47 Y ), Y ) }.
% 1.09/1.47 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.09/1.47 ( mult( X, Y ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (894) {G6,W19,D5,L1,V1,M1} { ld( mult( ld( X, X ), ld( X, X ) ),
% 1.09/1.47 ld( X, X ) ) ==> rd( ld( X, X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.09/1.47 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 13]: (891) {G5,W11,D4,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> rd
% 1.09/1.47 ( ld( X, Y ), Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, X )
% 1.09/1.47 Y := ld( X, X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (895) {G7,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) ) ==> rd
% 1.09/1.47 ( ld( X, X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 1.09/1.47 , ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 2]: (894) {G6,W19,D5,L1,V1,M1} { ld( mult( ld( X, X ), ld( X, X
% 1.09/1.47 ) ), ld( X, X ) ) ==> rd( ld( X, X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (896) {G8,W11,D4,L1,V1,M1} { ld( X, X ) ==> rd( ld( X, X ), ld( X
% 1.09/1.47 , X ) ) }.
% 1.09/1.47 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.09/1.47 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 1]: (895) {G7,W15,D4,L1,V1,M1} { ld( ld( X, X ), ld( X, X ) )
% 1.09/1.47 ==> rd( ld( X, X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (897) {G8,W11,D4,L1,V1,M1} { rd( ld( X, X ), ld( X, X ) ) ==> ld(
% 1.09/1.47 X, X ) }.
% 1.09/1.47 parent0[0]: (896) {G8,W11,D4,L1,V1,M1} { ld( X, X ) ==> rd( ld( X, X ), ld
% 1.09/1.47 ( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld(
% 1.09/1.47 X, X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent0: (897) {G8,W11,D4,L1,V1,M1} { rd( ld( X, X ), ld( X, X ) ) ==> ld
% 1.09/1.47 ( X, X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (899) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X, mult( Y, X
% 1.09/1.47 ) ), mult( ld( Z, Y ), X ) ) }.
% 1.09/1.47 parent0[0]: (144) {G10,W15,D5,L1,V3,M1} P(140,7) { rd( ld( X, mult( Z, X )
% 1.09/1.47 ), mult( ld( Y, Z ), X ) ) ==> ld( X, Y ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (903) {G11,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld( ld
% 1.09/1.47 ( X, X ), mult( X, ld( X, X ) ) ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 1.09/1.47 , ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 16]: (899) {G10,W15,D5,L1,V3,M1} { ld( X, Z ) ==> rd( ld( X,
% 1.09/1.47 mult( Y, X ) ), mult( ld( Z, Y ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, X )
% 1.09/1.47 Y := X
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (904) {G12,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> ld( ld( X,
% 1.09/1.47 X ), rd( X, rd( ld( X, X ), ld( X, X ) ) ) ) }.
% 1.09/1.47 parent0[0]: (167) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, mult( Z, Y )
% 1.09/1.47 ), X ) ==> ld( Y, rd( Z, rd( X, Y ) ) ) }.
% 1.09/1.47 parent1[0; 6]: (903) {G11,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd(
% 1.09/1.47 ld( ld( X, X ), mult( X, ld( X, X ) ) ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := ld( X, X )
% 1.09/1.47 Y := ld( X, X )
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (905) {G13,W15,D5,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld( ld
% 1.09/1.47 ( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (178) {G14,W19,D6,L1,V3,M1} P(7,172) { ld( ld( Y, X ), rd( Y,
% 1.09/1.47 rd( Z, ld( Y, X ) ) ) ) ==> rd( ld( ld( Y, X ), X ), Z ) }.
% 1.09/1.47 parent1[0; 6]: (904) {G12,W19,D6,L1,V1,M1} { ld( ld( X, X ), X ) ==> ld(
% 1.09/1.47 ld( X, X ), rd( X, rd( ld( X, X ), ld( X, X ) ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 Z := ld( X, X )
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (906) {G13,W15,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 1.09/1.47 ) ==> ld( ld( X, X ), X ) }.
% 1.09/1.47 parent0[0]: (905) {G13,W15,D5,L1,V1,M1} { ld( ld( X, X ), X ) ==> rd( ld(
% 1.09/1.47 ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld
% 1.09/1.47 ( ld( X, X ), X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 1.09/1.47 parent0: (906) {G13,W15,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 1.09/1.47 ) ==> ld( ld( X, X ), X ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (908) {G1,W19,D6,L1,V3,M1} { mult( ld( X, Y ), mult( Z, Y ) ) ==>
% 1.09/1.47 mult( mult( mult( ld( X, Y ), Z ), X ), ld( X, Y ) ) }.
% 1.09/1.47 parent0[0]: (10) {G1,W19,D6,L1,V3,M1} P(0,4) { mult( mult( mult( ld( X, Y )
% 1.09/1.47 , Z ), X ), ld( X, Y ) ) ==> mult( ld( X, Y ), mult( Z, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (912) {G2,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X, X ),
% 1.09/1.47 X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (217) {G16,W11,D4,L1,V1,M1} P(212,58);d(212) { mult( ld( X, X )
% 1.09/1.47 , ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 12]: (908) {G1,W19,D6,L1,V3,M1} { mult( ld( X, Y ), mult( Z, Y
% 1.09/1.47 ) ) ==> mult( mult( mult( ld( X, Y ), Z ), X ), ld( X, Y ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 Z := ld( X, X )
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (914) {G3,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X, X ),
% 1.09/1.47 X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.09/1.47 ld( ld( Y, X ), Y ) }.
% 1.09/1.47 parent1[0; 11]: (912) {G2,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X
% 1.09/1.47 , X ), X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (915) {G4,W19,D5,L1,V1,M1} { mult( ld( X, X ), ld( ld( X, X ), X
% 1.09/1.47 ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.09/1.47 ld( ld( Y, X ), Y ) }.
% 1.09/1.47 parent1[0; 5]: (914) {G3,W19,D5,L1,V1,M1} { mult( ld( X, X ), mult( ld( X
% 1.09/1.47 , X ), X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (916) {G1,W11,D5,L1,V1,M1} { X ==> mult( ld( ld( X, X ), X ), ld
% 1.09/1.47 ( X, X ) ) }.
% 1.09/1.47 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 1]: (915) {G4,W19,D5,L1,V1,M1} { mult( ld( X, X ), ld( ld( X, X
% 1.09/1.47 ), X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := ld( X, X )
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (917) {G1,W11,D5,L1,V1,M1} { mult( ld( ld( X, X ), X ), ld( X, X )
% 1.09/1.47 ) ==> X }.
% 1.09/1.47 parent0[0]: (916) {G1,W11,D5,L1,V1,M1} { X ==> mult( ld( ld( X, X ), X ),
% 1.09/1.47 ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld(
% 1.09/1.47 ld( X, X ), X ), ld( X, X ) ) ==> X }.
% 1.09/1.47 parent0: (917) {G1,W11,D5,L1,V1,M1} { mult( ld( ld( X, X ), X ), ld( X, X
% 1.09/1.47 ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (919) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Z ), X ) ==> mult( mult
% 1.09/1.47 ( X, Y ), rd( ld( Y, Z ), X ) ) }.
% 1.09/1.47 parent0[0]: (27) {G3,W15,D5,L1,V3,M1} P(0,18) { mult( mult( Z, X ), rd( ld
% 1.09/1.47 ( X, Y ), Z ) ) ==> rd( mult( Z, Y ), Z ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := Z
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (923) {G4,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld( X, X
% 1.09/1.47 ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (218) {G17,W11,D4,L1,V1,M1} P(212,40);d(217);d(212) { rd( ld( X
% 1.09/1.47 , X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.47 parent1[0; 16]: (919) {G3,W15,D5,L1,V3,M1} { rd( mult( X, Z ), X ) ==>
% 1.09/1.47 mult( mult( X, Y ), rd( ld( Y, Z ), X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, X )
% 1.09/1.47 Y := X
% 1.09/1.47 Z := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (925) {G5,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld( X, X
% 1.09/1.47 ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.09/1.47 ld( ld( Y, X ), Y ) }.
% 1.09/1.47 parent1[0; 11]: (923) {G4,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld
% 1.09/1.47 ( X, X ) ) ==> mult( mult( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (926) {G6,W19,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 1.09/1.47 ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 parent0[0]: (58) {G8,W11,D4,L1,V2,M1} P(52,0) { mult( ld( X, Y ), Y ) ==>
% 1.09/1.47 ld( ld( Y, X ), Y ) }.
% 1.09/1.47 parent1[0; 2]: (925) {G5,W19,D5,L1,V1,M1} { rd( mult( ld( X, X ), X ), ld
% 1.09/1.47 ( X, X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (928) {G7,W11,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X, X )
% 1.09/1.47 ) ==> X }.
% 1.09/1.47 parent0[0]: (240) {G17,W11,D5,L1,V1,M1} P(217,10);d(58);d(0) { mult( ld( ld
% 1.09/1.47 ( X, X ), X ), ld( X, X ) ) ==> X }.
% 1.09/1.47 parent1[0; 10]: (926) {G6,W19,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld(
% 1.09/1.47 X, X ) ) ==> mult( ld( ld( X, X ), X ), ld( X, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (929) {G8,W7,D4,L1,V1,M1} { ld( ld( X, X ), X ) ==> X }.
% 1.09/1.47 parent0[0]: (239) {G17,W15,D5,L1,V1,M1} P(217,144);d(167);d(178) { rd( ld(
% 1.09/1.47 ld( X, X ), X ), ld( X, X ) ) ==> ld( ld( X, X ), X ) }.
% 1.09/1.47 parent1[0; 1]: (928) {G7,W11,D5,L1,V1,M1} { rd( ld( ld( X, X ), X ), ld( X
% 1.09/1.47 , X ) ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 subsumption: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld
% 1.09/1.47 ( ld( X, X ), X ) ==> X }.
% 1.09/1.47 parent0: (929) {G8,W7,D4,L1,V1,M1} { ld( ld( X, X ), X ) ==> X }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 permutation0:
% 1.09/1.47 0 ==> 0
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (932) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) ) ==> rd
% 1.09/1.47 ( ld( X, Y ), mult( Z, X ) ) }.
% 1.09/1.47 parent0[0]: (166) {G12,W15,D5,L1,V3,M1} P(2,156) { rd( ld( Y, X ), mult( Z
% 1.09/1.47 , Y ) ) ==> ld( Y, rd( rd( X, Y ), Z ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := Y
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Z
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (934) {G13,W19,D6,L1,V2,M1} { ld( ld( X, X ), rd( rd( X, ld( X, X
% 1.09/1.47 ) ), Y ) ) ==> rd( X, mult( Y, ld( X, X ) ) ) }.
% 1.09/1.47 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.09/1.47 ld( X, X ), X ) ==> X }.
% 1.09/1.47 parent1[0; 13]: (932) {G12,W15,D5,L1,V3,M1} { ld( X, rd( rd( Y, X ), Z ) )
% 1.09/1.47 ==> rd( ld( X, Y ), mult( Z, X ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := ld( X, X )
% 1.09/1.47 Y := X
% 1.09/1.47 Z := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 paramod: (935) {G2,W15,D5,L1,V2,M1} { ld( ld( X, X ), rd( X, Y ) ) ==> rd
% 1.09/1.47 ( X, mult( Y, ld( X, X ) ) ) }.
% 1.09/1.47 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.47 parent1[0; 6]: (934) {G13,W19,D6,L1,V2,M1} { ld( ld( X, X ), rd( rd( X, ld
% 1.09/1.47 ( X, X ) ), Y ) ) ==> rd( X, mult( Y, ld( X, X ) ) ) }.
% 1.09/1.47 substitution0:
% 1.09/1.47 X := X
% 1.09/1.47 Y := X
% 1.09/1.47 end
% 1.09/1.47 substitution1:
% 1.09/1.47 X := X
% 1.09/1.47 Y := Y
% 1.09/1.47 end
% 1.09/1.47
% 1.09/1.47 eqswap: (936) {G2,W15,D5,L1,V2,M1} { rd( X, mult( Y, ld( X, X ) ) ) ==> ld
% 1.09/1.47 ( ld( X, X ), rd( X, Y ) ) }.
% 1.09/1.48 parent0[0]: (935) {G2,W15,D5,L1,V2,M1} { ld( ld( X, X ), rd( X, Y ) ) ==>
% 1.09/1.48 rd( X, mult( Y, ld( X, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y,
% 1.09/1.48 ld( X, X ) ) ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 1.09/1.48 parent0: (936) {G2,W15,D5,L1,V2,M1} { rd( X, mult( Y, ld( X, X ) ) ) ==>
% 1.09/1.48 ld( ld( X, X ), rd( X, Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (938) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) ) ==> rd
% 1.09/1.48 ( ld( ld( X, Y ), Z ), X ) }.
% 1.09/1.48 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 1.09/1.48 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (941) {G6,W11,D5,L1,V1,M1} { ld( X, rd( mult( X, X ), X ) ) ==>
% 1.09/1.48 rd( X, X ) }.
% 1.09/1.48 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.09/1.48 ld( X, X ), X ) ==> X }.
% 1.09/1.48 parent1[0; 9]: (938) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) )
% 1.09/1.48 ==> rd( ld( ld( X, Y ), Z ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 Z := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (943) {G1,W7,D3,L1,V1,M1} { ld( X, X ) ==> rd( X, X ) }.
% 1.09/1.48 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 1.09/1.48 parent1[0; 3]: (941) {G6,W11,D5,L1,V1,M1} { ld( X, rd( mult( X, X ), X ) )
% 1.09/1.48 ==> rd( X, X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (944) {G1,W7,D3,L1,V1,M1} { rd( X, X ) ==> ld( X, X ) }.
% 1.09/1.48 parent0[0]: (943) {G1,W7,D3,L1,V1,M1} { ld( X, X ) ==> rd( X, X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld
% 1.09/1.48 ( X, X ) }.
% 1.09/1.48 parent0: (944) {G1,W7,D3,L1,V1,M1} { rd( X, X ) ==> ld( X, X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (946) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X ) ) ==> rd
% 1.09/1.48 ( ld( ld( X, Y ), Z ), X ) }.
% 1.09/1.48 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 1.09/1.48 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (951) {G6,W19,D6,L1,V2,M1} { ld( X, rd( mult( ld( X, X ), Y ), ld
% 1.09/1.48 ( X, X ) ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.09/1.48 ld( X, X ), X ) ==> X }.
% 1.09/1.48 parent1[0; 14]: (946) {G5,W15,D5,L1,V3,M1} { ld( Y, rd( mult( X, Z ), X )
% 1.09/1.48 ) ==> rd( ld( ld( X, Y ), Z ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := X
% 1.09/1.48 Z := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (952) {G5,W19,D6,L1,V2,M1} { ld( X, mult( mult( ld( X, X ), rd( Y
% 1.09/1.48 , X ) ), X ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 1.09/1.48 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.09/1.48 parent1[0; 3]: (951) {G6,W19,D6,L1,V2,M1} { ld( X, rd( mult( ld( X, X ), Y
% 1.09/1.48 ), ld( X, X ) ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 Z := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (953) {G4,W15,D5,L1,V2,M1} { mult( ld( X, ld( X, X ) ), Y ) ==>
% 1.09/1.48 rd( ld( X, Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (21) {G3,W15,D6,L1,V3,M1} P(15,1) { ld( X, mult( mult( Y, rd( Z
% 1.09/1.48 , X ) ), X ) ) ==> mult( ld( X, Y ), Z ) }.
% 1.09/1.48 parent1[0; 1]: (952) {G5,W19,D6,L1,V2,M1} { ld( X, mult( mult( ld( X, X )
% 1.09/1.48 , rd( Y, X ) ), X ) ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := ld( X, X )
% 1.09/1.48 Z := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (954) {G4,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==> mult
% 1.09/1.48 ( ld( X, ld( X, X ) ), Y ) }.
% 1.09/1.48 parent0[0]: (953) {G4,W15,D5,L1,V2,M1} { mult( ld( X, ld( X, X ) ), Y )
% 1.09/1.48 ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld( X
% 1.09/1.48 , Y ), ld( X, X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 1.09/1.48 parent0: (954) {G4,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 1.09/1.48 mult( ld( X, ld( X, X ) ), Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (956) {G16,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X, rd
% 1.09/1.48 ( X, X ) ) }.
% 1.09/1.48 parent0[0]: (216) {G16,W11,D4,L1,V1,M1} P(212,38);d(40);d(0) { ld( X, rd( X
% 1.09/1.48 , X ) ) ==> ld( mult( X, X ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (957) {G17,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X, ld
% 1.09/1.48 ( X, X ) ) }.
% 1.09/1.48 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 1.09/1.48 X, X ) }.
% 1.09/1.48 parent1[0; 8]: (956) {G16,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld
% 1.09/1.48 ( X, rd( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (958) {G17,W11,D4,L1,V1,M1} { ld( X, ld( X, X ) ) ==> ld( mult( X
% 1.09/1.48 , X ), X ) }.
% 1.09/1.48 parent0[0]: (957) {G17,W11,D4,L1,V1,M1} { ld( mult( X, X ), X ) ==> ld( X
% 1.09/1.48 , ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) )
% 1.09/1.48 ==> ld( mult( X, X ), X ) }.
% 1.09/1.48 parent0: (958) {G17,W11,D4,L1,V1,M1} { ld( X, ld( X, X ) ) ==> ld( mult( X
% 1.09/1.48 , X ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (960) {G14,W15,D5,L1,V3,M1} { mult( Y, rd( ld( Y, X ), Z ) ) ==>
% 1.09/1.48 rd( rd( X, Y ), rd( Z, Y ) ) }.
% 1.09/1.48 parent0[0]: (179) {G14,W15,D5,L1,V3,M1} P(172,0) { rd( rd( Y, X ), rd( Z, X
% 1.09/1.48 ) ) ==> mult( X, rd( ld( X, Y ), Z ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (966) {G15,W15,D5,L1,V2,M1} { mult( X, rd( ld( X, Y ), X ) ) ==>
% 1.09/1.48 rd( rd( Y, X ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 1.09/1.48 X, X ) }.
% 1.09/1.48 parent1[0; 12]: (960) {G14,W15,D5,L1,V3,M1} { mult( Y, rd( ld( Y, X ), Z )
% 1.09/1.48 ) ==> rd( rd( X, Y ), rd( Z, Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 Z := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (970) {G15,W15,D5,L1,V2,M1} { rd( rd( Y, X ), ld( X, X ) ) ==>
% 1.09/1.48 mult( X, rd( ld( X, Y ), X ) ) }.
% 1.09/1.48 parent0[0]: (966) {G15,W15,D5,L1,V2,M1} { mult( X, rd( ld( X, Y ), X ) )
% 1.09/1.48 ==> rd( rd( Y, X ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X
% 1.09/1.48 , X ) ) ==> mult( X, rd( ld( X, Y ), X ) ) }.
% 1.09/1.48 parent0: (970) {G15,W15,D5,L1,V2,M1} { rd( rd( Y, X ), ld( X, X ) ) ==>
% 1.09/1.48 mult( X, rd( ld( X, Y ), X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (972) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X, rd(
% 1.09/1.48 rd( Y, X ), rd( Z, X ) ) ) }.
% 1.09/1.48 parent0[0]: (172) {G13,W15,D5,L1,V3,M1} P(2,166) { ld( Y, rd( rd( Z, Y ),
% 1.09/1.48 rd( X, Y ) ) ) ==> rd( ld( Y, Z ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Z
% 1.09/1.48 Y := X
% 1.09/1.48 Z := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (975) {G14,W15,D5,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( X, ld(
% 1.09/1.48 rd( Y, X ), rd( Y, X ) ) ) }.
% 1.09/1.48 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 1.09/1.48 X, X ) }.
% 1.09/1.48 parent1[0; 8]: (972) {G13,W15,D5,L1,V3,M1} { rd( ld( X, Y ), Z ) ==> ld( X
% 1.09/1.48 , rd( rd( Y, X ), rd( Z, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := rd( Y, X )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (978) {G6,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X, ld
% 1.09/1.48 ( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.09/1.48 parent0[0]: (40) {G5,W11,D4,L1,V2,M1} P(3,31) { rd( ld( Y, X ), X ) ==> ld
% 1.09/1.48 ( mult( X, Y ), X ) }.
% 1.09/1.48 parent1[0; 1]: (975) {G14,W15,D5,L1,V2,M1} { rd( ld( X, Y ), Y ) ==> ld( X
% 1.09/1.48 , ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (979) {G6,W15,D5,L1,V2,M1} { ld( Y, ld( rd( X, Y ), rd( X, Y ) ) )
% 1.09/1.48 ==> ld( mult( X, Y ), X ) }.
% 1.09/1.48 parent0[0]: (978) {G6,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X,
% 1.09/1.48 ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd(
% 1.09/1.48 X, Y ), rd( X, Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 1.09/1.48 parent0: (979) {G6,W15,D5,L1,V2,M1} { ld( Y, ld( rd( X, Y ), rd( X, Y ) )
% 1.09/1.48 ) ==> ld( mult( X, Y ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 *** allocated 22500 integers for termspace/termends
% 1.09/1.48 eqswap: (981) {G0,W14,D4,L2,V0,M2} { ! skol1 ==> mult( skol1, rd( skol2,
% 1.09/1.48 skol2 ) ), ! mult( rd( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 parent0[0]: (5) {G0,W14,D4,L2,V0,M2} I { ! mult( skol1, rd( skol2, skol2 )
% 1.09/1.48 ) ==> skol1, ! mult( rd( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (985) {G1,W14,D4,L2,V0,M2} { ! mult( ld( skol2, skol2 ), skol1 )
% 1.09/1.48 ==> skol1, ! skol1 ==> mult( skol1, rd( skol2, skol2 ) ) }.
% 1.09/1.48 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 1.09/1.48 X, X ) }.
% 1.09/1.48 parent1[1; 3]: (981) {G0,W14,D4,L2,V0,M2} { ! skol1 ==> mult( skol1, rd(
% 1.09/1.48 skol2, skol2 ) ), ! mult( rd( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := skol2
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (986) {G2,W14,D4,L2,V0,M2} { ! skol1 ==> mult( skol1, ld( skol2,
% 1.09/1.48 skol2 ) ), ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 parent0[0]: (255) {G19,W7,D3,L1,V1,M1} P(242,37);d(3) { rd( X, X ) ==> ld(
% 1.09/1.48 X, X ) }.
% 1.09/1.48 parent1[1; 5]: (985) {G1,W14,D4,L2,V0,M2} { ! mult( ld( skol2, skol2 ),
% 1.09/1.48 skol1 ) ==> skol1, ! skol1 ==> mult( skol1, rd( skol2, skol2 ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := skol2
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (990) {G2,W14,D4,L2,V0,M2} { ! mult( skol1, ld( skol2, skol2 ) )
% 1.09/1.48 ==> skol1, ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 parent0[0]: (986) {G2,W14,D4,L2,V0,M2} { ! skol1 ==> mult( skol1, ld(
% 1.09/1.48 skol2, skol2 ) ), ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (278) {G20,W14,D4,L2,V0,M2} P(255,5) { ! mult( skol1, ld(
% 1.09/1.48 skol2, skol2 ) ) ==> skol1, ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1
% 1.09/1.48 }.
% 1.09/1.48 parent0: (990) {G2,W14,D4,L2,V0,M2} { ! mult( skol1, ld( skol2, skol2 ) )
% 1.09/1.48 ==> skol1, ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 1 ==> 1
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (997) {G20,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld( X, ld
% 1.09/1.48 ( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.09/1.48 parent0[0]: (272) {G20,W15,D5,L1,V2,M1} P(255,172);d(40) { ld( Y, ld( rd( X
% 1.09/1.48 , Y ), rd( X, Y ) ) ) ==> ld( mult( X, Y ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1001) {G2,W19,D6,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X ) ==>
% 1.09/1.48 ld( ld( Y, X ), ld( rd( X, ld( Y, X ) ), Y ) ) }.
% 1.09/1.48 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.48 parent1[0; 18]: (997) {G20,W15,D5,L1,V2,M1} { ld( mult( Y, X ), Y ) ==> ld
% 1.09/1.48 ( X, ld( rd( Y, X ), rd( Y, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := ld( Y, X )
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1002) {G2,W15,D5,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X ) ==>
% 1.09/1.48 ld( ld( Y, X ), ld( Y, Y ) ) }.
% 1.09/1.48 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.48 parent1[0; 13]: (1001) {G2,W19,D6,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X
% 1.09/1.48 ) ==> ld( ld( Y, X ), ld( rd( X, ld( Y, X ) ), Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1004) {G2,W15,D5,L1,V2,M1} { ld( ld( Y, X ), ld( Y, Y ) ) ==> ld
% 1.09/1.48 ( mult( X, ld( Y, X ) ), X ) }.
% 1.09/1.48 parent0[0]: (1002) {G2,W15,D5,L1,V2,M1} { ld( mult( X, ld( Y, X ) ), X )
% 1.09/1.48 ==> ld( ld( Y, X ), ld( Y, Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (322) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y,
% 1.09/1.48 Y ) ) = ld( mult( X, ld( Y, X ) ), X ) }.
% 1.09/1.48 parent0: (1004) {G2,W15,D5,L1,V2,M1} { ld( ld( Y, X ), ld( Y, Y ) ) ==> ld
% 1.09/1.48 ( mult( X, ld( Y, X ) ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1007) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.09/1.48 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1008) {G2,W15,D5,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> ld( ld(
% 1.09/1.48 ld( Y, Y ), rd( Y, X ) ), Y ) }.
% 1.09/1.48 parent0[0]: (244) {G19,W15,D5,L1,V2,M1} P(242,166);d(7) { rd( X, mult( Y,
% 1.09/1.48 ld( X, X ) ) ) ==> ld( ld( X, X ), rd( X, Y ) ) }.
% 1.09/1.48 parent1[0; 7]: (1007) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := mult( X, ld( Y, Y ) )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1009) {G2,W15,D5,L1,V2,M1} { ld( ld( ld( Y, Y ), rd( Y, X ) ), Y
% 1.09/1.48 ) ==> mult( X, ld( Y, Y ) ) }.
% 1.09/1.48 parent0[0]: (1008) {G2,W15,D5,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> ld( ld
% 1.09/1.48 ( ld( Y, Y ), rd( Y, X ) ), Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (364) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd
% 1.09/1.48 ( X, Y ) ), X ) ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.48 parent0: (1009) {G2,W15,D5,L1,V2,M1} { ld( ld( ld( Y, Y ), rd( Y, X ) ), Y
% 1.09/1.48 ) ==> mult( X, ld( Y, Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1011) {G20,W15,D5,L1,V2,M1} { mult( Y, ld( X, X ) ) ==> ld( ld(
% 1.09/1.48 ld( X, X ), rd( X, Y ) ), X ) }.
% 1.09/1.48 parent0[0]: (364) {G20,W15,D5,L1,V2,M1} P(244,6) { ld( ld( ld( X, X ), rd(
% 1.09/1.48 X, Y ) ), X ) ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1014) {G2,W15,D5,L1,V2,M1} { mult( ld( X, Y ), ld( Y, Y ) ) ==>
% 1.09/1.48 ld( ld( ld( Y, Y ), X ), Y ) }.
% 1.09/1.48 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 1.09/1.48 parent1[0; 13]: (1011) {G20,W15,D5,L1,V2,M1} { mult( Y, ld( X, X ) ) ==>
% 1.09/1.48 ld( ld( ld( X, X ), rd( X, Y ) ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := ld( X, Y )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (367) {G21,W15,D5,L1,V2,M1} P(7,364) { mult( ld( Y, X ), ld( X
% 1.09/1.48 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 1.09/1.48 parent0: (1014) {G2,W15,D5,L1,V2,M1} { mult( ld( X, Y ), ld( Y, Y ) ) ==>
% 1.09/1.48 ld( ld( ld( Y, Y ), X ), Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1018) {G20,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 1.09/1.48 mult( ld( mult( X, X ), X ), Y ) }.
% 1.09/1.48 parent0[0]: (264) {G20,W11,D4,L1,V1,M1} P(255,216) { ld( X, ld( X, X ) )
% 1.09/1.48 ==> ld( mult( X, X ), X ) }.
% 1.09/1.48 parent1[0; 9]: (256) {G19,W15,D5,L1,V2,M1} P(242,37);d(194);d(21) { rd( ld
% 1.09/1.48 ( X, Y ), ld( X, X ) ) ==> mult( ld( X, ld( X, X ) ), Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (540) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld
% 1.09/1.48 ( X, X ) ) ==> mult( ld( mult( X, X ), X ), Y ) }.
% 1.09/1.48 parent0: (1018) {G20,W15,D5,L1,V2,M1} { rd( ld( X, Y ), ld( X, X ) ) ==>
% 1.09/1.48 mult( ld( mult( X, X ), X ), Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1021) {G21,W15,D5,L1,V2,M1} { mult( ld( mult( X, X ), X ), Y )
% 1.09/1.48 ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (540) {G21,W15,D5,L1,V2,M1} S(256);d(264) { rd( ld( X, Y ), ld
% 1.09/1.48 ( X, X ) ) ==> mult( ld( mult( X, X ), X ), Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1029) {G22,W27,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ), ld( X
% 1.09/1.48 , X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( mult( X, ld(
% 1.09/1.48 X, X ) ), X ) ) }.
% 1.09/1.48 parent0[0]: (322) {G21,W15,D5,L1,V2,M1} P(7,272) { ld( ld( Y, X ), ld( Y, Y
% 1.09/1.48 ) ) = ld( mult( X, ld( Y, X ) ), X ) }.
% 1.09/1.48 parent1[0; 20]: (1021) {G21,W15,D5,L1,V2,M1} { mult( ld( mult( X, X ), X )
% 1.09/1.48 , Y ) ==> rd( ld( X, Y ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1030) {G1,W23,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ), ld( X,
% 1.09/1.48 X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.48 parent1[0; 21]: (1029) {G22,W27,D6,L1,V2,M1} { mult( ld( mult( ld( X, X )
% 1.09/1.48 , ld( X, X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( mult(
% 1.09/1.48 X, ld( X, X ) ), X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1031) {G2,W23,D7,L1,V2,M1} { mult( ld( ld( ld( ld( X, X ), X ),
% 1.09/1.48 X ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (367) {G21,W15,D5,L1,V2,M1} P(7,364) { mult( ld( Y, X ), ld( X
% 1.09/1.48 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 1.09/1.48 parent1[0; 3]: (1030) {G1,W23,D6,L1,V2,M1} { mult( ld( mult( ld( X, X ),
% 1.09/1.48 ld( X, X ) ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) )
% 1.09/1.48 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1032) {G3,W19,D5,L1,V2,M1} { mult( ld( ld( X, X ), ld( X, X ) )
% 1.09/1.48 , Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.09/1.48 ld( X, X ), X ) ==> X }.
% 1.09/1.48 parent1[0; 4]: (1031) {G2,W23,D7,L1,V2,M1} { mult( ld( ld( ld( ld( X, X )
% 1.09/1.48 , X ), X ), ld( X, X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) )
% 1.09/1.48 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1033) {G4,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld(
% 1.09/1.48 ld( X, X ), Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.09/1.48 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.48 parent1[0; 2]: (1032) {G3,W19,D5,L1,V2,M1} { mult( ld( ld( X, X ), ld( X,
% 1.09/1.48 X ) ), Y ) ==> rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1034) {G4,W15,D5,L1,V2,M1} { rd( ld( ld( X, X ), Y ), ld( X, X )
% 1.09/1.48 ) ==> mult( ld( X, X ), Y ) }.
% 1.09/1.48 parent0[0]: (1033) {G4,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld
% 1.09/1.48 ( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (544) {G22,W15,D5,L1,V2,M1} P(322,540);d(0);d(367);d(242);d(
% 1.09/1.48 212) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y )
% 1.09/1.48 }.
% 1.09/1.48 parent0: (1034) {G4,W15,D5,L1,V2,M1} { rd( ld( ld( X, X ), Y ), ld( X, X )
% 1.09/1.48 ) ==> mult( ld( X, X ), Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1036) {G20,W15,D5,L1,V2,M1} { mult( Y, rd( ld( Y, X ), Y ) ) ==>
% 1.09/1.48 rd( rd( X, Y ), ld( Y, Y ) ) }.
% 1.09/1.48 parent0[0]: (270) {G20,W15,D5,L1,V2,M1} P(255,179) { rd( rd( Y, X ), ld( X
% 1.09/1.48 , X ) ) ==> mult( X, rd( ld( X, Y ), X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1044) {G21,W31,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 1.09/1.48 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X ), Y ),
% 1.09/1.48 ld( ld( X, X ), ld( X, X ) ) ) }.
% 1.09/1.48 parent0[0]: (544) {G22,W15,D5,L1,V2,M1} P(322,540);d(0);d(367);d(242);d(212
% 1.09/1.48 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 1.09/1.48 parent1[0; 19]: (1036) {G20,W15,D5,L1,V2,M1} { mult( Y, rd( ld( Y, X ), Y
% 1.09/1.48 ) ) ==> rd( rd( X, Y ), ld( Y, Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := ld( ld( X, X ), Y )
% 1.09/1.48 Y := ld( X, X )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1046) {G16,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 1.09/1.48 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X ), Y ),
% 1.09/1.48 ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (212) {G15,W11,D4,L1,V1,M1} P(209,21);d(2);d(129) { ld( ld( X,
% 1.09/1.48 X ), ld( X, X ) ) ==> ld( X, X ) }.
% 1.09/1.48 parent1[0; 24]: (1044) {G21,W31,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld(
% 1.09/1.48 ld( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X
% 1.09/1.48 ), Y ), ld( ld( X, X ), ld( X, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1047) {G5,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld( X, X
% 1.09/1.48 ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> mult( mult( ld( X, X ), rd
% 1.09/1.48 ( Y, X ) ), X ) }.
% 1.09/1.48 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 1.09/1.48 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.09/1.48 parent1[0; 18]: (1046) {G16,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld(
% 1.09/1.48 ld( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> rd( mult( ld( X, X
% 1.09/1.48 ), Y ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 Z := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1048) {G6,W27,D6,L1,V2,M1} { mult( ld( X, X ), ld( mult( ld( X,
% 1.09/1.48 X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd
% 1.09/1.48 ( Y, X ) ), X ) }.
% 1.09/1.48 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.09/1.48 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.09/1.48 parent1[0; 5]: (1047) {G5,W27,D7,L1,V2,M1} { mult( ld( X, X ), rd( ld( ld
% 1.09/1.48 ( X, X ), ld( ld( X, X ), Y ) ), ld( X, X ) ) ) ==> mult( mult( ld( X, X
% 1.09/1.48 ), rd( Y, X ) ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := ld( X, X )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1049) {G7,W27,D7,L1,V2,M1} { mult( ld( X, X ), ld( ld( ld( ld( X
% 1.09/1.48 , X ), X ), X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd(
% 1.09/1.48 Y, X ) ), X ) }.
% 1.09/1.48 parent0[0]: (367) {G21,W15,D5,L1,V2,M1} P(7,364) { mult( ld( Y, X ), ld( X
% 1.09/1.48 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 1.09/1.48 parent1[0; 6]: (1048) {G6,W27,D6,L1,V2,M1} { mult( ld( X, X ), ld( mult(
% 1.09/1.48 ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X,
% 1.09/1.48 X ), rd( Y, X ) ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1050) {G8,W23,D6,L1,V2,M1} { mult( ld( X, X ), ld( ld( X, X ),
% 1.09/1.48 rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd( Y, X ) ), X ) }.
% 1.09/1.48 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.09/1.48 ld( X, X ), X ) ==> X }.
% 1.09/1.48 parent1[0; 7]: (1049) {G7,W27,D7,L1,V2,M1} { mult( ld( X, X ), ld( ld( ld
% 1.09/1.48 ( ld( X, X ), X ), X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X
% 1.09/1.48 ), rd( Y, X ) ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1051) {G1,W15,D5,L1,V2,M1} { rd( Y, ld( X, X ) ) ==> mult( mult
% 1.09/1.48 ( ld( X, X ), rd( Y, X ) ), X ) }.
% 1.09/1.48 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.48 parent1[0; 1]: (1050) {G8,W23,D6,L1,V2,M1} { mult( ld( X, X ), ld( ld( X,
% 1.09/1.48 X ), rd( Y, ld( X, X ) ) ) ) ==> mult( mult( ld( X, X ), rd( Y, X ) ), X
% 1.09/1.48 ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := rd( Y, ld( X, X ) )
% 1.09/1.48 Y := ld( X, X )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1052) {G1,W15,D5,L1,V2,M1} { mult( mult( ld( Y, Y ), rd( X, Y ) )
% 1.09/1.48 , Y ) ==> rd( X, ld( Y, Y ) ) }.
% 1.09/1.48 parent0[0]: (1051) {G1,W15,D5,L1,V2,M1} { rd( Y, ld( X, X ) ) ==> mult(
% 1.09/1.48 mult( ld( X, X ), rd( Y, X ) ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (554) {G23,W15,D5,L1,V2,M1} P(544,270);d(212);d(194);d(38);d(
% 1.09/1.48 367);d(242);d(0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y,
% 1.09/1.48 ld( X, X ) ) }.
% 1.09/1.48 parent0: (1052) {G1,W15,D5,L1,V2,M1} { mult( mult( ld( Y, Y ), rd( X, Y )
% 1.09/1.48 ), Y ) ==> rd( X, ld( Y, Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1053) {G22,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==> rd( ld(
% 1.09/1.48 ld( X, X ), Y ), ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (544) {G22,W15,D5,L1,V2,M1} P(322,540);d(0);d(367);d(242);d(212
% 1.09/1.48 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1058) {G6,W23,D5,L1,V2,M1} { mult( ld( X, X ), ld( ld( X, X ), Y
% 1.09/1.48 ) ) ==> ld( mult( ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) ) }.
% 1.09/1.48 parent0[0]: (38) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( Z, ld( X, Y ) ), X
% 1.09/1.48 ) ==> ld( mult( X, Z ), rd( Y, X ) ) }.
% 1.09/1.48 parent1[0; 10]: (1053) {G22,W15,D5,L1,V2,M1} { mult( ld( X, X ), Y ) ==>
% 1.09/1.48 rd( ld( ld( X, X ), Y ), ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := ld( X, X )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := ld( ld( X, X ), Y )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1059) {G1,W15,D5,L1,V2,M1} { Y ==> ld( mult( ld( X, X ), ld( X,
% 1.09/1.48 X ) ), rd( Y, ld( X, X ) ) ) }.
% 1.09/1.48 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.48 parent1[0; 1]: (1058) {G6,W23,D5,L1,V2,M1} { mult( ld( X, X ), ld( ld( X,
% 1.09/1.48 X ), Y ) ) ==> ld( mult( ld( X, X ), ld( X, X ) ), rd( Y, ld( X, X ) ) )
% 1.09/1.48 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := ld( X, X )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1060) {G2,W15,D6,L1,V2,M1} { X ==> ld( ld( ld( ld( Y, Y ), Y ),
% 1.09/1.48 Y ), rd( X, ld( Y, Y ) ) ) }.
% 1.09/1.48 parent0[0]: (367) {G21,W15,D5,L1,V2,M1} P(7,364) { mult( ld( Y, X ), ld( X
% 1.09/1.48 , X ) ) ==> ld( ld( ld( X, X ), Y ), X ) }.
% 1.09/1.48 parent1[0; 3]: (1059) {G1,W15,D5,L1,V2,M1} { Y ==> ld( mult( ld( X, X ),
% 1.09/1.48 ld( X, X ) ), rd( Y, ld( X, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1061) {G3,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, Y ), rd( X, ld( Y
% 1.09/1.48 , Y ) ) ) }.
% 1.09/1.48 parent0[0]: (242) {G18,W7,D4,L1,V1,M1} P(218,27);d(58);d(240);d(239) { ld(
% 1.09/1.48 ld( X, X ), X ) ==> X }.
% 1.09/1.48 parent1[0; 4]: (1060) {G2,W15,D6,L1,V2,M1} { X ==> ld( ld( ld( ld( Y, Y )
% 1.09/1.48 , Y ), Y ), rd( X, ld( Y, Y ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1062) {G3,W11,D5,L1,V2,M1} { ld( ld( Y, Y ), rd( X, ld( Y, Y ) )
% 1.09/1.48 ) ==> X }.
% 1.09/1.48 parent0[0]: (1061) {G3,W11,D5,L1,V2,M1} { X ==> ld( ld( Y, Y ), rd( X, ld
% 1.09/1.48 ( Y, Y ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (558) {G23,W11,D5,L1,V2,M1} P(544,38);d(0);d(367);d(242) { ld
% 1.09/1.48 ( ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.09/1.48 parent0: (1062) {G3,W11,D5,L1,V2,M1} { ld( ld( Y, Y ), rd( X, ld( Y, Y ) )
% 1.09/1.48 ) ==> X }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1064) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y, ld( X
% 1.09/1.48 , X ) ) ) }.
% 1.09/1.48 parent0[0]: (558) {G23,W11,D5,L1,V2,M1} P(544,38);d(0);d(367);d(242) { ld(
% 1.09/1.48 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1067) {G23,W15,D5,L1,V2,M1} { ld( ld( X, X ), Y ) ==> ld( ld( X
% 1.09/1.48 , X ), mult( ld( X, X ), Y ) ) }.
% 1.09/1.48 parent0[0]: (544) {G22,W15,D5,L1,V2,M1} P(322,540);d(0);d(367);d(242);d(212
% 1.09/1.48 ) { rd( ld( ld( X, X ), Y ), ld( X, X ) ) ==> mult( ld( X, X ), Y ) }.
% 1.09/1.48 parent1[0; 10]: (1064) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y
% 1.09/1.48 , ld( X, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := ld( ld( X, X ), Y )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1068) {G1,W7,D4,L1,V2,M1} { ld( ld( X, X ), Y ) ==> Y }.
% 1.09/1.48 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 1.09/1.48 parent1[0; 6]: (1067) {G23,W15,D5,L1,V2,M1} { ld( ld( X, X ), Y ) ==> ld(
% 1.09/1.48 ld( X, X ), mult( ld( X, X ), Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := ld( X, X )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y
% 1.09/1.48 ) ==> Y }.
% 1.09/1.48 parent0: (1068) {G1,W7,D4,L1,V2,M1} { ld( ld( X, X ), Y ) ==> Y }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1071) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) ) ==>
% 1.09/1.48 mult( ld( X, rd( Y, Z ) ), Z ) }.
% 1.09/1.48 parent0[0]: (129) {G8,W15,D5,L1,V3,M1} P(120,0) { mult( ld( X, rd( Y, Z ) )
% 1.09/1.48 , Z ) ==> ld( ld( Z, X ), ld( Z, Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1076) {G9,W19,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X ) ),
% 1.09/1.48 ld( ld( X, X ), Y ) ) ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (558) {G23,W11,D5,L1,V2,M1} P(544,38);d(0);d(367);d(242) { ld(
% 1.09/1.48 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.09/1.48 parent1[0; 15]: (1071) {G8,W15,D5,L1,V3,M1} { ld( ld( Z, X ), ld( Z, Y ) )
% 1.09/1.48 ==> mult( ld( X, rd( Y, Z ) ), Z ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := ld( X, X )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1079) {G10,W15,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X ) ),
% 1.09/1.48 Y ) ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y
% 1.09/1.48 ) ==> Y }.
% 1.09/1.48 parent1[0; 9]: (1076) {G9,W19,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X
% 1.09/1.48 ) ), ld( ld( X, X ), Y ) ) ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1081) {G11,W7,D4,L1,V2,M1} { Y ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.48 parent0[0]: (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y
% 1.09/1.48 ) ==> Y }.
% 1.09/1.48 parent1[0; 1]: (1079) {G10,W15,D5,L1,V2,M1} { ld( ld( ld( X, X ), ld( X, X
% 1.09/1.48 ) ), Y ) ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1083) {G11,W7,D4,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> X }.
% 1.09/1.48 parent0[0]: (1081) {G11,W7,D4,L1,V2,M1} { Y ==> mult( Y, ld( X, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (584) {G25,W7,D4,L1,V2,M1} P(558,129);d(565);d(565) { mult( Y
% 1.09/1.48 , ld( X, X ) ) ==> Y }.
% 1.09/1.48 parent0: (1083) {G11,W7,D4,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> X }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1086) {G7,W15,D5,L1,V3,M1} { Z ==> ld( ld( X, rd( Y, Z ) ), ld(
% 1.09/1.48 ld( Z, X ), ld( Z, Y ) ) ) }.
% 1.09/1.48 parent0[0]: (120) {G7,W15,D5,L1,V3,M1} P(0,109) { ld( ld( Y, rd( Z, X ) ),
% 1.09/1.48 ld( ld( X, Y ), ld( X, Z ) ) ) ==> X }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Z
% 1.09/1.48 Y := X
% 1.09/1.48 Z := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1089) {G8,W19,D6,L1,V2,M1} { ld( X, X ) ==> ld( Y, ld( ld( ld( X
% 1.09/1.48 , X ), ld( X, X ) ), ld( ld( X, X ), Y ) ) ) }.
% 1.09/1.48 parent0[0]: (558) {G23,W11,D5,L1,V2,M1} P(544,38);d(0);d(367);d(242) { ld(
% 1.09/1.48 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.09/1.48 parent1[0; 5]: (1086) {G7,W15,D5,L1,V3,M1} { Z ==> ld( ld( X, rd( Y, Z ) )
% 1.09/1.48 , ld( ld( Z, X ), ld( Z, Y ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := ld( X, X )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1096) {G9,W15,D6,L1,V2,M1} { ld( X, X ) ==> ld( Y, ld( ld( ld( X
% 1.09/1.48 , X ), ld( X, X ) ), Y ) ) }.
% 1.09/1.48 parent0[0]: (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y
% 1.09/1.48 ) ==> Y }.
% 1.09/1.48 parent1[0; 14]: (1089) {G8,W19,D6,L1,V2,M1} { ld( X, X ) ==> ld( Y, ld( ld
% 1.09/1.48 ( ld( X, X ), ld( X, X ) ), ld( ld( X, X ), Y ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1098) {G10,W7,D3,L1,V2,M1} { ld( X, X ) ==> ld( Y, Y ) }.
% 1.09/1.48 parent0[0]: (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y
% 1.09/1.48 ) ==> Y }.
% 1.09/1.48 parent1[0; 6]: (1096) {G9,W15,D6,L1,V2,M1} { ld( X, X ) ==> ld( Y, ld( ld
% 1.09/1.48 ( ld( X, X ), ld( X, X ) ), Y ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (585) {G25,W7,D3,L1,V2,M1} P(558,120);d(565);d(565) { ld( Y, Y
% 1.09/1.48 ) = ld( X, X ) }.
% 1.09/1.48 parent0: (1098) {G10,W7,D3,L1,V2,M1} { ld( X, X ) ==> ld( Y, Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1102) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y, ld( X
% 1.09/1.48 , X ) ) ) }.
% 1.09/1.48 parent0[0]: (558) {G23,W11,D5,L1,V2,M1} P(544,38);d(0);d(367);d(242) { ld(
% 1.09/1.48 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1112) {G6,W23,D7,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 1.09/1.48 ( ld( X, X ), ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) ) }.
% 1.09/1.48 parent0[0]: (37) {G5,W15,D5,L1,V3,M1} P(0,31) { rd( ld( ld( X, Y ), Z ), X
% 1.09/1.48 ) ==> ld( Y, rd( mult( X, Z ), X ) ) }.
% 1.09/1.48 parent1[0; 12]: (1102) {G23,W11,D5,L1,V2,M1} { Y ==> ld( ld( X, X ), rd( Y
% 1.09/1.48 , ld( X, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := ld( X, X )
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := ld( ld( ld( X, X ), Y ), Z )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1114) {G7,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 1.09/1.48 ( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) }.
% 1.09/1.48 parent0[0]: (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y
% 1.09/1.48 ) ==> Y }.
% 1.09/1.48 parent1[0; 8]: (1112) {G6,W23,D7,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 1.09/1.48 ==> ld( ld( X, X ), ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) )
% 1.09/1.48 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1116) {G5,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 1.09/1.48 ( Y, mult( mult( ld( X, X ), rd( Z, X ) ), X ) ) }.
% 1.09/1.48 parent0[0]: (194) {G4,W19,D5,L1,V3,M1} P(7,28) { rd( mult( ld( Y, X ), Z )
% 1.09/1.48 , ld( Y, X ) ) ==> mult( mult( ld( Y, X ), rd( Z, X ) ), Y ) }.
% 1.09/1.48 parent1[0; 10]: (1114) {G7,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 1.09/1.48 ==> ld( Y, rd( mult( ld( X, X ), Z ), ld( X, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := X
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1117) {G6,W15,D5,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z ) ==> ld
% 1.09/1.48 ( Y, rd( Z, ld( X, X ) ) ) }.
% 1.09/1.48 parent0[0]: (554) {G23,W15,D5,L1,V2,M1} P(544,270);d(212);d(194);d(38);d(
% 1.09/1.48 367);d(242);d(0) { mult( mult( ld( X, X ), rd( Y, X ) ), X ) ==> rd( Y,
% 1.09/1.48 ld( X, X ) ) }.
% 1.09/1.48 parent1[0; 10]: (1116) {G5,W19,D6,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 1.09/1.48 ==> ld( Y, mult( mult( ld( X, X ), rd( Z, X ) ), X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Z
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1118) {G7,W11,D5,L1,V3,M1} { ld( Y, Z ) ==> ld( Y, rd( Z, ld( X
% 1.09/1.48 , X ) ) ) }.
% 1.09/1.48 parent0[0]: (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y
% 1.09/1.48 ) ==> Y }.
% 1.09/1.48 parent1[0; 2]: (1117) {G6,W15,D5,L1,V3,M1} { ld( ld( ld( X, X ), Y ), Z )
% 1.09/1.48 ==> ld( Y, rd( Z, ld( X, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 Z := Z
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1119) {G7,W11,D5,L1,V3,M1} { ld( X, rd( Y, ld( Z, Z ) ) ) ==> ld
% 1.09/1.48 ( X, Y ) }.
% 1.09/1.48 parent0[0]: (1118) {G7,W11,D5,L1,V3,M1} { ld( Y, Z ) ==> ld( Y, rd( Z, ld
% 1.09/1.48 ( X, X ) ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Z
% 1.09/1.48 Y := X
% 1.09/1.48 Z := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (591) {G25,W11,D5,L1,V3,M1} P(37,558);d(565);d(194);d(554);d(
% 1.09/1.48 565) { ld( Y, rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 1.09/1.48 parent0: (1119) {G7,W11,D5,L1,V3,M1} { ld( X, rd( Y, ld( Z, Z ) ) ) ==> ld
% 1.09/1.48 ( X, Y ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := Z
% 1.09/1.48 Z := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1121) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ), X ), ld
% 1.09/1.48 ( Y, X ) ) }.
% 1.09/1.48 parent0[0]: (43) {G6,W11,D5,L1,V2,M1} P(40,6) { ld( ld( mult( Y, X ), Y ),
% 1.09/1.48 ld( X, Y ) ) ==> Y }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1126) {G7,W23,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld(
% 1.09/1.48 mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), rd( X, ld( Y, Y ) ) ), X ) }.
% 1.09/1.48 parent0[0]: (558) {G23,W11,D5,L1,V2,M1} P(544,38);d(0);d(367);d(242) { ld(
% 1.09/1.48 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.09/1.48 parent1[0; 22]: (1121) {G6,W11,D5,L1,V2,M1} { X ==> ld( ld( mult( X, Y ),
% 1.09/1.48 X ), ld( Y, X ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := rd( X, ld( Y, Y ) )
% 1.09/1.48 Y := ld( Y, Y )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1127) {G8,W19,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld(
% 1.09/1.48 mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), X ), X ) }.
% 1.09/1.48 parent0[0]: (591) {G25,W11,D5,L1,V3,M1} P(37,558);d(565);d(194);d(554);d(
% 1.09/1.48 565) { ld( Y, rd( Z, ld( X, X ) ) ) ==> ld( Y, Z ) }.
% 1.09/1.48 parent1[0; 7]: (1126) {G7,W23,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 1.09/1.48 ld( mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), rd( X, ld( Y, Y ) ) ), X )
% 1.09/1.48 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) )
% 1.09/1.48 Z := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1128) {G9,W15,D6,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld( rd
% 1.09/1.48 ( X, ld( Y, Y ) ), X ), X ) }.
% 1.09/1.48 parent0[0]: (584) {G25,W7,D4,L1,V2,M1} P(558,129);d(565);d(565) { mult( Y,
% 1.09/1.48 ld( X, X ) ) ==> Y }.
% 1.09/1.48 parent1[0; 8]: (1127) {G8,W19,D7,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 1.09/1.48 ld( mult( rd( X, ld( Y, Y ) ), ld( Y, Y ) ), X ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := rd( X, ld( Y, Y ) )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1129) {G2,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld( ld( Y,
% 1.09/1.48 Y ), X ) }.
% 1.09/1.48 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 1.09/1.48 parent1[0; 7]: (1128) {G9,W15,D6,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 1.09/1.48 ld( rd( X, ld( Y, Y ) ), X ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := ld( Y, Y )
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1130) {G3,W7,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> X }.
% 1.09/1.48 parent0[0]: (565) {G24,W7,D4,L1,V2,M1} P(544,558);d(1) { ld( ld( X, X ), Y
% 1.09/1.48 ) ==> Y }.
% 1.09/1.48 parent1[0; 6]: (1129) {G2,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> ld(
% 1.09/1.48 ld( Y, Y ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (595) {G26,W7,D4,L1,V2,M1} P(558,43);d(591);d(584);d(6);d(565)
% 1.09/1.48 { rd( Y, ld( X, X ) ) ==> Y }.
% 1.09/1.48 parent0: (1130) {G3,W7,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> X }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1133) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) ) }.
% 1.09/1.48 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1135) {G1,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> mult( ld( Y
% 1.09/1.48 , Y ), X ) }.
% 1.09/1.48 parent0[0]: (558) {G23,W11,D5,L1,V2,M1} P(544,38);d(0);d(367);d(242) { ld(
% 1.09/1.48 ld( X, X ), rd( Y, ld( X, X ) ) ) ==> Y }.
% 1.09/1.48 parent1[0; 10]: (1133) {G0,W7,D4,L1,V2,M1} { Y ==> mult( X, ld( X, Y ) )
% 1.09/1.48 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := ld( Y, Y )
% 1.09/1.48 Y := rd( X, ld( Y, Y ) )
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1136) {G2,W7,D4,L1,V2,M1} { X ==> mult( ld( Y, Y ), X ) }.
% 1.09/1.48 parent0[0]: (595) {G26,W7,D4,L1,V2,M1} P(558,43);d(591);d(584);d(6);d(565)
% 1.09/1.48 { rd( Y, ld( X, X ) ) ==> Y }.
% 1.09/1.48 parent1[0; 1]: (1135) {G1,W11,D4,L1,V2,M1} { rd( X, ld( Y, Y ) ) ==> mult
% 1.09/1.48 ( ld( Y, Y ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1137) {G2,W7,D4,L1,V2,M1} { mult( ld( Y, Y ), X ) ==> X }.
% 1.09/1.48 parent0[0]: (1136) {G2,W7,D4,L1,V2,M1} { X ==> mult( ld( Y, Y ), X ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := Y
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (599) {G27,W7,D4,L1,V2,M1} P(558,0);d(595) { mult( ld( X, X )
% 1.09/1.48 , Y ) ==> Y }.
% 1.09/1.48 parent0: (1137) {G2,W7,D4,L1,V2,M1} { mult( ld( Y, Y ), X ) ==> X }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := Y
% 1.09/1.48 Y := X
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 0 ==> 0
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqswap: (1138) {G20,W14,D4,L2,V0,M2} { ! skol1 ==> mult( skol1, ld( skol2
% 1.09/1.48 , skol2 ) ), ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 parent0[0]: (278) {G20,W14,D4,L2,V0,M2} P(255,5) { ! mult( skol1, ld( skol2
% 1.09/1.48 , skol2 ) ) ==> skol1, ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1144) {G21,W14,D4,L2,V1,M2} { ! mult( ld( X, X ), skol1 ) ==>
% 1.09/1.48 skol1, ! skol1 ==> mult( skol1, ld( skol2, skol2 ) ) }.
% 1.09/1.48 parent0[0]: (585) {G25,W7,D3,L1,V2,M1} P(558,120);d(565);d(565) { ld( Y, Y
% 1.09/1.48 ) = ld( X, X ) }.
% 1.09/1.48 parent1[1; 3]: (1138) {G20,W14,D4,L2,V0,M2} { ! skol1 ==> mult( skol1, ld
% 1.09/1.48 ( skol2, skol2 ) ), ! mult( ld( skol2, skol2 ), skol1 ) ==> skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := skol2
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1146) {G22,W10,D4,L2,V1,M2} { ! skol1 ==> skol1, ! mult( ld( X,
% 1.09/1.48 X ), skol1 ) ==> skol1 }.
% 1.09/1.48 parent0[0]: (584) {G25,W7,D4,L1,V2,M1} P(558,129);d(565);d(565) { mult( Y,
% 1.09/1.48 ld( X, X ) ) ==> Y }.
% 1.09/1.48 parent1[1; 3]: (1144) {G21,W14,D4,L2,V1,M2} { ! mult( ld( X, X ), skol1 )
% 1.09/1.48 ==> skol1, ! skol1 ==> mult( skol1, ld( skol2, skol2 ) ) }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := skol2
% 1.09/1.48 Y := skol1
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 paramod: (1147) {G23,W6,D2,L2,V0,M2} { ! skol1 ==> skol1, ! skol1 ==>
% 1.09/1.48 skol1 }.
% 1.09/1.48 parent0[0]: (599) {G27,W7,D4,L1,V2,M1} P(558,0);d(595) { mult( ld( X, X ),
% 1.09/1.48 Y ) ==> Y }.
% 1.09/1.48 parent1[1; 2]: (1146) {G22,W10,D4,L2,V1,M2} { ! skol1 ==> skol1, ! mult(
% 1.09/1.48 ld( X, X ), skol1 ) ==> skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 X := X
% 1.09/1.48 Y := skol1
% 1.09/1.48 end
% 1.09/1.48 substitution1:
% 1.09/1.48 X := X
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqrefl: (1150) {G0,W3,D2,L1,V0,M1} { ! skol1 ==> skol1 }.
% 1.09/1.48 parent0[0]: (1147) {G23,W6,D2,L2,V0,M2} { ! skol1 ==> skol1, ! skol1 ==>
% 1.09/1.48 skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 eqrefl: (1151) {G0,W0,D0,L0,V0,M0} { }.
% 1.09/1.48 parent0[0]: (1150) {G0,W3,D2,L1,V0,M1} { ! skol1 ==> skol1 }.
% 1.09/1.48 substitution0:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 subsumption: (622) {G28,W0,D0,L0,V0,M0} P(585,278);d(584);d(599);q;q { }.
% 1.09/1.48 parent0: (1151) {G0,W0,D0,L0,V0,M0} { }.
% 1.09/1.48 substitution0:
% 1.09/1.48 end
% 1.09/1.48 permutation0:
% 1.09/1.48 end
% 1.09/1.48
% 1.09/1.48 Proof check complete!
% 1.09/1.48
% 1.09/1.48 Memory use:
% 1.09/1.48
% 1.09/1.48 space for terms: 10626
% 1.09/1.48 space for clauses: 98447
% 1.09/1.48
% 1.09/1.48
% 1.09/1.48 clauses generated: 7327
% 1.09/1.48 clauses kept: 623
% 1.09/1.48 clauses selected: 120
% 1.09/1.48 clauses deleted: 22
% 1.09/1.48 clauses inuse deleted: 0
% 1.09/1.48
% 1.09/1.48 subsentry: 1521
% 1.09/1.48 literals s-matched: 484
% 1.09/1.48 literals matched: 460
% 1.09/1.48 full subsumption: 0
% 1.09/1.48
% 1.09/1.48 checksum: -2090944593
% 1.09/1.48
% 1.09/1.48
% 1.09/1.48 Bliksem ended
%------------------------------------------------------------------------------