%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : GRP684-1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n007.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 : 600s % DateTime : Sat Jul 16 10:57:50 EDT 2022 % Result : Unsatisfiable 91.19s 90.66s % Output : Proof 91.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : GRP684-1 : TPTP v8.1.0. Released v4.0.0. % 0.04/0.13 % Command : moca.sh %s % 0.13/0.34 % Computer : n007.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.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon Jun 13 11:54:39 EDT 2022 % 0.13/0.35 % CPUTime : % 91.19/90.66 % SZS status Unsatisfiable % 91.19/90.66 % SZS output start Proof % 91.19/90.66 The input problem is unsatisfiable because % 91.19/90.66 % 91.19/90.66 [1] the following set of Horn clauses is unsatisfiable: % 91.19/90.66 % 91.19/90.66 ld(A, mult(A, A)) = A % 91.19/90.66 rd(mult(A, A), A) = A % 91.19/90.66 mult(A, ld(A, B)) = ld(A, mult(A, B)) % 91.19/90.66 mult(rd(A, B), B) = rd(mult(A, B), B) % 91.19/90.66 ld(ld(A, B), mult(ld(A, B), mult(C, D))) = mult(ld(A, mult(A, C)), D) % 91.19/90.66 rd(mult(mult(A, B), rd(C, D)), rd(C, D)) = mult(A, rd(mult(B, D), D)) % 91.19/90.66 ld(A, mult(A, ld(B, B))) = rd(mult(rd(A, A), B), B) % 91.19/90.66 rd(mult(a, mult(b, c)), mult(b, c)) = rd(mult(a, c), c) ==> \bottom % 91.19/90.66 % 91.19/90.66 This holds because % 91.19/90.66 % 91.19/90.66 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 91.19/90.66 % 91.19/90.66 E: % 91.19/90.66 f1(rd(mult(a, c), c)) = false__ % 91.19/90.66 f1(rd(mult(a, mult(b, c)), mult(b, c))) = true__ % 91.19/90.66 ld(A, mult(A, A)) = A % 91.19/90.66 ld(A, mult(A, ld(B, B))) = rd(mult(rd(A, A), B), B) % 91.19/90.66 ld(ld(A, B), mult(ld(A, B), mult(C, D))) = mult(ld(A, mult(A, C)), D) % 91.19/90.66 mult(A, ld(A, B)) = ld(A, mult(A, B)) % 91.19/90.66 mult(rd(A, B), B) = rd(mult(A, B), B) % 91.19/90.66 rd(mult(A, A), A) = A % 91.19/90.66 rd(mult(mult(A, B), rd(C, D)), rd(C, D)) = mult(A, rd(mult(B, D), D)) % 91.19/90.66 G: % 91.19/90.66 true__ = false__ % 91.19/90.66 % 91.19/90.66 This holds because % 91.19/90.66 % 91.19/90.66 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 91.19/90.66 % 91.19/90.66 ld(Y0, rd(Y0, mult(rd(Y0, X1), X1))) = mult(rd(Y0, Y0), ld(Y0, rd(X1, X1))) % 91.19/90.66 ld(rd(X0, rd(X1, X2)), mult(rd(X0, X2), X2)) = mult(rd(X0, rd(X1, X2)), ld(rd(X0, rd(X1, X2)), rd(X1, X2))) % 91.19/90.66 mult(X0, mult(X0, rd(Y2, Y2))) = mult(mult(X0, X0), rd(X0, mult(rd(X0, Y2), Y2))) % 91.19/90.66 mult(X0, mult(X0, rd(Y2, Y2))) = mult(mult(X0, X0), rd(false__, mult(rd(false__, Y2), Y2))) % 91.19/90.66 mult(X0, mult(X1, rd(Y2, Y2))) = mult(mult(X0, X1), rd(X1, mult(rd(X1, Y2), Y2))) % 91.19/90.66 mult(X0, mult(Y1, rd(Y2, Y2))) = mult(mult(X0, rd(Y1, Y1)), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(X0, mult(rd(X0, X0), mult(rd(rd(Y1, Y1), Y2), Y2))) = mult(rd(X0, Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(X0, mult(rd(X0, X0), rd(Y1, mult(rd(Y1, Y2), Y2)))) = mult(rd(X0, Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(X0, mult(rd(Y1, Y1), rd(Y2, Y2))) = mult(rd(X0, Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(X0, rd(Y1, Y1)) = mult(mult(rd(X0, Y1), Y1), rd(Y2, mult(rd(Y2, Y1), Y1))) % 91.19/90.66 mult(X0, rd(Y1, mult(rd(Y1, Y2), Y2))) = mult(rd(X0, X1), mult(rd(X1, Y2), Y2)) % 91.19/90.66 mult(X0, rd(Y1, mult(rd(Y1, Y2), Y2))) = mult(rd(X0, Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(X0, rd(Y2, Y2)) = mult(rd(X0, Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(X0, rd(false__, mult(rd(false__, Y2), Y2))) = mult(rd(X0, Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(X0, rd(false__, mult(rd(false__, Y2), Y2))) = mult(rd(X0, rd(Y1, mult(rd(Y1, Y2), Y2))), rd(Y2, Y2)) % 91.19/90.66 mult(Y0, mult(X1, rd(Y2, Y2))) = mult(Y0, mult(rd(ld(rd(Y0, Y0), X1), Y2), Y2)) % 91.19/90.66 mult(Y0, mult(X1, rd(Y2, Y2))) = mult(mult(Y0, X1), rd(false__, mult(rd(false__, Y2), Y2))) % 91.19/90.66 mult(Y0, mult(ld(Y0, X0), rd(Y2, Y2))) = mult(mult(rd(Y0, Y0), rd(X0, Y2)), Y2) % 91.19/90.66 mult(Y0, mult(rd(Y1, Y1), rd(X0, mult(rd(X0, X1), X1)))) = mult(rd(Y0, X1), X1) % 91.19/90.66 mult(Y0, mult(rd(Y1, Y1), rd(Y2, Y2))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, mult(rd(rd(Y0, Y0), X2), mult(rd(X2, X1), X1))) = mult(Y0, rd(X1, X1)) % 91.19/90.66 mult(Y0, mult(rd(rd(false__, false__), false__), mult(rd(false__, X1), X1))) = mult(rd(Y0, X1), X1) % 91.19/90.66 mult(Y0, rd(X0, mult(X0, rd(X1, mult(rd(X1, Y2), Y2))))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, rd(X0, mult(X0, rd(false__, mult(rd(false__, Y2), Y2))))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, rd(X0, mult(rd(X0, X1), X1))) = mult(Y0, rd(Y2, mult(rd(Y2, X1), X1))) % 91.19/90.66 mult(Y0, rd(X0, mult(rd(X0, X1), mult(rd(X1, Y2), Y2)))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, rd(X0, mult(rd(X0, Y2), Y2))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, rd(Y1, Y1)) = mult(Y0, mult(rd(rd(false__, false__), false__), mult(rd(false__, Y1), Y1))) % 91.19/90.66 mult(Y0, rd(Y1, Y1)) = mult(Y0, rd(Y2, mult(rd(Y2, Y1), Y1))) % 91.19/90.66 mult(Y0, rd(Y2, mult(rd(Y2, mult(Y2, Y2)), mult(Y2, Y2)))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, rd(false__, mult(rd(false__, X2), X2))) = mult(Y0, rd(X1, mult(rd(X1, X2), X2))) % 91.19/90.66 mult(Y0, rd(mult(X0, Y2), mult(X0, Y2))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, rd(mult(X0, rd(Y2, Y2)), mult(rd(X0, Y2), Y2))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, rd(mult(rd(X0, Y2), Y2), mult(X0, rd(Y2, Y2)))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(Y0, rd(rd(Y1, Y2), rd(Y1, Y2))) = mult(rd(Y0, Y2), Y2) % 91.19/90.66 mult(mult(X0, rd(Y1, Y1)), rd(Y2, Y2)) = mult(rd(X0, Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(mult(X0, rd(Y1, mult(rd(Y1, Y2), Y2))), Y2) = mult(mult(rd(X0, mult(rd(Y1, Y2), Y2)), Y1), Y2) % 91.19/90.66 mult(mult(Y0, Y1), mult(rd(mult(Y0, Y1), mult(Y0, Y1)), rd(Y2, Y2))) = mult(Y0, mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(mult(Y0, Y1), rd(X0, mult(rd(X0, X1), X1))) = mult(Y0, mult(rd(Y1, X1), X1)) % 91.19/90.66 mult(mult(Y0, Y1), rd(Y2, Y2)) = mult(Y0, mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(mult(Y0, Y1), rd(false__, mult(rd(false__, Y2), Y2))) = mult(Y0, mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(mult(rd(X0, X0), rd(X0, X1)), X1) = mult(X0, rd(X1, X1)) % 91.19/90.66 mult(mult(rd(X0, X0), rd(rd(X0, X0), Y1)), Y1) = mult(rd(X0, X0), rd(Y1, Y1)) % 91.19/90.66 mult(mult(rd(Y0, X1), X1), rd(Y2, Y2)) = mult(Y0, rd(X1, mult(rd(X1, Y2), Y2))) % 91.19/90.66 mult(mult(rd(Y0, X2), X2), rd(false__, mult(rd(false__, mult(X1, X2)), mult(X1, X2)))) = mult(rd(Y0, mult(X1, X2)), mult(X1, X2)) % 91.19/90.66 mult(mult(rd(Y0, Y0), rd(rd(Y1, Y1), Y1)), Y1) = mult(rd(rd(Y0, Y0), Y1), Y1) % 91.19/90.66 mult(mult(rd(Y0, Y0), rd(rd(Y1, Y1), Y1)), Y1) = rd(Y0, mult(rd(Y0, Y1), Y1)) % 91.19/90.66 mult(rd(X0, X0), mult(rd(X0, X0), rd(Y1, Y1))) = mult(rd(rd(X0, X0), Y1), Y1) % 91.19/90.66 mult(rd(X0, X0), rd(Y1, Y1)) = mult(rd(X0, mult(X0, rd(false__, mult(rd(false__, Y1), Y1)))), rd(false__, mult(rd(false__, Y1), Y1))) % 91.19/90.66 mult(rd(X0, X0), rd(Y1, Y1)) = mult(rd(rd(X0, X0), X0), mult(rd(X0, Y1), Y1)) % 91.19/90.66 mult(rd(X0, X0), rd(Y1, Y1)) = mult(rd(rd(X0, X0), mult(rd(X0, X0), rd(false__, mult(rd(false__, Y1), Y1)))), rd(false__, mult(rd(false__, Y1), Y1))) % 91.19/90.66 mult(rd(X0, X0), rd(Y1, Y1)) = rd(X0, mult(X0, rd(X1, mult(rd(X1, Y1), Y1)))) % 91.19/90.66 mult(rd(X0, X0), rd(Y1, Y1)) = rd(X0, mult(X0, rd(false__, mult(rd(false__, Y1), Y1)))) % 91.19/90.66 mult(rd(X0, X0), rd(Y1, Y1)) = rd(X0, mult(rd(X0, X1), mult(rd(X1, Y1), Y1))) % 91.19/90.66 mult(rd(X0, X0), rd(Y1, Y1)) = rd(rd(X0, X0), rd(X0, mult(rd(X0, Y1), Y1))) % 91.19/90.66 mult(rd(X0, X1), rd(Y2, Y2)) = mult(rd(X0, X1), rd(X1, mult(rd(X1, Y2), Y2))) % 91.19/90.66 mult(rd(X0, Y1), Y1) = mult(mult(X0, rd(Y1, Y1)), rd(Y1, Y1)) % 91.19/90.66 mult(rd(X0, Y1), Y1) = mult(mult(X0, rd(Y1, Y1)), rd(Y1, mult(rd(Y1, mult(Y1, Y1)), mult(Y1, Y1)))) % 91.19/90.66 mult(rd(X0, Y1), Y1) = mult(mult(mult(X0, rd(Y1, Y1)), rd(Y1, Y1)), rd(Y1, Y1)) % 91.19/90.66 mult(rd(X0, Y1), rd(Y2, Y2)) = mult(rd(rd(X0, Y1), Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(rd(X0, mult(rd(X0, X1), X1)), rd(Y1, Y1)) = rd(X0, mult(X0, rd(false__, mult(rd(false__, Y1), Y1)))) % 91.19/90.66 mult(rd(X1, X1), mult(rd(rd(X1, X1), X1), mult(X1, rd(Y1, Y1)))) = rd(X1, mult(rd(X1, Y1), Y1)) % 91.19/90.66 mult(rd(Y0, X1), X1) = mult(Y0, mult(rd(Y0, Y0), rd(X1, X1))) % 91.19/90.66 mult(rd(Y0, X1), X1) = mult(Y0, rd(X1, X1)) % 91.19/90.66 mult(rd(Y0, X1), mult(X1, rd(Y2, Y2))) = mult(Y0, rd(X1, mult(rd(X1, Y2), Y2))) % 91.19/90.66 mult(rd(Y0, Y0), rd(X2, X2)) = mult(rd(Y0, Y0), rd(X1, mult(rd(X1, X2), X2))) % 91.19/90.66 mult(rd(Y0, Y0), rd(X2, X2)) = rd(Y0, mult(rd(Y0, mult(X1, X2)), mult(X1, X2))) % 91.19/90.66 mult(rd(Y0, Y0), rd(X2, mult(rd(X2, X1), X1))) = rd(Y0, mult(rd(Y0, X1), X1)) % 91.19/90.66 mult(rd(Y0, Y0), rd(Y1, Y1)) = mult(rd(rd(Y0, Y0), Y1), Y1) % 91.19/90.66 mult(rd(Y0, Y0), rd(Y1, Y1)) = rd(Y0, mult(rd(Y0, Y1), Y1)) % 91.19/90.66 mult(rd(Y0, Y1), Y1) = mult(rd(Y0, Y2), mult(rd(Y2, Y1), Y1)) % 91.19/90.66 mult(rd(Y0, mult(Y0, rd(false__, mult(rd(false__, X1), X1)))), rd(false__, mult(rd(false__, X1), X1))) = rd(Y0, mult(rd(Y0, X1), X1)) % 91.19/90.66 mult(rd(rd(X0, X0), X1), mult(rd(X1, Y2), Y2)) = mult(rd(X0, X0), mult(rd(rd(X1, X1), Y2), Y2)) % 91.19/90.66 mult(rd(rd(X0, X0), X1), mult(rd(X1, Y2), Y2)) = mult(rd(X0, X0), rd(X1, mult(rd(X1, Y2), Y2))) % 91.19/90.66 mult(rd(rd(X0, Y1), Y2), Y2) = mult(rd(rd(X0, Y1), Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 mult(rd(rd(Y0, Y0), Y0), mult(Y0, rd(Y2, Y2))) = mult(rd(Y0, Y0), rd(false__, mult(rd(false__, Y2), Y2))) % 91.19/90.66 mult(rd(rd(Y1, Y1), Y2), Y2) = mult(rd(rd(Y1, Y1), Y1), mult(rd(Y1, Y2), Y2)) % 91.19/90.66 rd(X0, mult(rd(X0, X1), X1)) = mult(rd(rd(X0, X0), X0), mult(rd(X0, X1), X1)) % 91.19/90.66 rd(X0, mult(rd(X0, Y1), Y1)) = mult(rd(rd(X0, X0), X0), mult(X0, rd(Y1, Y1))) % 91.19/90.66 rd(X0, mult(rd(X1, X2), X2)) = mult(rd(rd(X0, X1), X1), mult(rd(X1, X2), X2)) % 91.19/90.66 rd(X0, mult(rd(false__, X0), X0)) = mult(rd(X0, false__), rd(false__, mult(rd(false__, X0), X0))) % 91.19/90.66 rd(mult(X0, X1), mult(X0, mult(rd(X1, X2), X2))) = rd(mult(X0, X1), mult(mult(X0, X1), rd(false__, mult(rd(false__, X2), X2)))) % 91.28/90.67 rd(mult(rd(X0, X1), X1), mult(rd(X0, X1), X1)) = mult(rd(rd(X0, X0), X0), mult(rd(X0, X1), X1)) % 91.28/90.67 rd(mult(rd(X0, X1), X1), mult(rd(X0, X1), X1)) = mult(rd(rd(X0, X0), X0), mult(rd(X0, mult(rd(X0, X1), X1)), mult(rd(X0, X1), X1))) % 91.28/90.67 f1(mult(a, mult(rd(rd(a, a), false__), mult(rd(false__, c), c)))) -> false__ % 91.28/90.67 f1(mult(a, mult(rd(rd(false__, false__), false__), mult(rd(false__, c), c)))) -> false__ % 91.28/90.67 f1(mult(a, rd(X0, mult(X0, mult(rd(rd(false__, false__), false__), mult(rd(false__, c), c)))))) -> false__ % 91.28/90.67 f1(mult(a, rd(X0, mult(X0, rd(X1, mult(rd(X1, c), c)))))) -> false__ % 91.28/90.67 f1(mult(a, rd(X0, mult(rd(X0, X1), mult(rd(X1, c), c))))) -> false__ % 91.28/90.67 f1(mult(a, rd(X0, mult(rd(X0, false__), mult(rd(false__, c), c))))) -> false__ % 91.28/90.67 f1(mult(a, rd(X2, mult(rd(X2, c), c)))) -> false__ % 91.28/90.67 f1(mult(mult(rd(a, false__), mult(rd(false__, c), c)), mult(rd(rd(false__, false__), false__), mult(rd(false__, c), c)))) -> false__ % 91.28/90.67 f1(mult(rd(a, X2), mult(rd(X2, c), c))) -> false__ % 91.28/90.67 f1(mult(rd(a, c), c)) -> false__ % 91.28/90.67 f1(mult(rd(a, false__), mult(rd(false__, c), c))) -> false__ % 91.28/90.67 f1(mult(rd(a, mult(X0, mult(rd(rd(false__, false__), false__), mult(rd(false__, c), c)))), mult(rd(X0, c), c))) -> false__ % 91.28/90.67 f1(mult(rd(a, mult(X0, rd(X1, X1))), mult(rd(X0, c), c))) -> false__ % 91.28/90.67 f1(mult(rd(a, mult(b, c)), mult(b, c))) -> true__ % 91.28/90.67 f1(mult(rd(a, mult(rd(X0, X1), X1)), mult(rd(X0, c), c))) -> false__ % 91.28/90.67 f1(rd(mult(a, c), c)) -> false__ % 91.28/90.67 f1(rd(mult(a, mult(b, c)), mult(b, c))) -> true__ % 91.28/90.67 ld(A, mult(A, A)) -> A % 91.28/90.67 ld(A, mult(A, B)) -> mult(A, ld(A, B)) % 91.28/90.67 ld(A, mult(A, ld(B, B))) -> rd(mult(rd(A, A), B), B) % 91.28/90.67 ld(Y0, mult(mult(Y0, X1), rd(X2, X2))) -> mult(mult(rd(Y0, Y0), rd(X1, X2)), X2) % 91.28/90.67 ld(Y0, mult(mult(Y0, ld(Y0, Y0)), mult(Y2, Y3))) -> mult(mult(Y0, ld(Y0, Y2)), Y3) % 91.28/90.67 ld(Y0, mult(mult(rd(Y0, Y0), X1), X2)) -> mult(rd(Y0, Y0), ld(Y0, mult(X1, X2))) % 91.28/90.67 ld(Y0, mult(rd(Y0, X1), X1)) -> mult(rd(Y0, Y0), rd(X1, X1)) % 91.28/90.67 ld(Y0, mult(rd(Y0, X2), mult(rd(X2, X1), X1))) -> rd(Y0, mult(rd(Y0, X1), X1)) % 91.28/90.67 ld(Y0, mult(rd(Y0, Y0), X1)) -> mult(rd(Y0, Y0), ld(Y0, X1)) % 91.28/90.67 ld(Y1, Y1) -> mult(rd(rd(Y1, Y1), Y1), Y1) % 91.28/90.67 ld(ld(A, B), mult(ld(A, B), mult(C, D))) -> mult(ld(A, mult(A, C)), D) % 91.28/90.67 ld(mult(X0, X1), mult(X0, mult(rd(X1, X2), X2))) -> rd(mult(X0, X1), mult(X0, mult(rd(X1, X2), X2))) % 91.28/90.67 ld(mult(X0, ld(X0, X1)), mult(rd(X0, X0), X1)) -> mult(rd(rd(mult(X0, ld(X0, X1)), mult(X0, ld(X0, X1))), X1), X1) % 91.28/90.67 ld(mult(X0, mult(rd(X1, Y1), Y1)), mult(mult(X0, X1), Y1)) -> mult(mult(X0, mult(rd(X1, Y1), Y1)), ld(mult(X0, mult(rd(X1, Y1), Y1)), Y1)) % 91.28/90.67 ld(mult(X0, rd(X1, X1)), mult(X0, Y1)) -> mult(X0, ld(mult(X0, rd(X1, X1)), Y1)) % 91.28/90.67 ld(mult(X0, rd(X1, X1)), mult(X0, mult(X0, rd(X1, X1)))) -> mult(X0, rd(X1, X1)) % 91.28/90.67 ld(mult(X0, rd(X1, X1)), mult(rd(X0, X1), X1)) -> mult(rd(mult(X0, rd(X1, X1)), mult(X0, rd(X1, X1))), rd(false__, mult(rd(false__, X1), X1))) % 91.28/90.67 ld(mult(X0, rd(Y1, Y1)), mult(X0, Y1)) -> mult(rd(mult(X0, rd(Y1, Y1)), mult(X0, rd(Y1, Y1))), Y1) % 91.28/90.67 ld(mult(Y0, ld(Y0, Y0)), mult(Y0, mult(Y2, Y3))) -> mult(mult(Y0, ld(Y0, Y2)), Y3) % 91.28/90.67 ld(mult(mult(rd(X0, Y1), Y1), X2), mult(mult(X0, X2), Y1)) -> mult(mult(mult(rd(X0, Y1), Y1), X2), ld(mult(mult(rd(X0, Y1), Y1), X2), Y1)) % 91.28/90.67 ld(mult(rd(X0, X0), rd(X0, Y1)), mult(X0, rd(Y1, Y1))) -> mult(rd(mult(rd(X0, X0), rd(X0, Y1)), mult(rd(X0, X0), rd(X0, Y1))), Y1) % 91.28/90.67 ld(mult(rd(X0, X0), rd(X1, X1)), mult(X0, rd(X1, X1))) -> mult(X0, rd(X1, X1)) % 91.28/90.67 ld(mult(rd(X0, X0), rd(X1, X1)), rd(X0, Y1)) -> rd(X0, Y1) % 91.28/90.67 ld(mult(rd(X0, X0), rd(Y1, Y1)), rd(X0, Y1)) -> rd(X0, Y1) % 91.28/90.67 ld(mult(rd(X0, X1), X1), mult(X0, Y1)) -> mult(X0, ld(mult(rd(X0, X1), X1), Y1)) % 91.28/90.67 ld(mult(rd(X0, X1), X1), mult(X0, mult(rd(X0, X1), X1))) -> mult(rd(X0, X1), X1) % 91.28/90.67 ld(mult(rd(X0, X1), X1), mult(X0, rd(X2, X1))) -> mult(mult(rd(X0, X1), X1), ld(mult(rd(X0, X1), X1), rd(X2, X1))) % 91.28/90.67 ld(mult(rd(X0, Y1), Y1), mult(X0, Y1)) -> mult(mult(rd(X0, Y1), Y1), ld(mult(rd(X0, Y1), Y1), Y1)) % 91.28/90.67 ld(mult(rd(X0, rd(Y1, Y1)), rd(Y1, Y1)), mult(X0, rd(Y1, Y1))) -> mult(rd(rd(mult(rd(X0, rd(Y1, Y1)), rd(Y1, Y1)), mult(rd(X0, rd(Y1, Y1)), rd(Y1, Y1))), Y1), Y1) % 91.28/90.67 ld(mult(rd(Y1, Y1), rd(rd(Y1, Y1), Y1)), rd(Y1, Y1)) -> mult(rd(mult(rd(Y1, Y1), rd(rd(Y1, Y1), Y1)), mult(rd(Y1, Y1), rd(rd(Y1, Y1), Y1))), Y1) % 91.28/90.67 ld(rd(X0, X0), ld(X0, rd(X0, X0))) -> ld(X0, rd(X0, X0)) % 91.28/90.67 ld(rd(X0, X0), mult(rd(rd(X0, X0), X1), X1)) -> mult(rd(rd(X0, X0), X1), X1) % 91.28/90.67 ld(rd(X0, X0), rd(X0, X1)) -> rd(X0, X1) % 91.28/90.67 ld(rd(X0, X0), rd(X0, mult(rd(X0, X1), X1))) -> rd(X0, mult(rd(X0, X1), X1)) % 91.28/90.67 ld(rd(X0, X0), rd(rd(X0, X0), Y1)) -> rd(rd(X0, X0), Y1) % 91.28/90.67 ld(rd(X0, X1), mult(X0, rd(X2, X2))) -> mult(mult(rd(rd(X0, X1), rd(X0, X1)), rd(X1, X2)), X2) % 91.28/90.67 ld(rd(X0, X1), mult(rd(X0, X2), X2)) -> mult(mult(rd(rd(X0, X1), rd(X0, X1)), rd(X1, X2)), X2) % 91.28/90.67 ld(rd(X0, Y1), mult(X0, rd(X2, mult(rd(X2, Y1), Y1)))) -> mult(rd(rd(X0, Y1), rd(X0, Y1)), Y1) % 91.28/90.67 ld(rd(X0, Y1), mult(X0, rd(Y1, Y1))) -> mult(rd(rd(X0, Y1), rd(X0, Y1)), Y1) % 91.28/90.67 ld(rd(X0, Y1), mult(X0, rd(rd(X2, Y1), rd(X2, Y1)))) -> mult(rd(rd(X0, Y1), rd(X0, Y1)), Y1) % 91.28/90.67 ld(rd(X0, Y1), mult(mult(X0, rd(Y1, Y1)), rd(Y1, Y1))) -> mult(rd(rd(X0, Y1), rd(X0, Y1)), Y1) % 91.28/90.67 ld(rd(X0, Y1), mult(rd(X0, X2), mult(rd(X2, Y1), Y1))) -> mult(rd(rd(X0, Y1), rd(X0, Y1)), Y1) % 91.28/90.67 ld(rd(X0, false__), X0) -> mult(mult(rd(rd(X0, false__), rd(X0, false__)), rd(false__, X0)), X0) % 91.28/90.67 ld(rd(X0, mult(X0, X0)), X0) -> mult(mult(rd(rd(X0, mult(X0, X0)), rd(X0, mult(X0, X0))), X0), X0) % 91.28/90.67 ld(rd(X0, mult(X1, X0)), X0) -> mult(mult(rd(rd(X0, mult(X1, X0)), rd(X0, mult(X1, X0))), X1), X0) % 91.28/90.67 ld(rd(X0, mult(rd(X0, X1), X1)), mult(rd(X0, X1), X1)) -> mult(rd(X0, X1), X1) % 91.28/90.67 ld(rd(X0, mult(rd(X0, X1), X1)), rd(X0, Y1)) -> rd(X0, Y1) % 91.28/90.67 ld(rd(X0, mult(rd(X0, Y1), Y1)), rd(X0, Y1)) -> rd(X0, Y1) % 91.28/90.67 ld(rd(X0, rd(X1, X2)), mult(rd(X0, X2), X2)) -> mult(rd(rd(X0, rd(X1, X2)), rd(X0, rd(X1, X2))), rd(X1, X2)) % 91.28/90.67 ld(rd(X0, rd(Y1, Y1)), mult(X0, mult(rd(X0, X0), rd(Y1, Y1)))) -> mult(mult(rd(rd(X0, rd(Y1, Y1)), rd(X0, rd(Y1, Y1))), rd(rd(Y1, Y1), Y1)), Y1) % 91.28/90.67 ld(rd(X1, X1), rd(rd(X1, X1), rd(X1, X1))) -> rd(rd(X1, X1), rd(X1, X1)) % 91.28/90.67 ld(rd(Y0, Y0), Y0) -> Y0 % 91.28/90.67 ld(rd(ld(Y1, Y1), ld(Y1, Y1)), ld(Y1, Y1)) -> mult(rd(rd(rd(ld(Y1, Y1), ld(Y1, Y1)), rd(ld(Y1, Y1), ld(Y1, Y1))), Y1), Y1) % 91.28/90.67 ld(rd(mult(X0, X1), Y1), mult(X0, mult(rd(X1, Y1), Y1))) -> mult(rd(mult(X0, X1), Y1), ld(rd(mult(X0, X1), Y1), Y1)) % 91.28/90.67 ld(rd(mult(X0, Y1), mult(X0, Y1)), mult(rd(X0, Y1), Y1)) -> mult(rd(X0, Y1), Y1) % 91.28/90.67 ld(rd(rd(X0, X0), Y1), mult(rd(X0, X0), rd(Y1, Y1))) -> mult(rd(rd(rd(X0, X0), Y1), rd(rd(X0, X0), Y1)), Y1) % 91.28/90.67 ld(rd(rd(X0, Y1), Y1), rd(X0, Y1)) -> mult(rd(rd(X0, Y1), Y1), ld(rd(rd(X0, Y1), Y1), Y1)) % 91.28/90.67 ld(rd(rd(X0, mult(Y1, Y1)), Y1), rd(X0, mult(Y1, Y1))) -> mult(rd(rd(X0, mult(Y1, Y1)), Y1), ld(rd(rd(X0, mult(Y1, Y1)), Y1), Y1)) % 91.28/90.67 ld(rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1)), rd(X0, rd(Y1, Y1))) -> mult(rd(rd(rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1)), rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1))), Y1), Y1) % 91.28/90.67 ld(rd(rd(Y1, Y1), Y1), rd(Y1, Y1)) -> mult(rd(rd(Y1, Y1), Y1), ld(rd(rd(Y1, Y1), Y1), Y1)) % 91.28/90.67 ld(rd(rd(rd(Y1, Y1), Y1), Y1), rd(rd(Y1, Y1), Y1)) -> mult(rd(rd(rd(Y1, Y1), Y1), Y1), ld(rd(rd(rd(Y1, Y1), Y1), Y1), Y1)) % 91.28/90.67 ld(rd(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1), rd(Y1, Y1)) -> mult(rd(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1), ld(rd(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1), Y1)) % 91.28/90.67 ld(rd(rd(rd(Y1, Y1), rd(Y1, Y1)), rd(rd(Y1, Y1), rd(Y1, Y1))), rd(Y1, Y1)) -> mult(rd(rd(rd(rd(rd(Y1, Y1), rd(Y1, Y1)), rd(rd(Y1, Y1), rd(Y1, Y1))), rd(rd(rd(Y1, Y1), rd(Y1, Y1)), rd(rd(Y1, Y1), rd(Y1, Y1)))), Y1), Y1) % 91.28/90.67 mult(X0, ld(mult(X0, rd(Y1, Y1)), Y1)) -> mult(rd(X0, X0), Y1) % 91.28/90.67 mult(X0, ld(mult(rd(X0, X0), rd(X1, X1)), Y1)) -> mult(X0, Y1) % 91.28/90.67 mult(X0, ld(mult(rd(X0, Y1), Y1), Y1)) -> mult(rd(X0, X0), Y1) % 91.28/90.67 mult(X0, ld(rd(X0, mult(rd(X0, X1), X1)), Y1)) -> mult(X0, Y1) % 91.28/90.67 mult(X0, mult(X0, ld(mult(X0, rd(X1, X1)), rd(X1, X1)))) -> mult(X0, rd(X1, X1)) % 91.28/90.67 mult(X0, mult(rd(X0, mult(rd(X0, X1), X1)), Y1)) -> mult(X0, Y1) % 91.28/90.67 mult(X0, mult(rd(Y1, Y1), rd(X0, mult(rd(X0, X1), X1)))) -> mult(rd(X0, X1), X1) % 91.28/90.67 mult(X0, mult(rd(ld(X0, X1), X1), X1)) -> rd(mult(rd(X0, X0), X1), rd(X1, X1)) % 91.28/90.67 mult(Y0, ld(Y0, Y1)) -> mult(rd(Y0, Y0), Y1) % 91.28/90.67 mult(Y0, ld(Y0, ld(Y0, Y0))) -> ld(Y0, Y0) % 91.28/90.67 mult(Y0, ld(Y0, ld(Y0, ld(Y0, rd(Y0, Y0))))) -> ld(Y0, ld(Y0, rd(Y0, Y0))) % 91.28/90.67 mult(Y0, ld(Y0, ld(Y0, rd(X1, X1)))) -> ld(Y0, mult(rd(rd(Y0, Y0), X1), X1)) % 91.28/90.67 mult(Y0, ld(Y0, ld(Y0, rd(Y0, Y0)))) -> ld(Y0, rd(Y0, Y0)) % 91.28/90.67 mult(Y0, ld(Y0, mult(Y1, Y2))) -> mult(mult(Y0, ld(Y0, Y1)), Y2) % 91.28/90.67 mult(Y0, ld(Y0, mult(rd(X1, mult(Y0, X1)), mult(Y0, X1)))) -> mult(Y0, ld(Y0, X1)) % 91.28/90.67 mult(Y0, ld(Y0, mult(rd(rd(Y0, Y0), X1), X1))) -> ld(Y0, mult(rd(Y0, X1), X1)) % 91.28/90.67 mult(Y0, ld(Y0, rd(Y1, Y1))) -> mult(rd(rd(Y0, Y0), Y1), Y1) % 91.28/90.67 mult(Y0, ld(mult(Y0, rd(Y1, Y1)), X1)) -> mult(rd(Y0, Y0), X1) % 91.28/90.67 mult(Y0, ld(mult(Y0, rd(Y1, Y1)), mult(rd(Y0, Y0), rd(Y1, Y1)))) -> mult(rd(Y0, Y0), rd(Y1, Y1)) % 91.28/90.67 mult(Y0, ld(mult(rd(Y0, Y1), Y1), X1)) -> mult(rd(Y0, mult(rd(Y0, Y1), Y1)), X1) % 91.28/90.67 mult(Y0, ld(mult(rd(Y0, Y1), Y1), rd(Y0, mult(rd(Y0, Y1), Y1)))) -> rd(Y0, mult(rd(Y0, Y1), Y1)) % 91.28/90.67 mult(Y0, ld(rd(Y0, Y0), X1)) -> mult(Y0, X1) % 91.28/90.67 mult(Y0, mult(Y0, ld(mult(Y0, rd(Y1, Y1)), ld(mult(Y0, rd(Y1, Y1)), rd(Y1, Y1))))) -> mult(Y0, ld(mult(Y0, rd(Y1, Y1)), rd(Y1, Y1))) % 91.28/90.67 mult(Y0, mult(ld(Y0, X1), rd(false__, mult(rd(false__, X1), X1)))) -> mult(rd(Y0, Y0), X1) % 91.28/90.67 mult(Y0, mult(ld(Y0, Y1), rd(Y1, Y1))) -> mult(rd(Y0, Y0), Y1) % 91.28/90.67 mult(Y0, mult(ld(Y0, rd(X1, X1)), rd(X2, X2))) -> mult(rd(Y0, Y0), rd(X2, X2)) % 91.28/90.67 mult(Y0, mult(ld(Y0, rd(X1, X1)), rd(Y0, Y0))) -> rd(Y0, Y0) % 91.28/90.67 mult(Y0, mult(ld(Y0, rd(Y0, Y0)), rd(X1, X1))) -> mult(rd(Y0, Y0), rd(X1, X1)) % 91.28/90.67 mult(Y0, mult(rd(X0, mult(rd(X0, X1), X1)), rd(Y0, Y0))) -> Y0 % 91.28/90.67 mult(Y0, mult(rd(X1, ld(rd(Y0, Y0), X1)), ld(rd(Y0, Y0), X1))) -> mult(Y0, X1) % 91.28/90.67 mult(Y0, mult(rd(X1, mult(rd(Y0, Y0), X1)), mult(rd(Y0, Y0), X1))) -> mult(Y0, X1) % 91.28/90.67 mult(Y0, mult(rd(Y1, Y1), rd(X2, mult(rd(X2, Y0), Y0)))) -> Y0 % 91.28/90.67 mult(Y0, mult(rd(Y1, Y1), rd(Y0, Y0))) -> Y0 % 91.28/90.67 mult(Y0, mult(rd(Y1, mult(Y0, Y1)), mult(Y0, Y1))) -> mult(Y0, Y1) % 91.28/90.67 mult(Y0, mult(rd(Y1, rd(mult(Y0, Y1), mult(Y0, Y1))), rd(mult(Y0, Y1), mult(Y0, Y1)))) -> mult(Y0, Y1) % 91.28/90.67 mult(Y0, mult(rd(Y2, Y2), rd(Y1, Y1))) -> mult(Y0, rd(Y1, Y1)) % 91.28/90.67 mult(Y0, mult(rd(ld(Y0, X1), Y2), Y2)) -> mult(rd(Y0, Y0), mult(rd(X1, Y2), Y2)) % 91.28/90.67 mult(Y0, mult(rd(ld(Y0, rd(Y0, Y0)), Y2), Y2)) -> mult(rd(rd(Y0, Y0), Y0), mult(rd(Y0, Y2), Y2)) % 91.28/90.67 mult(Y0, mult(rd(rd(X1, X1), X1), mult(X1, rd(Y0, Y0)))) -> Y0 % 91.28/90.67 mult(Y0, mult(rd(rd(Y0, Y0), Y0), mult(rd(Y0, Y2), Y2))) -> mult(rd(Y0, Y2), Y2) % 91.28/90.67 mult(Y0, mult(rd(rd(Y0, Y0), Y2), Y2)) -> mult(rd(Y0, Y2), Y2) % 91.28/90.67 mult(Y0, mult(rd(rd(Y1, Y1), X2), mult(rd(X2, Y0), Y0))) -> Y0 % 91.28/90.67 mult(Y0, mult(rd(rd(false__, false__), false__), mult(rd(false__, Y0), Y0))) -> Y0 % 91.28/90.67 mult(Y0, rd(X0, mult(X0, rd(X1, mult(rd(X1, Y0), Y0))))) -> Y0 % 91.28/90.67 mult(Y0, rd(X0, mult(X0, rd(false__, mult(rd(false__, Y0), Y0))))) -> Y0 % 91.28/90.67 mult(Y0, rd(X1, mult(rd(X1, mult(rd(Y0, Y0), rd(X1, X1))), mult(rd(Y0, Y0), rd(X1, X1))))) -> mult(Y0, rd(X1, X1)) % 91.28/90.67 mult(Y0, rd(Y0, Y0)) -> Y0 % 91.28/90.67 mult(Y0, rd(Y0, mult(rd(Y0, Y1), Y1))) -> mult(rd(Y0, Y1), Y1) % 91.28/90.67 mult(Y0, rd(Y1, mult(rd(Y1, X2), mult(rd(X2, Y0), Y0)))) -> Y0 % 91.28/90.67 mult(Y0, rd(rd(Y2, Y1), rd(Y2, Y1))) -> mult(Y0, rd(Y1, Y1)) % 91.28/90.67 mult(Y1, ld(Y1, Y1)) -> Y1 % 91.28/90.67 mult(Y1, mult(rd(Y1, Y1), Y2)) -> mult(Y1, Y2) % 91.28/90.67 mult(Y1, rd(Y2, mult(rd(Y2, Y1), Y1))) -> Y1 % 91.28/90.67 mult(ld(X0, Y1), rd(Y2, mult(rd(Y2, Y1), Y1))) -> ld(X0, Y1) % 91.28/90.67 mult(ld(Y0, Y1), ld(ld(Y0, Y1), Y2)) -> mult(mult(Y0, ld(Y0, Y2)), rd(Y2, Y2)) % 91.28/90.67 mult(ld(Y0, mult(X0, rd(X1, X1))), rd(X1, X1)) -> ld(Y0, mult(X0, rd(X1, X1))) % 91.28/90.67 mult(ld(Y0, mult(rd(X0, X1), X1)), rd(X0, mult(rd(X0, X1), X1))) -> ld(Y0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(ld(Y0, rd(X0, X0)), rd(X0, X0)) -> ld(Y0, rd(X0, X0)) % 91.28/90.67 mult(ld(Y1, X1), rd(X1, X1)) -> ld(Y1, X1) % 91.28/90.67 mult(ld(Y1, X1), rd(mult(rd(Y1, Y1), X1), mult(rd(Y1, Y1), X1))) -> ld(Y1, X1) % 91.28/90.67 mult(ld(Y1, rd(Y1, Y1)), rd(Y1, Y1)) -> ld(Y1, rd(Y1, Y1)) % 91.28/90.67 mult(ld(rd(Y1, Y1), X1), rd(X1, X1)) -> ld(rd(Y1, Y1), X1) % 91.28/90.67 mult(mult(X0, X0), rd(X0, mult(rd(X0, mult(X0, X0)), mult(X0, X0)))) -> mult(X0, X0) % 91.28/90.67 mult(mult(X0, Y1), rd(Y1, Y1)) -> mult(X0, Y1) % 91.28/90.67 mult(mult(X0, Y1), rd(Y2, mult(rd(Y2, Y1), Y1))) -> mult(X0, Y1) % 91.28/90.67 mult(mult(X0, mult(rd(X0, X1), X1)), rd(X0, mult(rd(X0, X1), X1))) -> mult(X0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(mult(X0, mult(rd(X1, X2), X2)), rd(X2, X2)) -> mult(X0, mult(rd(X1, X2), X2)) % 91.28/90.67 mult(mult(X0, mult(rd(X1, Y1), Y1)), Y1) -> mult(mult(X0, X1), Y1) % 91.28/90.67 mult(mult(X0, mult(rd(X1, Y1), Y1)), Y2) -> mult(mult(X0, X1), Y2) % 91.28/90.67 mult(mult(Y0, X1), rd(X1, mult(rd(X1, mult(rd(Y0, Y0), X1)), mult(rd(Y0, Y0), X1)))) -> mult(Y0, X1) % 91.28/90.67 mult(mult(Y0, X1), rd(false__, mult(rd(false__, X1), X1))) -> mult(Y0, X1) % 91.28/90.67 mult(mult(Y0, Y1), rd(Y1, mult(rd(Y1, mult(Y0, Y1)), mult(Y0, Y1)))) -> mult(Y0, Y1) % 91.28/90.67 mult(mult(Y0, Y1), rd(Y2, Y2)) -> mult(Y0, mult(Y1, rd(Y2, Y2))) % 91.28/90.67 mult(mult(Y0, ld(Y0, Y3)), rd(Y3, Y3)) -> mult(rd(Y0, Y0), Y3) % 91.28/90.67 mult(mult(Y0, ld(mult(rd(Y0, Y1), Y1), rd(Y0, mult(rd(Y0, Y1), Y1)))), Y1) -> mult(rd(Y0, mult(rd(Y0, Y1), Y1)), Y1) % 91.28/90.67 mult(mult(Y0, mult(Y0, ld(Y0, X1))), rd(mult(Y0, X1), mult(Y0, X1))) -> mult(rd(Y0, Y0), mult(Y0, X1)) % 91.28/90.67 mult(mult(Y0, mult(Y1, rd(Y2, Y2))), Y2) -> mult(mult(Y0, Y1), Y2) % 91.28/90.67 mult(mult(Y0, mult(Y2, Y2)), rd(Y2, Y2)) -> mult(Y0, mult(Y2, Y2)) % 91.28/90.67 mult(mult(Y0, mult(rd(X0, X1), X1)), rd(X0, mult(rd(X0, X1), X1))) -> mult(Y0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(mult(Y0, rd(X0, mult(rd(X0, X1), X1))), Y2) -> mult(Y0, Y2) % 91.28/90.67 mult(mult(Y0, rd(X0, mult(rd(X0, X1), X1))), mult(rd(X0, X1), X1)) -> mult(Y0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(mult(Y0, rd(X1, X1)), mult(rd(X1, ld(rd(Y0, Y0), X1)), ld(rd(Y0, Y0), X1))) -> mult(Y0, X1) % 91.28/90.67 mult(mult(Y0, rd(X1, X1)), mult(rd(X1, mult(rd(Y0, Y0), X1)), mult(rd(Y0, Y0), X1))) -> mult(Y0, X1) % 91.28/90.67 mult(mult(Y0, rd(X1, X1)), rd(X1, X1)) -> mult(Y0, rd(X1, X1)) % 91.28/90.67 mult(mult(Y0, rd(X2, mult(rd(X2, Y1), Y1))), Y1) -> mult(Y0, Y1) % 91.28/90.67 mult(mult(Y0, rd(Y1, Y1)), Y1) -> mult(Y0, Y1) % 91.28/90.67 mult(mult(Y0, rd(Y1, Y1)), Y2) -> mult(Y0, Y2) % 91.28/90.67 mult(mult(Y0, rd(Y1, Y1)), mult(rd(Y1, mult(Y0, Y1)), mult(Y0, Y1))) -> mult(Y0, Y1) % 91.28/90.67 mult(mult(Y0, rd(Y1, Y1)), rd(false__, mult(rd(false__, Y0), Y0))) -> Y0 % 91.28/90.67 mult(mult(Y0, rd(mult(rd(Y0, Y1), Y1), mult(rd(Y0, Y1), Y1))), Y1) -> mult(Y0, Y1) % 91.28/90.67 mult(mult(Y0, rd(rd(X2, Y1), rd(X2, Y1))), Y1) -> mult(Y0, Y1) % 91.28/90.67 mult(mult(Y1, Y1), mult(rd(Y2, Y2), rd(Y1, Y1))) -> mult(Y1, Y1) % 91.28/90.67 mult(mult(Y1, Y1), rd(Y1, Y1)) -> mult(Y1, Y1) % 91.28/90.67 mult(mult(Y1, Y1), rd(Y2, mult(rd(Y2, Y1), Y1))) -> mult(Y1, Y1) % 91.28/90.67 mult(mult(mult(rd(X0, X0), rd(Y1, Y1)), rd(rd(Y1, Y1), Y1)), Y1) -> mult(rd(X0, X0), rd(Y1, Y1)) % 91.28/90.67 mult(mult(mult(rd(X0, Y2), Y2), Y1), Y2) -> mult(mult(X0, Y1), Y2) % 91.28/90.67 mult(mult(mult(rd(Y0, Y0), rd(X1, X1)), mult(rd(Y0, X1), X1)), mult(rd(Y0, X1), X1)) -> mult(Y0, mult(rd(Y0, X1), X1)) % 91.28/90.67 mult(mult(rd(X0, X0), rd(Y1, Y1)), Y1) -> mult(rd(X0, X0), Y1) % 91.28/90.67 mult(mult(rd(X0, Y1), Y1), mult(rd(X2, Y1), Y1)) -> mult(X0, mult(rd(X2, Y1), Y1)) % 91.28/90.67 mult(mult(rd(X0, Y1), Y1), mult(rd(Y1, Y2), Y2)) -> mult(X0, mult(rd(Y1, Y2), Y2)) % 91.28/90.67 mult(mult(rd(X0, Y1), Y1), rd(Y1, mult(rd(Y1, mult(Y1, Y1)), mult(Y1, Y1)))) -> mult(rd(X0, Y1), Y1) % 91.28/90.67 mult(mult(rd(X0, mult(rd(X0, X1), X1)), rd(X0, X1)), X1) -> mult(rd(X0, X1), X1) % 91.28/90.67 mult(mult(rd(X0, mult(rd(X0, Y1), Y1)), rd(rd(Y1, Y1), Y1)), Y1) -> mult(rd(X0, mult(rd(X0, Y1), Y1)), rd(Y1, Y1)) % 91.28/90.67 mult(mult(rd(X0, mult(rd(Y1, Y2), Y2)), Y1), Y2) -> mult(X0, Y2) % 91.28/90.67 mult(mult(rd(Y0, X2), X2), Y1) -> mult(Y0, Y1) % 91.28/90.67 mult(mult(rd(Y0, X2), X2), rd(X1, X2)) -> mult(Y0, rd(X1, X2)) % 91.28/90.67 mult(mult(rd(Y0, Y0), Y1), ld(Y1, rd(Y1, Y1))) -> mult(rd(Y0, Y0), rd(Y1, Y1)) % 91.28/90.67 mult(mult(rd(Y0, Y0), Y1), rd(Y1, Y1)) -> mult(rd(Y0, Y0), Y1) % 91.28/90.67 mult(mult(rd(Y0, Y0), rd(X1, X1)), mult(rd(X1, ld(Y0, X1)), ld(Y0, X1))) -> mult(rd(Y0, Y0), X1) % 91.28/90.67 mult(mult(rd(Y0, Y0), rd(X1, mult(Y0, X1))), mult(Y0, X1)) -> mult(rd(Y0, Y0), X1) % 91.28/90.67 mult(mult(rd(Y0, Y0), rd(Y0, Y1)), Y1) -> mult(rd(Y0, Y1), Y1) % 91.28/90.67 mult(mult(rd(Y0, Y2), Y2), Y2) -> mult(Y0, Y2) % 91.28/90.67 mult(mult(rd(Y1, Y2), rd(Y1, Y2)), rd(Y2, Y2)) -> mult(rd(Y1, Y2), rd(Y1, Y2)) % 91.28/90.67 mult(mult(rd(ld(X0, X1), ld(X0, X1)), rd(rd(X1, X1), X1)), X1) -> rd(ld(X0, X1), ld(X0, X1)) % 91.28/90.67 mult(mult(rd(mult(X0, rd(Y1, Y1)), mult(X0, rd(Y1, Y1))), rd(rd(Y1, Y1), Y1)), Y1) -> mult(rd(mult(X0, rd(Y1, Y1)), mult(X0, rd(Y1, Y1))), rd(Y1, Y1)) % 91.28/90.67 mult(mult(rd(mult(Y1, Y2), mult(Y1, Y2)), Y1), Y2) -> mult(Y1, Y2) % 91.28/90.67 mult(mult(rd(mult(rd(Y1, Y2), Y2), mult(rd(Y1, Y2), Y2)), Y1), Y2) -> mult(Y1, Y2) % 91.28/90.67 mult(mult(rd(rd(X0, Y1), rd(X0, Y1)), rd(Y1, mult(X2, Y1))), mult(X2, Y1)) -> mult(rd(rd(X0, Y1), rd(X0, Y1)), Y1) % 91.28/90.67 mult(mult(rd(rd(X0, Y1), rd(X0, Y1)), rd(Y1, rd(X2, Y1))), rd(X2, Y1)) -> mult(rd(rd(X0, Y1), rd(X0, Y1)), Y1) % 91.28/90.67 mult(mult(rd(rd(X0, mult(rd(X0, Y1), Y1)), rd(X0, mult(rd(X0, Y1), Y1))), rd(rd(Y1, Y1), Y1)), Y1) -> mult(rd(rd(X0, mult(rd(X0, Y1), Y1)), rd(X0, mult(rd(X0, Y1), Y1))), rd(Y1, Y1)) % 91.28/90.67 mult(mult(rd(rd(X0, mult(rd(Y1, Y2), Y2)), mult(rd(Y1, Y2), Y2)), Y1), Y2) -> mult(rd(X0, mult(rd(Y1, Y2), Y2)), Y2) % 91.28/90.67 mult(mult(rd(rd(X0, rd(Y1, Y1)), rd(X0, rd(Y1, Y1))), rd(rd(Y1, Y1), Y1)), Y1) -> mult(rd(rd(X0, rd(Y1, Y1)), rd(X0, rd(Y1, Y1))), rd(Y1, Y1)) % 91.28/90.67 mult(mult(rd(rd(mult(rd(Y1, Y2), Y2), mult(rd(Y1, Y2), Y2)), mult(rd(Y1, Y2), Y2)), Y1), Y2) -> mult(rd(mult(rd(Y1, Y2), Y2), mult(rd(Y1, Y2), Y2)), Y2) % 91.28/90.67 mult(mult(rd(rd(mult(rd(Y1, Y2), Y2), mult(rd(Y1, Y2), Y2)), rd(mult(rd(Y1, Y2), Y2), mult(rd(Y1, Y2), Y2))), Y1), Y2) -> mult(Y1, Y2) % 91.28/90.67 mult(mult(rd(rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1)), rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1))), rd(rd(Y1, Y1), Y1)), Y1) -> mult(rd(rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1)), rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1))), rd(Y1, Y1)) % 91.28/90.67 mult(rd(X0, X0), ld(rd(X0, X0), ld(rd(X0, X0), X0))) -> ld(rd(X0, X0), ld(rd(X0, X0), X0)) % 91.28/90.67 mult(rd(X0, X0), ld(rd(X0, X0), mult(X0, X0))) -> ld(rd(X0, X0), mult(X0, X0)) % 91.28/90.67 mult(rd(X0, X0), ld(rd(X0, X0), mult(rd(X0, X1), X1))) -> ld(rd(X0, X0), mult(rd(X0, X1), X1)) % 91.28/90.67 mult(rd(X0, X0), mult(X0, mult(rd(X0, Y2), Y2))) -> mult(X0, mult(rd(X0, Y2), Y2)) % 91.28/90.67 mult(rd(X0, X0), mult(rd(X0, X0), Y1)) -> mult(rd(X0, X0), Y1) % 91.28/90.67 mult(rd(X0, X0), mult(rd(X0, mult(rd(X0, mult(X0, X0)), mult(X0, X0))), mult(X0, X0))) -> mult(X0, X0) % 91.28/90.67 mult(rd(X0, X0), mult(rd(Y1, Y1), rd(X0, X0))) -> rd(X0, X0) % 91.28/90.67 mult(rd(X0, X0), mult(rd(ld(rd(X0, X0), X0), Y2), Y2)) -> mult(rd(ld(rd(X0, X0), X0), Y2), Y2) % 91.28/90.67 mult(rd(X0, X0), mult(rd(rd(X0, X0), Y2), Y2)) -> mult(rd(rd(X0, X0), Y2), Y2) % 91.28/90.67 mult(rd(X0, X0), rd(X0, Y1)) -> rd(X0, Y1) % 91.28/90.67 mult(rd(X0, X0), rd(mult(X0, X0), mult(X0, X0))) -> rd(mult(X0, X0), mult(X0, X0)) % 91.28/90.67 mult(rd(X0, X0), rd(rd(X0, X0), Y1)) -> rd(rd(X0, X0), Y1) % 91.28/90.67 mult(rd(X0, Y1), mult(rd(Y1, mult(X0, rd(Y1, Y1))), mult(rd(X0, Y1), Y1))) -> mult(rd(X0, Y1), Y1) % 91.28/90.67 mult(rd(X0, Y1), mult(rd(Y1, mult(rd(X0, Y1), Y1)), mult(X0, rd(Y1, Y1)))) -> mult(rd(X0, Y1), Y1) % 91.28/90.67 mult(rd(X0, Y1), rd(Y2, mult(rd(Y2, Y1), Y1))) -> rd(X0, Y1) % 91.28/90.67 mult(rd(X0, mult(rd(X0, X1), X1)), mult(X0, mult(rd(X0, X1), X1))) -> mult(X0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(rd(X0, mult(rd(X0, X1), X1)), rd(X0, Y1)) -> rd(X0, Y1) % 91.28/90.67 mult(rd(X0, mult(rd(X0, X1), X1)), rd(X0, mult(rd(X0, X1), X1))) -> rd(X0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(rd(X0, mult(rd(X0, Y1), Y1)), Y1) -> mult(rd(X0, X0), Y1) % 91.28/90.67 mult(rd(X0, mult(rd(X0, Y1), Y1)), Y2) -> mult(rd(X0, X0), Y2) % 91.28/90.67 mult(rd(X0, mult(rd(X0, Y1), Y1)), rd(X0, Y1)) -> rd(X0, Y1) % 91.28/90.67 mult(rd(X0, mult(rd(X0, Y1), Y1)), rd(Y1, Y1)) -> rd(X0, mult(rd(X0, Y1), Y1)) % 91.28/90.67 mult(rd(X0, rd(Y1, Y1)), Y1) -> mult(X0, Y1) % 91.28/90.67 mult(rd(X1, X1), ld(rd(X1, mult(rd(X1, X2), X2)), rd(X2, X2))) -> rd(X1, mult(rd(X1, X2), X2)) % 91.28/90.67 mult(rd(X1, X1), rd(Y1, mult(Y1, rd(X2, mult(rd(X2, X1), X1))))) -> rd(X1, X1) % 91.28/90.67 mult(rd(X1, mult(X0, rd(X2, X2))), mult(rd(X0, X1), mult(rd(X1, X2), X2))) -> mult(rd(X1, X2), X2) % 91.28/90.67 mult(rd(X1, mult(rd(X0, X1), mult(rd(X1, X2), X2))), mult(X0, rd(X2, X2))) -> mult(rd(X1, X2), X2) % 91.28/90.67 mult(rd(X1, mult(rd(X1, X2), X2)), rd(false__, mult(rd(false__, X2), X2))) -> rd(X1, mult(rd(X1, X2), X2)) % 91.28/90.67 mult(rd(Y0, Y0), ld(Y0, rd(Y0, Y0))) -> ld(Y0, rd(Y0, Y0)) % 91.28/90.67 mult(rd(Y0, Y0), mult(Y0, X1)) -> mult(Y0, mult(rd(Y0, Y0), X1)) % 91.28/90.67 mult(rd(Y0, Y0), mult(Y0, Y0)) -> mult(Y0, Y0) % 91.28/90.67 mult(rd(Y0, Y0), mult(rd(X1, ld(Y0, X1)), ld(Y0, X1))) -> mult(rd(Y0, Y0), X1) % 91.28/90.67 mult(rd(Y0, Y0), mult(rd(Y0, Y0), rd(Y1, Y1))) -> mult(rd(Y0, Y0), rd(Y1, Y1)) % 91.28/90.67 mult(rd(Y0, Y0), mult(rd(rd(Y0, Y0), Y0), mult(rd(Y0, Y2), Y2))) -> mult(rd(rd(Y0, Y0), Y0), mult(rd(Y0, Y2), Y2)) % 91.28/90.67 mult(rd(Y0, Y0), mult(rd(rd(false__, false__), false__), mult(rd(false__, Y0), Y0))) -> rd(Y0, Y0) % 91.28/90.67 mult(rd(Y0, Y0), rd(X1, mult(rd(X1, Y0), Y0))) -> rd(Y0, Y0) % 91.28/90.67 mult(rd(Y0, Y0), rd(Y0, Y0)) -> rd(Y0, Y0) % 91.28/90.67 mult(rd(Y0, Y1), mult(Y1, rd(Y2, Y2))) -> mult(Y0, rd(Y2, Y2)) % 91.28/90.67 mult(rd(Y0, Y1), rd(Y1, Y1)) -> rd(Y0, Y1) % 91.28/90.67 mult(rd(Y0, false__), mult(mult(false__, rd(Y0, Y0)), rd(false__, mult(rd(false__, Y0), Y0)))) -> Y0 % 91.28/90.67 mult(rd(Y0, false__), mult(rd(false__, X2), mult(rd(X2, Y0), Y0))) -> Y0 % 91.28/90.67 mult(rd(Y0, false__), mult(rd(false__, Y0), Y0)) -> Y0 % 91.28/90.67 mult(rd(Y0, ld(Y0, Y0)), ld(Y0, Y0)) -> rd(Y0, ld(Y0, Y0)) % 91.28/90.67 mult(rd(Y0, ld(Y1, X1)), ld(Y1, X1)) -> mult(Y0, rd(false__, mult(rd(false__, X1), X1))) % 91.28/90.67 mult(rd(Y0, ld(Y1, rd(Y1, Y1))), ld(Y1, rd(Y1, Y1))) -> mult(Y0, rd(Y1, Y1)) % 91.28/90.67 mult(rd(Y0, mult(X0, Y0)), mult(X0, Y0)) -> Y0 % 91.28/90.67 mult(rd(Y0, mult(X0, rd(X1, X1))), rd(X1, X1)) -> rd(Y0, mult(X0, rd(X1, X1))) % 91.28/90.67 mult(rd(Y0, mult(X0, rd(X2, mult(rd(X2, Y0), Y0)))), mult(rd(X0, Y0), Y0)) -> Y0 % 91.28/90.67 mult(rd(Y0, mult(X0, rd(Y0, Y0))), mult(rd(X0, Y0), Y0)) -> Y0 % 91.28/90.67 mult(rd(Y0, mult(Y0, Y0)), mult(Y0, Y0)) -> Y0 % 91.28/90.67 mult(rd(Y0, mult(Y1, Y1)), rd(Y1, Y1)) -> rd(Y0, mult(Y1, Y1)) % 91.28/90.67 mult(rd(Y0, mult(Y1, Y2)), mult(Y1, Y2)) -> mult(rd(Y0, Y2), Y2) % 91.28/90.67 mult(rd(Y0, mult(rd(X0, X1), X1)), rd(X0, mult(rd(X0, X1), X1))) -> rd(Y0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(rd(Y0, mult(rd(X0, X2), mult(rd(X2, Y0), Y0))), mult(rd(X0, Y0), Y0)) -> Y0 % 91.28/90.67 mult(rd(Y0, mult(rd(X0, Y0), Y0)), mult(X0, rd(X2, mult(rd(X2, Y0), Y0)))) -> Y0 % 91.28/90.67 mult(rd(Y0, mult(rd(X0, Y0), Y0)), mult(X0, rd(Y0, Y0))) -> Y0 % 91.28/90.67 mult(rd(Y0, mult(rd(X0, Y0), Y0)), mult(rd(X0, X2), mult(rd(X2, Y0), Y0))) -> Y0 % 91.28/90.67 mult(rd(Y0, mult(rd(X0, Y2), Y2)), mult(rd(X0, Y2), Y2)) -> mult(rd(Y0, Y2), Y2) % 91.28/90.67 mult(rd(Y0, mult(rd(X1, X1), rd(Y0, Y0))), mult(rd(X1, X1), rd(Y0, Y0))) -> rd(Y0, mult(rd(X1, X1), rd(Y0, Y0))) % 91.28/90.67 mult(rd(Y0, rd(X0, mult(rd(X0, X1), X1))), mult(rd(X0, X1), X1)) -> mult(Y0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(rd(Y0, rd(Y0, Y0)), rd(Y0, Y0)) -> rd(Y0, rd(Y0, Y0)) % 91.28/90.67 mult(rd(Y0, rd(Y2, Y3)), rd(Y2, Y3)) -> mult(rd(Y0, Y3), Y3) % 91.28/90.67 mult(rd(Y0, rd(rd(Y0, Y0), rd(Y0, Y0))), rd(rd(Y0, Y0), rd(Y0, Y0))) -> Y0 % 91.28/90.67 mult(rd(Y1, Y1), Y1) -> Y1 % 91.28/90.67 mult(rd(Y1, Y1), ld(rd(Y1, Y1), Y1)) -> ld(rd(Y1, Y1), Y1) % 91.28/90.67 mult(rd(Y1, Y1), mult(rd(Y1, Y2), Y2)) -> mult(rd(Y1, Y2), Y2) % 91.28/90.67 mult(rd(Y1, Y1), rd(Y1, mult(rd(Y1, mult(Y1, Y1)), mult(Y1, Y1)))) -> rd(Y1, Y1) % 91.28/90.67 mult(rd(Y1, Y1), rd(rd(Y1, Y1), Y1)) -> rd(rd(Y1, Y1), Y1) % 91.28/90.67 mult(rd(Y1, Y2), mult(rd(rd(Y1, Y2), Y2), Y2)) -> mult(rd(Y1, Y2), rd(Y1, Y2)) % 91.28/90.67 mult(rd(Y1, mult(rd(Y1, mult(Y1, Y1)), mult(Y1, Y1))), rd(Y1, Y1)) -> rd(Y1, mult(rd(Y1, mult(Y1, Y1)), mult(Y1, Y1))) % 91.28/90.67 mult(rd(ld(X0, X1), ld(X0, X1)), rd(X1, X1)) -> rd(ld(X0, X1), ld(X0, X1)) % 91.28/90.67 mult(rd(ld(X0, X1), ld(X0, X1)), rd(false__, mult(rd(false__, X1), X1))) -> rd(ld(X0, X1), ld(X0, X1)) % 91.28/90.67 mult(rd(mult(X0, X1), mult(X0, X1)), rd(false__, mult(rd(false__, X1), X1))) -> rd(mult(X0, X1), mult(X0, X1)) % 91.28/90.67 mult(rd(mult(X0, X1), mult(mult(X0, X1), rd(false__, mult(rd(false__, X2), X2)))), rd(false__, mult(rd(false__, X2), X2))) -> mult(rd(mult(X0, X1), mult(X0, X1)), rd(false__, mult(rd(false__, X2), X2))) % 91.28/90.67 mult(rd(mult(X0, Y1), mult(X0, Y1)), mult(rd(X0, Y1), Y1)) -> mult(rd(X0, Y1), Y1) % 91.28/90.67 mult(rd(mult(X0, Y1), mult(X0, Y1)), rd(Y1, Y1)) -> rd(mult(X0, Y1), mult(X0, Y1)) % 91.28/90.67 mult(rd(mult(Y0, X1), false__), mult(rd(false__, ld(rd(Y0, Y0), X1)), ld(rd(Y0, Y0), X1))) -> mult(Y0, X1) % 91.28/90.67 mult(rd(mult(Y0, Y1), Y3), Y3) -> mult(Y0, mult(rd(Y1, Y3), Y3)) % 91.28/90.67 mult(rd(mult(rd(Y0, Y0), X1), false__), mult(rd(false__, ld(Y0, X1)), ld(Y0, X1))) -> mult(rd(Y0, Y0), X1) % 91.28/90.67 mult(rd(rd(X0, X0), X0), mult(rd(X0, mult(X0, X0)), mult(X0, X0))) -> rd(mult(X0, X0), mult(X0, X0)) % 91.28/90.67 mult(rd(rd(X0, X0), X1), X1) -> rd(X0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(rd(rd(X0, X0), mult(rd(X0, X0), rd(false__, mult(rd(false__, X1), X1)))), rd(false__, mult(rd(false__, X1), X1))) -> rd(X0, mult(rd(X0, X1), X1)) % 91.28/90.67 mult(rd(rd(X0, Y1), rd(X0, Y1)), rd(Y1, Y1)) -> rd(rd(X0, Y1), rd(X0, Y1)) % 91.28/90.67 mult(rd(rd(X0, mult(rd(X0, X1), X1)), Y2), Y2) -> mult(rd(X0, X0), rd(X1, mult(rd(X1, Y2), Y2))) % 91.28/90.67 mult(rd(rd(X0, mult(rd(X0, Y1), Y1)), Y1), Y1) -> mult(rd(X0, mult(rd(X0, Y1), Y1)), rd(Y1, Y1)) % 91.28/90.67 mult(rd(rd(X0, rd(X0, X0)), rd(X0, X0)), rd(X0, X0)) -> rd(rd(X0, rd(X0, X0)), rd(X0, X0)) % 91.28/90.68 mult(rd(rd(X0, rd(X1, X2)), X2), X2) -> rd(X0, rd(X1, X2)) % 91.28/90.68 mult(rd(rd(X1, X1), X1), mult(rd(X1, ld(X0, X1)), ld(X0, X1))) -> rd(X1, X1) % 91.28/90.68 mult(rd(rd(X1, X1), false__), mult(false__, rd(X2, mult(rd(X2, X1), X1)))) -> rd(X1, X1) % 91.28/90.68 mult(rd(rd(X1, X1), mult(Y1, rd(X1, X1))), mult(Y1, rd(X2, mult(rd(X2, X1), X1)))) -> rd(X1, X1) % 91.28/90.68 mult(rd(rd(X1, X1), mult(Y1, rd(X1, X1))), mult(rd(Y1, X1), X1)) -> rd(X1, X1) % 91.28/90.68 mult(rd(rd(X1, X1), mult(Y1, rd(X1, X1))), mult(rd(Y1, X2), mult(rd(X2, X1), X1))) -> rd(X1, X1) % 91.28/90.68 mult(rd(rd(X1, X1), mult(Y1, rd(X1, mult(rd(X1, X2), X2)))), mult(Y1, rd(X2, X2))) -> rd(X1, mult(rd(X1, X2), X2)) % 91.28/90.68 mult(rd(rd(X1, X1), mult(Y1, rd(X2, X2))), mult(Y1, rd(X1, mult(rd(X1, X2), X2)))) -> rd(X1, mult(rd(X1, X2), X2)) % 91.28/90.68 mult(rd(rd(X1, X1), mult(Y1, rd(X2, X2))), mult(rd(Y1, X2), X2)) -> mult(rd(X1, X1), rd(X2, X2)) % 91.28/90.68 mult(rd(rd(X1, X1), mult(Y1, rd(X2, mult(rd(X2, X1), X1)))), mult(Y1, rd(X1, X1))) -> rd(X1, X1) % 91.28/90.68 mult(rd(rd(X1, X1), mult(rd(Y1, X1), X1)), mult(Y1, rd(X1, X1))) -> rd(X1, X1) % 91.28/90.68 mult(rd(rd(X1, X1), mult(rd(Y1, X2), mult(rd(X2, X1), X1))), mult(Y1, rd(X1, X1))) -> rd(X1, X1) % 91.28/90.68 mult(rd(rd(X1, mult(rd(X1, X2), X2)), mult(Y1, rd(X1, mult(rd(X1, X2), X2)))), mult(rd(Y1, X2), X2)) -> rd(X1, mult(rd(X1, X2), X2)) % 91.28/90.68 mult(rd(rd(X1, mult(rd(X1, X2), X2)), mult(rd(Y1, X2), X2)), mult(Y1, rd(X1, mult(rd(X1, X2), X2)))) -> rd(X1, mult(rd(X1, X2), X2)) % 91.28/90.68 mult(rd(rd(X1, mult(rd(X1, X2), X2)), rd(X1, mult(rd(X1, X2), X2))), rd(X2, X2)) -> rd(X1, mult(rd(X1, X2), X2)) % 91.28/90.68 mult(rd(rd(X2, X2), mult(X0, mult(X1, rd(X2, X2)))), mult(X0, mult(rd(X1, X2), X2))) -> rd(X2, X2) % 91.28/90.68 mult(rd(rd(X2, X2), mult(X0, mult(rd(X1, X2), X2))), mult(X0, mult(X1, rd(X2, X2)))) -> rd(X2, X2) % 91.28/90.68 mult(rd(rd(Y0, Y0), Y0), mult(rd(Y0, ld(Y0, rd(Y0, Y0))), ld(Y0, rd(Y0, Y0)))) -> rd(Y0, Y0) % 91.28/90.68 mult(rd(rd(Y0, Y0), false__), mult(rd(false__, ld(Y0, rd(Y0, Y0))), ld(Y0, rd(Y0, Y0)))) -> rd(Y0, Y0) % 91.28/90.68 mult(rd(rd(Y0, mult(Y2, Y2)), Y2), Y2) -> rd(Y0, mult(Y2, Y2)) % 91.28/90.68 mult(rd(rd(Y1, Y1), Y1), Y1) -> rd(Y1, Y1) % 91.28/90.68 mult(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1) -> Y1 % 91.28/90.68 mult(rd(rd(Y1, Y1), rd(Y1, Y1)), ld(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1)) -> ld(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1) % 91.28/90.68 mult(rd(rd(Y1, Y1), rd(Y1, Y1)), mult(rd(Y1, Y2), Y2)) -> mult(rd(Y1, Y2), Y2) % 91.28/90.68 mult(rd(rd(Y1, Y2), Y2), Y2) -> rd(Y1, Y2) % 91.28/90.68 mult(rd(rd(ld(Y1, Y1), ld(Y1, Y1)), Y1), Y1) -> ld(Y1, Y1) % 91.28/90.68 mult(rd(rd(mult(X0, X1), Y1), Y1), Y1) -> rd(mult(X0, mult(rd(X1, Y1), Y1)), Y1) % 91.28/90.68 mult(rd(rd(mult(X1, X2), mult(X1, X2)), mult(Y1, rd(false__, mult(rd(false__, X2), X2)))), mult(rd(Y1, X2), X2)) -> rd(mult(X1, X2), mult(X1, X2)) % 91.28/90.68 mult(rd(rd(mult(X1, X2), mult(X1, X2)), mult(rd(Y1, X2), X2)), mult(Y1, rd(false__, mult(rd(false__, X2), X2)))) -> rd(mult(X1, X2), mult(X1, X2)) % 91.28/90.68 mult(rd(rd(mult(Y1, Y1), mult(Y1, Y1)), Y1), Y1) -> rd(mult(Y1, Y1), mult(Y1, Y1)) % 91.28/90.68 mult(rd(rd(rd(X0, rd(X0, X0)), rd(X0, rd(X0, X0))), X0), X0) -> rd(rd(X0, rd(X0, X0)), rd(X0, rd(X0, X0))) % 91.28/90.68 mult(rd(rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1)), rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1))), rd(Y1, Y1)) -> rd(rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1)), rd(rd(X0, rd(Y1, Y1)), rd(Y1, Y1))) % 91.28/90.68 mult(rd(rd(rd(Y1, Y1), Y1), Y1), Y1) -> rd(rd(Y1, Y1), Y1) % 91.28/90.68 mult(rd(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1), Y1) -> rd(Y1, Y1) % 91.28/90.68 mult(rd(rd(rd(Y1, Y2), rd(Y1, Y2)), Y2), Y2) -> rd(rd(Y1, Y2), rd(Y1, Y2)) % 91.28/90.68 mult(rd(rd(rd(rd(Y1, Y1), Y1), Y1), Y1), Y1) -> rd(rd(rd(Y1, Y1), Y1), Y1) % 91.28/90.68 mult(rd(rd(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1), Y1), Y1) -> rd(rd(Y1, Y1), Y1) % 91.28/90.68 rd(X0, mult(rd(X0, X0), rd(X1, X1))) -> mult(X0, rd(X1, X1)) % 91.28/90.68 rd(X0, mult(rd(Y1, Y1), rd(X0, mult(rd(X0, X1), X1)))) -> mult(rd(X0, X1), X1) % 91.28/90.68 rd(X1, mult(rd(X1, mult(X1, X1)), mult(X1, X1))) -> rd(X1, X1) % 91.28/90.68 rd(Y0, mult(Y0, rd(Y1, Y1))) -> mult(rd(Y0, Y0), rd(Y1, Y1)) % 91.28/90.68 rd(Y0, mult(rd(X0, X0), rd(X1, X1))) -> mult(rd(Y0, X1), X1) % 91.28/90.68 rd(Y0, mult(rd(X0, mult(rd(X0, X1), X1)), rd(Y0, Y0))) -> Y0 % 91.28/90.68 rd(Y0, mult(rd(Y1, Y1), rd(X2, mult(rd(X2, Y0), Y0)))) -> Y0 % 91.28/90.68 rd(Y0, mult(rd(Y1, Y1), rd(Y0, Y0))) -> Y0 % 91.28/90.68 rd(Y0, mult(rd(rd(X1, X1), X1), mult(X1, rd(Y0, Y0)))) -> Y0 % 91.28/90.68 rd(Y0, mult(rd(rd(Y1, Y1), X2), mult(rd(X2, Y0), Y0))) -> Y0 % 91.28/90.68 rd(Y0, rd(X0, mult(X0, rd(X1, mult(rd(X1, Y0), Y0))))) -> Y0 % 91.28/90.68 rd(Y0, rd(X0, mult(X0, rd(false__, mult(rd(false__, Y0), Y0))))) -> Y0 % 91.28/90.68 rd(Y0, rd(X0, mult(rd(X0, X1), X1))) -> mult(rd(Y0, X1), X1) % 91.28/90.68 rd(Y0, rd(X0, mult(rd(X0, X1), mult(rd(X1, Y0), Y0)))) -> Y0 % 91.28/90.68 rd(Y0, rd(X1, X1)) -> mult(rd(Y0, X1), X1) % 91.28/90.68 rd(Y0, rd(X1, mult(rd(X1, Y0), Y0))) -> Y0 % 91.28/90.68 rd(Y0, rd(Y0, Y0)) -> Y0 % 91.28/90.68 rd(ld(Y0, rd(Y0, Y0)), ld(Y0, ld(Y0, rd(Y0, Y0)))) -> mult(rd(Y0, ld(Y0, ld(Y0, rd(Y0, Y0)))), ld(Y0, ld(Y0, rd(Y0, Y0)))) % 91.28/90.68 rd(ld(rd(X0, X0), X0), ld(rd(X0, X0), X0)) -> mult(rd(rd(X0, X0), ld(rd(X0, X0), X0)), ld(rd(X0, X0), X0)) % 91.28/90.68 rd(mult(A, A), A) -> A % 91.28/90.68 rd(mult(A, B), B) -> mult(rd(A, B), B) % 91.28/90.68 rd(mult(X0, X0), mult(X0, X0)) -> rd(X0, mult(rd(X0, mult(X0, X0)), mult(X0, X0))) % 91.28/90.68 rd(mult(X0, X1), mult(X0, mult(rd(X1, X2), X2))) -> mult(rd(mult(X0, X1), mult(X0, X1)), rd(false__, mult(rd(false__, X2), X2))) % 91.28/90.68 rd(mult(X0, mult(rd(X1, Y1), Y1)), Y1) -> rd(mult(X0, X1), Y1) % 91.28/90.68 rd(mult(X0, mult(rd(X1, Y1), Y1)), Y2) -> rd(mult(X0, X1), Y2) % 91.28/90.68 rd(mult(X0, rd(X2, mult(rd(X2, Y1), Y1))), Y1) -> rd(X0, Y1) % 91.28/90.68 rd(mult(X0, rd(Y1, Y1)), Y1) -> rd(X0, Y1) % 91.28/90.68 rd(mult(X0, rd(rd(X2, Y1), rd(X2, Y1))), Y1) -> rd(X0, Y1) % 91.28/90.68 rd(mult(Y0, X1), ld(rd(Y0, Y0), X1)) -> mult(rd(Y0, ld(rd(Y0, Y0), X1)), ld(rd(Y0, Y0), X1)) % 91.28/90.68 rd(mult(Y0, X1), mult(rd(X1, X2), X2)) -> mult(rd(Y0, X2), X2) % 91.28/90.68 rd(mult(Y0, X1), mult(rd(X1, mult(Y0, X1)), mult(Y0, X1))) -> mult(rd(Y0, mult(rd(X1, mult(Y0, X1)), mult(Y0, X1))), mult(rd(X1, mult(Y0, X1)), mult(Y0, X1))) % 91.28/90.68 rd(mult(Y0, X1), mult(rd(Y0, Y0), X1)) -> mult(rd(Y0, mult(rd(Y0, Y0), X1)), mult(rd(Y0, Y0), X1)) % 91.28/90.68 rd(mult(Y0, mult(X1, rd(X2, X2))), mult(rd(X1, X2), X2)) -> mult(rd(Y0, X2), X2) % 91.28/90.68 rd(mult(Y0, rd(X0, mult(rd(X0, X1), X1))), Y2) -> rd(Y0, Y2) % 91.28/90.68 rd(mult(Y0, rd(X0, mult(rd(X0, X1), X1))), mult(rd(X0, X1), X1)) -> rd(Y0, mult(rd(X0, X1), X1)) % 91.28/90.68 rd(mult(Y0, rd(Y1, Y1)), Y2) -> rd(Y0, Y2) % 91.28/90.68 rd(mult(mult(A, B), rd(C, D)), rd(C, D)) -> mult(A, rd(mult(B, D), D)) % 91.28/90.68 rd(mult(mult(Y0, Y1), Y3), mult(rd(Y3, Y3), Y3)) -> mult(Y0, mult(rd(Y1, Y3), Y3)) % 91.28/90.68 rd(mult(mult(rd(Y0, Y0), X1), X2), ld(Y0, mult(X1, X2))) -> mult(rd(Y0, ld(Y0, mult(X1, X2))), ld(Y0, mult(X1, X2))) % 91.28/90.68 rd(mult(rd(X0, X0), X1), rd(X1, X1)) -> mult(rd(X0, X0), X1) % 91.28/90.68 rd(mult(rd(X0, X0), rd(Y1, Y1)), Y1) -> rd(rd(X0, X0), Y1) % 91.28/90.68 rd(mult(rd(X0, X2), X2), Y1) -> rd(X0, Y1) % 91.28/90.68 rd(mult(rd(X0, X2), X2), rd(X1, X2)) -> rd(X0, rd(X1, X2)) % 91.28/90.68 rd(mult(rd(Y0, X1), X1), mult(rd(Y0, Y0), rd(X1, X1))) -> mult(rd(Y0, mult(rd(Y0, Y0), rd(X1, X1))), mult(rd(Y0, Y0), rd(X1, X1))) % 91.28/90.68 rd(mult(rd(Y0, X1), X1), mult(rd(rd(Y0, Y0), X1), X1)) -> mult(rd(Y0, mult(rd(rd(Y0, Y0), X1), X1)), mult(rd(rd(Y0, Y0), X1), X1)) % 91.28/90.68 rd(mult(rd(Y0, X2), X2), mult(rd(X1, X1), rd(X2, X2))) -> mult(rd(Y0, mult(rd(X1, X1), rd(X2, X2))), mult(rd(X1, X1), rd(X2, X2))) % 91.28/90.68 rd(mult(rd(Y0, X2), X2), rd(X1, mult(rd(X1, X2), X2))) -> mult(rd(Y0, X2), X2) % 91.28/90.68 rd(mult(rd(Y0, Y0), X1), ld(Y0, X1)) -> mult(rd(Y0, ld(Y0, X1)), ld(Y0, X1)) % 91.28/90.68 rd(mult(rd(Y0, Y1), Y1), mult(rd(X0, Y1), Y1)) -> rd(Y0, mult(rd(X0, Y1), Y1)) % 91.28/90.68 rd(mult(rd(rd(Y0, Y0), X1), X1), ld(Y0, rd(X1, X1))) -> mult(rd(Y0, ld(Y0, rd(X1, X1))), ld(Y0, rd(X1, X1))) % 91.28/90.68 rd(rd(X0, X0), mult(rd(X0, X0), rd(Y1, Y1))) -> mult(rd(X0, X0), rd(Y1, Y1)) % 91.28/90.68 rd(rd(X0, X0), mult(rd(Y1, Y1), rd(X0, X0))) -> rd(X0, X0) % 91.28/90.68 rd(rd(X0, X0), rd(X0, X0)) -> rd(X0, X0) % 91.28/90.68 rd(rd(X0, X0), rd(X0, mult(rd(X0, X1), X1))) -> rd(X0, mult(rd(X0, X1), X1)) % 91.28/90.68 rd(rd(X0, X0), rd(X1, X1)) -> mult(rd(rd(X0, X0), X1), X1) % 91.28/90.68 rd(rd(X0, X1), rd(X0, X1)) -> rd(X0, mult(rd(X0, X1), X1)) % 91.28/90.68 rd(rd(X0, mult(rd(X0, X1), X1)), rd(X1, X1)) -> rd(X0, mult(rd(X0, X1), X1)) % 91.28/90.68 rd(rd(X0, mult(rd(X0, Y1), Y1)), Y1) -> rd(rd(X0, X0), Y1) % 91.28/90.68 rd(rd(X0, mult(rd(X0, Y1), Y1)), Y2) -> rd(rd(X0, X0), Y2) % 91.28/90.68 rd(rd(X0, rd(Y1, Y1)), Y1) -> rd(X0, Y1) % 91.28/90.68 rd(rd(X1, X1), rd(Y1, mult(Y1, rd(X2, mult(rd(X2, X1), X1))))) -> rd(X1, X1) % 91.28/90.68 rd(rd(X1, mult(rd(X1, X2), X2)), rd(X1, mult(rd(X1, X2), X2))) -> rd(X1, mult(rd(X1, X2), X2)) % 91.28/90.68 rd(rd(Y0, Y0), ld(Y0, rd(Y0, Y0))) -> mult(rd(Y0, ld(Y0, rd(Y0, Y0))), ld(Y0, rd(Y0, Y0))) % 91.28/90.68 rd(rd(Y0, rd(X0, mult(rd(X0, X1), X1))), mult(rd(X0, X1), X1)) -> rd(Y0, mult(rd(X0, X1), X1)) % 91.28/90.68 rd(rd(rd(Y1, Y1), rd(Y1, Y1)), Y1) -> rd(rd(Y1, Y1), Y1) % 91.28/90.68 true__ -> false__ % 91.28/90.68 with the LPO induced by % 91.28/90.68 b > c > a > f1 > ld > rd > mult > true__ > false__ % 91.28/90.68 % 91.28/90.68 % SZS output end Proof % 91.28/90.68 %------------------------------------------------------------------------------