%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP658+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n015.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:26 EDT 2022
% Result : Theorem 0.70s 1.16s
% Output : Refutation 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP658+1 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Tue Jun 14 01:38:38 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.70/1.16 *** allocated 10000 integers for termspace/termends
% 0.70/1.16 *** allocated 10000 integers for clauses
% 0.70/1.16 *** allocated 10000 integers for justifications
% 0.70/1.16 Bliksem 1.12
% 0.70/1.16
% 0.70/1.16
% 0.70/1.16 Automatic Strategy Selection
% 0.70/1.16
% 0.70/1.16
% 0.70/1.16 Clauses:
% 0.70/1.16
% 0.70/1.16 { mult( Y, ld( Y, X ) ) = X }.
% 0.70/1.16 { ld( Y, mult( Y, X ) ) = X }.
% 0.70/1.16 { mult( rd( Y, X ), X ) = Y }.
% 0.70/1.16 { rd( mult( Y, X ), X ) = Y }.
% 0.70/1.16 { mult( mult( Z, mult( Y, Y ) ), X ) = mult( mult( Z, Y ), mult( Y, X ) ) }
% 0.70/1.16 .
% 0.70/1.16 { ! mult( skol1( X ), X ) = skol1( X ), ! mult( X, skol1( X ) ) = skol1( X
% 0.70/1.16 ) }.
% 0.70/1.16
% 0.70/1.16 percentage equality = 1.000000, percentage horn = 1.000000
% 0.70/1.16 This is a pure equality problem
% 0.70/1.16
% 0.70/1.16
% 0.70/1.16
% 0.70/1.16 Options Used:
% 0.70/1.16
% 0.70/1.16 useres = 1
% 0.70/1.16 useparamod = 1
% 0.70/1.16 useeqrefl = 1
% 0.70/1.16 useeqfact = 1
% 0.70/1.16 usefactor = 1
% 0.70/1.16 usesimpsplitting = 0
% 0.70/1.16 usesimpdemod = 5
% 0.70/1.16 usesimpres = 3
% 0.70/1.16
% 0.70/1.16 resimpinuse = 1000
% 0.70/1.16 resimpclauses = 20000
% 0.70/1.16 substype = eqrewr
% 0.70/1.16 backwardsubs = 1
% 0.70/1.16 selectoldest = 5
% 0.70/1.16
% 0.70/1.16 litorderings [0] = split
% 0.70/1.16 litorderings [1] = extend the termordering, first sorting on arguments
% 0.70/1.16
% 0.70/1.16 termordering = kbo
% 0.70/1.16
% 0.70/1.16 litapriori = 0
% 0.70/1.16 termapriori = 1
% 0.70/1.16 litaposteriori = 0
% 0.70/1.16 termaposteriori = 0
% 0.70/1.16 demodaposteriori = 0
% 0.70/1.16 ordereqreflfact = 0
% 0.70/1.16
% 0.70/1.16 litselect = negord
% 0.70/1.16
% 0.70/1.16 maxweight = 15
% 0.70/1.16 maxdepth = 30000
% 0.70/1.16 maxlength = 115
% 0.70/1.16 maxnrvars = 195
% 0.70/1.16 excuselevel = 1
% 0.70/1.16 increasemaxweight = 1
% 0.70/1.16
% 0.70/1.16 maxselected = 10000000
% 0.70/1.16 maxnrclauses = 10000000
% 0.70/1.16
% 0.70/1.16 showgenerated = 0
% 0.70/1.16 showkept = 0
% 0.70/1.16 showselected = 0
% 0.70/1.16 showdeleted = 0
% 0.70/1.16 showresimp = 1
% 0.70/1.16 showstatus = 2000
% 0.70/1.16
% 0.70/1.16 prologoutput = 0
% 0.70/1.16 nrgoals = 5000000
% 0.70/1.16 totalproof = 1
% 0.70/1.16
% 0.70/1.16 Symbols occurring in the translation:
% 0.70/1.16
% 0.70/1.16 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.70/1.16 . [1, 2] (w:1, o:17, a:1, s:1, b:0),
% 0.70/1.16 ! [4, 1] (w:0, o:11, a:1, s:1, b:0),
% 0.70/1.16 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.16 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.16 ld [37, 2] (w:1, o:41, a:1, s:1, b:0),
% 0.70/1.16 mult [38, 2] (w:1, o:42, a:1, s:1, b:0),
% 0.70/1.16 rd [39, 2] (w:1, o:43, a:1, s:1, b:0),
% 0.70/1.16 skol1 [43, 1] (w:1, o:16, a:1, s:1, b:1).
% 0.70/1.16
% 0.70/1.16
% 0.70/1.16 Starting Search:
% 0.70/1.16
% 0.70/1.16 *** allocated 15000 integers for clauses
% 0.70/1.16 *** allocated 22500 integers for clauses
% 0.70/1.16 *** allocated 33750 integers for clauses
% 0.70/1.16 *** allocated 50625 integers for clauses
% 0.70/1.16
% 0.70/1.16 Bliksems!, er is een bewijs:
% 0.70/1.16 % SZS status Theorem
% 0.70/1.16 % SZS output start Refutation
% 0.70/1.16
% 0.70/1.16 (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.70/1.16 (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.70/1.16 (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.70/1.16 (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.70/1.16 (4) {G0,W15,D5,L1,V3,M1} I { mult( mult( Z, Y ), mult( Y, X ) ) ==> mult(
% 0.70/1.16 mult( Z, mult( Y, Y ) ), X ) }.
% 0.70/1.16 (5) {G0,W14,D4,L2,V1,M2} I { ! mult( skol1( X ), X ) ==> skol1( X ), ! mult
% 0.70/1.16 ( X, skol1( X ) ) ==> skol1( X ) }.
% 0.70/1.16 (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.70/1.16 (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.70/1.16 (11) {G1,W15,D5,L1,V3,M1} P(0,4) { mult( mult( Z, mult( X, X ) ), ld( X, Y
% 0.70/1.16 ) ) ==> mult( mult( Z, X ), Y ) }.
% 0.70/1.16 (16) {G2,W15,D5,L1,V3,M1} P(11,1) { ld( mult( X, mult( Y, Y ) ), mult( mult
% 0.70/1.16 ( X, Y ), Z ) ) ==> ld( Y, Z ) }.
% 0.70/1.16 (19) {G3,W15,D5,L1,V3,M1} P(0,16) { ld( Y, ld( mult( X, Y ), Z ) ) ==> ld(
% 0.70/1.16 mult( X, mult( Y, Y ) ), Z ) }.
% 0.70/1.16 (23) {G4,W15,D5,L1,V3,M1} P(2,19) { ld( mult( rd( X, Y ), mult( Y, Y ) ), Z
% 0.70/1.16 ) ==> ld( Y, ld( X, Z ) ) }.
% 0.70/1.16 (24) {G5,W15,D5,L1,V3,M1} P(23,7) { rd( Z, ld( Y, ld( X, Z ) ) ) = mult( rd
% 0.70/1.16 ( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 (28) {G6,W15,D5,L1,V3,M1} P(6,24) { mult( rd( rd( X, Y ), Z ), mult( Z, Z )
% 0.70/1.16 ) ==> rd( X, ld( Z, Y ) ) }.
% 0.70/1.16 (29) {G6,W15,D6,L1,V3,M1} P(24,1) { ld( rd( X, Y ), rd( Z, ld( Y, ld( X, Z
% 0.70/1.16 ) ) ) ) ==> mult( Y, Y ) }.
% 0.70/1.16 (30) {G6,W15,D4,L1,V3,M1} P(1,24) { rd( mult( X, Y ), ld( Z, Y ) ) = mult(
% 0.70/1.16 rd( X, Z ), mult( Z, Z ) ) }.
% 0.70/1.16 (32) {G7,W15,D4,L1,V4,M1} P(30,30) { rd( mult( X, T ), ld( Y, T ) ) = rd(
% 0.70/1.16 mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.16 (39) {G8,W15,D5,L1,V4,M1} P(6,32) { rd( mult( Z, T ), ld( rd( X, Y ), T ) )
% 0.70/1.16 ==> rd( mult( Z, X ), Y ) }.
% 0.70/1.16 (41) {G8,W15,D5,L1,V4,M1} P(2,32) { rd( mult( rd( X, Y ), T ), ld( Z, T ) )
% 0.70/1.16 ==> rd( X, ld( Z, Y ) ) }.
% 0.70/1.16 (43) {G9,W15,D5,L1,V4,M1} P(39,6) { ld( rd( mult( X, Z ), T ), mult( X, Y )
% 0.70/1.16 ) ==> ld( rd( Z, T ), Y ) }.
% 0.70/1.16 (46) {G9,W15,D5,L1,V4,M1} P(2,39) { rd( X, ld( rd( Z, T ), Y ) ) ==> rd(
% 0.70/1.16 mult( rd( X, Y ), Z ), T ) }.
% 0.70/1.16 (47) {G10,W15,D6,L1,V4,M1} P(7,43) { ld( rd( Y, ld( Z, mult( X, Y ) ) ), T
% 0.70/1.16 ) ==> ld( Z, mult( X, T ) ) }.
% 0.70/1.16 (48) {G10,W15,D5,L1,V4,M1} P(0,43) { ld( rd( Y, Z ), mult( X, T ) ) ==> ld
% 0.70/1.16 ( rd( ld( X, Y ), Z ), T ) }.
% 0.70/1.16 (51) {G10,W7,D4,L1,V2,M1} P(3,43);d(1) { ld( rd( Y, Y ), Z ) ==> Z }.
% 0.70/1.16 (53) {G11,W11,D5,L1,V3,M1} P(51,43) { ld( rd( Y, mult( X, Y ) ), Z ) ==>
% 0.70/1.16 mult( X, Z ) }.
% 0.70/1.16 (55) {G11,W7,D3,L1,V2,M1} P(51,7) { rd( Y, Y ) = rd( X, X ) }.
% 0.70/1.16 (57) {G12,W11,D5,L1,V3,M1} P(55,43);d(48);d(53) { ld( rd( ld( X, Z ), Z ),
% 0.70/1.16 T ) ==> mult( X, T ) }.
% 0.70/1.16 (90) {G13,W15,D5,L1,V4,M1} P(57,24);d(28) { rd( Z, ld( T, mult( X, Z ) ) )
% 0.70/1.16 = rd( ld( X, Y ), ld( T, Y ) ) }.
% 0.70/1.16 (92) {G13,W11,D4,L1,V3,M1} P(57,7) { rd( Z, mult( X, Z ) ) = rd( ld( X, Y )
% 0.70/1.16 , Y ) }.
% 0.70/1.16 (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==> ld( rd( Y, X
% 0.70/1.16 ), Z ) }.
% 0.70/1.16 (103) {G14,W11,D5,L1,V3,M1} P(2,92) { rd( ld( rd( X, Y ), Z ), Z ) ==> rd(
% 0.70/1.16 Y, X ) }.
% 0.70/1.16 (116) {G14,W15,D5,L1,V4,M1} P(93,32);d(41) { rd( ld( rd( Y, X ), Z ), ld( T
% 0.70/1.16 , Z ) ) ==> rd( X, ld( T, Y ) ) }.
% 0.70/1.16 (117) {G15,W15,D5,L1,V3,M1} P(93,30);d(116);d(93);d(48) { ld( rd( ld( T, T
% 0.70/1.16 ), rd( X, Y ) ), T ) ==> rd( X, ld( T, Y ) ) }.
% 0.70/1.16 (127) {G16,W15,D5,L1,V4,M1} P(53,24);d(93);d(48);d(117) { rd( Z, ld( T,
% 0.70/1.16 mult( Y, Z ) ) ) = rd( X, ld( T, mult( Y, X ) ) ) }.
% 0.70/1.16 (159) {G17,W15,D5,L1,V4,M1} P(127,103);d(103) { rd( ld( Y, mult( Z, T ) ),
% 0.70/1.16 T ) = rd( ld( Y, mult( Z, X ) ), X ) }.
% 0.70/1.16 (161) {G18,W15,D5,L1,V4,M1} P(0,159) { rd( ld( Z, Y ), ld( X, Y ) ) = rd(
% 0.70/1.16 ld( Z, mult( X, T ) ), T ) }.
% 0.70/1.16 (164) {G19,W15,D5,L1,V4,M1} P(161,93);d(93);d(47) { ld( rd( ld( Z, Y ), ld
% 0.70/1.16 ( X, Y ) ), U ) ==> ld( X, mult( Z, U ) ) }.
% 0.70/1.16 (173) {G14,W15,D5,L1,V4,M1} S(46);d(93) { rd( X, ld( rd( Z, T ), Y ) ) ==>
% 0.70/1.16 rd( ld( rd( Y, X ), Z ), T ) }.
% 0.70/1.16 (177) {G11,W11,D5,L1,V2,M1} P(51,29);d(7) { ld( rd( rd( X, X ), Z ), Z )
% 0.70/1.16 ==> mult( Z, Z ) }.
% 0.70/1.16 (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X ) ) ==> Y }.
% 0.70/1.16 (198) {G16,W7,D3,L1,V2,M1} P(193,29);d(173);d(103);d(7);d(93);d(51) { ld( X
% 0.70/1.16 , X ) = rd( Y, Y ) }.
% 0.70/1.16 (200) {G16,W11,D4,L1,V3,M1} P(193,173);d(193) { rd( Z, ld( X, T ) ) ==> ld
% 0.70/1.16 ( rd( T, Z ), X ) }.
% 0.70/1.16 (202) {G16,W11,D4,L1,V3,M1} P(193,48);d(193) { ld( X, mult( Z, T ) ) ==> ld
% 0.70/1.16 ( ld( Z, X ), T ) }.
% 0.70/1.16 (216) {G16,W11,D5,L1,V3,M1} P(193,93) { ld( rd( rd( Y, Y ), X ), Z ) ==>
% 0.70/1.16 mult( X, Z ) }.
% 0.70/1.16 (232) {G17,W7,D4,L1,V2,M1} P(198,90);d(193);d(200);d(202);d(7) { ld( ld( X
% 0.70/1.16 , X ), Y ) ==> Y }.
% 0.70/1.16 (249) {G20,W11,D4,L1,V3,M1} P(198,164);d(216);d(202) { mult( ld( Z, X ), T
% 0.70/1.16 ) ==> ld( ld( X, Z ), T ) }.
% 0.70/1.16 (259) {G17,W11,D4,L1,V3,M1} P(198,39);d(193) { rd( mult( T, X ), Y ) ==>
% 0.70/1.16 mult( T, rd( X, Y ) ) }.
% 0.70/1.16 (260) {G18,W7,D4,L1,V2,M1} P(198,39);d(259);d(7);d(3) { mult( Z, ld( Y, Y )
% 0.70/1.16 ) ==> Z }.
% 0.70/1.16 (287) {G21,W0,D0,L0,V0,M0} R(260,5);d(249);d(232);q { }.
% 0.70/1.16
% 0.70/1.16
% 0.70/1.16 % SZS output end Refutation
% 0.70/1.16 found a proof!
% 0.70/1.16
% 0.70/1.16
% 0.70/1.16 Unprocessed initial clauses:
% 0.70/1.16
% 0.70/1.16 (289) {G0,W7,D4,L1,V2,M1} { mult( Y, ld( Y, X ) ) = X }.
% 0.70/1.16 (290) {G0,W7,D4,L1,V2,M1} { ld( Y, mult( Y, X ) ) = X }.
% 0.70/1.16 (291) {G0,W7,D4,L1,V2,M1} { mult( rd( Y, X ), X ) = Y }.
% 0.70/1.16 (292) {G0,W7,D4,L1,V2,M1} { rd( mult( Y, X ), X ) = Y }.
% 0.70/1.16 (293) {G0,W15,D5,L1,V3,M1} { mult( mult( Z, mult( Y, Y ) ), X ) = mult(
% 0.70/1.16 mult( Z, Y ), mult( Y, X ) ) }.
% 0.70/1.16 (294) {G0,W14,D4,L2,V1,M2} { ! mult( skol1( X ), X ) = skol1( X ), ! mult
% 0.70/1.16 ( X, skol1( X ) ) = skol1( X ) }.
% 0.70/1.16
% 0.70/1.16
% 0.70/1.16 Total Proof:
% 0.70/1.16
% 0.70/1.16 subsumption: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.70/1.16 parent0: (289) {G0,W7,D4,L1,V2,M1} { mult( Y, ld( Y, X ) ) = X }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.70/1.16 parent0: (290) {G0,W7,D4,L1,V2,M1} { ld( Y, mult( Y, X ) ) = X }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.70/1.16 parent0: (291) {G0,W7,D4,L1,V2,M1} { mult( rd( Y, X ), X ) = Y }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.70/1.16 parent0: (292) {G0,W7,D4,L1,V2,M1} { rd( mult( Y, X ), X ) = Y }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (309) {G0,W15,D5,L1,V3,M1} { mult( mult( X, Y ), mult( Y, Z ) ) =
% 0.70/1.16 mult( mult( X, mult( Y, Y ) ), Z ) }.
% 0.70/1.16 parent0[0]: (293) {G0,W15,D5,L1,V3,M1} { mult( mult( Z, mult( Y, Y ) ), X
% 0.70/1.16 ) = mult( mult( Z, Y ), mult( Y, X ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (4) {G0,W15,D5,L1,V3,M1} I { mult( mult( Z, Y ), mult( Y, X )
% 0.70/1.16 ) ==> mult( mult( Z, mult( Y, Y ) ), X ) }.
% 0.70/1.16 parent0: (309) {G0,W15,D5,L1,V3,M1} { mult( mult( X, Y ), mult( Y, Z ) ) =
% 0.70/1.16 mult( mult( X, mult( Y, Y ) ), Z ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := X
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (5) {G0,W14,D4,L2,V1,M2} I { ! mult( skol1( X ), X ) ==> skol1
% 0.70/1.16 ( X ), ! mult( X, skol1( X ) ) ==> skol1( X ) }.
% 0.70/1.16 parent0: (294) {G0,W14,D4,L2,V1,M2} { ! mult( skol1( X ), X ) = skol1( X )
% 0.70/1.16 , ! mult( X, skol1( X ) ) = skol1( X ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 1 ==> 1
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (319) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.70/1.16 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (320) {G1,W7,D4,L1,V2,M1} { X ==> ld( rd( Y, X ), Y ) }.
% 0.70/1.16 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.70/1.16 parent1[0; 6]: (319) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := rd( Y, X )
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (321) {G1,W7,D4,L1,V2,M1} { ld( rd( Y, X ), Y ) ==> X }.
% 0.70/1.16 parent0[0]: (320) {G1,W7,D4,L1,V2,M1} { X ==> ld( rd( Y, X ), Y ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.70/1.16 parent0: (321) {G1,W7,D4,L1,V2,M1} { ld( rd( Y, X ), Y ) ==> X }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (323) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 0.70/1.16 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (324) {G1,W7,D4,L1,V2,M1} { X ==> rd( Y, ld( X, Y ) ) }.
% 0.70/1.16 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.70/1.16 parent1[0; 3]: (323) {G0,W7,D4,L1,V2,M1} { X ==> rd( mult( X, Y ), Y ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := X
% 0.70/1.16 Y := ld( X, Y )
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (325) {G1,W7,D4,L1,V2,M1} { rd( Y, ld( X, Y ) ) ==> X }.
% 0.70/1.16 parent0[0]: (324) {G1,W7,D4,L1,V2,M1} { X ==> rd( Y, ld( X, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.70/1.16 parent0: (325) {G1,W7,D4,L1,V2,M1} { rd( Y, ld( X, Y ) ) ==> X }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (327) {G0,W15,D5,L1,V3,M1} { mult( mult( X, mult( Y, Y ) ), Z )
% 0.70/1.16 ==> mult( mult( X, Y ), mult( Y, Z ) ) }.
% 0.70/1.16 parent0[0]: (4) {G0,W15,D5,L1,V3,M1} I { mult( mult( Z, Y ), mult( Y, X ) )
% 0.70/1.16 ==> mult( mult( Z, mult( Y, Y ) ), X ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (330) {G1,W15,D5,L1,V3,M1} { mult( mult( X, mult( Y, Y ) ), ld( Y
% 0.70/1.16 , Z ) ) ==> mult( mult( X, Y ), Z ) }.
% 0.70/1.16 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.70/1.16 parent1[0; 14]: (327) {G0,W15,D5,L1,V3,M1} { mult( mult( X, mult( Y, Y ) )
% 0.70/1.16 , Z ) ==> mult( mult( X, Y ), mult( Y, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := ld( Y, Z )
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (11) {G1,W15,D5,L1,V3,M1} P(0,4) { mult( mult( Z, mult( X, X )
% 0.70/1.16 ), ld( X, Y ) ) ==> mult( mult( Z, X ), Y ) }.
% 0.70/1.16 parent0: (330) {G1,W15,D5,L1,V3,M1} { mult( mult( X, mult( Y, Y ) ), ld( Y
% 0.70/1.16 , Z ) ) ==> mult( mult( X, Y ), Z ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := X
% 0.70/1.16 Z := Y
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (335) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.70/1.16 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (338) {G1,W15,D5,L1,V3,M1} { ld( X, Y ) ==> ld( mult( Z, mult( X
% 0.70/1.16 , X ) ), mult( mult( Z, X ), Y ) ) }.
% 0.70/1.16 parent0[0]: (11) {G1,W15,D5,L1,V3,M1} P(0,4) { mult( mult( Z, mult( X, X )
% 0.70/1.16 ), ld( X, Y ) ) ==> mult( mult( Z, X ), Y ) }.
% 0.70/1.16 parent1[0; 10]: (335) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) )
% 0.70/1.16 }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := mult( Z, mult( X, X ) )
% 0.70/1.16 Y := ld( X, Y )
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (339) {G1,W15,D5,L1,V3,M1} { ld( mult( Z, mult( X, X ) ), mult(
% 0.70/1.16 mult( Z, X ), Y ) ) ==> ld( X, Y ) }.
% 0.70/1.16 parent0[0]: (338) {G1,W15,D5,L1,V3,M1} { ld( X, Y ) ==> ld( mult( Z, mult
% 0.70/1.16 ( X, X ) ), mult( mult( Z, X ), Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (16) {G2,W15,D5,L1,V3,M1} P(11,1) { ld( mult( X, mult( Y, Y )
% 0.70/1.16 ), mult( mult( X, Y ), Z ) ) ==> ld( Y, Z ) }.
% 0.70/1.16 parent0: (339) {G1,W15,D5,L1,V3,M1} { ld( mult( Z, mult( X, X ) ), mult(
% 0.70/1.16 mult( Z, X ), Y ) ) ==> ld( X, Y ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := Z
% 0.70/1.16 Z := X
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (341) {G2,W15,D5,L1,V3,M1} { ld( Y, Z ) ==> ld( mult( X, mult( Y,
% 0.70/1.16 Y ) ), mult( mult( X, Y ), Z ) ) }.
% 0.70/1.16 parent0[0]: (16) {G2,W15,D5,L1,V3,M1} P(11,1) { ld( mult( X, mult( Y, Y ) )
% 0.70/1.16 , mult( mult( X, Y ), Z ) ) ==> ld( Y, Z ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (344) {G1,W15,D5,L1,V3,M1} { ld( X, ld( mult( Y, X ), Z ) ) ==>
% 0.70/1.16 ld( mult( Y, mult( X, X ) ), Z ) }.
% 0.70/1.16 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.70/1.16 parent1[0; 14]: (341) {G2,W15,D5,L1,V3,M1} { ld( Y, Z ) ==> ld( mult( X,
% 0.70/1.16 mult( Y, Y ) ), mult( mult( X, Y ), Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := mult( Y, X )
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 Z := ld( mult( Y, X ), Z )
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (19) {G3,W15,D5,L1,V3,M1} P(0,16) { ld( Y, ld( mult( X, Y ), Z
% 0.70/1.16 ) ) ==> ld( mult( X, mult( Y, Y ) ), Z ) }.
% 0.70/1.16 parent0: (344) {G1,W15,D5,L1,V3,M1} { ld( X, ld( mult( Y, X ), Z ) ) ==>
% 0.70/1.16 ld( mult( Y, mult( X, X ) ), Z ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (349) {G3,W15,D5,L1,V3,M1} { ld( mult( Y, mult( X, X ) ), Z ) ==>
% 0.70/1.16 ld( X, ld( mult( Y, X ), Z ) ) }.
% 0.70/1.16 parent0[0]: (19) {G3,W15,D5,L1,V3,M1} P(0,16) { ld( Y, ld( mult( X, Y ), Z
% 0.70/1.16 ) ) ==> ld( mult( X, mult( Y, Y ) ), Z ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (351) {G1,W15,D5,L1,V3,M1} { ld( mult( rd( X, Y ), mult( Y, Y ) )
% 0.70/1.16 , Z ) ==> ld( Y, ld( X, Z ) ) }.
% 0.70/1.16 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.70/1.16 parent1[0; 13]: (349) {G3,W15,D5,L1,V3,M1} { ld( mult( Y, mult( X, X ) ),
% 0.70/1.16 Z ) ==> ld( X, ld( mult( Y, X ), Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := rd( X, Y )
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (23) {G4,W15,D5,L1,V3,M1} P(2,19) { ld( mult( rd( X, Y ), mult
% 0.70/1.16 ( Y, Y ) ), Z ) ==> ld( Y, ld( X, Z ) ) }.
% 0.70/1.16 parent0: (351) {G1,W15,D5,L1,V3,M1} { ld( mult( rd( X, Y ), mult( Y, Y ) )
% 0.70/1.16 , Z ) ==> ld( Y, ld( X, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (355) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 0.70/1.16 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (358) {G2,W15,D5,L1,V3,M1} { mult( rd( X, Y ), mult( Y, Y ) ) ==>
% 0.70/1.16 rd( Z, ld( Y, ld( X, Z ) ) ) }.
% 0.70/1.16 parent0[0]: (23) {G4,W15,D5,L1,V3,M1} P(2,19) { ld( mult( rd( X, Y ), mult
% 0.70/1.16 ( Y, Y ) ), Z ) ==> ld( Y, ld( X, Z ) ) }.
% 0.70/1.16 parent1[0; 10]: (355) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := mult( rd( X, Y ), mult( Y, Y ) )
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (359) {G2,W15,D5,L1,V3,M1} { rd( Z, ld( Y, ld( X, Z ) ) ) ==> mult
% 0.70/1.16 ( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 parent0[0]: (358) {G2,W15,D5,L1,V3,M1} { mult( rd( X, Y ), mult( Y, Y ) )
% 0.70/1.16 ==> rd( Z, ld( Y, ld( X, Z ) ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (24) {G5,W15,D5,L1,V3,M1} P(23,7) { rd( Z, ld( Y, ld( X, Z ) )
% 0.70/1.16 ) = mult( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 parent0: (359) {G2,W15,D5,L1,V3,M1} { rd( Z, ld( Y, ld( X, Z ) ) ) ==>
% 0.70/1.16 mult( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (361) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y ) ) = rd
% 0.70/1.16 ( X, ld( Y, ld( Z, X ) ) ) }.
% 0.70/1.16 parent0[0]: (24) {G5,W15,D5,L1,V3,M1} P(23,7) { rd( Z, ld( Y, ld( X, Z ) )
% 0.70/1.16 ) = mult( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (365) {G2,W15,D5,L1,V3,M1} { mult( rd( rd( X, Y ), Z ), mult( Z,
% 0.70/1.16 Z ) ) = rd( X, ld( Z, Y ) ) }.
% 0.70/1.16 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.70/1.16 parent1[0; 14]: (361) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y
% 0.70/1.16 ) ) = rd( X, ld( Y, ld( Z, X ) ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Z
% 0.70/1.16 Z := rd( X, Y )
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (28) {G6,W15,D5,L1,V3,M1} P(6,24) { mult( rd( rd( X, Y ), Z )
% 0.70/1.16 , mult( Z, Z ) ) ==> rd( X, ld( Z, Y ) ) }.
% 0.70/1.16 parent0: (365) {G2,W15,D5,L1,V3,M1} { mult( rd( rd( X, Y ), Z ), mult( Z,
% 0.70/1.16 Z ) ) = rd( X, ld( Z, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (368) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y ) ) = rd
% 0.70/1.16 ( X, ld( Y, ld( Z, X ) ) ) }.
% 0.70/1.16 parent0[0]: (24) {G5,W15,D5,L1,V3,M1} P(23,7) { rd( Z, ld( Y, ld( X, Z ) )
% 0.70/1.16 ) = mult( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (369) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.70/1.16 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (370) {G1,W15,D6,L1,V3,M1} { mult( X, X ) ==> ld( rd( Y, X ), rd
% 0.70/1.16 ( Z, ld( X, ld( Y, Z ) ) ) ) }.
% 0.70/1.16 parent0[0]: (368) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y ) )
% 0.70/1.16 = rd( X, ld( Y, ld( Z, X ) ) ) }.
% 0.70/1.16 parent1[0; 8]: (369) {G0,W7,D4,L1,V2,M1} { Y ==> ld( X, mult( X, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := X
% 0.70/1.16 Z := Y
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := rd( Y, X )
% 0.70/1.16 Y := mult( X, X )
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (371) {G1,W15,D6,L1,V3,M1} { ld( rd( Y, X ), rd( Z, ld( X, ld( Y,
% 0.70/1.16 Z ) ) ) ) ==> mult( X, X ) }.
% 0.70/1.16 parent0[0]: (370) {G1,W15,D6,L1,V3,M1} { mult( X, X ) ==> ld( rd( Y, X ),
% 0.70/1.16 rd( Z, ld( X, ld( Y, Z ) ) ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (29) {G6,W15,D6,L1,V3,M1} P(24,1) { ld( rd( X, Y ), rd( Z, ld
% 0.70/1.16 ( Y, ld( X, Z ) ) ) ) ==> mult( Y, Y ) }.
% 0.70/1.16 parent0: (371) {G1,W15,D6,L1,V3,M1} { ld( rd( Y, X ), rd( Z, ld( X, ld( Y
% 0.70/1.16 , Z ) ) ) ) ==> mult( X, X ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (373) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y ) ) = rd
% 0.70/1.16 ( X, ld( Y, ld( Z, X ) ) ) }.
% 0.70/1.16 parent0[0]: (24) {G5,W15,D5,L1,V3,M1} P(23,7) { rd( Z, ld( Y, ld( X, Z ) )
% 0.70/1.16 ) = mult( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (376) {G1,W15,D4,L1,V3,M1} { mult( rd( X, Y ), mult( Y, Y ) ) =
% 0.70/1.16 rd( mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.16 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.70/1.16 parent1[0; 14]: (373) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y
% 0.70/1.16 ) ) = rd( X, ld( Y, ld( Z, X ) ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := mult( X, Z )
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := X
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (377) {G1,W15,D4,L1,V3,M1} { rd( mult( X, Z ), ld( Y, Z ) ) = mult
% 0.70/1.16 ( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 parent0[0]: (376) {G1,W15,D4,L1,V3,M1} { mult( rd( X, Y ), mult( Y, Y ) )
% 0.70/1.16 = rd( mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (30) {G6,W15,D4,L1,V3,M1} P(1,24) { rd( mult( X, Y ), ld( Z, Y
% 0.70/1.16 ) ) = mult( rd( X, Z ), mult( Z, Z ) ) }.
% 0.70/1.16 parent0: (377) {G1,W15,D4,L1,V3,M1} { rd( mult( X, Z ), ld( Y, Z ) ) =
% 0.70/1.16 mult( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Z
% 0.70/1.16 Z := Y
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (378) {G6,W15,D4,L1,V3,M1} { mult( rd( X, Z ), mult( Z, Z ) ) = rd
% 0.70/1.16 ( mult( X, Y ), ld( Z, Y ) ) }.
% 0.70/1.16 parent0[0]: (30) {G6,W15,D4,L1,V3,M1} P(1,24) { rd( mult( X, Y ), ld( Z, Y
% 0.70/1.16 ) ) = mult( rd( X, Z ), mult( Z, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (379) {G6,W15,D4,L1,V3,M1} { mult( rd( X, Z ), mult( Z, Z ) ) = rd
% 0.70/1.16 ( mult( X, Y ), ld( Z, Y ) ) }.
% 0.70/1.16 parent0[0]: (30) {G6,W15,D4,L1,V3,M1} P(1,24) { rd( mult( X, Y ), ld( Z, Y
% 0.70/1.16 ) ) = mult( rd( X, Z ), mult( Z, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (380) {G7,W15,D4,L1,V4,M1} { rd( mult( X, T ), ld( Y, T ) ) = rd
% 0.70/1.16 ( mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.16 parent0[0]: (378) {G6,W15,D4,L1,V3,M1} { mult( rd( X, Z ), mult( Z, Z ) )
% 0.70/1.16 = rd( mult( X, Y ), ld( Z, Y ) ) }.
% 0.70/1.16 parent1[0; 1]: (379) {G6,W15,D4,L1,V3,M1} { mult( rd( X, Z ), mult( Z, Z )
% 0.70/1.16 ) = rd( mult( X, Y ), ld( Z, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := T
% 0.70/1.16 Z := Y
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Z
% 0.70/1.16 Z := Y
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (32) {G7,W15,D4,L1,V4,M1} P(30,30) { rd( mult( X, T ), ld( Y,
% 0.70/1.16 T ) ) = rd( mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.16 parent0: (380) {G7,W15,D4,L1,V4,M1} { rd( mult( X, T ), ld( Y, T ) ) = rd
% 0.70/1.16 ( mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 T := T
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (389) {G2,W15,D5,L1,V4,M1} { rd( mult( X, Y ), ld( rd( Z, T ), Y
% 0.70/1.16 ) ) = rd( mult( X, Z ), T ) }.
% 0.70/1.16 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.70/1.16 parent1[0; 14]: (32) {G7,W15,D4,L1,V4,M1} P(30,30) { rd( mult( X, T ), ld(
% 0.70/1.16 Y, T ) ) = rd( mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := T
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := X
% 0.70/1.16 Y := rd( Z, T )
% 0.70/1.16 Z := Z
% 0.70/1.16 T := Y
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (39) {G8,W15,D5,L1,V4,M1} P(6,32) { rd( mult( Z, T ), ld( rd(
% 0.70/1.16 X, Y ), T ) ) ==> rd( mult( Z, X ), Y ) }.
% 0.70/1.16 parent0: (389) {G2,W15,D5,L1,V4,M1} { rd( mult( X, Y ), ld( rd( Z, T ), Y
% 0.70/1.16 ) ) = rd( mult( X, Z ), T ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := T
% 0.70/1.16 Z := X
% 0.70/1.16 T := Y
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (394) {G1,W15,D5,L1,V4,M1} { rd( mult( rd( X, Y ), Z ), ld( T, Z
% 0.70/1.16 ) ) = rd( X, ld( T, Y ) ) }.
% 0.70/1.16 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.70/1.16 parent1[0; 11]: (32) {G7,W15,D4,L1,V4,M1} P(30,30) { rd( mult( X, T ), ld(
% 0.70/1.16 Y, T ) ) = rd( mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Y
% 0.70/1.16 Y := X
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := rd( X, Y )
% 0.70/1.16 Y := T
% 0.70/1.16 Z := Y
% 0.70/1.16 T := Z
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (41) {G8,W15,D5,L1,V4,M1} P(2,32) { rd( mult( rd( X, Y ), T )
% 0.70/1.16 , ld( Z, T ) ) ==> rd( X, ld( Z, Y ) ) }.
% 0.70/1.16 parent0: (394) {G1,W15,D5,L1,V4,M1} { rd( mult( rd( X, Y ), Z ), ld( T, Z
% 0.70/1.16 ) ) = rd( X, ld( T, Y ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := T
% 0.70/1.16 T := Z
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (396) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 0.70/1.16 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (398) {G2,W15,D5,L1,V4,M1} { ld( rd( X, Y ), Z ) ==> ld( rd( mult
% 0.70/1.16 ( T, X ), Y ), mult( T, Z ) ) }.
% 0.70/1.16 parent0[0]: (39) {G8,W15,D5,L1,V4,M1} P(6,32) { rd( mult( Z, T ), ld( rd( X
% 0.70/1.16 , Y ), T ) ) ==> rd( mult( Z, X ), Y ) }.
% 0.70/1.16 parent1[0; 7]: (396) {G1,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, Y ), X ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := T
% 0.70/1.16 T := Z
% 0.70/1.16 end
% 0.70/1.16 substitution1:
% 0.70/1.16 X := mult( T, Z )
% 0.70/1.16 Y := ld( rd( X, Y ), Z )
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (399) {G2,W15,D5,L1,V4,M1} { ld( rd( mult( T, X ), Y ), mult( T, Z
% 0.70/1.16 ) ) ==> ld( rd( X, Y ), Z ) }.
% 0.70/1.16 parent0[0]: (398) {G2,W15,D5,L1,V4,M1} { ld( rd( X, Y ), Z ) ==> ld( rd(
% 0.70/1.16 mult( T, X ), Y ), mult( T, Z ) ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := X
% 0.70/1.16 Y := Y
% 0.70/1.16 Z := Z
% 0.70/1.16 T := T
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 subsumption: (43) {G9,W15,D5,L1,V4,M1} P(39,6) { ld( rd( mult( X, Z ), T )
% 0.70/1.16 , mult( X, Y ) ) ==> ld( rd( Z, T ), Y ) }.
% 0.70/1.16 parent0: (399) {G2,W15,D5,L1,V4,M1} { ld( rd( mult( T, X ), Y ), mult( T,
% 0.70/1.16 Z ) ) ==> ld( rd( X, Y ), Z ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := T
% 0.70/1.16 Z := Y
% 0.70/1.16 T := X
% 0.70/1.16 end
% 0.70/1.16 permutation0:
% 0.70/1.16 0 ==> 0
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 eqswap: (401) {G8,W15,D5,L1,V4,M1} { rd( mult( X, Z ), T ) ==> rd( mult( X
% 0.70/1.16 , Y ), ld( rd( Z, T ), Y ) ) }.
% 0.70/1.16 parent0[0]: (39) {G8,W15,D5,L1,V4,M1} P(6,32) { rd( mult( Z, T ), ld( rd( X
% 0.70/1.16 , Y ), T ) ) ==> rd( mult( Z, X ), Y ) }.
% 0.70/1.16 substitution0:
% 0.70/1.16 X := Z
% 0.70/1.16 Y := T
% 0.70/1.16 Z := X
% 0.70/1.16 T := Y
% 0.70/1.16 end
% 0.70/1.16
% 0.70/1.16 paramod: (405) {G1,W15,D5,L1,V4,M1} { rd( mult( rd( X, Y ), Z ), T ) ==>
% 0.70/1.16 rd( X, ld( rd( Z, T ), Y ) ) }.
% 0.70/1.17 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.70/1.17 parent1[0; 9]: (401) {G8,W15,D5,L1,V4,M1} { rd( mult( X, Z ), T ) ==> rd(
% 0.70/1.17 mult( X, Y ), ld( rd( Z, T ), Y ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := X
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := rd( X, Y )
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (407) {G1,W15,D5,L1,V4,M1} { rd( X, ld( rd( Z, T ), Y ) ) ==> rd(
% 0.70/1.17 mult( rd( X, Y ), Z ), T ) }.
% 0.70/1.17 parent0[0]: (405) {G1,W15,D5,L1,V4,M1} { rd( mult( rd( X, Y ), Z ), T )
% 0.70/1.17 ==> rd( X, ld( rd( Z, T ), Y ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (46) {G9,W15,D5,L1,V4,M1} P(2,39) { rd( X, ld( rd( Z, T ), Y )
% 0.70/1.17 ) ==> rd( mult( rd( X, Y ), Z ), T ) }.
% 0.70/1.17 parent0: (407) {G1,W15,D5,L1,V4,M1} { rd( X, ld( rd( Z, T ), Y ) ) ==> rd
% 0.70/1.17 ( mult( rd( X, Y ), Z ), T ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (409) {G9,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), T ) ==> ld( rd( mult
% 0.70/1.17 ( X, Y ), Z ), mult( X, T ) ) }.
% 0.70/1.17 parent0[0]: (43) {G9,W15,D5,L1,V4,M1} P(39,6) { ld( rd( mult( X, Z ), T ),
% 0.70/1.17 mult( X, Y ) ) ==> ld( rd( Z, T ), Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := T
% 0.70/1.17 Z := Y
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (413) {G2,W15,D6,L1,V4,M1} { ld( rd( X, ld( Y, mult( Z, X ) ) ),
% 0.70/1.17 T ) ==> ld( Y, mult( Z, T ) ) }.
% 0.70/1.17 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.70/1.17 parent1[0; 11]: (409) {G9,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), T ) ==> ld(
% 0.70/1.17 rd( mult( X, Y ), Z ), mult( X, T ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := mult( Z, X )
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := Z
% 0.70/1.17 Y := X
% 0.70/1.17 Z := ld( Y, mult( Z, X ) )
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (47) {G10,W15,D6,L1,V4,M1} P(7,43) { ld( rd( Y, ld( Z, mult( X
% 0.70/1.17 , Y ) ) ), T ) ==> ld( Z, mult( X, T ) ) }.
% 0.70/1.17 parent0: (413) {G2,W15,D6,L1,V4,M1} { ld( rd( X, ld( Y, mult( Z, X ) ) ),
% 0.70/1.17 T ) ==> ld( Y, mult( Z, T ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := Z
% 0.70/1.17 Z := X
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (417) {G9,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), T ) ==> ld( rd( mult
% 0.70/1.17 ( X, Y ), Z ), mult( X, T ) ) }.
% 0.70/1.17 parent0[0]: (43) {G9,W15,D5,L1,V4,M1} P(39,6) { ld( rd( mult( X, Z ), T ),
% 0.70/1.17 mult( X, Y ) ) ==> ld( rd( Z, T ), Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := T
% 0.70/1.17 Z := Y
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (420) {G1,W15,D5,L1,V4,M1} { ld( rd( ld( X, Y ), Z ), T ) ==> ld
% 0.70/1.17 ( rd( Y, Z ), mult( X, T ) ) }.
% 0.70/1.17 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.70/1.17 parent1[0; 10]: (417) {G9,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), T ) ==> ld(
% 0.70/1.17 rd( mult( X, Y ), Z ), mult( X, T ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := X
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := X
% 0.70/1.17 Y := ld( X, Y )
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (422) {G1,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), mult( X, T ) ) ==> ld
% 0.70/1.17 ( rd( ld( X, Y ), Z ), T ) }.
% 0.70/1.17 parent0[0]: (420) {G1,W15,D5,L1,V4,M1} { ld( rd( ld( X, Y ), Z ), T ) ==>
% 0.70/1.17 ld( rd( Y, Z ), mult( X, T ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (48) {G10,W15,D5,L1,V4,M1} P(0,43) { ld( rd( Y, Z ), mult( X,
% 0.70/1.17 T ) ) ==> ld( rd( ld( X, Y ), Z ), T ) }.
% 0.70/1.17 parent0: (422) {G1,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), mult( X, T ) ) ==>
% 0.70/1.17 ld( rd( ld( X, Y ), Z ), T ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (425) {G9,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), T ) ==> ld( rd( mult
% 0.70/1.17 ( X, Y ), Z ), mult( X, T ) ) }.
% 0.70/1.17 parent0[0]: (43) {G9,W15,D5,L1,V4,M1} P(39,6) { ld( rd( mult( X, Z ), T ),
% 0.70/1.17 mult( X, Y ) ) ==> ld( rd( Z, T ), Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := T
% 0.70/1.17 Z := Y
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (428) {G1,W11,D4,L1,V3,M1} { ld( rd( X, X ), Y ) ==> ld( Z, mult
% 0.70/1.17 ( Z, Y ) ) }.
% 0.70/1.17 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.70/1.17 parent1[0; 7]: (425) {G9,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), T ) ==> ld( rd
% 0.70/1.17 ( mult( X, Y ), Z ), mult( X, T ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Z
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := Z
% 0.70/1.17 Y := X
% 0.70/1.17 Z := X
% 0.70/1.17 T := Y
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (429) {G1,W7,D4,L1,V2,M1} { ld( rd( X, X ), Y ) ==> Y }.
% 0.70/1.17 parent0[0]: (1) {G0,W7,D4,L1,V2,M1} I { ld( Y, mult( Y, X ) ) ==> X }.
% 0.70/1.17 parent1[0; 6]: (428) {G1,W11,D4,L1,V3,M1} { ld( rd( X, X ), Y ) ==> ld( Z
% 0.70/1.17 , mult( Z, Y ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := Z
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (51) {G10,W7,D4,L1,V2,M1} P(3,43);d(1) { ld( rd( Y, Y ), Z )
% 0.70/1.17 ==> Z }.
% 0.70/1.17 parent0: (429) {G1,W7,D4,L1,V2,M1} { ld( rd( X, X ), Y ) ==> Y }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := Z
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (431) {G10,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, X ), Y ) }.
% 0.70/1.17 parent0[0]: (51) {G10,W7,D4,L1,V2,M1} P(3,43);d(1) { ld( rd( Y, Y ), Z )
% 0.70/1.17 ==> Z }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Z
% 0.70/1.17 Y := X
% 0.70/1.17 Z := Y
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (433) {G10,W11,D5,L1,V3,M1} { mult( X, Y ) ==> ld( rd( Z, mult( X
% 0.70/1.17 , Z ) ), Y ) }.
% 0.70/1.17 parent0[0]: (43) {G9,W15,D5,L1,V4,M1} P(39,6) { ld( rd( mult( X, Z ), T ),
% 0.70/1.17 mult( X, Y ) ) ==> ld( rd( Z, T ), Y ) }.
% 0.70/1.17 parent1[0; 4]: (431) {G10,W7,D4,L1,V2,M1} { Y ==> ld( rd( X, X ), Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := mult( X, Z )
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := mult( X, Z )
% 0.70/1.17 Y := mult( X, Y )
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (434) {G10,W11,D5,L1,V3,M1} { ld( rd( Z, mult( X, Z ) ), Y ) ==>
% 0.70/1.17 mult( X, Y ) }.
% 0.70/1.17 parent0[0]: (433) {G10,W11,D5,L1,V3,M1} { mult( X, Y ) ==> ld( rd( Z, mult
% 0.70/1.17 ( X, Z ) ), Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (53) {G11,W11,D5,L1,V3,M1} P(51,43) { ld( rd( Y, mult( X, Y )
% 0.70/1.17 ), Z ) ==> mult( X, Z ) }.
% 0.70/1.17 parent0: (434) {G10,W11,D5,L1,V3,M1} { ld( rd( Z, mult( X, Z ) ), Y ) ==>
% 0.70/1.17 mult( X, Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Z
% 0.70/1.17 Z := Y
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (436) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 0.70/1.17 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := X
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (437) {G2,W7,D3,L1,V2,M1} { rd( X, X ) ==> rd( Y, Y ) }.
% 0.70/1.17 parent0[0]: (51) {G10,W7,D4,L1,V2,M1} P(3,43);d(1) { ld( rd( Y, Y ), Z )
% 0.70/1.17 ==> Z }.
% 0.70/1.17 parent1[0; 6]: (436) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Z
% 0.70/1.17 Y := X
% 0.70/1.17 Z := Y
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := rd( X, X )
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (55) {G11,W7,D3,L1,V2,M1} P(51,7) { rd( Y, Y ) = rd( X, X )
% 0.70/1.17 }.
% 0.70/1.17 parent0: (437) {G2,W7,D3,L1,V2,M1} { rd( X, X ) ==> rd( Y, Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := X
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (438) {G9,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), T ) ==> ld( rd( mult
% 0.70/1.17 ( X, Y ), Z ), mult( X, T ) ) }.
% 0.70/1.17 parent0[0]: (43) {G9,W15,D5,L1,V4,M1} P(39,6) { ld( rd( mult( X, Z ), T ),
% 0.70/1.17 mult( X, Y ) ) ==> ld( rd( Z, T ), Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := T
% 0.70/1.17 Z := Y
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (442) {G10,W15,D5,L1,V4,M1} { ld( rd( X, mult( Y, X ) ), Z ) ==>
% 0.70/1.17 ld( rd( T, T ), mult( Y, Z ) ) }.
% 0.70/1.17 parent0[0]: (55) {G11,W7,D3,L1,V2,M1} P(51,7) { rd( Y, Y ) = rd( X, X ) }.
% 0.70/1.17 parent1[0; 9]: (438) {G9,W15,D5,L1,V4,M1} { ld( rd( Y, Z ), T ) ==> ld( rd
% 0.70/1.17 ( mult( X, Y ), Z ), mult( X, T ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := T
% 0.70/1.17 Y := mult( Y, X )
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := X
% 0.70/1.17 Z := mult( Y, X )
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (443) {G11,W15,D5,L1,V4,M1} { ld( rd( X, mult( Y, X ) ), Z ) ==>
% 0.70/1.17 ld( rd( ld( Y, T ), T ), Z ) }.
% 0.70/1.17 parent0[0]: (48) {G10,W15,D5,L1,V4,M1} P(0,43) { ld( rd( Y, Z ), mult( X, T
% 0.70/1.17 ) ) ==> ld( rd( ld( X, Y ), Z ), T ) }.
% 0.70/1.17 parent1[0; 8]: (442) {G10,W15,D5,L1,V4,M1} { ld( rd( X, mult( Y, X ) ), Z
% 0.70/1.17 ) ==> ld( rd( T, T ), mult( Y, Z ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := T
% 0.70/1.17 Z := T
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (444) {G12,W11,D5,L1,V3,M1} { mult( Y, Z ) ==> ld( rd( ld( Y, T )
% 0.70/1.17 , T ), Z ) }.
% 0.70/1.17 parent0[0]: (53) {G11,W11,D5,L1,V3,M1} P(51,43) { ld( rd( Y, mult( X, Y ) )
% 0.70/1.17 , Z ) ==> mult( X, Z ) }.
% 0.70/1.17 parent1[0; 1]: (443) {G11,W15,D5,L1,V4,M1} { ld( rd( X, mult( Y, X ) ), Z
% 0.70/1.17 ) ==> ld( rd( ld( Y, T ), T ), Z ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := X
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (445) {G12,W11,D5,L1,V3,M1} { ld( rd( ld( X, Z ), Z ), Y ) ==>
% 0.70/1.17 mult( X, Y ) }.
% 0.70/1.17 parent0[0]: (444) {G12,W11,D5,L1,V3,M1} { mult( Y, Z ) ==> ld( rd( ld( Y,
% 0.70/1.17 T ), T ), Z ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := T
% 0.70/1.17 Y := X
% 0.70/1.17 Z := Y
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (57) {G12,W11,D5,L1,V3,M1} P(55,43);d(48);d(53) { ld( rd( ld(
% 0.70/1.17 X, Z ), Z ), T ) ==> mult( X, T ) }.
% 0.70/1.17 parent0: (445) {G12,W11,D5,L1,V3,M1} { ld( rd( ld( X, Z ), Z ), Y ) ==>
% 0.70/1.17 mult( X, Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := T
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (447) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y ) ) = rd
% 0.70/1.17 ( X, ld( Y, ld( Z, X ) ) ) }.
% 0.70/1.17 parent0[0]: (24) {G5,W15,D5,L1,V3,M1} P(23,7) { rd( Z, ld( Y, ld( X, Z ) )
% 0.70/1.17 ) = mult( rd( X, Y ), mult( Y, Y ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Z
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := X
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (451) {G6,W19,D6,L1,V4,M1} { mult( rd( rd( ld( X, Y ), Y ), Z ),
% 0.70/1.17 mult( Z, Z ) ) = rd( T, ld( Z, mult( X, T ) ) ) }.
% 0.70/1.17 parent0[0]: (57) {G12,W11,D5,L1,V3,M1} P(55,43);d(48);d(53) { ld( rd( ld( X
% 0.70/1.17 , Z ), Z ), T ) ==> mult( X, T ) }.
% 0.70/1.17 parent1[0; 16]: (447) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y
% 0.70/1.17 ) ) = rd( X, ld( Y, ld( Z, X ) ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := U
% 0.70/1.17 Z := Y
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := T
% 0.70/1.17 Y := Z
% 0.70/1.17 Z := rd( ld( X, Y ), Y )
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (452) {G7,W15,D5,L1,V4,M1} { rd( ld( X, Y ), ld( Z, Y ) ) = rd( T
% 0.70/1.17 , ld( Z, mult( X, T ) ) ) }.
% 0.70/1.17 parent0[0]: (28) {G6,W15,D5,L1,V3,M1} P(6,24) { mult( rd( rd( X, Y ), Z ),
% 0.70/1.17 mult( Z, Z ) ) ==> rd( X, ld( Z, Y ) ) }.
% 0.70/1.17 parent1[0; 1]: (451) {G6,W19,D6,L1,V4,M1} { mult( rd( rd( ld( X, Y ), Y )
% 0.70/1.17 , Z ), mult( Z, Z ) ) = rd( T, ld( Z, mult( X, T ) ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := ld( X, Y )
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (453) {G7,W15,D5,L1,V4,M1} { rd( T, ld( Z, mult( X, T ) ) ) = rd(
% 0.70/1.17 ld( X, Y ), ld( Z, Y ) ) }.
% 0.70/1.17 parent0[0]: (452) {G7,W15,D5,L1,V4,M1} { rd( ld( X, Y ), ld( Z, Y ) ) = rd
% 0.70/1.17 ( T, ld( Z, mult( X, T ) ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (90) {G13,W15,D5,L1,V4,M1} P(57,24);d(28) { rd( Z, ld( T, mult
% 0.70/1.17 ( X, Z ) ) ) = rd( ld( X, Y ), ld( T, Y ) ) }.
% 0.70/1.17 parent0: (453) {G7,W15,D5,L1,V4,M1} { rd( T, ld( Z, mult( X, T ) ) ) = rd
% 0.70/1.17 ( ld( X, Y ), ld( Z, Y ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := T
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (455) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 0.70/1.17 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := X
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (456) {G2,W11,D4,L1,V3,M1} { rd( ld( X, Y ), Y ) ==> rd( Z, mult
% 0.70/1.17 ( X, Z ) ) }.
% 0.70/1.17 parent0[0]: (57) {G12,W11,D5,L1,V3,M1} P(55,43);d(48);d(53) { ld( rd( ld( X
% 0.70/1.17 , Z ), Z ), T ) ==> mult( X, T ) }.
% 0.70/1.17 parent1[0; 8]: (455) {G1,W7,D4,L1,V2,M1} { Y ==> rd( X, ld( Y, X ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := T
% 0.70/1.17 Z := Y
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := Z
% 0.70/1.17 Y := rd( ld( X, Y ), Y )
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (457) {G2,W11,D4,L1,V3,M1} { rd( Z, mult( X, Z ) ) ==> rd( ld( X,
% 0.70/1.17 Y ), Y ) }.
% 0.70/1.17 parent0[0]: (456) {G2,W11,D4,L1,V3,M1} { rd( ld( X, Y ), Y ) ==> rd( Z,
% 0.70/1.17 mult( X, Z ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (92) {G13,W11,D4,L1,V3,M1} P(57,7) { rd( Z, mult( X, Z ) ) =
% 0.70/1.17 rd( ld( X, Y ), Y ) }.
% 0.70/1.17 parent0: (457) {G2,W11,D4,L1,V3,M1} { rd( Z, mult( X, Z ) ) ==> rd( ld( X
% 0.70/1.17 , Y ), Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (459) {G12,W11,D5,L1,V3,M1} { mult( X, Z ) ==> ld( rd( ld( X, Y )
% 0.70/1.17 , Y ), Z ) }.
% 0.70/1.17 parent0[0]: (57) {G12,W11,D5,L1,V3,M1} P(55,43);d(48);d(53) { ld( rd( ld( X
% 0.70/1.17 , Z ), Z ), T ) ==> mult( X, T ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := T
% 0.70/1.17 Z := Y
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (463) {G2,W11,D4,L1,V3,M1} { mult( rd( X, Y ), Z ) ==> ld( rd( Y
% 0.70/1.17 , X ), Z ) }.
% 0.70/1.17 parent0[0]: (6) {G1,W7,D4,L1,V2,M1} P(2,1) { ld( rd( X, Y ), X ) ==> Y }.
% 0.70/1.17 parent1[0; 8]: (459) {G12,W11,D5,L1,V3,M1} { mult( X, Z ) ==> ld( rd( ld(
% 0.70/1.17 X, Y ), Y ), Z ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := rd( X, Y )
% 0.70/1.17 Y := X
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.70/1.17 ld( rd( Y, X ), Z ) }.
% 0.70/1.17 parent0: (463) {G2,W11,D4,L1,V3,M1} { mult( rd( X, Y ), Z ) ==> ld( rd( Y
% 0.70/1.17 , X ), Z ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (467) {G13,W11,D4,L1,V3,M1} { rd( ld( Y, Z ), Z ) = rd( X, mult( Y
% 0.70/1.17 , X ) ) }.
% 0.70/1.17 parent0[0]: (92) {G13,W11,D4,L1,V3,M1} P(57,7) { rd( Z, mult( X, Z ) ) = rd
% 0.70/1.17 ( ld( X, Y ), Y ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := Z
% 0.70/1.17 Z := X
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (472) {G1,W11,D5,L1,V3,M1} { rd( ld( rd( X, Y ), Z ), Z ) = rd( Y
% 0.70/1.17 , X ) }.
% 0.70/1.17 parent0[0]: (2) {G0,W7,D4,L1,V2,M1} I { mult( rd( Y, X ), X ) ==> Y }.
% 0.70/1.17 parent1[0; 10]: (467) {G13,W11,D4,L1,V3,M1} { rd( ld( Y, Z ), Z ) = rd( X
% 0.70/1.17 , mult( Y, X ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := X
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := Y
% 0.70/1.17 Y := rd( X, Y )
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 subsumption: (103) {G14,W11,D5,L1,V3,M1} P(2,92) { rd( ld( rd( X, Y ), Z )
% 0.70/1.17 , Z ) ==> rd( Y, X ) }.
% 0.70/1.17 parent0: (472) {G1,W11,D5,L1,V3,M1} { rd( ld( rd( X, Y ), Z ), Z ) = rd( Y
% 0.70/1.17 , X ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 end
% 0.70/1.17 permutation0:
% 0.70/1.17 0 ==> 0
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (479) {G8,W19,D5,L1,V5,M1} { rd( mult( rd( X, Y ), Z ), ld( T, Z
% 0.70/1.17 ) ) = rd( ld( rd( Y, X ), U ), ld( T, U ) ) }.
% 0.70/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.70/1.17 ld( rd( Y, X ), Z ) }.
% 0.70/1.17 parent1[0; 11]: (32) {G7,W15,D4,L1,V4,M1} P(30,30) { rd( mult( X, T ), ld(
% 0.70/1.17 Y, T ) ) = rd( mult( X, Z ), ld( Y, Z ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := U
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := rd( X, Y )
% 0.70/1.17 Y := T
% 0.70/1.17 Z := U
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 paramod: (481) {G9,W15,D5,L1,V4,M1} { rd( X, ld( T, Y ) ) = rd( ld( rd( Y
% 0.70/1.17 , X ), U ), ld( T, U ) ) }.
% 0.70/1.17 parent0[0]: (41) {G8,W15,D5,L1,V4,M1} P(2,32) { rd( mult( rd( X, Y ), T ),
% 0.70/1.17 ld( Z, T ) ) ==> rd( X, ld( Z, Y ) ) }.
% 0.70/1.17 parent1[0; 1]: (479) {G8,W19,D5,L1,V5,M1} { rd( mult( rd( X, Y ), Z ), ld
% 0.70/1.17 ( T, Z ) ) = rd( ld( rd( Y, X ), U ), ld( T, U ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := T
% 0.70/1.17 T := Z
% 0.70/1.17 end
% 0.70/1.17 substitution1:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Y
% 0.70/1.17 Z := Z
% 0.70/1.17 T := T
% 0.70/1.17 U := U
% 0.70/1.17 end
% 0.70/1.17
% 0.70/1.17 eqswap: (482) {G9,W15,D5,L1,V4,M1} { rd( ld( rd( Z, X ), T ), ld( Y, T ) )
% 0.70/1.17 = rd( X, ld( Y, Z ) ) }.
% 0.70/1.17 parent0[0]: (481) {G9,W15,D5,L1,V4,M1} { rd( X, ld( T, Y ) ) = rd( ld( rd
% 0.70/1.17 ( Y, X ), U ), ld( T, U ) ) }.
% 0.70/1.17 substitution0:
% 0.70/1.17 X := X
% 0.70/1.17 Y := Z
% 0.70/1.17 Z := U
% 0.70/1.17 T := Y
% 0.75/1.17 U := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (116) {G14,W15,D5,L1,V4,M1} P(93,32);d(41) { rd( ld( rd( Y, X
% 0.75/1.17 ), Z ), ld( T, Z ) ) ==> rd( X, ld( T, Y ) ) }.
% 0.75/1.17 parent0: (482) {G9,W15,D5,L1,V4,M1} { rd( ld( rd( Z, X ), T ), ld( Y, T )
% 0.75/1.17 ) = rd( X, ld( Y, Z ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := T
% 0.75/1.17 Z := Y
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (484) {G6,W15,D4,L1,V3,M1} { mult( rd( X, Z ), mult( Z, Z ) ) = rd
% 0.75/1.17 ( mult( X, Y ), ld( Z, Y ) ) }.
% 0.75/1.17 parent0[0]: (30) {G6,W15,D4,L1,V3,M1} P(1,24) { rd( mult( X, Y ), ld( Z, Y
% 0.75/1.17 ) ) = mult( rd( X, Z ), mult( Z, Z ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (493) {G7,W19,D5,L1,V4,M1} { mult( rd( rd( X, Y ), Z ), mult( Z,
% 0.75/1.17 Z ) ) = rd( ld( rd( Y, X ), T ), ld( Z, T ) ) }.
% 0.75/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.75/1.17 ld( rd( Y, X ), Z ) }.
% 0.75/1.17 parent1[0; 11]: (484) {G6,W15,D4,L1,V3,M1} { mult( rd( X, Z ), mult( Z, Z
% 0.75/1.17 ) ) = rd( mult( X, Y ), ld( Z, Y ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := T
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := rd( X, Y )
% 0.75/1.17 Y := T
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (496) {G8,W15,D5,L1,V3,M1} { mult( rd( rd( X, Y ), Z ), mult( Z,
% 0.75/1.17 Z ) ) = rd( X, ld( Z, Y ) ) }.
% 0.75/1.17 parent0[0]: (116) {G14,W15,D5,L1,V4,M1} P(93,32);d(41) { rd( ld( rd( Y, X )
% 0.75/1.17 , Z ), ld( T, Z ) ) ==> rd( X, ld( T, Y ) ) }.
% 0.75/1.17 parent1[0; 10]: (493) {G7,W19,D5,L1,V4,M1} { mult( rd( rd( X, Y ), Z ),
% 0.75/1.17 mult( Z, Z ) ) = rd( ld( rd( Y, X ), T ), ld( Z, T ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := T
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (497) {G9,W15,D5,L1,V3,M1} { ld( rd( Z, rd( X, Y ) ), mult( Z, Z
% 0.75/1.17 ) ) = rd( X, ld( Z, Y ) ) }.
% 0.75/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.75/1.17 ld( rd( Y, X ), Z ) }.
% 0.75/1.17 parent1[0; 1]: (496) {G8,W15,D5,L1,V3,M1} { mult( rd( rd( X, Y ), Z ),
% 0.75/1.17 mult( Z, Z ) ) = rd( X, ld( Z, Y ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := rd( X, Y )
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := mult( Z, Z )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (498) {G10,W15,D5,L1,V3,M1} { ld( rd( ld( X, X ), rd( Y, Z ) ), X
% 0.75/1.17 ) = rd( Y, ld( X, Z ) ) }.
% 0.75/1.17 parent0[0]: (48) {G10,W15,D5,L1,V4,M1} P(0,43) { ld( rd( Y, Z ), mult( X, T
% 0.75/1.17 ) ) ==> ld( rd( ld( X, Y ), Z ), T ) }.
% 0.75/1.17 parent1[0; 1]: (497) {G9,W15,D5,L1,V3,M1} { ld( rd( Z, rd( X, Y ) ), mult
% 0.75/1.17 ( Z, Z ) ) = rd( X, ld( Z, Y ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := X
% 0.75/1.17 Z := rd( Y, Z )
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (117) {G15,W15,D5,L1,V3,M1} P(93,30);d(116);d(93);d(48) { ld(
% 0.75/1.17 rd( ld( T, T ), rd( X, Y ) ), T ) ==> rd( X, ld( T, Y ) ) }.
% 0.75/1.17 parent0: (498) {G10,W15,D5,L1,V3,M1} { ld( rd( ld( X, X ), rd( Y, Z ) ), X
% 0.75/1.17 ) = rd( Y, ld( X, Z ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Y
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (501) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y ) ) = rd
% 0.75/1.17 ( X, ld( Y, ld( Z, X ) ) ) }.
% 0.75/1.17 parent0[0]: (24) {G5,W15,D5,L1,V3,M1} P(23,7) { rd( Z, ld( Y, ld( X, Z ) )
% 0.75/1.17 ) = mult( rd( X, Y ), mult( Y, Y ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (511) {G6,W19,D6,L1,V4,M1} { mult( rd( rd( X, mult( Y, X ) ), Z )
% 0.75/1.17 , mult( Z, Z ) ) = rd( T, ld( Z, mult( Y, T ) ) ) }.
% 0.75/1.17 parent0[0]: (53) {G11,W11,D5,L1,V3,M1} P(51,43) { ld( rd( Y, mult( X, Y ) )
% 0.75/1.17 , Z ) ==> mult( X, Z ) }.
% 0.75/1.17 parent1[0; 16]: (501) {G5,W15,D5,L1,V3,M1} { mult( rd( Z, Y ), mult( Y, Y
% 0.75/1.17 ) ) = rd( X, ld( Y, ld( Z, X ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := X
% 0.75/1.17 Z := T
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := T
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := rd( X, mult( Y, X ) )
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (512) {G7,W19,D6,L1,V4,M1} { ld( rd( Z, rd( X, mult( Y, X ) ) ),
% 0.75/1.17 mult( Z, Z ) ) = rd( T, ld( Z, mult( Y, T ) ) ) }.
% 0.75/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.75/1.17 ld( rd( Y, X ), Z ) }.
% 0.75/1.17 parent1[0; 1]: (511) {G6,W19,D6,L1,V4,M1} { mult( rd( rd( X, mult( Y, X )
% 0.75/1.17 ), Z ), mult( Z, Z ) ) = rd( T, ld( Z, mult( Y, T ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := rd( X, mult( Y, X ) )
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := mult( Z, Z )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (513) {G8,W19,D6,L1,V4,M1} { ld( rd( ld( X, X ), rd( Y, mult( Z,
% 0.75/1.17 Y ) ) ), X ) = rd( T, ld( X, mult( Z, T ) ) ) }.
% 0.75/1.17 parent0[0]: (48) {G10,W15,D5,L1,V4,M1} P(0,43) { ld( rd( Y, Z ), mult( X, T
% 0.75/1.17 ) ) ==> ld( rd( ld( X, Y ), Z ), T ) }.
% 0.75/1.17 parent1[0; 1]: (512) {G7,W19,D6,L1,V4,M1} { ld( rd( Z, rd( X, mult( Y, X )
% 0.75/1.17 ) ), mult( Z, Z ) ) = rd( T, ld( Z, mult( Y, T ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := X
% 0.75/1.17 Z := rd( Y, mult( Z, Y ) )
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := X
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (514) {G9,W15,D5,L1,V4,M1} { rd( Y, ld( X, mult( Z, Y ) ) ) = rd
% 0.75/1.17 ( T, ld( X, mult( Z, T ) ) ) }.
% 0.75/1.17 parent0[0]: (117) {G15,W15,D5,L1,V3,M1} P(93,30);d(116);d(93);d(48) { ld(
% 0.75/1.17 rd( ld( T, T ), rd( X, Y ) ), T ) ==> rd( X, ld( T, Y ) ) }.
% 0.75/1.17 parent1[0; 1]: (513) {G8,W19,D6,L1,V4,M1} { ld( rd( ld( X, X ), rd( Y,
% 0.75/1.17 mult( Z, Y ) ) ), X ) = rd( T, ld( X, mult( Z, T ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := mult( Z, Y )
% 0.75/1.17 Z := U
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (127) {G16,W15,D5,L1,V4,M1} P(53,24);d(93);d(48);d(117) { rd(
% 0.75/1.17 Z, ld( T, mult( Y, Z ) ) ) = rd( X, ld( T, mult( Y, X ) ) ) }.
% 0.75/1.17 parent0: (514) {G9,W15,D5,L1,V4,M1} { rd( Y, ld( X, mult( Z, Y ) ) ) = rd
% 0.75/1.17 ( T, ld( X, mult( Z, T ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := Y
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (515) {G14,W11,D5,L1,V3,M1} { rd( Y, X ) ==> rd( ld( rd( X, Y ), Z
% 0.75/1.17 ), Z ) }.
% 0.75/1.17 parent0[0]: (103) {G14,W11,D5,L1,V3,M1} P(2,92) { rd( ld( rd( X, Y ), Z ),
% 0.75/1.17 Z ) ==> rd( Y, X ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (518) {G15,W19,D7,L1,V5,M1} { rd( ld( X, mult( Y, Z ) ), Z ) ==>
% 0.75/1.17 rd( ld( rd( U, ld( X, mult( Y, U ) ) ), T ), T ) }.
% 0.75/1.17 parent0[0]: (127) {G16,W15,D5,L1,V4,M1} P(53,24);d(93);d(48);d(117) { rd( Z
% 0.75/1.17 , ld( T, mult( Y, Z ) ) ) = rd( X, ld( T, mult( Y, X ) ) ) }.
% 0.75/1.17 parent1[0; 10]: (515) {G14,W11,D5,L1,V3,M1} { rd( Y, X ) ==> rd( ld( rd( X
% 0.75/1.17 , Y ), Z ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := U
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := ld( X, mult( Y, Z ) )
% 0.75/1.17 Z := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (519) {G15,W15,D5,L1,V4,M1} { rd( ld( X, mult( Y, Z ) ), Z ) ==>
% 0.75/1.17 rd( ld( X, mult( Y, T ) ), T ) }.
% 0.75/1.17 parent0[0]: (103) {G14,W11,D5,L1,V3,M1} P(2,92) { rd( ld( rd( X, Y ), Z ),
% 0.75/1.17 Z ) ==> rd( Y, X ) }.
% 0.75/1.17 parent1[0; 8]: (518) {G15,W19,D7,L1,V5,M1} { rd( ld( X, mult( Y, Z ) ), Z
% 0.75/1.17 ) ==> rd( ld( rd( U, ld( X, mult( Y, U ) ) ), T ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := ld( X, mult( Y, T ) )
% 0.75/1.17 Z := U
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := U
% 0.75/1.17 U := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (159) {G17,W15,D5,L1,V4,M1} P(127,103);d(103) { rd( ld( Y,
% 0.75/1.17 mult( Z, T ) ), T ) = rd( ld( Y, mult( Z, X ) ), X ) }.
% 0.75/1.17 parent0: (519) {G15,W15,D5,L1,V4,M1} { rd( ld( X, mult( Y, Z ) ), Z ) ==>
% 0.75/1.17 rd( ld( X, mult( Y, T ) ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := T
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (521) {G1,W15,D5,L1,V4,M1} { rd( ld( X, Z ), ld( Y, Z ) ) = rd(
% 0.75/1.17 ld( X, mult( Y, T ) ), T ) }.
% 0.75/1.17 parent0[0]: (0) {G0,W7,D4,L1,V2,M1} I { mult( Y, ld( Y, X ) ) ==> X }.
% 0.75/1.17 parent1[0; 4]: (159) {G17,W15,D5,L1,V4,M1} P(127,103);d(103) { rd( ld( Y,
% 0.75/1.17 mult( Z, T ) ), T ) = rd( ld( Y, mult( Z, X ) ), X ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := T
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Y
% 0.75/1.17 T := ld( Y, Z )
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (161) {G18,W15,D5,L1,V4,M1} P(0,159) { rd( ld( Z, Y ), ld( X,
% 0.75/1.17 Y ) ) = rd( ld( Z, mult( X, T ) ), T ) }.
% 0.75/1.17 parent0: (521) {G1,W15,D5,L1,V4,M1} { rd( ld( X, Z ), ld( Y, Z ) ) = rd(
% 0.75/1.17 ld( X, mult( Y, T ) ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Y
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (523) {G18,W15,D5,L1,V4,M1} { rd( ld( X, mult( Z, T ) ), T ) = rd
% 0.75/1.17 ( ld( X, Y ), ld( Z, Y ) ) }.
% 0.75/1.17 parent0[0]: (161) {G18,W15,D5,L1,V4,M1} P(0,159) { rd( ld( Z, Y ), ld( X, Y
% 0.75/1.17 ) ) = rd( ld( Z, mult( X, T ) ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := X
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (524) {G13,W11,D4,L1,V3,M1} { ld( rd( Y, X ), Z ) ==> mult( rd( X
% 0.75/1.17 , Y ), Z ) }.
% 0.75/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.75/1.17 ld( rd( Y, X ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (528) {G14,W19,D6,L1,V5,M1} { ld( rd( X, ld( Y, mult( Z, X ) ) )
% 0.75/1.17 , T ) ==> mult( rd( ld( Y, U ), ld( Z, U ) ), T ) }.
% 0.75/1.17 parent0[0]: (523) {G18,W15,D5,L1,V4,M1} { rd( ld( X, mult( Z, T ) ), T ) =
% 0.75/1.17 rd( ld( X, Y ), ld( Z, Y ) ) }.
% 0.75/1.17 parent1[0; 11]: (524) {G13,W11,D4,L1,V3,M1} { ld( rd( Y, X ), Z ) ==> mult
% 0.75/1.17 ( rd( X, Y ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := U
% 0.75/1.17 Z := Z
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := ld( Y, mult( Z, X ) )
% 0.75/1.17 Y := X
% 0.75/1.17 Z := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (529) {G14,W19,D6,L1,V5,M1} { ld( rd( X, ld( Y, mult( Z, X ) ) )
% 0.75/1.17 , T ) ==> ld( rd( ld( Z, U ), ld( Y, U ) ), T ) }.
% 0.75/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.75/1.17 ld( rd( Y, X ), Z ) }.
% 0.75/1.17 parent1[0; 10]: (528) {G14,W19,D6,L1,V5,M1} { ld( rd( X, ld( Y, mult( Z, X
% 0.75/1.17 ) ) ), T ) ==> mult( rd( ld( Y, U ), ld( Z, U ) ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := ld( Y, U )
% 0.75/1.17 Y := ld( Z, U )
% 0.75/1.17 Z := T
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 U := U
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (530) {G11,W15,D5,L1,V4,M1} { ld( Y, mult( Z, T ) ) ==> ld( rd(
% 0.75/1.17 ld( Z, U ), ld( Y, U ) ), T ) }.
% 0.75/1.17 parent0[0]: (47) {G10,W15,D6,L1,V4,M1} P(7,43) { ld( rd( Y, ld( Z, mult( X
% 0.75/1.17 , Y ) ) ), T ) ==> ld( Z, mult( X, T ) ) }.
% 0.75/1.17 parent1[0; 1]: (529) {G14,W19,D6,L1,V5,M1} { ld( rd( X, ld( Y, mult( Z, X
% 0.75/1.17 ) ) ), T ) ==> ld( rd( ld( Z, U ), ld( Y, U ) ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Y
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 U := U
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (531) {G11,W15,D5,L1,V4,M1} { ld( rd( ld( Y, T ), ld( X, T ) ), Z
% 0.75/1.17 ) ==> ld( X, mult( Y, Z ) ) }.
% 0.75/1.17 parent0[0]: (530) {G11,W15,D5,L1,V4,M1} { ld( Y, mult( Z, T ) ) ==> ld( rd
% 0.75/1.17 ( ld( Z, U ), ld( Y, U ) ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := U
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Y
% 0.75/1.17 T := Z
% 0.75/1.17 U := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (164) {G19,W15,D5,L1,V4,M1} P(161,93);d(93);d(47) { ld( rd( ld
% 0.75/1.17 ( Z, Y ), ld( X, Y ) ), U ) ==> ld( X, mult( Z, U ) ) }.
% 0.75/1.17 parent0: (531) {G11,W15,D5,L1,V4,M1} { ld( rd( ld( Y, T ), ld( X, T ) ), Z
% 0.75/1.17 ) ==> ld( X, mult( Y, Z ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := U
% 0.75/1.17 T := Y
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (534) {G10,W15,D5,L1,V4,M1} { rd( X, ld( rd( Y, Z ), T ) ) ==> rd
% 0.75/1.17 ( ld( rd( T, X ), Y ), Z ) }.
% 0.75/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.75/1.17 ld( rd( Y, X ), Z ) }.
% 0.75/1.17 parent1[0; 9]: (46) {G9,W15,D5,L1,V4,M1} P(2,39) { rd( X, ld( rd( Z, T ), Y
% 0.75/1.17 ) ) ==> rd( mult( rd( X, Y ), Z ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := T
% 0.75/1.17 Z := Y
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := T
% 0.75/1.17 Z := Y
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (173) {G14,W15,D5,L1,V4,M1} S(46);d(93) { rd( X, ld( rd( Z, T
% 0.75/1.17 ), Y ) ) ==> rd( ld( rd( Y, X ), Z ), T ) }.
% 0.75/1.17 parent0: (534) {G10,W15,D5,L1,V4,M1} { rd( X, ld( rd( Y, Z ), T ) ) ==> rd
% 0.75/1.17 ( ld( rd( T, X ), Y ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := T
% 0.75/1.17 T := Y
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (537) {G6,W15,D6,L1,V3,M1} { mult( Y, Y ) ==> ld( rd( X, Y ), rd(
% 0.75/1.17 Z, ld( Y, ld( X, Z ) ) ) ) }.
% 0.75/1.17 parent0[0]: (29) {G6,W15,D6,L1,V3,M1} P(24,1) { ld( rd( X, Y ), rd( Z, ld(
% 0.75/1.17 Y, ld( X, Z ) ) ) ) ==> mult( Y, Y ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (542) {G7,W15,D5,L1,V3,M1} { mult( X, X ) ==> ld( rd( rd( Y, Y )
% 0.75/1.17 , X ), rd( Z, ld( X, Z ) ) ) }.
% 0.75/1.17 parent0[0]: (51) {G10,W7,D4,L1,V2,M1} P(3,43);d(1) { ld( rd( Y, Y ), Z )
% 0.75/1.17 ==> Z }.
% 0.75/1.17 parent1[0; 14]: (537) {G6,W15,D6,L1,V3,M1} { mult( Y, Y ) ==> ld( rd( X, Y
% 0.75/1.17 ), rd( Z, ld( Y, ld( X, Z ) ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := rd( Y, Y )
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (543) {G2,W11,D5,L1,V2,M1} { mult( X, X ) ==> ld( rd( rd( Y, Y )
% 0.75/1.17 , X ), X ) }.
% 0.75/1.17 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.75/1.17 parent1[0; 10]: (542) {G7,W15,D5,L1,V3,M1} { mult( X, X ) ==> ld( rd( rd(
% 0.75/1.17 Y, Y ), X ), rd( Z, ld( X, Z ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (544) {G2,W11,D5,L1,V2,M1} { ld( rd( rd( Y, Y ), X ), X ) ==> mult
% 0.75/1.17 ( X, X ) }.
% 0.75/1.17 parent0[0]: (543) {G2,W11,D5,L1,V2,M1} { mult( X, X ) ==> ld( rd( rd( Y, Y
% 0.75/1.17 ), X ), X ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (177) {G11,W11,D5,L1,V2,M1} P(51,29);d(7) { ld( rd( rd( X, X )
% 0.75/1.17 , Z ), Z ) ==> mult( Z, Z ) }.
% 0.75/1.17 parent0: (544) {G2,W11,D5,L1,V2,M1} { ld( rd( rd( Y, Y ), X ), X ) ==>
% 0.75/1.17 mult( X, X ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := X
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (546) {G14,W11,D5,L1,V3,M1} { rd( Y, X ) ==> rd( ld( rd( X, Y ), Z
% 0.75/1.17 ), Z ) }.
% 0.75/1.17 parent0[0]: (103) {G14,W11,D5,L1,V3,M1} P(2,92) { rd( ld( rd( X, Y ), Z ),
% 0.75/1.17 Z ) ==> rd( Y, X ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (548) {G12,W11,D4,L1,V2,M1} { rd( X, rd( Y, Y ) ) ==> rd( mult( X
% 0.75/1.17 , X ), X ) }.
% 0.75/1.17 parent0[0]: (177) {G11,W11,D5,L1,V2,M1} P(51,29);d(7) { ld( rd( rd( X, X )
% 0.75/1.17 , Z ), Z ) ==> mult( Z, Z ) }.
% 0.75/1.17 parent1[0; 7]: (546) {G14,W11,D5,L1,V3,M1} { rd( Y, X ) ==> rd( ld( rd( X
% 0.75/1.17 , Y ), Z ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := rd( Y, Y )
% 0.75/1.17 Y := X
% 0.75/1.17 Z := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (549) {G1,W7,D4,L1,V2,M1} { rd( X, rd( Y, Y ) ) ==> X }.
% 0.75/1.17 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.75/1.17 parent1[0; 6]: (548) {G12,W11,D4,L1,V2,M1} { rd( X, rd( Y, Y ) ) ==> rd(
% 0.75/1.17 mult( X, X ), X ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent0: (549) {G1,W7,D4,L1,V2,M1} { rd( X, rd( Y, Y ) ) ==> X }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := X
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (552) {G6,W15,D6,L1,V3,M1} { mult( Y, Y ) ==> ld( rd( X, Y ), rd(
% 0.75/1.17 Z, ld( Y, ld( X, Z ) ) ) ) }.
% 0.75/1.17 parent0[0]: (29) {G6,W15,D6,L1,V3,M1} P(24,1) { ld( rd( X, Y ), rd( Z, ld(
% 0.75/1.17 Y, ld( X, Z ) ) ) ) ==> mult( Y, Y ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (558) {G7,W19,D6,L1,V3,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 0.75/1.17 ld( Y, rd( Z, ld( rd( X, X ), ld( Y, Z ) ) ) ) }.
% 0.75/1.17 parent0[0]: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent1[0; 9]: (552) {G6,W15,D6,L1,V3,M1} { mult( Y, Y ) ==> ld( rd( X, Y
% 0.75/1.17 ), rd( Z, ld( Y, ld( X, Z ) ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := rd( X, X )
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (559) {G8,W19,D7,L1,V3,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 0.75/1.17 ld( Y, rd( ld( rd( ld( Y, Z ), Z ), X ), X ) ) }.
% 0.75/1.17 parent0[0]: (173) {G14,W15,D5,L1,V4,M1} S(46);d(93) { rd( X, ld( rd( Z, T )
% 0.75/1.17 , Y ) ) ==> rd( ld( rd( Y, X ), Z ), T ) }.
% 0.75/1.17 parent1[0; 10]: (558) {G7,W19,D6,L1,V3,M1} { mult( rd( X, X ), rd( X, X )
% 0.75/1.17 ) ==> ld( Y, rd( Z, ld( rd( X, X ), ld( Y, Z ) ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := ld( Y, Z )
% 0.75/1.17 Z := X
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (560) {G9,W15,D5,L1,V3,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 0.75/1.17 ld( Y, rd( Z, ld( Y, Z ) ) ) }.
% 0.75/1.17 parent0[0]: (103) {G14,W11,D5,L1,V3,M1} P(2,92) { rd( ld( rd( X, Y ), Z ),
% 0.75/1.17 Z ) ==> rd( Y, X ) }.
% 0.75/1.17 parent1[0; 10]: (559) {G8,W19,D7,L1,V3,M1} { mult( rd( X, X ), rd( X, X )
% 0.75/1.17 ) ==> ld( Y, rd( ld( rd( ld( Y, Z ), Z ), X ), X ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := ld( Y, Z )
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (561) {G2,W11,D4,L1,V2,M1} { mult( rd( X, X ), rd( X, X ) ) ==>
% 0.75/1.17 ld( Y, Y ) }.
% 0.75/1.17 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.75/1.17 parent1[0; 10]: (560) {G9,W15,D5,L1,V3,M1} { mult( rd( X, X ), rd( X, X )
% 0.75/1.17 ) ==> ld( Y, rd( Z, ld( Y, Z ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (562) {G3,W11,D4,L1,V2,M1} { ld( rd( X, X ), rd( X, X ) ) ==> ld
% 0.75/1.17 ( Y, Y ) }.
% 0.75/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.75/1.17 ld( rd( Y, X ), Z ) }.
% 0.75/1.17 parent1[0; 1]: (561) {G2,W11,D4,L1,V2,M1} { mult( rd( X, X ), rd( X, X ) )
% 0.75/1.17 ==> ld( Y, Y ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := X
% 0.75/1.17 Z := rd( X, X )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (563) {G4,W7,D3,L1,V2,M1} { rd( X, X ) ==> ld( Y, Y ) }.
% 0.75/1.17 parent0[0]: (51) {G10,W7,D4,L1,V2,M1} P(3,43);d(1) { ld( rd( Y, Y ), Z )
% 0.75/1.17 ==> Z }.
% 0.75/1.17 parent1[0; 1]: (562) {G3,W11,D4,L1,V2,M1} { ld( rd( X, X ), rd( X, X ) )
% 0.75/1.17 ==> ld( Y, Y ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := X
% 0.75/1.17 Z := rd( X, X )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (564) {G4,W7,D3,L1,V2,M1} { ld( Y, Y ) ==> rd( X, X ) }.
% 0.75/1.17 parent0[0]: (563) {G4,W7,D3,L1,V2,M1} { rd( X, X ) ==> ld( Y, Y ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (198) {G16,W7,D3,L1,V2,M1} P(193,29);d(173);d(103);d(7);d(93);
% 0.75/1.17 d(51) { ld( X, X ) = rd( Y, Y ) }.
% 0.75/1.17 parent0: (564) {G4,W7,D3,L1,V2,M1} { ld( Y, Y ) ==> rd( X, X ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := X
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (566) {G14,W15,D5,L1,V4,M1} { rd( ld( rd( T, X ), Y ), Z ) ==> rd
% 0.75/1.17 ( X, ld( rd( Y, Z ), T ) ) }.
% 0.75/1.17 parent0[0]: (173) {G14,W15,D5,L1,V4,M1} S(46);d(93) { rd( X, ld( rd( Z, T )
% 0.75/1.17 , Y ) ) ==> rd( ld( rd( Y, X ), Z ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := T
% 0.75/1.17 Z := Y
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (572) {G15,W15,D5,L1,V4,M1} { rd( ld( rd( X, Y ), Z ), rd( T, T )
% 0.75/1.17 ) ==> rd( Y, ld( Z, X ) ) }.
% 0.75/1.17 parent0[0]: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent1[0; 13]: (566) {G14,W15,D5,L1,V4,M1} { rd( ld( rd( T, X ), Y ), Z )
% 0.75/1.17 ==> rd( X, ld( rd( Y, Z ), T ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := rd( T, T )
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (574) {G16,W11,D4,L1,V3,M1} { ld( rd( X, Y ), Z ) ==> rd( Y, ld(
% 0.75/1.17 Z, X ) ) }.
% 0.75/1.17 parent0[0]: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent1[0; 1]: (572) {G15,W15,D5,L1,V4,M1} { rd( ld( rd( X, Y ), Z ), rd(
% 0.75/1.17 T, T ) ) ==> rd( Y, ld( Z, X ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := ld( rd( X, Y ), Z )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (575) {G16,W11,D4,L1,V3,M1} { rd( Y, ld( Z, X ) ) ==> ld( rd( X, Y
% 0.75/1.17 ), Z ) }.
% 0.75/1.17 parent0[0]: (574) {G16,W11,D4,L1,V3,M1} { ld( rd( X, Y ), Z ) ==> rd( Y,
% 0.75/1.17 ld( Z, X ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (200) {G16,W11,D4,L1,V3,M1} P(193,173);d(193) { rd( Z, ld( X,
% 0.75/1.17 T ) ) ==> ld( rd( T, Z ), X ) }.
% 0.75/1.17 parent0: (575) {G16,W11,D4,L1,V3,M1} { rd( Y, ld( Z, X ) ) ==> ld( rd( X,
% 0.75/1.17 Y ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := X
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (577) {G10,W15,D5,L1,V4,M1} { ld( rd( ld( Z, X ), Y ), T ) ==> ld
% 0.75/1.17 ( rd( X, Y ), mult( Z, T ) ) }.
% 0.75/1.17 parent0[0]: (48) {G10,W15,D5,L1,V4,M1} P(0,43) { ld( rd( Y, Z ), mult( X, T
% 0.75/1.17 ) ) ==> ld( rd( ld( X, Y ), Z ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Y
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (580) {G11,W15,D5,L1,V4,M1} { ld( rd( ld( X, Y ), rd( Z, Z ) ), T
% 0.75/1.17 ) ==> ld( Y, mult( X, T ) ) }.
% 0.75/1.17 parent0[0]: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent1[0; 11]: (577) {G10,W15,D5,L1,V4,M1} { ld( rd( ld( Z, X ), Y ), T )
% 0.75/1.17 ==> ld( rd( X, Y ), mult( Z, T ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := rd( Z, Z )
% 0.75/1.17 Z := X
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (582) {G12,W11,D4,L1,V3,M1} { ld( ld( X, Y ), T ) ==> ld( Y, mult
% 0.75/1.17 ( X, T ) ) }.
% 0.75/1.17 parent0[0]: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent1[0; 2]: (580) {G11,W15,D5,L1,V4,M1} { ld( rd( ld( X, Y ), rd( Z, Z
% 0.75/1.17 ) ), T ) ==> ld( Y, mult( X, T ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := ld( X, Y )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (583) {G12,W11,D4,L1,V3,M1} { ld( Y, mult( X, Z ) ) ==> ld( ld( X
% 0.75/1.17 , Y ), Z ) }.
% 0.75/1.17 parent0[0]: (582) {G12,W11,D4,L1,V3,M1} { ld( ld( X, Y ), T ) ==> ld( Y,
% 0.75/1.17 mult( X, T ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := T
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (202) {G16,W11,D4,L1,V3,M1} P(193,48);d(193) { ld( X, mult( Z
% 0.75/1.17 , T ) ) ==> ld( ld( Z, X ), T ) }.
% 0.75/1.17 parent0: (583) {G12,W11,D4,L1,V3,M1} { ld( Y, mult( X, Z ) ) ==> ld( ld( X
% 0.75/1.17 , Y ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := X
% 0.75/1.17 Z := T
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (585) {G13,W11,D4,L1,V3,M1} { ld( rd( Y, X ), Z ) ==> mult( rd( X
% 0.75/1.17 , Y ), Z ) }.
% 0.75/1.17 parent0[0]: (93) {G13,W11,D4,L1,V3,M1} P(6,57) { mult( rd( X, Y ), Z ) ==>
% 0.75/1.17 ld( rd( Y, X ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (587) {G14,W11,D5,L1,V3,M1} { ld( rd( rd( X, X ), Y ), Z ) ==>
% 0.75/1.17 mult( Y, Z ) }.
% 0.75/1.17 parent0[0]: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent1[0; 9]: (585) {G13,W11,D4,L1,V3,M1} { ld( rd( Y, X ), Z ) ==> mult
% 0.75/1.17 ( rd( X, Y ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := rd( X, X )
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (216) {G16,W11,D5,L1,V3,M1} P(193,93) { ld( rd( rd( Y, Y ), X
% 0.75/1.17 ), Z ) ==> mult( X, Z ) }.
% 0.75/1.17 parent0: (587) {G14,W11,D5,L1,V3,M1} { ld( rd( rd( X, X ), Y ), Z ) ==>
% 0.75/1.17 mult( Y, Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (591) {G13,W15,D5,L1,V4,M1} { rd( ld( Z, T ), ld( Y, T ) ) = rd( X
% 0.75/1.17 , ld( Y, mult( Z, X ) ) ) }.
% 0.75/1.17 parent0[0]: (90) {G13,W15,D5,L1,V4,M1} P(57,24);d(28) { rd( Z, ld( T, mult
% 0.75/1.17 ( X, Z ) ) ) = rd( ld( X, Y ), ld( T, Y ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := T
% 0.75/1.17 Z := X
% 0.75/1.17 T := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (601) {G14,W15,D5,L1,V4,M1} { rd( ld( X, Y ), ld( mult( X, Z ), Y
% 0.75/1.17 ) ) = rd( Z, rd( T, T ) ) }.
% 0.75/1.17 parent0[0]: (198) {G16,W7,D3,L1,V2,M1} P(193,29);d(173);d(103);d(7);d(93);d
% 0.75/1.17 (51) { ld( X, X ) = rd( Y, Y ) }.
% 0.75/1.17 parent1[0; 12]: (591) {G13,W15,D5,L1,V4,M1} { rd( ld( Z, T ), ld( Y, T ) )
% 0.75/1.17 = rd( X, ld( Y, mult( Z, X ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := mult( X, Z )
% 0.75/1.17 Y := T
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := mult( X, Z )
% 0.75/1.17 Z := X
% 0.75/1.17 T := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (602) {G15,W11,D5,L1,V3,M1} { rd( ld( X, Y ), ld( mult( X, Z ), Y
% 0.75/1.17 ) ) = Z }.
% 0.75/1.17 parent0[0]: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent1[0; 10]: (601) {G14,W15,D5,L1,V4,M1} { rd( ld( X, Y ), ld( mult( X
% 0.75/1.17 , Z ), Y ) ) = rd( Z, rd( T, T ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (603) {G16,W11,D5,L1,V3,M1} { ld( rd( Y, ld( X, Y ) ), mult( X, Z
% 0.75/1.17 ) ) = Z }.
% 0.75/1.17 parent0[0]: (200) {G16,W11,D4,L1,V3,M1} P(193,173);d(193) { rd( Z, ld( X, T
% 0.75/1.17 ) ) ==> ld( rd( T, Z ), X ) }.
% 0.75/1.17 parent1[0; 1]: (602) {G15,W11,D5,L1,V3,M1} { rd( ld( X, Y ), ld( mult( X,
% 0.75/1.17 Z ), Y ) ) = Z }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := mult( X, Z )
% 0.75/1.17 Y := T
% 0.75/1.17 Z := ld( X, Y )
% 0.75/1.17 T := Y
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (605) {G17,W11,D6,L1,V3,M1} { ld( ld( Y, rd( X, ld( Y, X ) ) ), Z
% 0.75/1.17 ) = Z }.
% 0.75/1.17 parent0[0]: (202) {G16,W11,D4,L1,V3,M1} P(193,48);d(193) { ld( X, mult( Z,
% 0.75/1.17 T ) ) ==> ld( ld( Z, X ), T ) }.
% 0.75/1.17 parent1[0; 1]: (603) {G16,W11,D5,L1,V3,M1} { ld( rd( Y, ld( X, Y ) ), mult
% 0.75/1.17 ( X, Z ) ) = Z }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := rd( X, ld( Y, X ) )
% 0.75/1.17 Y := T
% 0.75/1.17 Z := Y
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (606) {G2,W7,D4,L1,V2,M1} { ld( ld( X, X ), Z ) = Z }.
% 0.75/1.17 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.75/1.17 parent1[0; 4]: (605) {G17,W11,D6,L1,V3,M1} { ld( ld( Y, rd( X, ld( Y, X )
% 0.75/1.17 ) ), Z ) = Z }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (232) {G17,W7,D4,L1,V2,M1} P(198,90);d(193);d(200);d(202);d(7)
% 0.75/1.17 { ld( ld( X, X ), Y ) ==> Y }.
% 0.75/1.17 parent0: (606) {G2,W7,D4,L1,V2,M1} { ld( ld( X, X ), Z ) = Z }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := Y
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (609) {G19,W15,D5,L1,V4,M1} { ld( Z, mult( X, T ) ) ==> ld( rd( ld
% 0.75/1.17 ( X, Y ), ld( Z, Y ) ), T ) }.
% 0.75/1.17 parent0[0]: (164) {G19,W15,D5,L1,V4,M1} P(161,93);d(93);d(47) { ld( rd( ld
% 0.75/1.17 ( Z, Y ), ld( X, Y ) ), U ) ==> ld( X, mult( Z, U ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := X
% 0.75/1.17 T := U
% 0.75/1.17 U := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (617) {G17,W15,D5,L1,V4,M1} { ld( X, mult( Y, Z ) ) ==> ld( rd(
% 0.75/1.17 rd( T, T ), ld( X, Y ) ), Z ) }.
% 0.75/1.17 parent0[0]: (198) {G16,W7,D3,L1,V2,M1} P(193,29);d(173);d(103);d(7);d(93);d
% 0.75/1.17 (51) { ld( X, X ) = rd( Y, Y ) }.
% 0.75/1.17 parent1[0; 8]: (609) {G19,W15,D5,L1,V4,M1} { ld( Z, mult( X, T ) ) ==> ld
% 0.75/1.17 ( rd( ld( X, Y ), ld( Z, Y ) ), T ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := T
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := X
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (619) {G17,W11,D4,L1,V3,M1} { ld( X, mult( Y, Z ) ) ==> mult( ld
% 0.75/1.17 ( X, Y ), Z ) }.
% 0.75/1.17 parent0[0]: (216) {G16,W11,D5,L1,V3,M1} P(193,93) { ld( rd( rd( Y, Y ), X )
% 0.75/1.17 , Z ) ==> mult( X, Z ) }.
% 0.75/1.17 parent1[0; 6]: (617) {G17,W15,D5,L1,V4,M1} { ld( X, mult( Y, Z ) ) ==> ld
% 0.75/1.17 ( rd( rd( T, T ), ld( X, Y ) ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := ld( X, Y )
% 0.75/1.17 Y := T
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (620) {G17,W11,D4,L1,V3,M1} { ld( ld( Y, X ), Z ) ==> mult( ld( X
% 0.75/1.17 , Y ), Z ) }.
% 0.75/1.17 parent0[0]: (202) {G16,W11,D4,L1,V3,M1} P(193,48);d(193) { ld( X, mult( Z,
% 0.75/1.17 T ) ) ==> ld( ld( Z, X ), T ) }.
% 0.75/1.17 parent1[0; 1]: (619) {G17,W11,D4,L1,V3,M1} { ld( X, mult( Y, Z ) ) ==>
% 0.75/1.17 mult( ld( X, Y ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := T
% 0.75/1.17 Z := Y
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (621) {G17,W11,D4,L1,V3,M1} { mult( ld( Y, X ), Z ) ==> ld( ld( X
% 0.75/1.17 , Y ), Z ) }.
% 0.75/1.17 parent0[0]: (620) {G17,W11,D4,L1,V3,M1} { ld( ld( Y, X ), Z ) ==> mult( ld
% 0.75/1.17 ( X, Y ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (249) {G20,W11,D4,L1,V3,M1} P(198,164);d(216);d(202) { mult(
% 0.75/1.17 ld( Z, X ), T ) ==> ld( ld( X, Z ), T ) }.
% 0.75/1.17 parent0: (621) {G17,W11,D4,L1,V3,M1} { mult( ld( Y, X ), Z ) ==> ld( ld( X
% 0.75/1.17 , Y ), Z ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := T
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (623) {G8,W15,D5,L1,V4,M1} { rd( mult( X, Z ), T ) ==> rd( mult( X
% 0.75/1.17 , Y ), ld( rd( Z, T ), Y ) ) }.
% 0.75/1.17 parent0[0]: (39) {G8,W15,D5,L1,V4,M1} P(6,32) { rd( mult( Z, T ), ld( rd( X
% 0.75/1.17 , Y ), T ) ) ==> rd( mult( Z, X ), Y ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := T
% 0.75/1.17 Z := X
% 0.75/1.17 T := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (629) {G9,W15,D5,L1,V4,M1} { rd( mult( X, Y ), Z ) ==> rd( mult(
% 0.75/1.17 X, rd( Y, Z ) ), rd( T, T ) ) }.
% 0.75/1.17 parent0[0]: (198) {G16,W7,D3,L1,V2,M1} P(193,29);d(173);d(103);d(7);d(93);d
% 0.75/1.17 (51) { ld( X, X ) = rd( Y, Y ) }.
% 0.75/1.17 parent1[0; 12]: (623) {G8,W15,D5,L1,V4,M1} { rd( mult( X, Z ), T ) ==> rd
% 0.75/1.17 ( mult( X, Y ), ld( rd( Z, T ), Y ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := rd( Y, Z )
% 0.75/1.17 Y := T
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := rd( Y, Z )
% 0.75/1.17 Z := Y
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (630) {G10,W11,D4,L1,V3,M1} { rd( mult( X, Y ), Z ) ==> mult( X,
% 0.75/1.17 rd( Y, Z ) ) }.
% 0.75/1.17 parent0[0]: (193) {G15,W7,D4,L1,V2,M1} P(177,103);d(3) { rd( Y, rd( X, X )
% 0.75/1.17 ) ==> Y }.
% 0.75/1.17 parent1[0; 6]: (629) {G9,W15,D5,L1,V4,M1} { rd( mult( X, Y ), Z ) ==> rd(
% 0.75/1.17 mult( X, rd( Y, Z ) ), rd( T, T ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := mult( X, rd( Y, Z ) )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (259) {G17,W11,D4,L1,V3,M1} P(198,39);d(193) { rd( mult( T, X
% 0.75/1.17 ), Y ) ==> mult( T, rd( X, Y ) ) }.
% 0.75/1.17 parent0: (630) {G10,W11,D4,L1,V3,M1} { rd( mult( X, Y ), Z ) ==> mult( X,
% 0.75/1.17 rd( Y, Z ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := X
% 0.75/1.17 Z := Y
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (632) {G16,W7,D3,L1,V2,M1} { rd( Y, Y ) = ld( X, X ) }.
% 0.75/1.17 parent0[0]: (198) {G16,W7,D3,L1,V2,M1} P(193,29);d(173);d(103);d(7);d(93);d
% 0.75/1.17 (51) { ld( X, X ) = rd( Y, Y ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (633) {G8,W15,D5,L1,V4,M1} { rd( mult( X, Z ), T ) ==> rd( mult( X
% 0.75/1.17 , Y ), ld( rd( Z, T ), Y ) ) }.
% 0.75/1.17 parent0[0]: (39) {G8,W15,D5,L1,V4,M1} P(6,32) { rd( mult( Z, T ), ld( rd( X
% 0.75/1.17 , Y ), T ) ) ==> rd( mult( Z, X ), Y ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := T
% 0.75/1.17 Z := X
% 0.75/1.17 T := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (638) {G9,W15,D5,L1,V4,M1} { rd( mult( X, Y ), Y ) ==> rd( mult(
% 0.75/1.17 X, Z ), ld( ld( T, T ), Z ) ) }.
% 0.75/1.17 parent0[0]: (632) {G16,W7,D3,L1,V2,M1} { rd( Y, Y ) = ld( X, X ) }.
% 0.75/1.17 parent1[0; 11]: (633) {G8,W15,D5,L1,V4,M1} { rd( mult( X, Z ), T ) ==> rd
% 0.75/1.17 ( mult( X, Y ), ld( rd( Z, T ), Y ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := T
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := Y
% 0.75/1.17 T := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (640) {G10,W15,D6,L1,V4,M1} { rd( mult( X, Y ), Y ) ==> mult( X,
% 0.75/1.17 rd( Z, ld( ld( T, T ), Z ) ) ) }.
% 0.75/1.17 parent0[0]: (259) {G17,W11,D4,L1,V3,M1} P(198,39);d(193) { rd( mult( T, X )
% 0.75/1.17 , Y ) ==> mult( T, rd( X, Y ) ) }.
% 0.75/1.17 parent1[0; 6]: (638) {G9,W15,D5,L1,V4,M1} { rd( mult( X, Y ), Y ) ==> rd(
% 0.75/1.17 mult( X, Z ), ld( ld( T, T ), Z ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := ld( ld( T, T ), Z )
% 0.75/1.17 Z := U
% 0.75/1.17 T := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (642) {G2,W11,D4,L1,V3,M1} { rd( mult( X, Y ), Y ) ==> mult( X,
% 0.75/1.17 ld( T, T ) ) }.
% 0.75/1.17 parent0[0]: (7) {G1,W7,D4,L1,V2,M1} P(0,3) { rd( Y, ld( X, Y ) ) ==> X }.
% 0.75/1.17 parent1[0; 8]: (640) {G10,W15,D6,L1,V4,M1} { rd( mult( X, Y ), Y ) ==>
% 0.75/1.17 mult( X, rd( Z, ld( ld( T, T ), Z ) ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := ld( T, T )
% 0.75/1.17 Y := Z
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := Z
% 0.75/1.17 T := T
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (643) {G1,W7,D4,L1,V2,M1} { X ==> mult( X, ld( Z, Z ) ) }.
% 0.75/1.17 parent0[0]: (3) {G0,W7,D4,L1,V2,M1} I { rd( mult( Y, X ), X ) ==> Y }.
% 0.75/1.17 parent1[0; 1]: (642) {G2,W11,D4,L1,V3,M1} { rd( mult( X, Y ), Y ) ==> mult
% 0.75/1.17 ( X, ld( T, T ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Y
% 0.75/1.17 Y := X
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := T
% 0.75/1.17 T := Z
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (644) {G1,W7,D4,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> X }.
% 0.75/1.17 parent0[0]: (643) {G1,W7,D4,L1,V2,M1} { X ==> mult( X, ld( Z, Z ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Z
% 0.75/1.17 Z := Y
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (260) {G18,W7,D4,L1,V2,M1} P(198,39);d(259);d(7);d(3) { mult(
% 0.75/1.17 Z, ld( Y, Y ) ) ==> Z }.
% 0.75/1.17 parent0: (644) {G1,W7,D4,L1,V2,M1} { mult( X, ld( Y, Y ) ) ==> X }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := Y
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 0 ==> 0
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (645) {G18,W7,D4,L1,V2,M1} { X ==> mult( X, ld( Y, Y ) ) }.
% 0.75/1.17 parent0[0]: (260) {G18,W7,D4,L1,V2,M1} P(198,39);d(259);d(7);d(3) { mult( Z
% 0.75/1.17 , ld( Y, Y ) ) ==> Z }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := Z
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqswap: (646) {G0,W14,D4,L2,V1,M2} { ! skol1( X ) ==> mult( skol1( X ), X
% 0.75/1.17 ), ! mult( X, skol1( X ) ) ==> skol1( X ) }.
% 0.75/1.17 parent0[0]: (5) {G0,W14,D4,L2,V1,M2} I { ! mult( skol1( X ), X ) ==> skol1
% 0.75/1.17 ( X ), ! mult( X, skol1( X ) ) ==> skol1( X ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 resolution: (651) {G1,W13,D5,L1,V1,M1} { ! mult( ld( X, X ), skol1( ld( X
% 0.75/1.17 , X ) ) ) ==> skol1( ld( X, X ) ) }.
% 0.75/1.17 parent0[0]: (646) {G0,W14,D4,L2,V1,M2} { ! skol1( X ) ==> mult( skol1( X )
% 0.75/1.17 , X ), ! mult( X, skol1( X ) ) ==> skol1( X ) }.
% 0.75/1.17 parent1[0]: (645) {G18,W7,D4,L1,V2,M1} { X ==> mult( X, ld( Y, Y ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := ld( X, X )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := skol1( ld( X, X ) )
% 0.75/1.17 Y := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (652) {G2,W13,D5,L1,V1,M1} { ! ld( ld( X, X ), skol1( ld( X, X )
% 0.75/1.17 ) ) ==> skol1( ld( X, X ) ) }.
% 0.75/1.17 parent0[0]: (249) {G20,W11,D4,L1,V3,M1} P(198,164);d(216);d(202) { mult( ld
% 0.75/1.17 ( Z, X ), T ) ==> ld( ld( X, Z ), T ) }.
% 0.75/1.17 parent1[0; 2]: (651) {G1,W13,D5,L1,V1,M1} { ! mult( ld( X, X ), skol1( ld
% 0.75/1.17 ( X, X ) ) ) ==> skol1( ld( X, X ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := Y
% 0.75/1.17 Z := X
% 0.75/1.17 T := skol1( ld( X, X ) )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 paramod: (653) {G3,W9,D4,L1,V1,M1} { ! skol1( ld( X, X ) ) ==> skol1( ld(
% 0.75/1.17 X, X ) ) }.
% 0.75/1.17 parent0[0]: (232) {G17,W7,D4,L1,V2,M1} P(198,90);d(193);d(200);d(202);d(7)
% 0.75/1.17 { ld( ld( X, X ), Y ) ==> Y }.
% 0.75/1.17 parent1[0; 2]: (652) {G2,W13,D5,L1,V1,M1} { ! ld( ld( X, X ), skol1( ld( X
% 0.75/1.17 , X ) ) ) ==> skol1( ld( X, X ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 Y := skol1( ld( X, X ) )
% 0.75/1.17 end
% 0.75/1.17 substitution1:
% 0.75/1.17 X := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 eqrefl: (654) {G0,W0,D0,L0,V0,M0} { }.
% 0.75/1.17 parent0[0]: (653) {G3,W9,D4,L1,V1,M1} { ! skol1( ld( X, X ) ) ==> skol1(
% 0.75/1.17 ld( X, X ) ) }.
% 0.75/1.17 substitution0:
% 0.75/1.17 X := X
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 subsumption: (287) {G21,W0,D0,L0,V0,M0} R(260,5);d(249);d(232);q { }.
% 0.75/1.17 parent0: (654) {G0,W0,D0,L0,V0,M0} { }.
% 0.75/1.17 substitution0:
% 0.75/1.17 end
% 0.75/1.17 permutation0:
% 0.75/1.17 end
% 0.75/1.17
% 0.75/1.17 Proof check complete!
% 0.75/1.17
% 0.75/1.17 Memory use:
% 0.75/1.17
% 0.75/1.17 space for terms: 4082
% 0.75/1.17 space for clauses: 36177
% 0.75/1.17
% 0.75/1.17
% 0.75/1.17 clauses generated: 6017
% 0.75/1.17 clauses kept: 288
% 0.75/1.17 clauses selected: 86
% 0.75/1.17 clauses deleted: 12
% 0.75/1.17 clauses inuse deleted: 0
% 0.75/1.17
% 0.75/1.17 subsentry: 1909
% 0.75/1.17 literals s-matched: 1334
% 0.75/1.17 literals matched: 1334
% 0.75/1.17 full subsumption: 0
% 0.75/1.17
% 0.75/1.17 checksum: -284417387
% 0.75/1.17
% 0.75/1.17
% 0.75/1.17 Bliksem ended
%------------------------------------------------------------------------------